limsInf_of_not_isBounded — Mathlib

English

If a filter f on ℝ is not bounded with respect to ≥, then liminf f = 0.

Русский

Если фильтр f на ℝ не ограничен относительно ≥, то liminf f = 0.

LaTeX

$$$\neg f.IsBounded(\ge) \Rightarrow \liminf f = 0.$$$

Lean4

@[simp]
theorem limsInf_of_not_isBounded {f : Filter ℝ} (hf : ¬f.IsBounded (· ≥ ·)) : limsInf f = 0 :=
  by
  rw [limsInf]
  convert sSup_empty
  simpa [Set.eq_empty_iff_forall_notMem, IsBounded] using hf

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