prev_eq_self — Mathlib

English

Let c be a ComplexShape on ι and j an index. If j is not related to its predecessor under c, then the predecessor of j is j.

Русский

Пусть c — комплексная форма на ι и j — индекс. Если j не связан с его предшественником по отношению c, то предшественник j равен j.

LaTeX

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

Lean4

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

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