not_boundaryGE_next — Mathlib

English

Under IsRelIff, if boundary grows at j is false and the j and k are related by next, then boundaryGE cannot hold at k.

Русский

При условии IsRelIff, если BoundaryGE(j) ложно и j связно с k по next, тогда BoundaryGE(k) невозможно.

LaTeX

$$$\\neg e.BoundaryGE(k)$ if $c.next(j)=k$ and notBoundaryGE(j)$$$

Lean4

theorem not_boundaryGE_next [e.IsRelIff] {j k : ι} (hk : c.Rel j k) : ¬e.BoundaryGE k :=
  by
  dsimp [BoundaryGE]
  simp only [not_and, not_forall, not_not]
  intro
  exact ⟨j, by simpa only [e.rel_iff] using hk⟩

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