iInf — Mathlib

English

Symmetric to iSup: the infimum of AEMeasurable functions is AEMeasurable.

Русский

Аналогично iSup: инфимум AEMeasurable функций — AEMeasurable.

LaTeX

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

Lean4

@[measurability, fun_prop]
protected theorem iInf {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α} (hf : ∀ i, AEMeasurable (f i) μ) :
    AEMeasurable (fun b => ⨅ i, f i b) μ :=
  .iSup (α := αᵒᵈ) hf

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