toENNRealVectorMeasure_add — Mathlib

English

The ENNReal vector measure of a sum equals the sum of ENNReal vector measures.

Русский

Векторная мера ENNReal суммы равна сумме ENNReal векторных мер.

LaTeX

$$$ (\mu + \nu).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure $$$

Lean4

@[simp]
theorem toENNRealVectorMeasure_add (μ ν : Measure α) :
    (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure :=
  by
  refine MeasureTheory.VectorMeasure.ext fun i hi => ?_
  rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
    toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]

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