liminf_of_not_isCoboundedUnder — Mathlib

English

Let f be a filter on ι and u : ι → ℝ≥0. If f.IsCoboundedUnder (≥) u is false, then the liminf of u along f is 0.

Русский

Пусть f — фильтр на ι и u : ι → ℝ≥0. Если f.IsCoboundedUnder (≥) u ложно, то liminf u по f равен 0.

LaTeX

$$$\\\\forall f : \\text{Filter } ι,\\\\;\\\\neg f.IsCoboundedUnder (\\\\ge) u \\\\Rightarrow \\\\ liminf u f = 0$$$

Lean4

@[simp]
theorem liminf_of_not_isCoboundedUnder (hf : ¬f.IsCoboundedUnder (· ≥ ·) u) : liminf u f = 0 :=
  limsInf_of_not_isCobounded hf

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