biUnion_Iic_eq_Iic

Mathlib.Order.Interval.Set.Disjoint

URI: https://scilib.ai/kg/mathlib#IsLUB.biUnion_Iic_eq_Iic

English

Same statement as above, repeated for different naming

Русский

Та же формула, повторённая под другим названием

LaTeX

$$$$\bigcup_{x\in s} Iic(x) = Iic(a)$$$$

Lean4

theorem biUnion_Iic_eq_Iic (a_lub : IsLUB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Iic x = Iic a :=
  a_lub.dual.biUnion_Ici_eq_Ici a_mem

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

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

Разделы

Аффилиация

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