def
definition
ChartCompatible
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Charts on GitHub at line 104.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
101/-! ## Chart Compatibility -/
102
103/-- Two charts are compatible if they agree on their overlap -/
104def ChartCompatible (φ₁ φ₂ : RecognitionChart L r n) : Prop :=
105 ∀ c : C, ∀ (h₁ : c ∈ φ₁.domain) (h₂ : c ∈ φ₂.domain),
106 φ₁.toFun ⟨c, h₁⟩ = φ₂.toFun ⟨c, h₂⟩
107
108/-- Chart compatibility is reflexive -/
109theorem chartCompatible_refl (φ : RecognitionChart L r n) :
110 ChartCompatible L r φ φ := by
111 intro c h₁ h₂
112 -- h₁ and h₂ are both proofs that c ∈ φ.domain, so they must give same result
113 rfl
114
115/-- Chart compatibility is symmetric -/
116theorem chartCompatible_symm (φ₁ φ₂ : RecognitionChart L r n)
117 (hcompat : ChartCompatible L r φ₁ φ₂) :
118 ChartCompatible L r φ₂ φ₁ := by
119 intro c h₂ h₁
120 exact (hcompat c h₁ h₂).symm
121
122/-! ## Recognition Atlas -/
123
124/-- A recognition atlas is a family of compatible charts that cover the space -/
125structure RecognitionAtlas (L : LocalConfigSpace C) (r : Recognizer C E) (n : ℕ) where
126 /-- The family of charts (indexed by some type) -/
127 charts : Set (RecognitionChart L r n)
128 /-- The charts are pairwise compatible -/
129 compatible : ∀ φ₁ ∈ charts, ∀ φ₂ ∈ charts, ChartCompatible L r φ₁ φ₂
130 /-- The charts cover the configuration space -/
131 covers : ∀ c : C, ∃ φ ∈ charts, c ∈ φ.domain
132
133/-- An atlas covers the quotient space -/
134theorem atlas_covers_quotient (A : RecognitionAtlas L r n) (q : RecognitionQuotient r) :