coeff_zero_iff — Mathlib

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]

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