biUnion_Iio_eq

Mathlib.Order.Interval.Set.Disjoint

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

English

Let s be a set with IsLUB a for a. Then the union over x ∈ s of the intervals Iio x equals Iio a.

Русский

Пусть s имеет верхнюю границу a. Тогда объединение по x ∈ s интервалов Iio x равно Iio a.

LaTeX

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

Lean4

theorem biUnion_Iio_eq (h : IsLUB s a) : ⋃ x ∈ s, Iio x = Iio a :=
  h.dual.biUnion_Ioi_eq

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

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

Разделы

Аффилиация

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