Multivariate polynomials and continuity

In this file we prove the following lemma:

• MvPolynomial.continuous_eval: MvPolynomial.eval is continuous

Tags

multivariate polynomial, continuity

theorem MvPolynomial.continuous_eval {X : Type u_1} {σ : Type u_2} [TopologicalSpace X] [CommSemiring X] [TopologicalSemiring X] (p : MvPolynomial σ X) : Continuous fun (x : σ → X) => (MvPolynomial.eval x) p