Iio_union_Ioi_of_lt

Mathlib.Order.Interval.Set.LinearOrder

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

English

Iio b ∪ Ioi a = univ whenever a < b.

Русский

Iio b ∪ Ioi a = всю множествo, если a < b.

LaTeX

$$$ a < b \Rightarrow Iio(b) \cup Ioi(a) = \mathbb{R} $$$

Lean4

theorem Iio_union_Ioi_of_lt (h : a < b) : Iio b ∪ Ioi a = univ :=
  eq_univ_of_forall fun x => (h.gt_or_lt x).symm

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

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

Разделы

Аффилиация

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