instEpiSimplexCategoryE

Mathlib.AlgebraicTopology.SimplicialObject.Split

URI: https://scilib.ai/kg/mathlib#SimplicialObject.Splitting.IndexSet.instEpiSimplexCategoryE

English

For i : Fin(n+1) and x : Fin(n+2), map' { toFun := i.predAbove, monotone' := Fin.predAbove_right_monotone i } x equals i.succ.castSucc.succAbove x.

Русский

Для i : Fin(n+1) и x : Fin(n+2) отображение map' с toFun = i.predAbove даёт i.succ.castSucc.succAbove x.

LaTeX

$$$map'\\{ toFun := i.predAbove, monotone' := Fin.predAbove_right_monotone i \\} x = i.succ.castSucc.succAbove x$$$

Lean4

instance : Epi A.e :=
  A.2.2

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

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

Разделы

Аффилиация

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