P_f_0_eq — Mathlib

English

The inductive step for Q is given by Q(q+1) = Q(q) − P(q) ∘ Hσ q.

Русский

Переход Q на следующую ступень: Q(q+1) = Q(q) − P(q) ∘ Hσ q.

LaTeX

$$$ Q_{q+1} = Q_q - P_q \circ H\sigma_q $$$

Lean4

/-- All the `P q` coincide with `𝟙 _` in degree 0. -/
@[simp]
theorem P_f_0_eq (q : ℕ) : ((P q).f 0 : X _⦋0⦌ ⟶ X _⦋0⦌) = 𝟙 _ := by
  induction q with
  | zero => rfl
  | succ q hq =>
    simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f, HomologicalComplex.id_f, id_comp, hq,
      Hσ_eq_zero, add_zero]

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