comp_eqToHom_iff — Mathlib

English

Two equalities f ≫ eqToHom(p) = g and f = g ≫ eqToHom(p^{-1}) are equivalent.

Русский

Две равенства f ≫ eqToHom(p) = g и f = g ≫ eqToHom(p^{-1}) эквивалентны.

LaTeX

$$$ {X Y Z} (p: Y= X) (f: X\to Y) (g: X\to Z) : f \circ eqToHom(p) = g \Leftrightarrow g = eqToHom(p)^{-1} \circ f.$$$

Lean4

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

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