Iio_succ_eq_insert

Mathlib.Order.SuccPred.Basic

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

English

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

Русский

Если a не максимален, то Iio(succ a) = insert 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 (a : α) : Iio (succ a) = insert a (Iio a) :=
  Iio_succ_eq_insert_of_not_isMax <| not_isMax a

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

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

Разделы

Аффилиация

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