Theorems · Theorem · commutative algebra

PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto

∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_2} (f : ι → PowerSeries R) (u : Filter ι)
  (g : PowerSeries R),
  Filter.Tendsto f u (nhds g) ↔
    ∀ (d : ℕ), Filter.Tendsto (fun i => (PowerSeries.coeff d) (f i)) u (nhds ((PowerSeries.coeff d) g))

A family of power series converges iff it converges coefficientwise

Defined in

Mathlib.RingTheory.PowerSeries.PiTopology

Cited by

5 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceSemiring