limsSup_of_not_isBounded — Mathlib

English

For f : Filter NNReal, if f is not bounded (≤), then limsSup f = 0.

Русский

Для f : Filter NNReal, если f не ограничен (≤), то limsSup f = 0.

LaTeX

$$$\text{[simp] }\text{If } \neg f.IsBounded(\le) \text{ then } \operatorname{limsSup} f = 0.$$$

Lean4

@[simp]
theorem limsSup_of_not_isBounded {f : Filter ℝ≥0} (hf : ¬f.IsBounded (· ≤ ·)) : limsSup f = 0 :=
  by
  rw [limsSup, ← bot_eq_zero]
  convert sInf_empty
  simpa [Set.eq_empty_iff_forall_notMem, IsBounded] using hf

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