ε_app_f_succ

Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ

English

For any X, and any natural number n, the component of ε.app X at level n+1 is zero.

Русский

Для любого X и любого n, компонент ε.app X в уровне n+1 равен нулю.

LaTeX

$$$\forall X, \forall n, \ (\varepsilon.{\rm app}\,X).f\,(n+1) = 0$$$

Lean4

@[simp]
theorem ε_app_f_succ [Limits.HasZeroObject C] (X : SimplicialObject.Augmented C) (n : ℕ) : (ε.app X).f (n + 1) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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