limsSup_eq_of_le_nhds — Mathlib

English

If a filter is converging, its limsup equals its liminf equals the limit, hence f ≤ 𝓝 a.

Русский

Если фильтр сходится, его limsup равен liminf и равен пределу a, следовательно f ≤ 𝓝 a.

LaTeX

$$$ (hl: f.IsBounded (≤)) (hg: f.IsBounded (≥)) (hs: f.limsSup = a) (hi: f.limsInf = a) : f ≤ 𝓝 a. $$$

Lean4

/-- If a filter is converging, its liminf coincides with its limit. -/
theorem limsSup_eq_of_le_nhds {f : Filter α} {a : α} [NeBot f] (h : f ≤ 𝓝 a) : f.limsSup = a :=
  limsInf_eq_of_le_nhds (α := αᵒᵈ) h

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