coeFn_smul — Mathlib

English

For any c ∈ R and μ ∈ FiniteMeasure Ω, the pointwise value of c · μ as a function on sets equals c times the value of μ as a function on sets: (c · μ)(A) = c · μ(A).

Русский

Пусть c ∈ R и μ — конечная мера. Тогда точечное значение c · μ по отношению к множествам равно c · μ по отношению к тем же множествам: (c · μ)(A) = c · μ(A).

LaTeX

$$$\forall A \subseteq \Omega,\ (c \cdot \mu)(A) = c \cdot \mu(A)$$$

Lean4

@[simp, norm_cast]
theorem coeFn_smul [IsScalarTower R ℝ≥0 ℝ≥0] (c : R) (μ : FiniteMeasure Ω) :
    (⇑(c • μ) : Set Ω → ℝ≥0) = c • (⇑μ : Set Ω → ℝ≥0) := by funext; simp [← ENNReal.coe_inj, ENNReal.coe_smul]

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