Q_is_eventually_constant

Mathlib.AlgebraicTopology.DoldKan.PInfty

URI: https://scilib.ai/kg/mathlib#AlgebraicTopology.DoldKan.Q_is_eventually_constant

← MathLib Explorer

English

For every n, the n-th component of PInfty coincides with the n-th component of P.

Русский

Для каждого n-ого уровня компонент PInfty.f n совпадает с компонентой P.f n.

LaTeX

$$$PInfty.f_n = P_n.f_n$$$

Lean4

theorem Q_is_eventually_constant {q n : ℕ} (hqn : n ≤ q) : ((Q (q + 1)).f n : X _⦋n⦌ ⟶ _) = (Q q).f n := by
  simp only [Q, HomologicalComplex.sub_f_apply, P_is_eventually_constant hqn]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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