uniformContinuous_coeff — Mathlib

English

For each d, the map coeff_d is uniformly continuous.

Русский

Для каждого фиксированного d отображение coeff_d uniformly continuous.

LaTeX

$$$ \\forall d, \\text{ UniformContinuous }( \\operatorname{coeff}_d ) $$$

Lean4

/-- Coefficients are uniformly continuous -/
theorem uniformContinuous_coeff [Semiring R] (d : ℕ) : UniformContinuous fun f : PowerSeries R ↦ coeff d f :=
  uniformContinuous_pi.mp uniformContinuous_id (Finsupp.single () d)

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