English
If A is a real subalgebra of C(X,ℝ) and f∈A, g∈ℝ[X], then the postcomposition (g.toContinuousMapOn Icc(-‖f‖,‖f‖)).comp (f: C(X,ℝ)).attachBound lies in A.
Русский
Если A — подалгебра реальных функций на X, и f∈A, g∈ℝ[X], то соответствующая композиция принадлежит A.
LaTeX
$$$ (g^{\sim}\!\! , f) \in A$$$
Lean4
/-- Given a continuous function `f` in a subalgebra of `C(X, ℝ)`, postcomposing by a polynomial
gives another function in `A`.
This lemma proves something slightly more subtle than this:
we take `f`, and think of it as a function into the restricted target `Set.Icc (-‖f‖) ‖f‖)`,
and then postcompose with a polynomial function on that interval.
This is in fact the same situation as above, and so also gives a function in `A`.
-/
theorem polynomial_comp_attachBound_mem (A : Subalgebra ℝ C(X, ℝ)) (f : A) (g : ℝ[X]) :
(g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (f : C(X, ℝ)).attachBound ∈ A :=
by
rw [polynomial_comp_attachBound]
apply SetLike.coe_mem
