X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ comp p (attachBound ↑f) ∈ Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
⊢ comp p (attachBound ↑f) ∈ Subalgebra.topologicalClosure A
have mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure :=
  continuousMap_mem_polynomialFunctions_closure _ _ p
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ comp p (attachBound ↑f) ∈ Subalgebra.topologicalClosure A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ comp p (attachBound ↑f) ∈ Subalgebra.topologicalClosure A
have frequently_mem_polynomials := mem_closure_iff_frequently.mp mem_closure
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ ∃ᶠ (x : C(X, ℝ)) in nhds (comp p (attachBound ↑f)), x ∈ ↑A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ comp p (attachBound ↑f) ∈ Subalgebra.topologicalClosure A
apply mem_closure_iff_frequently.mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ ∀ (x : C(↑(Set.Icc (-‖↑f‖) ‖↑f‖), ℝ)),
    x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)) → ↑(compRightContinuousMap ℝ (attachBound ↑f)) x ∈ ↑A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ ∃ᶠ (x : C(X, ℝ)) in nhds (comp p (attachBound ↑f)), x ∈ ↑A
refine'
  ((compRightContinuousMap ℝ (attachBound (f : C(X, ℝ)))).continuousAt
          p).tendsto.frequently_map
    _ _ frequently_mem_polynomials
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
g : ℝ[X]
⊢ ↑(compRightContinuousMap ℝ (attachBound ↑f)) (↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc (-‖f‖) ‖f‖)) g) ∈ ↑A
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
⊢ ∀ (x : C(↑(Set.Icc (-‖↑f‖) ‖↑f‖), ℝ)),
    x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)) → ↑(compRightContinuousMap ℝ (attachBound ↑f)) x ∈ ↑A
rintro _ ⟨g, ⟨-, rfl⟩⟩
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
g : ℝ[X]
⊢ comp (Polynomial.toContinuousMapOn g (Set.Icc (-‖f‖) ‖f‖)) (attachBound ↑f) ∈ A
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
g : ℝ[X]
⊢ ↑(compRightContinuousMap ℝ (attachBound ↑f)) (↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc (-‖f‖) ‖f‖)) g) ∈ ↑A
simp only [SetLike.mem_coe, AlgHom.coe_toRingHom, compRightContinuousMap_apply,
  Polynomial.toContinuousMapOnAlgHom_apply]
no goals
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : { x // x ∈ A }
p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)
mem_closure : p ∈ Subalgebra.topologicalClosure (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
frequently_mem_polynomials :
  ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖))
g : ℝ[X]
⊢ comp (Polynomial.toContinuousMapOn g (Set.Icc (-‖f‖) ‖f‖)) (attachBound ↑f) ∈ A
apply polynomial_comp_attachBound_mem