limsup — Mathlib

English

The lm sup for a general filter is measurable (generalization of limsup).

Русский

Обобщение limsup для произвольного фильтра: измеримо.

LaTeX

$$Measurable.limsup' {ι ι'} {f : ι → δ → α} {u : Filter ι} (hf : ∀ i, Measurable (f i)) {p : ι' → Prop} {s : ι' → Set ι} → Measurable fun x => Filter.limsup (fun i => f i x) u$$

Lean4

/-- `limsup` over `ℕ` is measurable. See `Measurable.limsup'` for a version with a general filter.
-/
@[measurability, fun_prop]
theorem limsup {f : ℕ → δ → α} (hf : ∀ i, Measurable (f i)) : Measurable fun x => limsup (fun i => f i x) atTop :=
  .limsup' hf atTop_countable_basis fun _ => to_countable _

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