le_limsup_of_frequently_le' — Mathlib

English

If u(a) ≥ x holds frequently along f, then x ≤ limsup u f.

Русский

Если x ≤ u(a) держится часто по фильтру f, тогда x ≤ limsup u f.

LaTeX

$$$\\exists^{\\text{ frequently }} a \\in f:\\ x \\le u(a) \\quad\\Rightarrow\\quad x \\le \\limsup u f$$$

Lean4

theorem le_limsup_of_frequently_le' {α β} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β}
    (h : ∃ᶠ a in f, x ≤ u a) : x ≤ limsup u f :=
  liminf_le_of_frequently_le' (β := βᵒᵈ) h

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