chore: rename misnamed lemmas involving isOpenMap (#11607)

- open_map_of_strict_deriv -> isOpenMap_of_hasStrictDerivAt - open_map_of_strict_fderiv_equiv -> isOpenMap_of_hasStrictFderivAt_equiv These lemmas have conclusion `isOpenMap`, hence should be named accordingly.
leanprover-community · Mar 23, 2024 · 853378f · 853378f
1 parent f2373e0
commit 853378f
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 5 deletions.
diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/Deriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/Deriv.lean
@@ -50,7 +50,8 @@ end HasStrictDerivAt
 variable {f}
 
 /-- If a function has a non-zero strict derivative at all points, then it is an open map. -/
-theorem open_map_of_strict_deriv {f' : 𝕜 → 𝕜}
+theorem isOpenMap_of_hasStrictDerivAt {f' : 𝕜 → 𝕜}
     (hf : ∀ x, HasStrictDerivAt f (f' x) x) (h0 : ∀ x, f' x ≠ 0) : IsOpenMap f :=
   isOpenMap_iff_nhds_le.2 fun x => ((hf x).map_nhds_eq (h0 x)).ge
-#align open_map_of_strict_deriv open_map_of_strict_deriv
+#align open_map_of_strict_deriv isOpenMap_of_hasStrictDerivAt
+@[deprecated] alias open_map_of_strict_deriv := isOpenMap_of_hasStrictDerivAt -- 2024-03-23
diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean
@@ -213,7 +213,9 @@ theorem to_local_left_inverse (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a)
 end HasStrictFDerivAt
 
 /-- If a function has an invertible strict derivative at all points, then it is an open map. -/
-theorem open_map_of_strict_fderiv_equiv [CompleteSpace E] {f : E → F} {f' : E → E ≃L[𝕜] F}
+theorem isOpenMap_of_hasStrictFDerivAt_equiv [CompleteSpace E] {f : E → F} {f' : E → E ≃L[𝕜] F}
     (hf : ∀ x, HasStrictFDerivAt f (f' x : E →L[𝕜] F) x) : IsOpenMap f :=
   isOpenMap_iff_nhds_le.2 fun x => (hf x).map_nhds_eq_of_equiv.ge
-#align open_map_of_strict_fderiv_equiv open_map_of_strict_fderiv_equiv
+#align open_map_of_strict_fderiv_equiv isOpenMap_of_hasStrictFDerivAt_equiv
+@[deprecated] alias open_map_of_strict_fderiv_equiv :=
+  isOpenMap_of_hasStrictFDerivAt_equiv -- 2024-03-23
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean b/Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
@@ -22,7 +22,7 @@ open scoped Real Topology
 namespace Complex
 
 theorem isOpenMap_exp : IsOpenMap exp :=
-  open_map_of_strict_deriv hasStrictDerivAt_exp exp_ne_zero
+  isOpenMap_of_hasStrictDerivAt hasStrictDerivAt_exp exp_ne_zero
 #align complex.is_open_map_exp Complex.isOpenMap_exp
 
 /-- `Complex.exp` as a `PartialHomeomorph` with `source = {z | -π < im z < π}` and