feat: add MDifferentiableOn.mdifferentiableAt (#5510)

leanprover-community · Aug 14, 2023 · 57a723e · 57a723e
1 parent b0b6670
commit 57a723e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Geometry/Manifold/MFDeriv.lean b/Mathlib/Geometry/Manifold/MFDeriv.lean
@@ -602,6 +602,10 @@ theorem MDifferentiableWithinAt.mdifferentiableAt (h : MDifferentiableWithinAt I
   rwa [this, mdifferentiableWithinAt_inter hs, mdifferentiableWithinAt_univ] at h
 #align mdifferentiable_within_at.mdifferentiable_at MDifferentiableWithinAt.mdifferentiableAt
 
+theorem MDifferentiableOn.mdifferentiableAt (h : MDifferentiableOn I I' f s) (hx : s ∈ 𝓝 x) :
+    MDifferentiableAt I I' f x :=
+  (h x (mem_of_mem_nhds hx)).mdifferentiableAt hx
+
 theorem MDifferentiableOn.mono (h : MDifferentiableOn I I' f t) (st : s ⊆ t) :
     MDifferentiableOn I I' f s := fun x hx => (h x (st hx)).mono st
 #align mdifferentiable_on.mono MDifferentiableOn.mono