a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
have w := mem_closure_iff_frequently.mp (continuousMap_mem_polynomialFunctions_closure _ _ f)
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(↑(Set.Icc a b), ℝ)) in nhds f, x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
rw [Metric.nhds_basis_ball.frequently_iff] at w
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m ∈ Metric.ball f ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
obtain ⟨-, H, ⟨m, ⟨-, rfl⟩⟩⟩ := w ε pos
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ‖↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m - f‖ < ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m ∈ Metric.ball f ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
rw [Metric.mem_ball, dist_eq_norm] at H
no goals
case intro.intro.intro.intro
a b : ℝ
f : C(↑(Set.Icc a b), ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x, x ∈ Metric.ball f i ∧ x ∈ ↑(polynomialFunctions (Set.Icc a b))
m : ℝ[X]
H : ‖↑↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc a b)) m - f‖ < ε
⊢ ∃ p, ‖Polynomial.toContinuousMapOn p (Set.Icc a b) - f‖ < ε
exact ⟨m, H⟩