differentiableAt_dslope_of_ne — Mathlib

English

For b ≠ a, dslope f a is differentiable at b if and only if f is differentiable at b.

Русский

При b ≠ a dslope f a дифференцируема в b тогда и только тогда, когда f дифференцируема в b.

LaTeX

$$$\text{DifferentiableAt} f b \quad \text{iff} \quad \text{DifferentiableAt} ( dslope\ f\ a ) b \; (\text{при } b \neq a)$$$

Lean4

theorem differentiableAt_dslope_of_ne (h : b ≠ a) : DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b := by
  simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]

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