Iio_union_Ici_of_le

Mathlib.Order.Interval.Set.LinearOrder

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

English

Iio b ∪ Ici a = univ when a ≤ b.

Русский

Iio b ∪ Ici a = всякое множество, когда a ≤ b.

LaTeX

$$$ a \le b \Rightarrow Iio(b) \cup Ici(a) = \mathbb{R} $$$

Lean4

theorem Iio_union_Ici_of_le (h : a ≤ b) : Iio b ∪ Ici a = univ :=
  eq_univ_of_forall fun x => (h.ge_or_lt x).symm

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

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

Разделы

Аффилиация

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