toContinuousMap — Mathlib

English

Let R be a topological semiring. For every polynomial p in R[X], the evaluation map x ↦ p(x) defines a continuous function R → R; equivalently, p determines a continuous map p.toContinuousMap : R → R.

Русский

Пусть R — топологическое полускольцо. Для каждого полинома p ∈ R[X] отображение x ↦ p(x) задаёт непрерывную функцию R → R; тождественно, полином определяет непрерывное отображение p.toContinuousMap : R → R.

LaTeX

$$$\\forall p \\in R[X],\\ p.toContinuousMap \\in C(R,R).$$$

Lean4

/-- Every polynomial with coefficients in a topological semiring gives a (bundled) continuous function.
-/
@[simps]
def toContinuousMap (p : R[X]) : C(R, R) :=
  ⟨fun x : R => p.eval x, by fun_prop⟩

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