heq_eqToHom_comp_iff — Mathlib

English

A mirrored version of conj_eqToHom_iff_heq: HEq g f is equivalent to g eqToHom after a relabeling.

Русский

Зеркальное утверждение conj_eqToHom_iff_heq: HEq g f эквивалентно g ≍ f после перестановки переменных.

LaTeX

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

Lean4

@[simp]
theorem heq_eqToHom_comp_iff {C} [Category C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) :
    g ≍ eqToHom h ≫ f ↔ g ≍ f :=
  ⟨(·.trans (eqToHom_comp_heq ..)), (·.trans (eqToHom_comp_heq ..).symm)⟩

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