uniqueHomToZero

Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

English

From any Δ there exists a unique morphism to the zero-simplex ⟦0⟧.

Русский

Из любого Δ существует единственный морфизм к нулевому простейшему ⟦0⟧.

LaTeX

$$$\\forall \\Delta,\\,\\exists ! f:\\Delta\\to \\langle 0 \\rangle.$$$

Lean4

instance uniqueHomToZero {Δ : SimplexCategory} : Unique (Δ ⟶ ⦋0⦌)
    where
  default := Δ.const _ 0
  uniq := eq_const_to_zero

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

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

Разделы

Аффилиация

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