Iic_subset_Iio_succ_of_not_isMax

Mathlib.Order.SuccPred.Basic

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

English

If a is not maximal, then a covBy succ(a).

Русский

Если a не максимален, то a покрывает succ(a).

LaTeX

$$$\\neg \\mathrm{IsMax}(a) \\Rightarrow a \\mathrm{CovBy} \\operatorname{succ}(a)$$$

Lean4

theorem Iic_subset_Iio_succ_of_not_isMax (ha : ¬IsMax a) : Iic a ⊆ Iio (succ a) := fun _ =>
  (lt_succ_of_le_of_not_isMax · ha)

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

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

Разделы

Аффилиация

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