coe_smul

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.coe_smul

English

For any scalar c and any set s, the scaled measure satisfies (c • μ)(s) = c • μ(s).

Русский

Для любого скаляра c и множества s выполняется (c • μ)(s) = c • μ(s).

LaTeX

$$$\forall c,\mu, s:\; (c \cdot \mu)(s) = c \cdot \mu(s).$$$

Lean4

@[simp, norm_cast]
theorem coe_smul {_m : MeasurableSpace α} (c : R) (μ : Measure α) : ⇑(c • μ) = c • ⇑μ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru