exists_eq_const_of_zero

Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

English

Any morphism from ⦋0⦌ to n factors as a constant morphism with some value a in Fin(n+1).

Русский

Любой морфизм из ⦋0⦌ в n факторизуется как константный морфизм с некоторым значением a ∈ Fin(n+1).

LaTeX

$$$\\exists a, f = const _ n a.$$$

Lean4

theorem exists_eq_const_of_zero {n : SimplexCategory} (f : ⦋0⦌ ⟶ n) : ∃ a, f = const _ n a :=
  ⟨_, eq_const_of_zero _⟩

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

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

Разделы

Аффилиация

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