PInfty_f_comp_QInfty_f — Mathlib

English

For each n, the composition PInfty.f n with QInfty.f n is the zero morphism.

Русский

Для каждого n композиция PInfty.f n с QInfty.f n равна нулю.

LaTeX

$$$ (PInfty.f n) \circ (QInfty.f n) = 0 $$$

Lean4

@[reassoc (attr := simp)]
theorem PInfty_f_comp_QInfty_f (n : ℕ) : (PInfty.f n : X _⦋n⦌ ⟶ _) ≫ QInfty.f n = 0 :=
  by
  dsimp only [QInfty]
  simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, comp_id, PInfty_f_idem, sub_self]

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