English
For a family f of elements in a linear order, the union of all open intervals Iio(f(i)) equals the whole space univ exactly when the image is not bounded above.
Русский
Для семейства элементов в линейном порядке объединение всех открытых интервалов Iio(f(i)) равно всей области тогда и только тогда, когда множество образов не ограничено сверху.
LaTeX
$$$$\bigcup_{i} Iio(f(i)) = \operatorname{univ} \quad\text{iff}\quad \neg \mathrm{BddAbove}(\operatorname{range}(f)).$$$$
Lean4
theorem iUnion_Iio_eq_univ_iff : ⋃ i, Iio (f i) = univ ↔ (¬BddAbove (range f)) := by
simp [not_bddAbove_iff, Set.eq_univ_iff_forall]