chore: audit remaining uses of "local homeomorphism" in comments (#9245)

Almost all of them should speak about partial homeomorphisms instead.
In two cases, I decided removing the "local" was clearer than adding "partial".

Follow-up to #8982; complements #9238.

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -1899,7 +1899,7 @@ namespace PartialHomeomorph
 
 variable (𝕜)
 
-/-- Restrict a local homeomorphism to the subsets of the source and target
+/-- Restrict a partial homeomorphism to the subsets of the source and target
 that consist of points `x ∈ f.source`, `y = f x ∈ f.target`
 such that `f` is `C^n` at `x` and `f.symm` is `C^n` at `y`.
 

Mathlib/Analysis/Calculus/Deriv/Inverse.lean

@@ -70,7 +70,7 @@ theorem HasStrictDerivAt.of_local_left_inverse {f g : 𝕜 → 𝕜} {f' a : 
   (hf.hasStrictFDerivAt_equiv hf').of_local_left_inverse hg hfg
 #align has_strict_deriv_at.of_local_left_inverse HasStrictDerivAt.of_local_left_inverse
 
-/-- If `f` is a local homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
+/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
 nonzero derivative `f'` at `f.symm a` in the strict sense, then `f.symm` has the derivative `f'⁻¹`
 at `a` in the strict sense.
 
@@ -93,7 +93,7 @@ theorem HasDerivAt.of_local_left_inverse {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg
   (hf.hasFDerivAt_equiv hf').of_local_left_inverse hg hfg
 #align has_deriv_at.of_local_left_inverse HasDerivAt.of_local_left_inverse
 
-/-- If `f` is a local homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
+/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
 nonzero derivative `f'` at `f.symm a`, then `f.symm` has the derivative `f'⁻¹` at `a`.
 
 This is one of the easy parts of the inverse function theorem: it assumes that we already have

Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

@@ -404,7 +404,7 @@ theorem HasFDerivAt.of_local_left_inverse {f : E → F} {f' : E ≃L[𝕜] F} {g
     simp only [(· ∘ ·), hp, hfg.self_of_nhds]
 #align has_fderiv_at.of_local_left_inverse HasFDerivAt.of_local_left_inverse
 
-/-- If `f` is a local homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
+/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
 invertible derivative `f'` in the sense of strict differentiability at `f.symm a`, then `f.symm` has
 the derivative `f'⁻¹` at `a`.
 
@@ -416,7 +416,7 @@ theorem PartialHomeomorph.hasStrictFDerivAt_symm (f : PartialHomeomorph E F) {f'
   htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)
 #align local_homeomorph.has_strict_fderiv_at_symm PartialHomeomorph.hasStrictFDerivAt_symm
 
-/-- If `f` is a local homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
+/-- If `f` is a partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
 invertible derivative `f'` at `f.symm a`, then `f.symm` has the derivative `f'⁻¹` at `a`.
 
 This is one of the easy parts of the inverse function theorem: it assumes that we already have

Mathlib/Analysis/Calculus/Implicit.lean

@@ -68,7 +68,7 @@ Consider two functions `f : E → F` and `g : E → G` and a point `a` such that
 * the derivatives are surjective;
 * the kernels of the derivatives are complementary subspaces of `E`.
 
-Note that the map `x ↦ (f x, g x)` has a bijective derivative, hence it is a local homeomorphism
+Note that the map `x ↦ (f x, g x)` has a bijective derivative, hence it is a partial homeomorphism
 between `E` and `F × G`. We use this fact to define a function `φ : F → G → E`
 (see `ImplicitFunctionData.implicitFunction`) such that for `(y, z)` close enough to `(f a, g a)`
 we have `f (φ y z) = y` and `g (φ y z) = z`.
@@ -141,7 +141,7 @@ protected theorem hasStrictFDerivAt :
 
 /-- Implicit function theorem. If `f : E → F` and `g : E → G` are two maps strictly differentiable
 at `a`, their derivatives `f'`, `g'` are surjective, and the kernels of these derivatives are
-complementary subspaces of `E`, then `x ↦ (f x, g x)` defines a local homeomorphism between
+complementary subspaces of `E`, then `x ↦ (f x, g x)` defines a partial homeomorphism between
 `E` and `F × G`. In particular, `{x | f x = f a}` is locally homeomorphic to `G`. -/
 def toPartialHomeomorph : PartialHomeomorph E (F × G) :=
   φ.hasStrictFDerivAt.toPartialHomeomorph _
@@ -260,7 +260,7 @@ def implicitFunctionDataOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' : ra
   isCompl_ker := LinearMap.isCompl_of_proj (Classical.choose_spec hker)
 #align has_strict_fderiv_at.implicit_function_data_of_complemented HasStrictFDerivAt.implicitFunctionDataOfComplemented
 
-/-- A local homeomorphism between `E` and `F × f'.ker` sending level surfaces of `f`
+/-- A partial homeomorphism between `E` and `F × f'.ker` sending level surfaces of `f`
 to vertical subspaces. -/
 def implicitToPartialHomeomorphOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤)
     (hker : (ker f').ClosedComplemented) : PartialHomeomorph E (F × ker f') :=
@@ -392,7 +392,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E :
   [NormedSpace 𝕜 F] [FiniteDimensional 𝕜 F] (f : E → F) (f' : E →L[𝕜] F) {a : E}
 
 /-- Given a map `f : E → F` to a finite dimensional space with a surjective derivative `f'`,
-returns a local homeomorphism between `E` and `F × ker f'`. -/
+returns a partial homeomorphism between `E` and `F × ker f'`. -/
 def implicitToPartialHomeomorph (hf : HasStrictFDerivAt f f' a) (hf' : range f' = ⊤) :
     PartialHomeomorph E (F × ker f') :=
   haveI := FiniteDimensional.complete 𝕜 F

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

@@ -355,7 +355,7 @@ protected theorem surjective [CompleteSpace E] (hf : ApproximatesLinearOn f (f'
     exact fun R h y hy => h hy
 #align approximates_linear_on.surjective ApproximatesLinearOn.surjective
 
-/-- A map approximating a linear equivalence on a set defines a local equivalence on this set.
+/-- A map approximating a linear equivalence on a set defines a partial equivalence on this set.
 Should not be used outside of this file, because it is superseded by `toPartialHomeomorph` below.
 
 This is a first step towards the inverse function. -/
@@ -403,7 +403,7 @@ section
 variable (f s)
 
 /-- Given a function `f` that approximates a linear equivalence on an open set `s`,
-returns a local homeomorph with `toFun = f` and `source = s`. -/
+returns a partial homeomorphism with `toFun = f` and `source = s`. -/
 def toPartialHomeomorph (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
     (hc : Subsingleton E ∨ c < N⁻¹) (hs : IsOpen s) : PartialHomeomorph E F where
   toPartialEquiv := hf.toPartialEquiv hc

Mathlib/Analysis/NormedSpace/HomeomorphBall.lean

@@ -114,7 +114,7 @@ def unitBallBall (c : P) (r : ℝ) (hr : 0 < r) : PartialHomeomorph E P :=
     rw [image_comp, image_smul, smul_unitBall hr.ne', IsometryEquiv.image_ball]
     simp [abs_of_pos hr]
 
-/-- If `r > 0`, then `PartialHomeomorph.univBall c r` is a smooth local homeomorphism
+/-- If `r > 0`, then `PartialHomeomorph.univBall c r` is a smooth partial homeomorphism
 with `source = Set.univ` and `target = Metric.ball c r`.
 Otherwise, it is the translation by `c`.
 Thus in all cases, it sends `0` to `c`, see `PartialHomeomorph.univBall_apply_zero`. -/

Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

@@ -11,7 +11,7 @@ import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
 /-!
 # Polar coordinates
 
-We define polar coordinates, as a local homeomorphism in `ℝ^2` between `ℝ^2 - (-∞, 0]` and
+We define polar coordinates, as a partial homeomorphism in `ℝ^2` between `ℝ^2 - (-∞, 0]` and
 `(0, +∞) × (-π, π)`. Its inverse is given by `(r, θ) ↦ (r cos θ, r sin θ)`.
 
 It satisfies the following change of variables formula (see `integral_comp_polarCoord_symm`):
@@ -25,7 +25,7 @@ open Real Set MeasureTheory
 
 open scoped Real Topology
 
-/-- The polar coordinates local homeomorphism in `ℝ^2`, mapping `(r cos θ, r sin θ)` to `(r, θ)`.
+/-- The polar coordinates partial homeomorphism in `ℝ^2`, mapping `(r cos θ, r sin θ)` to `(r, θ)`.
 It is a homeomorphism between `ℝ^2 - (-∞, 0]` and `(0, +∞) × (-π, π)`. -/
 @[simps]
 def polarCoord : PartialHomeomorph (ℝ × ℝ) (ℝ × ℝ) where
@@ -158,7 +158,7 @@ namespace Complex
 
 open scoped Real
 
-/-- The polar coordinates local homeomorphism in `ℂ`, mapping `r (cos θ + I * sin θ)` to `(r, θ)`.
+/-- The polar coordinates partial homeomorphism in `ℂ`, mapping `r (cos θ + I * sin θ)` to `(r, θ)`.
 It is a homeomorphism between `ℂ - ℝ≤0` and `(0, +∞) × (-π, π)`. -/
 protected noncomputable def polarCoord : PartialHomeomorph ℂ (ℝ × ℝ) :=
   equivRealProdClm.toHomeomorph.transPartialHomeomorph polarCoord