prod_smul_left — Mathlib

English

For any nonnegative scalar c, the product of the scaled measure c·μ with ν equals c times the product μ·ν: (c·μ) × ν = c·(μ × ν).

Русский

Для любого ненулевого множителя c выполняется: (c·μ) × ν = c·(μ × ν).

LaTeX

$$$(c \cdot \mu) \otimes \nu = c \cdot (\mu \otimes \nu)$$$

Lean4

theorem prod_smul_left {μ : Measure α} (c : ℝ≥0∞) : (c • μ).prod ν = c • (μ.prod ν) :=
  by
  ext s hs
  rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs]
  simp

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