tsupport_fderiv_subset

Mathlib.Analysis.Calculus.FDeriv.Const

URI: https://scilib.ai/kg/mathlib#tsupport_fderiv_subset

English

If f has compact support, then fderiv 𝕜 f also has compact support.

Русский

Если у f компактная опора, то и её производная имеет компактную опору.

LaTeX

$$$\text{HasCompactSupport } f \Rightarrow \text{HasCompactSupport } (fderiv 𝕜 f)$$$

Lean4

theorem tsupport_fderiv_subset : tsupport (fderiv 𝕜 f) ⊆ tsupport f :=
  closure_minimal (support_fderiv_subset 𝕜) isClosed_closure

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru