chartCompatible_refl

formal source

 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) :
 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