II_δ

Mathlib.AlgebraicTopology.SimplicialObject.II

URI: https://scilib.ai/kg/mathlib#SimplexCategory.II_δ

English

II.δ equals the opposite of δ at the successor index: II.δ i = (δ i.succ.castSucc).op.

Русский

II.δ равняется противоположности δ в индексе-смещении: II.δ i = (δ i.succ.castSucc).op.

LaTeX

$$$II.δ i = (δ i.succ.castSucc)^{op}$$$

Lean4

@[simp]
theorem II_δ {n : ℕ} (i : Fin (n + 2)) : II.δ i = (σ i).op :=
  Quiver.Hom.unop_inj (by ext : 3; apply II.map'_succAboveOrderEmb)

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

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

Разделы

Аффилиация

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