map_add — Mathlib

English

MapRange is additive in its arguments: mapRange (v + w) hf = mapRange v hf + mapRange w hf.

Русский

MapRange аддитивен по аргументам: mapRange (v + w) hf = mapRange v hf + mapRange w hf.

LaTeX

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

Lean4

theorem map_add (v w : VectorMeasure α M) (f : α → β) : (v + w).map f = v.map f + w.map f :=
  by
  by_cases hf : Measurable f
  · ext i hi
    simp [map_apply _ hf hi]
  · simp [map, dif_neg hf]

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