hsum_embDomain — Mathlib

English

The embDomain construction preserves summation: (s.embDomain f).hsum = s.hsum for any summable family s and embedding f.

Русский

Операция embDomain сохраняет суммирование: (s.embDomain f).hsum = s.hsum для любой суммируемой семейства s и вложения f.

LaTeX

$$$ (s.embDomain f).hsum = s.hsum $$$

Lean4

@[simp]
theorem hsum_embDomain : (s.embDomain f).hsum = s.hsum := by
  classical
  ext g
  simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]
  exact finsum_emb_domain f fun a => (s a).coeff g

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