map_zero — Mathlib

English

The operation mapRange preserves addition: (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf.

Русский

Операция mapRange сохраняет сумму: (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf.

LaTeX

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

Lean4

@[simp]
theorem map_zero (f : α → β) : (0 : VectorMeasure α M).map f = 0 :=
  by
  by_cases hf : Measurable f
  · ext i hi
    rw [map_apply _ hf hi, zero_apply, zero_apply]
  · exact dif_neg hf

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