conj_eqToHom_iff_heq' — Mathlib

English

A variant of conj_eqToHom_iff_heq with swapped variables yields the same equivalence.

Русский

Вариант утверждения конъюгации eqToHom с поменяными переменными даёт ту же эквивалентность.

LaTeX

$$$ \forall C [\text{Category } C] {W X Y Z} (f: W\to X) (g: Y\to Z) (h: W=Y) (h': Z=X),\; f = eqToHom(h) \; g \; eqToHom(h').symm \Leftrightarrow \; f \approx g $$$

Lean4

theorem conj_eqToHom_iff_heq' {C} [Category C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : Z = X) :
    f = eqToHom h ≫ g ≫ eqToHom h' ↔ f ≍ g :=
  conj_eqToHom_iff_heq _ _ _ h'.symm

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