75structure RefinementConverges (sys : DirectedRefinement C) : Prop where 76 eventually_separates : ∀ c₁ c₂ : C, 77 (∀ i, Indistinguishable (sys.recognizer i) c₁ c₂) → c₁ = c₂ 78 79/-! ## U3: Dimension Invariance -/ 80 81/-- U3: Dimension invariance under refinement choice. 82Two directed refinement systems that both converge and both admit 83a common separation count produce the same dimension. 84(The full statement requires chart-atlas infrastructure; here we 85record it as a property of the separating-recognizer count.) -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.