false_of_from_star

Mathlib.CategoryTheory.WithTerminal.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.WithTerminal.false_of_from_star

English

There is no morphism from the terminal object star to any X in WithTerminal.

Русский

Нет морфизма от терминального объекта star к любому X в WithTerminal.

LaTeX

$$$ \forall X, \mathrm{Hom}(\mathrm{star}, \mathrm{of} X) = \varnothing. $$$

Lean4

@[aesop safe destruct (rule_sets := [CategoryTheory])]
theorem false_of_from_star {X : C} (f : star ⟶ of X) : False :=
  (f : PEmpty).elim

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

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

Разделы

Аффилиация

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