hasFDerivWithinAt_iff — Mathlib

English

If f0 and f1 coincide near x, then the Fréchet derivative within s at x with derivative f' exists for f0 if and only if it exists for f1 within the same s and derivative f'.

Русский

Если f0 и f1 совпадают в окрестности x, то существование внутри s Фреше-производной в x с производной f' для f0 эквивалентно существованию такой же внутри s для f1.

LaTeX

$$$ \\mathrm{HasFDerivWithinAt}(f_0,f',s,x) \\iff \\mathrm{HasFDerivWithinAt}(f_1,f',s,x) $$$

Lean4

theorem hasFDerivWithinAt_iff (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : f₀ x = f₁ x) :
    HasFDerivWithinAt f₀ f' s x ↔ HasFDerivWithinAt f₁ f' s x :=
  h.hasFDerivAtFilter_iff hx fun _ => _root_.rfl

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