next_f — Mathlib

English

If c.next j = k and not BoundaryGE j, then the next image equals the next of j under the embedding.

Русский

Если c.next j = k и BoundaryGE(j) ложно, то образ следующего элемента совпадает с next(j) под вложением.

LaTeX

$$Next_f [e.IsTruncGE] {j k} (hjk: c.next j = k) (hj: ¬e.BoundaryLE j) : c'.next (e.f j) = e.f k$$

Lean4

theorem next_f [e.IsTruncGE] {j k : ι} (hjk : c.next j = k) : c'.next (e.f j) = e.f k :=
  by
  by_cases hj : c'.Rel (e.f j) (c'.next (e.f j))
  · obtain ⟨k', hk'⟩ := e.mem_next hj
    rw [← hk', e.rel_iff] at hj
    rw [← hk', ← c.next_eq' hj, hjk]
  · rw [c'.next_eq_self _ hj, ← hjk, c.next_eq_self j]
    intro hj'
    apply hj
    rw [← e.rel_iff] at hj'
    simpa only [c'.next_eq' hj'] using hj'

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