Iic_union_Ioi_of_le

Mathlib.Order.Interval.Set.LinearOrder

URI: https://scilib.ai/kg/mathlib#Set.Iic_union_Ioi_of_le

English

Iic b ∪ Ioi a = univ whenever a ≤ b.

Русский

Iic b ∪ Ioi a = всю множество, когда a ≤ b.

LaTeX

$$$ a \le b \Rightarrow Iic(b) \cup Ioi(a) = \mathbb{R} $$$

Lean4

theorem Iic_union_Ioi_of_le (h : a ≤ b) : Iic b ∪ Ioi a = univ :=
  eq_univ_of_forall fun x => (h.gt_or_le x).symm

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

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

Разделы

Аффилиация

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