boundaryGE — Mathlib

English

If an embedding maps a relation between j and k, then boundary growth cannot occur at k for all next steps, given an IsRelIff structure.

Русский

Если вложение сохраняет отношение между j и k, граница не может расти в точке k на всех последующих шагах, при условии IsRelIff.

LaTeX

$$$\\forall {j,k}, c.Rel(j,k) \\Rightarrow \\neg e.BoundaryGE(k)$ under IsRelIff$$

Lean4

theorem boundaryGE {i' : ι'} {j : ι} (hj : c'.Rel i' (e.f j)) (hi' : ∀ i, e.f i ≠ i') : e.BoundaryGE j :=
  by
  constructor
  · simpa only [c'.prev_eq' hj] using hj
  · intro i hi
    apply hi' i
    rw [← c'.prev_eq' hj, c'.prev_eq' hi]

Похожие утверждения