not_boundaryLE_prev' — Mathlib

English

If e.IsRelIff holds and we know that not BoundaryLE at j, then not BoundaryLE at i when c.prev j = i.

Русский

При условии IsRelIff и не BoundaryLE для j, граница не держится для i, если c.prev j = i.

LaTeX

$$$(e.IsRelIff) \\Rightarrow (c.prev j = i) \\Rightarrow \\neg e.BoundaryLE i$$$

Lean4

theorem not_boundaryLE_prev' [e.IsRelIff] {i j : ι} (hj : ¬e.BoundaryLE j) (hk : c.prev j = i) : ¬e.BoundaryLE i :=
  by
  by_cases hij : c.Rel i j
  · exact e.not_boundaryLE_prev hij
  · subst hk
    simpa only [c.prev_eq_self j hij] using hj

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