derivWithin_eq_of_mem — Mathlib

English

If f1 =ᶠ[𝓝[s] x] f and x ∈ s, then derivWithin f1 s x = derivWithin f s x.

Русский

Если f1 ≈ f на nhdsWithin x s и x ∈ s, то производные внутри совпадают.

LaTeX

$$$(f_1 =ᶠ[𝓝[s] x] f) \\rightarrow x \\in s \\rightarrow derivWithin f_1 s x = derivWithin f s x$$$

Lean4

theorem derivWithin_eq_of_mem (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) : derivWithin f₁ s x = derivWithin f s x :=
  hs.derivWithin_eq <| hs.self_of_nhdsWithin hx

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