Iic_union_Ici

Mathlib.Order.Interval.Set.LinearOrder

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

English

Iic a ∪ Ici a = univ for any a.

Русский

Iic a ∪ Ici a = всякое множество для любого a.

LaTeX

$$$ Iic(a) \cup Ici(a) = \mathbb{R} $$$

Lean4

@[simp]
theorem Iic_union_Ici : Iic a ∪ Ici a = univ :=
  Iic_union_Ici_of_le le_rfl

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

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

Разделы

Аффилиация

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