congr_of_eventuallyEq_of_mem — Mathlib

English

If h is HasDerivWithinAt f f' s x, f1 =ᶠ[𝓝[s] x] f, and x ∈ s, then HasDerivWithinAt f1 f' s x.

Русский

Если у f есть производная f' внутри s в x, а f1 =ᶠ[𝓝[s] x] f и x ∈ s, то HasDerivWithinAt f1 f' s x.

LaTeX

$$$HasDerivWithinAt f f' s x \\rightarrow (f_1 =^\\!\\[𝓝[s] x\\!] f) \\rightarrow x \\in s \\rightarrow HasDerivWithinAt f_1 f' s x$$$

Lean4

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

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