mapRange_add — Mathlib

English

MapRange is additive: mapRange f hf is a homomorphism with respect to addition of vector measures.

Русский

MapRange сохраняет сумму: mapRange f hf является гомоморфизмом по сложению векторных мер.

LaTeX

$$$$ (v + w).\\mathrm{mapRange} f hf = v.\\mathrm{mapRange} f hf + w.\\mathrm{mapRange} f hf. $$$$

Lean4

@[simp]
theorem mapRange_add {v w : VectorMeasure α M} {f : M →+ N} (hf : Continuous f) :
    (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf :=
  by
  ext
  simp

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