map_add — Mathlib

English

The induced map from quotientPiLift preserves addition: the image of x + y equals the sum of the images.

Русский

Полученное отображение сохраняет сложение: образ суммы равен сумме образов.

LaTeX

$$LinearMap.map_add (quotientPiLift p ... ) x y$$

Lean4

theorem map_add (x y : ((i : ι) → Ms i) ⧸ pi Set.univ p) : toFun p (x + y) = toFun p x + toFun p y :=
  LinearMap.map_add (quotientPiLift p (fun i => (p i).mkQ) fun i => (ker_mkQ (p i)).ge) x y

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