toTopObj_one_add_eq_one

Mathlib.AlgebraicTopology.TopologicalSimplex

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

English

For every f in the 1-simplex top object, f(0) + f(1) = 1.

Русский

Для каждого f из 1-мерного топологического простейшего выполняется f(0) + f(1) = 1.

LaTeX

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

Lean4

theorem toTopObj_one_add_eq_one (f : ⦋1⦌.toTopObj) : f 0 + f 1 = 1 := by
  simpa [toType_apply, Finset.sum] using show ∑ _, _ = _ from f.2

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

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

Разделы

Аффилиация

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