monotone_separation_of_refinement

formal source

 105    ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂
 106
 107/-- Monotone separation follows from refinement. -/
 108theorem monotone_separation_of_refinement (sys : DirectedRefinement C) :
 109    ∀ i : ℕ, ∀ c₁ c₂ : C,
 110      ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
 111      ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂ := by
 112  intro i c₁ c₂ hne habs
 113  exact hne (sys.refines i c₁ c₂ habs)
 114
 115/-! ## U1: The Effective Manifold Bundle -/
 116
 117/-- U1: The complete hypothesis bundle for the effective-manifold assumption.
 118This packages U2 + U4 (U3 is a consequence when the limit exists). -/
 119structure EffectiveManifoldHypotheses (C : Type*) where
 120  system : DirectedRefinement C
 121  converges : RefinementConverges system
 122  nonCollapse : NonCollapseCondition system
 123
 124/-- U2 + refinement implies U4's monotone separation automatically. -/
 125theorem nonCollapse_monotone_automatic (sys : DirectedRefinement C) :
 126    ∀ i c₁ c₂,
 127      ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
 128      ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂ :=
 129  monotone_separation_of_refinement sys
 130
 131/-- The convergence condition implies: the intersection of all
 132equivalence relations is the identity (diagonal). -/
 133theorem convergence_implies_identity (sys : DirectedRefinement C)
 134    (hconv : RefinementConverges sys) :
 135    ∀ c₁ c₂ : C,
 136      (∀ i, Indistinguishable (sys.recognizer i) c₁ c₂) → c₁ = c₂ :=
 137  hconv.eventually_separates
 138