English
For a function a from an index set to mv power series, with S having a discrete topology, Tendsto a cofinitely to 0 if and only if for every coefficient index d, the set of indices s with (a s).coeff d ≠ 0 is finite.
Русский
Для функции a : σ → MvPowerSeries τ S при дискретной топологии S предел Tendsto a cofinitely к 0 эквивалентен тому, что для каждого коэффициента d множество индексов s с (a s).coeff d ≠ 0 конечно.
LaTeX
$$Tendsto a Filter.cofinite (nhds 0) ↔ ∀ d : τ →₀ ℕ, {s | (a s).coeff d ≠ 0}.Finite$$
Lean4
theorem coeff_zero_iff [TopologicalSpace S] [DiscreteTopology S] :
Filter.Tendsto a Filter.cofinite (nhds 0) ↔ ∀ d : τ →₀ ℕ, {s | (a s).coeff d ≠ 0}.Finite := by
simp [tendsto_iff_coeff_tendsto, coeff_zero, nhds_discrete]