toMvPowerSeries_isDenseInducing — Mathlib

English

The evaluation map from polynomials to power series is dense-inducing with respect to the Pi-topology.

Русский

Оценочная карта полиномов в степенные ряды является плотной индукцией относительно Pi- toplogии.

LaTeX

$$$\\text{toMvPowerSeries}_{\\sigma,R}$ is DenseInducing$$

Lean4

theorem _root_.MvPolynomial.toMvPowerSeries_isDenseInducing : IsDenseInducing (toMvPowerSeries (σ := σ) (R := R)) :=
  toMvPowerSeries_isUniformInducing.isDenseInducing denseRange_toMvPowerSeries

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