max — Mathlib

English

If f and g are almost everywhere measurable with respect to μ, then the pointwise maximum is also almost everywhere measurable with respect to μ.

Русский

Если f и g АЕ-измеримы по μ, то их точечное максимум также АЕ-измерим по μ.

LaTeX

$$$\text{AEMeasurable}(f,\mu) \land \text{AEMeasurable}(g,\mu) \Rightarrow \text{AEMeasurable}(\lambda a. \max(f(a), g(a)), \mu)$$$

Lean4

@[measurability, fun_prop]
nonrec theorem max {f g : δ → α} {μ : Measure δ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (fun a => max (f a) (g a)) μ :=
  ⟨fun a => max (hf.mk f a) (hg.mk g a), hf.measurable_mk.max hg.measurable_mk,
    EventuallyEq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩

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