eqToHom_comp_iff — Mathlib

English

For any p: X = X' and maps f,g, eqToHom p ≫ g = f iff g = eqToHom p^{-1} ≫ f.

Русский

При любом p: X = X' и отображениях f,g, eqToHom p ≫ g = f эквивалентно g = eqToHom p^{-1} ≫ f.

LaTeX

$$$ {X X' Y} (p: X = X') (f: X \to Y) (g: X' \to Y) : eqToHom(p) \; g = f \iff \ g = eqToHom(p)^{-1} \; f.$$$

Lean4

theorem eqToHom_comp_iff {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) :
    eqToHom p ≫ g = f ↔ g = eqToHom p.symm ≫ f :=
  { mp := fun h => h ▸ by simp
    mpr := fun h => h ▸ by simp }

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