inv_hom — Mathlib

English

Extensional lemma for Comma.Hom morphisms: equality of hom components implies equality of arrows in the comma.

Русский

Лемма экстенсиональности для морфизмов Comma.Hom: равенство гомкомпонент означает равенство стрелок в комме.

LaTeX

$$$\\text{ext'}:\\; \\forall X,Y: P.Comma L R Q W,\\; f,g: X\\to Y,\\; f.hom = g.hom \\Rightarrow f=g$$$

Lean4

theorem inv_hom {X Y : P.Comma L R Q W} (f : X ⟶ Y) [IsIso f] : (inv f).hom = inv f.hom :=
  by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← comp_hom, IsIso.hom_inv_id, id_hom]

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