eq_from

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsZero.eq_from

English

Let X be zero and f: Y → X. Then f equals h.from_Y, where h is IsZero X.

Русский

Пусть X нулевой. Тогда для любого f: Y → X выполняется f = h.from_Y, где h — IsZero X.

LaTeX

$$$\\\\forall {Y}(f: Y \\rightarrow X), f = h.from_Y$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru