mul — Mathlib

English

If f and g are AEFinStronglyMeasurable with respect to μ, then their pointwise product f·g is AEFinStronglyMeasurable with respect to μ.

Русский

Если f и g — AEFinStronglyMeasurable по μ, то их покомпонентное произведение f·g — AEFinStronglyMeasurable по μ.

LaTeX

$$$\text{AEFinStronglyMeasurable}(f, μ) \land \text{AEFinStronglyMeasurable}(g, μ) \Rightarrow \text{AEFinStronglyMeasurable}(f \cdot g, μ).$$$

Lean4

@[aesop safe 20 (rule_sets := [Measurable])]
protected theorem mul [MulZeroClass β] [ContinuousMul β] (hf : AEFinStronglyMeasurable f μ)
    (hg : AEFinStronglyMeasurable g μ) : AEFinStronglyMeasurable (f * g) μ :=
  ⟨hf.mk f * hg.mk g, hf.finStronglyMeasurable_mk.mul hg.finStronglyMeasurable_mk, hf.ae_eq_mk.mul hg.ae_eq_mk⟩

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