derivWithin_of_isOpen

Mathlib.Analysis.Calculus.Deriv.Basic

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

English

If s is open and x ∈ s, then derivWithin f s x = deriv f x.

Русский

Если s открыто и x ∈ s, то derivWithin f s x = deriv f x.

LaTeX

$$$$ \\ derivWithin f s x = deriv f x $$$$

Lean4

theorem derivWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) : derivWithin f s x = deriv f x :=
  derivWithin_of_mem_nhds (hs.mem_nhds hx)

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

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

Разделы

Аффилиация

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