instModuleNNReal — Mathlib

English

The collection of finite measures on Ω carries a natural module structure over ℝ≥0, with the scalar action given by (c, μ) ↦ c · μ, acting pointwise on set values: (c · μ)(A) = c · μ(A).

Русский

Множество конечных мер на Ω образует естественную структуру модуля над ℝ≥0, где скалярное умножение задаётся как (c, μ) ↦ c · μ и действует по значению на любом множестве: (c · μ)(A) = c · μ(A).

LaTeX

$$$\forall c \ge 0,\ \forall \mu,\nu,\ (c \cdot \mu)(A) = c \cdot \mu(A)\quad\text{for all } A \subseteq \Omega$$$

Lean4

instance {Ω : Type*} [MeasurableSpace Ω] : Module ℝ≥0 (FiniteMeasure Ω) :=
  Function.Injective.module _ toMeasureAddMonoidHom toMeasure_injective toMeasure_smul

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