mk_surjective

Mathlib.AlgebraicTopology.SimplicialSet.Simplices

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

English

Every element s of SSet.S arises from some finite n and some x in X._⟨n⟩ via the constructor mk.

Русский

Любой элемент s SSet.S появляется как mk x для некоторого конечного n и некоторого x в X_{⟨n⟩}.

LaTeX

$$$\exists n\, \exists x\, s = \mathrm{mk}(x)$$$

Lean4

theorem mk_surjective (s : X.S) : ∃ (n : ℕ) (x : X _⦋n⦌), s = mk x :=
  ⟨s.dim, s.simplex, rfl⟩

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

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

Разделы

Аффилиация

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