PInfty_comp_πSummand_id — Mathlib

English

The composition PInfty.f n with πSummand corresponding to the identity yields PInfty.f n, i.e., the projection onto the normalized part is unchanged by projecting onto the identity summand.

Русский

Композиция PInfty.f n с πSummand для идентичности дает PInfty.f n; проекция на нормализованную часть не изменяется при проекции на идентичную сумму.

LaTeX

$$$PInfty.f n \circ πSummand(Id) = PInfty.f n$$$

Lean4

@[reassoc (attr := simp)]
theorem PInfty_comp_πSummand_id (n : ℕ) :
    PInfty.f n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)) = s.πSummand (IndexSet.id (op ⦋n⦌)) :=
  by
  conv_rhs => rw [← id_comp (s.πSummand _)]
  symm
  rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem, sub_self]

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