limsup_eq_iInf_iSup — Mathlib

English

For a sequence u: ℕ → α in a complete lattice, limsup u atTop equals ⨅ n, ⨆ i ≥ n, u(i).

Русский

Для последовательности u: ℕ → α в полной решётке лимсуп на atTop равен ⨅ n, ⨆ i ≥ n, u(i).

LaTeX

$$$\\limsup u\\, {\\text{atTop}} = \\inf_{n∈\\mathbb{N}} \\; \\sup_{i≥n} u(i)$$$

Lean4

/-- In a complete lattice, the limsup of a function is the infimum over sets `s` in the filter
of the supremum of the function over `s` -/
theorem limsup_eq_iInf_iSup {f : Filter β} {u : β → α} : limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a :=
  (f.basis_sets.map u).limsSup_eq_iInf_sSup.trans <| by simp only [sSup_image, id]

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