next_eq_self — Mathlib

English

Let c be a ComplexShape on an index type ι. For any index j, if j is not related to its successor under c, then the successor of j is j itself.

Русский

Пусть c — комплексная форма на индексовом множестве ι. Если для некоторого j не выполняется relation c.Rel j (c.next j), то следующий индекс j равен самому j.

LaTeX

$$$\\forall ι \\ (c : ComplexShape ι) \\ (j : ι), \\neg c.Rel j (c.next j) \\Rightarrow c.next j = j$$$

Lean4

theorem next_eq_self (c : ComplexShape ι) (j : ι) (hj : ¬c.Rel j (c.next j)) : c.next j = j :=
  c.next_eq_self' j (fun k hk' => hj (by simpa only [c.next_eq' hk'] using hk'))

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