English
Given A⊂C(X,ℝ) a subalgebra and p a continuous bound function on the interval, p ∘ attachBound(f) lies in closure of A, by the Weierstrass theorem, using the postcomposition with attachBound.
Русский
Для подалгебры A и функции p непрерывной границы над интервалом, p ∘ attachBound(f) принадлежит замыканию A по теореме Вейерштрасса.
LaTeX
$$$p\circ\mathrm{attachBound}(f) \in A^{\mathrm{topologicalClosure}}$$$
Lean4
theorem comp_attachBound_mem_closure (A : Subalgebra ℝ C(X, ℝ)) (f : A) (p : C(Set.Icc (-‖f‖) ‖f‖, ℝ)) :
p.comp (attachBound (f : C(X, ℝ))) ∈ A.topologicalClosure := by
-- `p` itself is in the closure of polynomials, by the Weierstrass theorem,
have mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure :=
continuousMap_mem_polynomialFunctions_closure _ _ p
have frequently_mem_polynomials := mem_closure_iff_frequently.mp mem_closure
apply mem_closure_iff_frequently.mpr
refine
((compRightContinuousMap ℝ (attachBound (f : C(X, ℝ)))).continuousAt p).tendsto.frequently_map _ ?_
frequently_mem_polynomials
rintro _ ⟨g, ⟨-, rfl⟩⟩
simp only [SetLike.mem_coe, AlgHom.coe_toRingHom, compRightContinuousMap_apply,
Polynomial.toContinuousMapOnAlgHom_apply]
apply polynomial_comp_attachBound_mem
