iInter_Iic_eq_empty_iff — Mathlib

English

The intersection of all left-closed intervals Iic(f(i)) is empty if and only if the range of f is not bounded below.

Русский

Пересечение всех интервалов Iic(f(i)) пусто тогда и только тогда, когда образ f не ограничен снизу.

LaTeX

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

Lean4

theorem iInter_Iic_eq_empty_iff : ⋂ i, Iic (f i) = ∅ ↔ ¬BddBelow (range f) := by
  simp [not_bddBelow_iff, Set.eq_empty_iff_forall_notMem]

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