sup — Mathlib

English

If f and g are AEMeasurable, then x ↦ f(x) ⊔ g(x) is AEMeasurable.

Русский

Если f и g AEMeasurable, то x ↦ f(x) ⊔ g(x) измеримо практически.

LaTeX

$$$AEMeasurable f \mu \Rightarrow AEMeasurable g \mu \Rightarrow AEMeasurable\bigl(x \mapsto f(x) \sqcup g(x)\bigr) \mu$$$

Lean4

@[measurability]
theorem sup (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun a => f a ⊔ g a) μ :=
  measurable_sup.comp_aemeasurable (hf.prodMk hg)

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