iSup — Mathlib

English

The infimum over a countable set of measurable functions is measurable by duality.

Русский

Инфиксный инфимум над счетным множеством измеримых функций измерим благодаря двойственности.

LaTeX

$$∀ i, Measurable (f i) → Measurable fun b => iInf fun i => f i b$$

Lean4

@[measurability, fun_prop]
protected theorem iSup {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α} (hf : ∀ i, AEMeasurable (f i) μ) :
    AEMeasurable (fun b => ⨆ i, f i b) μ :=
  by
  refine ⟨fun b ↦ ⨆ i, (hf i).mk (f i) b, .iSup (fun i ↦ (hf i).measurable_mk), ?_⟩
  filter_upwards [ae_all_iff.2 (fun i ↦ (hf i).ae_eq_mk)] with b hb using by simp [hb]

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