case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : { x // x ∈ A }
b : ‖↑g - mk f‖ < ε
⊢ ∃ g, ∀ (x : X), ‖↑↑g x - f x‖ < ε
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
⊢ ∃ g, ∀ (x : X), ‖↑↑g x - f x‖ < ε
obtain ⟨g, b⟩ := exists_mem_subalgebra_near_continuousMap_of_separatesPoints A w ⟨f, c⟩ ε pos
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : { x // x ∈ A }
b : ‖↑g - mk f‖ < ε
⊢ ∀ (x : X), ‖↑↑g x - f x‖ < ε
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : { x // x ∈ A }
b : ‖↑g - mk f‖ < ε
⊢ ∃ g, ∀ (x : X), ‖↑↑g x - f x‖ < ε
use g
no goals
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : Subalgebra.SeparatesPoints A
f : X → ℝ
c : Continuous f
ε : ℝ
pos : 0 < ε
g : { x // x ∈ A }
b : ‖↑g - mk f‖ < ε
⊢ ∀ (x : X), ‖↑↑g x - f x‖ < ε
rwa [norm_lt_iff _ pos] at b