differentiableWithinAt_insert — Mathlib

English

For any y, differentiability within insert y s at x is equivalent to differentiability within s at x.

Русский

Для любого y дифференцируемость внутри вставки y в s в x эквивалентна дифференцируемости внутри s в x.

LaTeX

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

Lean4

theorem differentiableWithinAt_insert {y : E} :
    DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x :=
  by
  rcases eq_or_ne x y with (rfl | h)
  · exact differentiableWithinAt_insert_self
  apply differentiableWithinAt_congr_nhds
  exact nhdsWithin_insert_of_ne h

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