eventually_le_limsup — Mathlib

English

For any countable-intersection filter f, and any function u : α → ℝ≥0∞, one has u(y) ≤ limsup_f u for all y in a tail of f (i.e., eventually).

Русский

Для фильтра f с счётным пересечением и любой функции u: α → ℝ≥0∞ выполняется, что для всех y из хвоста фильтра f выполняется u(y) ≤ limsup_f u.

LaTeX

$$$\\\\forall u : α \\to \\mathbb{R}_{\\\\ge 0,\\\\infty},\\\\;\\\\forall y \\\\in f \\\\text{ eventually},\\\\; u(y) \\\\le f.limsup u$$$

Lean4

theorem eventually_le_limsup [CountableInterFilter f] (u : α → ℝ≥0∞) : ∀ᶠ y in f, u y ≤ f.limsup u :=
  _root_.eventually_le_limsup

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