iUnion_Iic_of_not_bddAbove_range — Mathlib

English

If the range of f is not bounded above, then the union over i of Iic(f(i)) equals the universal set.

Русский

Если образ f не ограничен сверху, то объединение Iic(f(i)) даёт всю пространство.

LaTeX

$$$$\neg \mathrm{BddAbove}(\operatorname{range}(f)) \Rightarrow \bigcup_{i} \mathrm{Iic}(f(i)) = \operatorname{univ}. $$$$

Lean4

theorem iUnion_Iic_of_not_bddAbove_range (hf : ¬BddAbove (range f)) : ⋃ i, Iic (f i) = univ :=
  by
  refine Set.eq_univ_of_subset ?_ (iUnion_Iio_eq_univ_iff.mpr hf)
  gcongr
  exact Iio_subset_Iic_self

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