tsupport_iteratedFDeriv_subset — Mathlib

English

For every n, tsupport (iteratedFDeriv 𝕜 n f) is contained in tsupport f, by induction on n.

Русский

Для каждого n опорная поддержка iteratedFDeriv 𝕜 n f ⊆ опорная поддержка f, доказано по индукции по n.

LaTeX

$$$\operatorname{tsupport}(\operatorname{iteratedFDeriv}_{\mathbb{K}}^{n} f) \subseteq \operatorname{tsupport}(f)$$$

Lean4

theorem tsupport_iteratedFDeriv_subset (n : ℕ) : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f := by
  induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact
      closure_minimal ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans subset_closure) isClosed_closure
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    exact
      closure_minimal
        ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans ((support_fderiv_subset 𝕜).trans IH))
        isClosed_closure

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