inf — Mathlib

English

Let f,g: α → M be AEMeasurable with respect to μ. Then the function a ↦ f(a) ⊓ g(a) is AEMeasurable μ.

Русский

Пусть f,g: α → M являются AEM-измеримыми по μ. Тогда a ↦ f(a) ⊓ g(a) является AEM-измеримой по μ.

LaTeX

$$$\text{AEMeasurable}(f,\mu) \;\land\; \text{AEMeasurable}(g,\mu) \Rightarrow \text{AEMeasurable}(a \mapsto f(a) \sqcap g(a),\mu).$$$

Lean4

@[measurability]
theorem inf (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun a => f a ⊓ g a) μ :=
  measurable_inf.comp_aemeasurable (hf.prodMk hg)

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