not_boundaryGE_next' — Mathlib

English

If the Rel relation fails between j and i while c.next j = k, then boundary constraints move forward impossibly, yielding a contradiction under IsRelIff.

Русский

Если отношение Rel между j и i нарушено при условии c.next j = k, границы переходят к невозможному, приводя к противоречию под IsRelIff.

LaTeX

$$$\\text{not_boundaryGE_next'}(e,\; hij,\; hk) :\\neg e.BoundaryGE(k)$$$

Lean4

theorem not_boundaryGE_next' [e.IsRelIff] {j k : ι} (hj : ¬e.BoundaryGE j) (hk : c.next j = k) : ¬e.BoundaryGE k :=
  by
  by_cases hjk : c.Rel j k
  · exact e.not_boundaryGE_next hjk
  · subst hk
    simpa only [c.next_eq_self j hjk] using hj

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