instNonemptyElemForallToTypeOrderHomFinHAddNatLenOfNatNNRealToTopObj

Mathlib.AlgebraicTopology.TopologicalSimplex

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

English

For every x in SimplexCategory, x.toTopObj is nonempty.

Русский

Для каждого x из SimplexCategory множество x.toTopObj непусто.

LaTeX

$$$\\forall x,\\; x^{\\mathrm{top}} \\\\text{непуст }$$

Lean4

instance (x : SimplexCategory) : Nonempty x.toTopObj :=
  ⟨⟨Pi.single 0 1, (show ∑ _, _ = _ by simp)⟩⟩

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

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

Разделы

Аффилиация

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