biUnion_Iic_eq_Iio

Mathlib.Order.Interval.Set.Disjoint

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

English

Let IsLUB s a hold. If a ∉ s, then ⋃ x ∈ s, Iic x = Iic a.

Русский

Пусть IsLUB s a выполняется. Если a ∉ s, тогда ⋃ x ∈ s Iic x = Iic a.

LaTeX

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

Lean4

theorem biUnion_Iic_eq_Iio (a_lub : IsLUB s a) (a_notMem : a ∉ s) : ⋃ x ∈ s, Iic x = Iio a :=
  a_lub.dual.biUnion_Ici_eq_Ioi a_notMem

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

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

Разделы

Аффилиация

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