toContinuousMapOn_X_eq_restrict_id

English

For any subset s ⊆ R, the polynomial X restricted to s coincides with the restriction of the identity on s: X.toContinuousMapOn s = restrict s (id_R).

Русский

Пусть s ⊆ R. Ограничение полинома X на s совпадает с ограничением тождественного отображения на s: X.toContinuousMapOn s = restrict s (id_R).

LaTeX

$$$X.toContinuousMapOn s = \\mathrm{restrict}\\,s\\ (\\mathrm{id}\\,R).$$$

Lean4

theorem toContinuousMapOn_X_eq_restrict_id (s : Set R) : X.toContinuousMapOn s = restrict s (.id R) := by ext;
  simp
    -- TODO some lemmas about when `toContinuousMapOn` is injective?

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