lineDerivWithin_of_mem_nhds — Mathlib

English

If x has a neighborhood in the ambient topology contained in s, then the line derivative within s equals the line derivative in the whole space.

Русский

Если для точки x существует окрестность в общей топологии, содержащаяся в s, то линейная производная внутри s равна линейной производной в полном пространстве.

LaTeX

$$$h : s \in 𝓝 x \Rightarrow lineDerivWithin_{\mathbb{k}}(f,s,x,v) = lineDeriv_{\mathbb{k}}(f,x,v)$$$

Lean4

theorem lineDerivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v :=
  by
  apply derivWithin_of_mem_nhds
  apply (Continuous.continuousAt _).preimage_mem_nhds (by simpa using h)
  fun_prop

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