P_succ

Mathlib.AlgebraicTopology.DoldKan.Projections

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

English

The inductive definition of P in successive stages satisfies P(q+1) = P(q) ∘ (I + Hσ q).

Русский

Переход к следующему ступеню: P(q+1) = P(q) ∘ (I + Hσ q).

LaTeX

$$$ P_{q+1} = P_q \circ (I + H\sigma_q) $$$

Lean4

theorem P_succ (q : ℕ) : (P (q + 1) : K[X] ⟶ K[X]) = P q ≫ (𝟙 _ + Hσ q) :=
  rfl

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

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

Разделы

Аффилиация

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