homAddEquiv_symm_sub — Mathlib

English

Symmetric additive equivalence preserves subtraction on the symmetric side.

Русский

Симметрическое аддитивное соответствие сохраняет вычитание на симметричной стороне.

LaTeX

$$((adj.homEquiv X Y).symm (f - g)) = ((adj.homEquiv X Y).symm f) - ((adj.homEquiv X Y).symm g)$$

Lean4

@[simp]
theorem homAddEquiv_symm_sub (X : C) (Y : D) (f f' : X ⟶ G.obj Y) :
    (adj.homEquiv X Y).symm (f - f') = (adj.homEquiv X Y).symm f - (adj.homEquiv X Y).symm f' :=
  map_sub (adj.homAddEquiv X Y).symm _ _

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