isSeparable_range_deriv

Mathlib.Analysis.Calculus.Deriv.Slope

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

← MathLib Explorer

English

If the domain is separable, the range of deriv f is separable.

Русский

Если область сепарабельна, образ производной f сепарабелен.

LaTeX

$$$\\mathrm{IsSeparable}(\\mathrm{range}(\\mathrm{deriv} f))$$$

Lean4

theorem isSeparable_range_deriv [SeparableSpace 𝕜] (f : 𝕜 → F) : IsSeparable (range (deriv f)) :=
  by
  rw [← derivWithin_univ]
  exact isSeparable_range_derivWithin _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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