chartCompatible_symm

formal source

 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) :
 135    ∃ φ ∈ A.charts, ∃ c ∈ φ.domain, recognitionQuotientMk r c = q := by
 136  obtain ⟨c, hc⟩ := Quotient.exists_rep q
 137  obtain ⟨φ, hφ, hcφ⟩ := A.covers c
 138  refine ⟨φ, hφ, c, hcφ, ?_⟩
 139  -- hc : ⟦c⟧ = q
 140  -- recognitionQuotientMk r c = Quotient.mk _ c = ⟦c⟧
 141  simp only [recognitionQuotientMk]
 142  exact hc
 143
 144/-! ## Recognition Dimension -/
 145
 146/-- The recognition dimension at a point is the dimension of any chart containing it -/