congr_of_eventuallyEq — Mathlib

English

If h: f ≈ f' near x and the direction v is fixed, then LineDifferentiableWithinAt is preserved under eventual equality.

Русский

Если функцияы совпадают рядом с x и направление фиксировано, то линейная дифференцируемость сохраняется при эквивалентности.

LaTeX

$$$(f\\equiv_{nhds(x)} f') \\Rightarrow \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f,s;x,v) \\iff \\mathrm{LineDifferentiableWithinAt}_{\\mathbb{K}}(f',s;x,v)$$$

Lean4

theorem congr_of_eventuallyEq (h : LineDifferentiableWithinAt 𝕜 f s x v) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    LineDifferentiableWithinAt 𝕜 f₁ s x v :=
  (h.hasLineDerivWithinAt.congr_of_eventuallyEq h₁ hx).differentiableWithinAt

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