hom_ext — Mathlib

English

If two arrows f, f' into a limit t have the same composites with every cone projection t.π.app j, then f = f'.

Русский

Если два морфиксся f и f' в предел t имеют одинаковые композиции с каждой проекцией конуса t.π.app j, то f = f'.

LaTeX

$$$\\forall j,\\; f\\circ t.π_{j} = f'\\circ t.π_{j} \\Rightarrow f = f'$$$

Lean4

/-- Two morphisms into a limit are equal if their compositions with
  each cone morphism are equal. -/
theorem hom_ext (h : IsLimit t) {W : C} {f f' : W ⟶ t.pt} (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) : f = f' := by
  rw [h.hom_lift f, h.hom_lift f']; congr; exact funext w

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