smul — Mathlib

English

If f and g are AEMeasurable, then the pointwise smul f(x) • g(x) is AEMeasurable.

Русский

Если f и g AEMеасurable, то точечное произведение f(x) • g(x) AEMеасurable.

LaTeX

$$$\text{AEMeasurable } f μ \land \text{AEMeasurable } g μ \Rightarrow \text{AEMeasurable}(\lambda x. f(x)\cdot g(x)) μ$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
theorem smul [MeasurableSMul₂ M X] {μ : Measure α} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    AEMeasurable (fun x => f x • g x) μ :=
  MeasurableSMul₂.measurable_smul.comp_aemeasurable (hf.prodMk hg)

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