lineDerivWithin_of_isOpen — Mathlib

English

If s is open and x ∈ s, then lineDerivWithin over s equals lineDeriv over the ambient space.

Русский

Если s открыто и x ∈ s, то lineDerivWithin по s равно lineDeriv по всему пространству.

LaTeX

$$$\text{IsOpen}(s) \land x \in s \Rightarrow lineDerivWithin_{\mathbb{k}}(f,s,x,v) = lineDeriv_{\mathbb{k}}(f,x,v)$$$

Lean4

theorem lineDerivWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) : lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v :=
  lineDerivWithin_of_mem_nhds (hs.mem_nhds hx)

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