pith. machine review for the scientific record. sign in
theorem proved term proof

monotone_separation_of_refinement

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.