Iio_union_right

Mathlib.Order.Interval.Set.Basic

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

English

The union of the open interval (−∞, a) with the singleton {a} equals the closed interval (−∞, a]: Iio(a) ∪ {a} = Iic(a).

Русский

Объединение открытого интервала (−∞, a) с {a} даёт интервал (−∞, a]: Iio(a) ∪ {a} = Iic(a).

LaTeX

$$$$ Iio(a) \\cup \\{a\\} = Iic(a) $$$$

Lean4

theorem Iio_union_right : Iio a ∪ { a } = Iic a :=
  ext fun _ => le_iff_lt_or_eq.symm

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

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

Разделы

Аффилиация

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