map_sub — Mathlib

English

For any f : α → β and x,y ∈ FreeAbelianGroup α, map f of (x - y) equals (map f x) - (map f y).

Русский

Для любой f : α → β и x,y ∈ FreeAbelianGroup α отображение f к (x - y) равно (map f x) - (map f y).

LaTeX

$$$ \forall {\alpha \to \beta} (f : \alpha \to \beta) (x y : FreeAbelianGroup(\alpha)),\; f <$> (x - y) = f <$> x - f <$> y$$$

Lean4

@[simp]
protected theorem map_sub (f : α → β) (x y : FreeAbelianGroup α) : f <$> (x - y) = f <$> x - f <$> y :=
  map_sub (lift <| of ∘ f) _ _

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