congr_of_eventuallyEq_of_mem — Mathlib

English

If f has MDifferentiableWithinAt f s x and f1 equals f eventually near insert x s, then f1 is MDifferentiableWithinAt on s.

Русский

Если f имеет MDifferentiableWithinAt f s x, и f1 эквивалентна f почти в окрестности вставленного множества insert x s, то f1 дифференцируема внутри s в x.

LaTeX

$$$MDifferentiableWithinAt\ I I'\ f\ s\ x\ f' \\land f_1 =^\![\mathcal{N}[insert x s] x]\ f \Rightarrow MDifferentiableWithinAt\ I I'\ f_1\ s\ x$$$

Lean4

theorem congr_of_eventuallyEq_of_mem (h : MDifferentiableWithinAt I I' f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) :
    MDifferentiableWithinAt I I' f₁ s x :=
  h.congr_of_eventuallyEq h₁ (mem_of_mem_nhdsWithin hx h₁ :)

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