toContinuousMapOn — Mathlib

English

Let p ∈ R[X] and X ⊆ R. The restriction of p to X defines a continuous map p.toContinuousMapOn X : C(X,R), i.e. the function x ∈ X ↦ p(x) is continuous on the subspace X.

Русский

Пусть p ∈ R[X] и X ⊆ R. Ограничение функции p на X задаёт непрерывное отображение p.toContinuousMapOn X: C(X,R); то есть x ↦ p(x) непрерывно на подпространстве X.

LaTeX

$$$p.toContinuousMapOn X\\in C(X,R).$$$

Lean4

/-- A polynomial as a continuous function,
with domain restricted to some subset of the semiring of coefficients.

(This is particularly useful when restricting to compact sets, e.g. `[0,1]`.)
-/
@[simps]
def toContinuousMapOn (p : R[X]) (X : Set R) : C(X, R) :=
  ⟨fun x : X => p.toContinuousMap x, by fun_prop⟩

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