X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ g, ‖↑g - f‖ < ε
have w :=
  mem_closure_iff_frequently.mp (continuousMap_mem_subalgebra_closure_of_separatesPoints A w f)
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
rw [Metric.nhds_basis_ball.frequently_iff] at w
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑A
g : C(X, ℝ)
H : g ∈ Metric.ball f ε
m : g ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
obtain ⟨g, H, m⟩ := w ε pos
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑A
g : C(X, ℝ)
H : ‖g - f‖ < ε
m : g ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑A
g : C(X, ℝ)
H : g ∈ Metric.ball f ε
m : g ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
rw [Metric.mem_ball, dist_eq_norm] at H
no goals
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : Subalgebra.SeparatesPoints A
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑A
g : C(X, ℝ)
H : ‖g - f‖ < ε
m : g ∈ ↑A
⊢ ∃ g, ‖↑g - f‖ < ε
exact ⟨⟨g, m⟩, H⟩