iInter_Iio_of_not_bddBelow_range — Mathlib

English

If the range of f is not bounded below, then the intersection of all Iio(f(i)) is empty.

Русский

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

LaTeX

$$$$ \bigcap_{i} \mathrm{Iio}(f(i)) = \emptyset \quad\Rightarrow\quad \neg \mathrm{BddBelow}(\operatorname{range}(f)). $$$$

Lean4

theorem iInter_Iio_of_not_bddBelow_range (hf : ¬BddBelow (range f)) : ⋂ i, Iio (f i) = ∅ :=
  by
  refine eq_empty_of_subset_empty ?_
  rw [← iInter_Iic_eq_empty_iff.mpr hf]
  gcongr
  exact Iio_subset_Iic_self

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