iUnion_Iio_eq_univ_iff — Mathlib

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]

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