Ici_add_one_eq_Ioi — Mathlib

English

Let α be a linear order with 1, addition, SuccAddOrder, and NoMaxOrder. Then for every a, Ici(a+1) = Ioi(a).

Русский

Пусть α — линейное множество с единицей, сложением, SuccAddOrder и NoMaxOrder. Тогда для каждого a выполняется Ici(a+1) = Ioi(a).

LaTeX

$$$ \forall a, \mathrm{Ici}(a + 1) = \mathrm{Ioi}(a) $$$

Lean4

theorem Ici_add_one_eq_Ioi (a : α) : Ici (a + 1) = Ioi a := by simpa [succ_eq_add_one] using Ici_succ_eq_Ioi a

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