Icc_subset_Ico_succ_right

Mathlib.Order.SuccPred.Basic

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

English

Icc(a,b) is contained in Ico(a, succ b).

Русский

Icc(a,b) содержится в Ico(a, succ(b)).

LaTeX

$$Icc(a,b) \subseteq Ico(a, \operatorname{succ} b)$$

Lean4

@[simp]
theorem Icc_subset_Ico_succ_right (a b : α) : Icc a b ⊆ Ico a (succ b) :=
  Icc_subset_Ico_succ_right_of_not_isMax <| not_isMax _

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

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

Разделы

Аффилиация

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