instAddCommMonoid — Mathlib

English

There is a canonical additive monoid homomorphism sending a measure to its evaluation map on sets: μ ↦ (s ↦ μ(s)).

Русский

Существует каноническое аддитивное моноидное гомоморфное отображение меры в отображение, сопоставляющее каждому множеству его меру: μ ↦ (s ↦ μ(s)).

LaTeX

$$$\text{coeAddHom}: \text{Measure}(\alpha) \to_+ (\mathsf{Set}(\alpha) \to \mathbb{R}_{\ge 0}^\infty)$ with toFun(s) = μ(s) and properties $0$-preserving and additive.$$

Lean4

instance instAddCommMonoid {_ : MeasurableSpace α} : AddCommMonoid (Measure α) :=
  toOuterMeasure_injective.addCommMonoid toOuterMeasure zero_toOuterMeasure add_toOuterMeasure fun _ _ =>
    smul_toOuterMeasure _ _

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