toTopObj_zero_apply_zero

Mathlib.AlgebraicTopology.TopologicalSimplex

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

English

For any f in the 0-simplex topological object, f(0) = 1.

Русский

Для любого f в вершине 0-мерного топологического простейшего выполняется f(0) = 1.

LaTeX

$$$\\forall f \\in (\\langle 0 \\rangle).toTopObj,\\; f(0)=1$$$

Lean4

@[simp]
theorem toTopObj_zero_apply_zero (f : ⦋0⦌.toTopObj) : f 0 = 1 := by simpa [toType_apply] using show ∑ _, _ = _ from f.2

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

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

Разделы

Аффилиация

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