II_σ

Mathlib.AlgebraicTopology.SimplicialObject.II

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

English

II.σ i is the opposite of δ at i.succ.castSucc: II.σ i = (δ i.succ.castSucc).op.

Русский

II.σ i — противоположность δ в i.succ.castSucc: II.σ i = (δ i.succ.castSucc).op.

LaTeX

$$$II_\\sigma i = (\\delta i.succ.castSucc).op$$$

Lean4

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

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

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

Разделы

Аффилиация

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