X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
⊢ f ∈ ⊤
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
⊢ f ∈ Subalgebra.topologicalClosure A
rw [subalgebra_topologicalClosure_eq_top_of_separatesPoints A w]
no goals
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
⊢ f ∈ ⊤
simp