nnreal_smul_coe_apply

Mathlib.MeasureTheory.Measure.MeasureSpace

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

English

If c is a nonnegative real number, then (c • μ)(s) = c * μ(s).

Русский

Если c неотрицательное число, то (c • μ)(s) = c * μ(s).

LaTeX

$$$\forall c:\\mathbb{R}_{\ge 0}, \; \forall \mu, s:\; (c \cdot \mu)(s) = c \cdot \mu(s).$$$

Lean4

@[simp]
theorem nnreal_smul_coe_apply {_m : MeasurableSpace α} (c : ℝ≥0) (μ : Measure α) (s : Set α) : c • μ s = c * μ s :=
  rfl

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

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

Разделы

Аффилиация

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