tsum_star — Mathlib

English

Under a T2 space, star commutes with the sum: star of the sum equals the sum of stars.

Русский

В пространстве T2 звезда коммутирует с суммой: звезда суммы равна сумме звезд.

LaTeX

$$$ star (tsum_{L} f) = tsum_{L} (star(f)) $$$

Lean4

theorem tsum_star [T2Space α] : star (∑'[L] b, f b) = ∑'[L] b, star (f b) :=
  Function.LeftInverse.map_tsum (g := starAddEquiv) f continuous_star continuous_star star_star

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