eq_to — Mathlib

English

Let X be a zero object. Then for every Y and every morphism f: X → Y, f equals the canonical map h.to_Y from X to Y.

Русский

Пусть X является нулевым объектом. Тогда для любого объекта Y и любого отображения f: X → Y выполняется f = h.to_Y, где h задаёт нулевой объект.

LaTeX

$$$\\\\forall Y\\\\, \\\\forall f : X \\\\rightarrow Y,\n f = h.to_Y$$$

Lean4

theorem eq_to (h : IsZero X) (f : X ⟶ Y) : f = h.to_ Y :=
  @Unique.eq_default _ (id _) _

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