iUnion_Iic

Mathlib.Order.Interval.Set.Disjoint

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

English

The union over all a of Iic(a) equals the whole space: ⋃_{a∈α} Iic(a) = univ.

Русский

Объединение по всем a из α множества Iic(a) даёт всю область: ⋃_{a∈α} Iic(a) = univ.

LaTeX

$$$$ \bigcup_{a \in \alpha} Iic(a) = \mathrm{univ}. $$$$

Lean4

@[simp]
theorem iUnion_Iic : ⋃ a : α, Iic a = univ :=
  iUnion_eq_univ_iff.2 fun x => ⟨x, right_mem_Iic⟩

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

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

Разделы

Аффилиация

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