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

maximal_cells_unsplittable

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)

 193theorem maximal_cells_unsplittable {E E' : Type*}
 194    (r : Recognizer C E) (r' : Recognizer C E')
 195    (hmax : IsFinerThan r' r → IsFinerThan r r')
 196    (c₁ c₂ : C) (h : Indistinguishable r c₁ c₂) :
 197    -- If r' is finer than r, then r is also finer than r'
 198    -- meaning r and r' have exactly the same resolution cells
 199    IsFinerThan r' r → Indistinguishable r' c₁ c₂ := by

proof body

Term-mode proof.

 200  intro hfiner
 201  exact hfiner c₁ c₂ h
 202
 203/-- If a maximal recognizer exists and another recognizer refines it,
 204    they induce the same equivalence relation. -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.