support_fderiv_subset — Mathlib

English

The tsupport of the derivative is contained in the tsupport of the function: tsupport(fderiv 𝕜 f) ⊆ tsupport f.

Русский

Опора производной (tsupport) принадлежит опоре самой функции.

LaTeX

$$$tsupport\bigl(fderiv 𝕜 f\bigr) \subseteq tsupport(f)$$$

Lean4

theorem support_fderiv_subset : support (fderiv 𝕜 f) ⊆ tsupport f := fun x ↦
  by
  rw [← not_imp_not, notMem_support]
  exact fderiv_of_notMem_tsupport _

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