δ₀_mk₂_eq

Mathlib.AlgebraicTopology.SimplicialSet.Nerve

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

English

The 2nd δ-face of the nerve of ComposableArrows on two arrows is mk₁ f.

Русский

δ₂ нерва ComposableArrows(f,g) равен mk₁ f.

LaTeX

$$$ (\nerve C).δ 2 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ f $$$

Lean4

theorem δ₀_mk₂_eq : (nerve C).δ 0 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ g :=
  ComposableArrows.ext₁ rfl rfl (by simp; rfl)

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

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

Разделы

Аффилиация

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