denseRange_toMvPowerSeries — Mathlib

English

The inclusion of polynomials into mv power series has dense range.

Русский

Включение полиномов в mvPowerSeries имеет плотное множество образа.

LaTeX

$$DenseRange (MvPolynomial.toMvPowerSeries (R := R) (σ := σ))$$

Lean4

/-- The inclusion of polynomials into power series has dense image -/
theorem denseRange_toMvPowerSeries [CommSemiring R] : DenseRange (MvPolynomial.toMvPowerSeries (R := R) (σ := σ)) :=
  fun f ↦ by classical exact mem_closure_of_tendsto (tendsto_trunc'_atTop f) <| .of_forall fun _ ↦ Set.mem_range_self _

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