star — Mathlib

English

Let α be a topological star-additive monoid and L a summation filter on β. If the series ∑_L f converges to a, then the series of star(f) converges to star(a).

Русский

Пусть α — топологический звёздовый аддитивный моноид, L — суммирующий фильтр на β. Если сумма ∑_L f равна a, то сумма звездой f равна звездe a.

LaTeX

$$$ HasSum f a L \rightarrow HasSum (\lambda b, \star (f b)) (\star a) L $$$

Lean4

theorem star (h : HasSum f a L) : HasSum (fun b ↦ star (f b)) (star a) L := by
  simpa only using h.map (starAddEquiv : α ≃+ α) continuous_star

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