X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
g : ℝ[X]
⊢ ↑(↑(Polynomial.aeval f) g) ∈ A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
g : ℝ[X]
⊢ comp (Polynomial.toContinuousMapOn g (Set.Icc (-‖f‖) ‖f‖)) (attachBound ↑f) ∈ A
rw [polynomial_comp_attachBound]
no goals
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
g : ℝ[X]
⊢ ↑(↑(Polynomial.aeval f) g) ∈ A
apply SetLike.coe_mem