next_add' — Mathlib

English

A variant of the previous relation with the opposite direction of the index-shift; a dual form of Next Add.

Русский

Вариант предыдущего отношения с противоположным направлением сдвига индекса; двойственная форма Next Add.

LaTeX

$$$\\text{next\_add}'(p,q): \\text{next}(p+q)=p+\\text{next}(q)$$$

Lean4

theorem next_add' (p q : I) (hq : c.Rel q (c.next q)) : c.next (p + q) = p + c.next q :=
  c.next_eq' (c.add_rel p hq)

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