add — Mathlib

English

The sum of two vector measures is a vector measure, with measureOf' given by the sum of the parts.

Русский

Сумма двух векторных мер является векторной мерой, measureOf' равна сумме частей.

LaTeX

$$def add (v w : VectorMeasure α M) : VectorMeasure α M$$

Lean4

/-- The sum of two vector measure is a vector measure. -/
def add (v w : VectorMeasure α M) : VectorMeasure α M
    where
  measureOf' := v + w
  empty' := by simp
  not_measurable' _ hi := by rw [Pi.add_apply, v.not_measurable hi, w.not_measurable hi, add_zero]
  m_iUnion' _ hf₁ hf₂ := HasSum.add (v.m_iUnion hf₁ hf₂) (w.m_iUnion hf₁ hf₂)

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