δ₀_eq

Mathlib.AlgebraicTopology.SimplicialSet.Nerve

URI: https://scilib.ai/kg/mathlib#CategoryTheory.nerve.δ₀_eq

English

The δ-face at 0 in the nerve equals the δ₀ component given by ComposableArrows.

Русский

δ‑глава на нуле в нерве равна δ₀ компоненте ComposableArrows.

LaTeX

$$$ (\CategoryTheory.SimplicialObject.δ (\CategoryTheory.nerve C) 0 x) = (\CategoryTheory.ComposableArrows.δ_0 x) $$$

Lean4

theorem δ₀_eq {x : nerve C _⦋n + 1⦌} : (nerve C).δ (0 : Fin (n + 2)) x = x.δ₀ :=
  rfl

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

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

Разделы

Аффилиация

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