map_sub — Mathlib

English

If f preserves subtraction, then mapping distributes over matrix subtraction: (M-N).map f = M.map f - N.map f.

Русский

Если f сохраняет вычитание, отображение распределено по вычитанию матриц: (M-N).map f = M.map f - N.map f.

LaTeX

$$$ (M - N).map\\ f = M.map\\ f - N.map\\ f $$$

Lean4

protected theorem map_sub [Sub α] [Sub β] (f : α → β) (hf : ∀ a₁ a₂, f (a₁ - a₂) = f a₁ - f a₂) (M N : Matrix m n α) :
    (M - N).map f = M.map f - N.map f :=
  ext fun _ _ => hf _ _

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