limsup_eq_zero_iff — Mathlib

English

For a countable-intersections filter f, and u : α → ℝ≥0∞, the limsup of u is zero if and only if u is eventually equal to 0 along f.

Русский

Для фильтра f с счётным пересечением и функции u : α → ℝ≥0∞, limsup u по f равен нулю тогда и только тогда, когда u эквивалентно нулю по f на некотором хвосте.

LaTeX

$$$f.limsup u = 0 \\iff u =_f 0$$$

Lean4

theorem limsup_eq_zero_iff [CountableInterFilter f] {u : α → ℝ≥0∞} : f.limsup u = 0 ↔ u =ᶠ[f] 0 :=
  limsup_eq_bot

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