smul_apply — Mathlib

English

The same as item 144309: the underlying function of c · μ equals c times the underlying function of μ on sets.

Русский

То же, что и в пункте 144309: базовая функция c · μ равна c умножению базовой функции μ на множествах.

LaTeX

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

Lean4

@[simp]
theorem smul_apply [IsScalarTower R ℝ≥0 ℝ≥0] (c : R) (μ : FiniteMeasure Ω) (s : Set Ω) : (c • μ) s = c • μ s := by
  rw [coeFn_smul, Pi.smul_apply]

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