English
If t is dense in s, then range (deriv f) is contained in the closure of span of f'' t.
Русский
Если t плотно в s, то образ производной f лежит в замыкании линейной оболочки образа t.
LaTeX
$$$\\mathrm{range}(\\mathrm{deriv} f) \\subseteq \\overline{\\mathrm{span}(f''t)}$$$
Lean4
/-- Given a dense set `t`, then the range of `deriv f` is contained in the closure of the submodule
spanned by the image of `t`. -/
theorem range_deriv_subset_closure_span_image (f : 𝕜 → F) {t : Set 𝕜} (h : Dense t) :
range (deriv f) ⊆ closure (Submodule.span 𝕜 (f '' t)) :=
by
rw [← derivWithin_univ]
apply range_derivWithin_subset_closure_span_image
simp [dense_iff_closure_eq.1 h]