map_tsum — Mathlib

English

Another form of the tsum equivalence under a continuous linear equivalence, relating sums before and after applying the inverse map.

Русский

Ещё одна форма эквивалентности сумм под эквивалентом: суммы до и после применения обратного отображения соответствуют друг другу.

LaTeX

$$$\\forall f:\\, ι \\to M\\; (e:\\, M \\simeq\\!\u2060SL[σ] M₂),\\; \\forall y:\\, M₂,\\ (\\operatorname{tsum}_L (λ z, e(f(z)))) = y \\iff \\operatorname{tsum}_L f = e.symm y$$$

Lean4

protected theorem map_tsum [T2Space M] [T2Space M₂] {f : ι → M} (e : M ≃SL[σ] M₂) :
    e (∑'[L] z, f z) = ∑'[L] z, e (f z) :=
  by
  refine symm (e.tsum_eq_iff.mpr ?_)
  rw [e.symm_apply_apply _]

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