liminf — Mathlib

English

The limsup over natural numbers of a sequence of measurable functions is measurable.

Русский

Лимасп над натуральными числами последовательности измеримых функций — измерим.

LaTeX

$$tf: ∀ i, Measurable (f i) → Measurable fun x => limsup (fun i => f i x) atTop$$

Lean4

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

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