of_dslope — Mathlib

English

If dslope f a is differentiable within s at b, then f is differentiable within s at b.

Русский

Если dslope f a дифференцируема в пределах s в точке b, то и f дифференцируема в пределах s в точке b.

LaTeX

$$$\text{DifferentiableWithinAt}( f, s, b) \Leftarrow \text{DifferentiableWithinAt}( dslope\ f\ a, s, b)$$$

Lean4

theorem of_dslope (h : DifferentiableWithinAt 𝕜 (dslope f a) s b) : DifferentiableWithinAt 𝕜 f s b := by
  simpa only [id, sub_smul_dslope f a, sub_add_cancel] using
    ((differentiableWithinAt_id.sub_const a).fun_smul h).add_const (f a)

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