105def quotientNeighborhoods (L : LocalConfigSpace C) : 106 RecognitionQuotient r → Set (Set (RecognitionQuotient r)) :=
proof body
Definition body.
107 fun q => {V | ∃ c : C, recognitionQuotientMk r c = q ∧ ∃ U ∈ L.N c, projectSet r U ⊆ V} 108 109/-! ## Summary Theorem -/ 110 111/-- Summary: The recognition quotient captures exactly the observable structure -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.