support_deriv_subset — Mathlib

English

The support of the derivative is contained in the tsupport of f: supp(deriv f) ⊆ tsupport f.

Русский

Опор поддержки производной ⊆ опорe функции: supp(deriv f) ⊆ tsupport f.

LaTeX

$$theorem support_deriv_subset : support (deriv f) ⊆ tsupport f$$

Lean4

theorem support_deriv_subset : support (deriv f) ⊆ tsupport f :=
  by
  intro x
  rw [← not_imp_not]
  intro h2x
  rw [notMem_tsupport_iff_eventuallyEq] at h2x
  exact notMem_support.mpr (h2x.deriv_eq.trans (deriv_const x 0))

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