Iio_succ_eq_insert_of_not_isMax

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.Iio_succ_eq_insert_of_not_isMax

English

If a is not maximal, then Iio(succ a) equals insert a Iio(a).

Русский

Если a не максимально, то Iio(succ a) равняется добавлению a к Iio(a).

LaTeX

$$$\neg\IsMax(a) \Rightarrow \mathrm{Iio}(\operatorname{succ} a) = \operatorname{insert}(a)(\mathrm{Iio}(a))$$$

Lean4

theorem Iio_succ_eq_insert_of_not_isMax (h : ¬IsMax a) : Iio (succ a) = insert a (Iio a) :=
  ext fun _ => lt_succ_iff_eq_or_lt_of_not_isMax h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru