hasDerivAtFilter_iff — Mathlib

English

If two functions are eventually equal with respect to a filter and share the same value at x, then a HasDerivAtFilter for one implies HasDerivAtFilter for the other.

Русский

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

LaTeX

$$$$ HasDerivAtFilter f_0 f_0' x L \\iff HasDerivAtFilter f_1 f_1' x L $$$$

Lean4

theorem hasDerivAtFilter_iff (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x) (h₁ : f₀' = f₁') :
    HasDerivAtFilter f₀ f₀' x L ↔ HasDerivAtFilter f₁ f₁' x L :=
  h₀.hasFDerivAtFilter_iff hx (by simp [h₁])

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