hasFDerivWithinAt — Mathlib

English

If f is differentiable within s at x, then there exists HasFDerivWithinAt with derivative fderivWithin 𝕜 f s x.

Русский

Если f дифференцируема внутри s в x, то существует HasFDerivWithinAt с производной fderivWithin 𝕜 f s x.

LaTeX

$$$\text{If } DifferentiableWithinAt\ 𝕜\ f\ s\ x,\ \text{then } HasFDerivWithinAt\ f\ (fderivWithin\ 𝕜\ f\ s\ x)\ s\ x$$$

Lean4

theorem hasFDerivWithinAt (h : DifferentiableWithinAt 𝕜 f s x) : HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x :=
  by
  simp only [fderivWithin, dif_pos h]
  split_ifs with h₀
  exacts [h₀, Classical.choose_spec h]

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