hasFDerivWithinAt_insert — Mathlib

English

If f has Fréchet derivative f' at x, then HasFDerivWithinAt f f' s x holds for any s.

Русский

Если у f есть производная Фреше в x, тогда HasFDerivWithinAt f f' s x выполняется для любого s.

LaTeX

$$$$\\text{HasFDerivAt } f\\,f'\\,x \\implies \\text{HasFDerivWithinAt } f\\,f'\\,s\\,x.$$$$

Lean4

@[simp]
theorem hasFDerivWithinAt_insert {y : E} : HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x :=
  by
  rcases eq_or_ne x y with (rfl | h)
  · simp_rw [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS]
    apply isLittleOTVS_insert
    simp only [sub_self, map_zero]
  refine ⟨fun h => h.mono <| subset_insert y s, fun hf => hf.mono_of_mem_nhdsWithin ?_⟩
  simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin]

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