hasDerivWithinAt_derivWithin_iff — Mathlib

English

Same as HasDerivWithinAt_derivWithin_iff but marked as simp.

Русский

Аналогично hasDerivWithinAt_derivWithin_iff, помечено как simp.

LaTeX

$$@[simp] hasDerivWithinAt_derivWithin_iff : HasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt 𝕜 f s x$$

Lean4

@[simp]
theorem hasDerivWithinAt_derivWithin_iff :
    HasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  ⟨fun h => h.differentiableWithinAt, fun h => h.hasDerivWithinAt⟩

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