δ₂_two_comp_σ₂_zero

Mathlib.AlgebraicTopology.SimplexCategory.Truncated

URI: https://scilib.ai/kg/mathlib#SimplexCategory.Truncated.δ₂_two_comp_σ₂_zero

English

In the 2-truncated setting, δ₂(2) followed by σ₂(0) equals σ₂(0) followed by δ₂(1).

Русский

В 2-усеченной настройке δ₂(2) затем σ₂(0) равно σ₂(0) затем δ₂(1).

LaTeX

$$$\\delta_2(2) \\circ \\sigma_2(0) = \\sigma_2(0) \\circ \\delta_2(1)$$$

Lean4

@[reassoc]
theorem δ₂_two_comp_σ₂_zero : δ₂ (2 : Fin 3) ≫ σ₂ 0 = σ₂ 0 ≫ δ₂ 1 :=
  SimplexCategory.δ_comp_σ_of_gt' (by decide)

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

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

Разделы

Аффилиация

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