ext' — Mathlib

English

An extensionality lemma for morphisms in Comma.Hom: if the left/right components are equal, the whole morphisms are equal.

Русский

Лемма экстенсиональности для морфизмов в 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

/-- Alternative `ext` lemma for `Comma.Hom`. -/
@[ext]
theorem ext' {X Y : P.Comma L R Q W} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g :=
  Comma.Hom.ext (congrArg CommaMorphism.left h) (congrArg CommaMorphism.right h)

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