extDerivWithin_eq_of_mem — Mathlib

English

If ω1 and ω2 are equal in the nhdsWithin of x relative to s, and x belongs to s, then extDerivWithin ω1 s x = extDerivWithin ω2 s x.

Русский

Если ω1 и ω2 равны в окрестности x внутри s, и x принадлежит s, тогда extDerivWithin ω1 s x = extDerivWithin ω2 s x.

LaTeX

$$$ (\\nhdsWithin x\, s).EventuallyEq(ω_1, ω_2) \\rightarrow x \\in s \\rightarrow extDerivWithin(ω_1\, s\, x) = extDerivWithin(ω_2\, s\, x) $$$

Lean4

theorem extDerivWithin_eq_of_mem (hs : ω₁ =ᶠ[𝓝[s] x] ω₂) (hx : x ∈ s) : extDerivWithin ω₁ s x = extDerivWithin ω₂ s x :=
  hs.extDerivWithin_eq (mem_of_mem_nhdsWithin hx hs :)

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