inf' — Mathlib

English

Let f,g: α → M be almost everywhere measurable with respect to μ, and M be a lattice with a measurable infimum operation. Then the pointwise infimum a ↦ f(a) ⊓ g(a) is AEMeasurable μ.

Русский

Пусть f,g: α → M почти измеримы по μ, и операция inf на M измерима. Тогда a ↦ f(a) ⊓ g(a) почти измерима по μ.

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 (f ⊓ g) μ :=
  measurable_inf.comp_aemeasurable (hf.prodMk hg)

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