mk_surjective

Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

URI: https://scilib.ai/kg/mathlib#SSet.N.mk_surjective

English

Every nerve simplex s arises as SSet.N.mk of some nondegenerate simplex.

Русский

Каждый симплекс нерва получается как SSet.N.mk от некоторого не degenerate-симплекса.

LaTeX

$$$\forall s:\, X.N,\; \exists n,\; \exists y:\, X.nonDegenerate n,\; s = SSet.N.mk y$$$

Lean4

theorem mk_surjective (x : X.N) : ∃ (n : ℕ) (y : X.nonDegenerate n), x = N.mk _ y.prop :=
  ⟨x.dim, ⟨_, x.nonDegenerate⟩, rfl⟩

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

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

Разделы

Аффилиация

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