differentiableWithinAt_insert_self

English

Differentiability within insert x s at x is equivalent to differentiability within s at x.

Русский

Дифференцируемость внутри вставки x в s в точке x равна дифференцируемости внутри s в x.

LaTeX

$$$\mathrm{DifferentiableWithinAt } 𝕜 f (\mathrm{Set.insert} x\, s) x \iff \mathrm{DifferentiableWithinAt } 𝕜 f s x$$$

Lean4

theorem differentiableWithinAt_insert_self :
    DifferentiableWithinAt 𝕜 f (insert x s) x ↔ DifferentiableWithinAt 𝕜 f s x :=
  ⟨fun h ↦ h.mono (subset_insert x s), fun h ↦ h.hasFDerivWithinAt.insert.differentiableWithinAt⟩

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