English
Infinitely smooth maps are dense in the space of continuous maps between two normed spaces.
Русский
Бесконечно гладкие отображения плотны в пространстве непрерывных отображений между двумя нормированными пространствами.
LaTeX
$$$ \overline{\{ f: E \to F : \ ContDiff \mathbb{R} \infty f \}} = C(E,F) $$$
Lean4
/-- Infinitely smooth functions are dense in the space of continuous functions. -/
theorem dense_setOf_contDiff : Dense {f : C(E, F) | ContDiff ℝ ∞ f} :=
by
intro f
rw [mem_closure_iff_nhds_basis (nhds_basis_uniformity uniformity_basis_dist.compactConvergenceUniformity)]
simp only [Prod.forall, mem_setOf_eq, and_imp]
intro K ε hK hε
have : UniformContinuousOn f (cthickening 1 K) := hK.cthickening.uniformContinuousOn_of_continuous <| by fun_prop
rcases Metric.uniformContinuousOn_iff.mp this (ε / 2) (half_pos hε) with ⟨δ, hδ, hfδ⟩
rcases (map_continuous f).exists_contDiff_dist_le_of_forall_mem_ball_dist_le (lt_min one_pos hδ) with ⟨g, hgc, hg⟩
refine ⟨⟨g, hgc.continuous⟩, hgc, fun x hx ↦ (hg _ _ fun y hy ↦ ?_).trans_lt (half_lt_self hε)⟩
rw [mem_ball, lt_min_iff] at hy
exact hfδ _ (mem_cthickening_of_dist_le _ x _ _ hx hy.1.le) _ (self_subset_cthickening _ hx) hy.2 |>.le
