iUnion_Iio_eq

Mathlib.Order.Interval.Set.Disjoint

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

English

If IsLUB holds for the range of f with limit a, then ⋃ Ioi(f i) = Ioi a.

Русский

Если для диапазона значений f выполняется IsLUB с пределом a, то ⋃ Ioi(f(i)) = Ioi(a).

LaTeX

$$$$\bigcup_i Ioi(f_i) = Ioi(a)$$$$

Lean4

theorem iUnion_Iio_eq (h : IsLUB (range f) a) : ⋃ x, Iio (f x) = Iio a :=
  h.dual.iUnion_Ioi_eq

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

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

Разделы

Аффилиация

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