range_deriv_subset_closure_span_image

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]

Похожие утверждения