hasFDerivAtFilter_iff — Mathlib

English

If HasFDerivAt f f' x holds and f ∼ f1 near x in a filter sense, then HasFDerivAt f1 f' x also holds.

Русский

Если существует производная f f' в точке x и f совпадает с f1 почти возле x в рамках фильтра, то и f1 имеет ту же производную.

LaTeX

$$$HasFDerivAt f f' x \\wedge f =\\!\\!\\!_{nhds x} f_1 \\Rightarrow HasFDerivAt f_1 f' x.$$$

Lean4

theorem hasFDerivAtFilter_iff (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : ∀ x, f₀' x = f₁' x) :
    HasFDerivAtFilter f₀ f₀' x L ↔ HasFDerivAtFilter f₁ f₁' x L :=
  by
  simp only [hasFDerivAtFilter_iff_isLittleOTVS]
  exact isLittleOTVS_congr (h₀.mono fun y hy => by simp only [hy, h₁, hx]) .rfl

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