Ioi_union_left

Mathlib.Order.Interval.Set.Basic

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

English

The union of the open interval (a, ∞) with the singleton {a} equals the closed interval [a, ∞): Ioi(a) ∪ {a} = Ici(a).

Русский

Объединение открытого интервала (a, ∞) с множестом {a} даёт замкнутый интервал [a, ∞): Ioi(a) ∪ {a} = Ici(a).

LaTeX

$$$$ Ioi(a) \\cup \\{a\\} = Ici(a) $$$$

Lean4

theorem Ioi_union_left : Ioi a ∪ { a } = Ici a :=
  ext fun x => by simp [eq_comm, le_iff_eq_or_lt]

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

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

Разделы

Аффилиация

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