polynomialFunctions — Mathlib

English

For X ⊆ R, the set of polynomial functions on X forms a subalgebra of C(X,R); it is the image of the top (free) polynomial ring under the map p ↦ p.toContinuousMapOn X.

Русский

Для X ⊆ R множество полином-функций образует подалгебру над R в C(X,R); это образ свободной полиномиальной алгебры под отображением p ↦ p.toContinuousMapOn X.

LaTeX

$$$polynomialFunctions(X) = (⊤ : Subalgebra\\,R\\,R[X]).map (toContinuousMapOnAlgHom X)$$$

Lean4

/-- The subalgebra of polynomial functions in `C(X, R)`, for `X` a subset of some topological semiring
`R`.
-/
noncomputable def polynomialFunctions (X : Set R) : Subalgebra R C(X, R) :=
  (⊤ : Subalgebra R R[X]).map (Polynomial.toContinuousMapOnAlgHom X)

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