of_dslope — Mathlib

English

If b ≠ a, then differentiability within at dslope f a, s, b is equivalent to differentiability within f at b.

Русский

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

LaTeX

$$$\text{DifferentiableWithinAt}( dslope\ f\ a, s, b) \iff \text{DifferentiableWithinAt}( f, s, b) \quad (b \neq a)$$$

Lean4

theorem of_dslope (h : DifferentiableAt 𝕜 (dslope f a) b) : DifferentiableAt 𝕜 f b :=
  differentiableWithinAt_univ.1 h.differentiableWithinAt.of_dslope

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