min — Mathlib

English

If f and g are a.e. measurable with respect to μ, then the a.e. minimum is also a.e. measurable with respect to μ.

Русский

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

LaTeX

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

Lean4

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

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