⊢ ⊤ ≤ Subalgebra.topologicalClosure (polynomialFunctions I)
⊢ Subalgebra.topologicalClosure (polynomialFunctions I) = ⊤
apply eq_top_iff.mpr
f : C(↑I, ℝ)
⊢ f ∈ Subalgebra.topologicalClosure (polynomialFunctions I)
⊢ ⊤ ≤ Subalgebra.topologicalClosure (polynomialFunctions I)
rintro f -
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : C(↑I, ℝ)) in nhds f, x ∈ ↑(polynomialFunctions I)
f : C(↑I, ℝ)
⊢ f ∈ Subalgebra.topologicalClosure (polynomialFunctions I)
refine' Filter.Frequently.mem_closure _
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : ℕ) in atTop, bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : C(↑I, ℝ)) in nhds f, x ∈ ↑(polynomialFunctions I)
refine' Filter.Tendsto.frequently (bernsteinApproximation_uniform f) _
case h
f : C(↑I, ℝ)
⊢ ∀ (x : ℕ), bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
f : C(↑I, ℝ)
⊢ ∃ᶠ (x : ℕ) in atTop, bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
apply frequently_of_forall
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ ↑(polynomialFunctions I)
case h
f : C(↑I, ℝ)
⊢ ∀ (x : ℕ), bernsteinApproximation x f ∈ ↑(polynomialFunctions I)
intro n
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ polynomialFunctions I
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ ↑(polynomialFunctions I)
simp only [SetLike.mem_coe]
case h.h
f : C(↑I, ℝ)
n : ℕ
⊢ ∀ (x : Fin (n + 1)), x ∈ Finset.univ → ↑f (bernstein.z x) • bernstein n ↑x ∈ polynomialFunctions I
case h
f : C(↑I, ℝ)
n : ℕ
⊢ bernsteinApproximation n f ∈ polynomialFunctions I
apply Subalgebra.sum_mem
case h.h
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ ↑f (bernstein.z n) • bernstein n✝ ↑n ∈ polynomialFunctions I
case h.h
f : C(↑I, ℝ)
n : ℕ
⊢ ∀ (x : Fin (n + 1)), x ∈ Finset.univ → ↑f (bernstein.z x) • bernstein n ↑x ∈ polynomialFunctions I
rintro n -
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ bernstein n✝ ↑n ∈ polynomialFunctions I
case h.h
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ ↑f (bernstein.z n) • bernstein n✝ ↑n ∈ polynomialFunctions I
apply Subalgebra.smul_mem
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ Polynomial.toContinuousMapOn (bernsteinPolynomial ℝ n✝ ↑n) I ∈ Subalgebra.map (Polynomial.toContinuousMapOnAlgHom I) ⊤
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ bernstein n✝ ↑n ∈ polynomialFunctions I
dsimp [bernstein, polynomialFunctions]
no goals
case h.h.hx
f : C(↑I, ℝ)
n✝ : ℕ
n : Fin (n✝ + 1)
⊢ Polynomial.toContinuousMapOn (bernsteinPolynomial ℝ n✝ ↑n) I ∈ Subalgebra.map (Polynomial.toContinuousMapOnAlgHom I) ⊤
simp