spine_arrow

Mathlib.AlgebraicTopology.SimplicialSet.Path

URI: https://scilib.ai/kg/mathlib#SSet.Truncated.spine_arrow

English

The arrow component of a spine path is the corresponding subpath built from edge data.

Русский

Стрелка позвоночника пути соответствует подпути на основе ребер.

LaTeX

$$$\\text{spine}_{\\text{arrow}}(f) = f$$$

Lean4

@[simp]
theorem spine_arrow (Δ : X _⦋m⦌ₙ ₊ ₁) (i : Fin m) : (X.spine m hₘ Δ).arrow i = X.map (tr (mkOfSucc i)).op Δ :=
  rfl

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

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

Разделы

Аффилиация

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