toMeasure_smul — Mathlib

English

Let Ω be a measurable space, μ a finite measure on Ω, and c a scalar. Then the underlying measure of c · μ is the scalar multiple c of the underlying measure μ.

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem toMeasure_smul (c : R) (μ : FiniteMeasure Ω) : ↑(c • μ) = c • (μ : Measure Ω) :=
  rfl

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