fderivWithin_of_isOpen

Mathlib.Analysis.Calculus.FDeriv.Basic

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

English

If s is open and x ∈ s, then fderivWithin 𝕜 f s x equals fderiv 𝕜 f x.

Русский

Если s открыто и x ∈ s, то fderivWithin 𝕜 f s x равно fderiv 𝕜 f x.

LaTeX

$$$\text{IsOpen } s \land x \in s \Rightarrow fderivWithin 𝕜 f s x = fderiv 𝕜 f x$$$

Lean4

theorem fderivWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x :=
  fderivWithin_of_mem_nhds (hs.mem_nhds hx)

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

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

Разделы

Аффилиация

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