uniformContinuous_coeff — Mathlib

English

For any d ∈ Finsupp σ ℕ, the map from mv-power-series to its coefficient at d is uniformly continuous.

Русский

Для любого индекса d коэффициентная цепь от mv-рядов к R равномерно непрерывна.

LaTeX

$$UniformContinuous (f ↦ coeff d f)$$

Lean4

/-- Coefficients of a multivariate power series are uniformly continuous -/
theorem uniformContinuous_coeff [Semiring R] (d : σ →₀ ℕ) : UniformContinuous fun f : MvPowerSeries σ R => coeff d f :=
  uniformContinuous_pi.mp uniformContinuous_id d

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