isGLB — Mathlib

English

If each f_i is a.e. measurable and ae-limit of LUB holds almost everywhere, then g is a.e. measurable.

Русский

Если каждый f_i а.е. измеримы и почти везде выполняется предел LUB, то g измерим а.е.

LaTeX

$$$\forall i,\text{AEMeasurable}(f_i) \Rightarrow (ae\,IsLUB\, on\, b) \Rightarrow \text{AEMeasurable}(g)$$$

Lean4

theorem isGLB {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α} {g : δ → α} (hf : ∀ i, AEMeasurable (f i) μ)
    (hg : ∀ᵐ b ∂μ, IsGLB {a | ∃ i, f i b = a} (g b)) : AEMeasurable g μ :=
  AEMeasurable.isLUB (α := αᵒᵈ) hf hg

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