heq_comp_eqToHom_iff — Mathlib

English

Let f: X → Y, g: Z → Z' and h: Y = W. Then g ≍ f ≫ eqToHom h iff g ≍ f; i.e. the left factor can be swapped through the right-hand composition with eqToHom.

Русский

Пусть f: X→Y, g: Z→Z' и h: Y = W. Тогда g ≍ f ≫ eqToHom h эквивалентно g ≍ f; то есть левая часть может быть перенесена через правую композицию с eqToHom.

LaTeX

$$$ g \\mathrel{\\equiv} f \\circ eqToHom(h) \\; \\Longleftrightarrow \\; g \\mathrel{\\equiv} f $$$

Lean4

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

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