const_inf — Mathlib

English

If f is AEMeasurable, then x ↦ c ⊓ f(x) is AEMeasurable for every c.

Русский

Если f AEMeasurable, то x ↦ c ⊓ f(x) является AEMeasurable для любого c.

LaTeX

$$$AEMeasurable(f,\mu) \Rightarrow \forall c, AEMeasurable\bigl(x \mapsto c \sqcap f(x)\bigr)\mu$$$

Lean4

@[measurability]
theorem const_inf (hf : AEMeasurable f μ) (c : M) : AEMeasurable (fun x => c ⊓ f x) μ :=
  (MeasurableInf.measurable_const_inf c).comp_aemeasurable hf

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