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 -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.