limsInf_of_not_isCobounded — Mathlib

English

Let f be a filter on the nonnegative reals. If f is not cobounded above with respect to the usual order, then the limit inferior of f is 0.

Русский

Пусть f — фильтр на множествах неотрицательных чисел. Если f не ограничен сверху в смысле кограницы (не cobounded), то нижний предел (lim inf) f равен 0.

LaTeX

$$$\\\\forall f : \\text{Filter } \\mathbb{R}_{\\\\ge 0},\\\\; \\\\neg f.IsCobounded(\\\\ge) \\\\Rightarrow \\\\ limsInf f = 0$$$

Lean4

@[simp]
theorem limsInf_of_not_isCobounded {f : Filter ℝ≥0} (hf : ¬f.IsCobounded (· ≥ ·)) : limsInf f = 0 := by
  rwa [limsInf, sSup_of_not_bddAbove]

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