mfderivWithin_eq_of_mem — Mathlib

English

If two functions f and f1 agree on a neighborhood of x inside a set s, then their MF derivatives at x relative to s are equal.

Русский

Если функции f и f1 совпадают на окрестности точки x внутри множества s, то их MF-дифференциалы по области s в точке x совпадают.

LaTeX

$$$\\big( f_1 =\\!\\!\\!\\!_{\\mathcal{N}[s]x} f \\big) \\land x \\in s \\quad\\Longrightarrow\\quad mfderivWithin\\,I\\,I'\\,f_1\\,s\\,x = mfderivWithin\\,I\\,I'\\,f\\,s\\,x$$$

Lean4

theorem mfderivWithin_eq_of_mem (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
    mfderivWithin I I' f₁ s x = mfderivWithin I I' f s x :=
  hL.mfderivWithin_eq (mem_of_mem_nhdsWithin hx hL :)

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