denseRange_toPowerSeries — Mathlib

English

The inclusion of polynomials into power series has dense image in PowerSeries(R).

Русский

Включение полиномов в степенные ряды имеет плотное изображение в PowerSeries(R).

LaTeX

$$$ \\overline{\\operatorname{range}(\\operatorname{Polynomial.toPowerSeries})} = \\PowerSeries(R) $$$

Lean4

/-- The inclusion of polynomials into power series has dense image -/
theorem denseRange_toPowerSeries [CommSemiring R] : DenseRange (Polynomial.toPowerSeries (R := R)) := fun f =>
  mem_closure_of_tendsto (tendsto_trunc_atTop R f) <| .of_forall fun _ ↦ Set.mem_range_self _

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