eq_const_to_zero

Mathlib.AlgebraicTopology.SimplexCategory.Basic

URI: https://scilib.ai/kg/mathlib#SimplexCategory.eq_const_to_zero

English

Any arrow f: n ⟶ ⦋0⦌ is constant with value 0.

Русский

Любой стрелке f: n ⟶ ⦋0⦌ соответствует константный морфизм со значением 0.

LaTeX

$$$f = const n _ 0.$$$

Lean4

theorem eq_const_to_zero {n : SimplexCategory} (f : n ⟶ ⦋0⦌) : f = const n _ 0 :=
  by
  ext : 3
  apply @Subsingleton.elim (Fin 1)

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

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

Разделы

Аффилиация

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