objX_add_one

Mathlib.AlgebraicTopology.MooreComplex

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.NormalizedMooreComplex.objX_add_one

English

The object at degree n+1 equals the infimum over the kernels of the degeneracy maps δ.

Русский

Для степени n+1 объект равен инфимума по кернелам карт δ.

LaTeX

$$$objX X (n+1) = \inf_{k : Fin\,(n+1)} kernelSubobject (X.δ k.succ)$$$

Lean4

@[simp]
theorem objX_add_one (n) : objX X (n + 1) = Finset.univ.inf fun k : Fin (n + 1) => kernelSubobject (X.δ k.succ) :=
  rfl

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

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

Разделы

Аффилиация

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