chore(MetricSpace/HausdorffDistance): split in two (#9809)

The file was becoming a bit large (1550 lines). Split in two files of about 900 and 700 lines:
the first file contains more basic material, the second file contains all material related to thickenings.

Extend the module docstrings by mentioning the main results in this file.

Mathlib.lean

@@ -3777,6 +3777,7 @@ import Mathlib.Topology.MetricSpace.ProperSpace
 import Mathlib.Topology.MetricSpace.PseudoMetric
 import Mathlib.Topology.MetricSpace.ShrinkingLemma
 import Mathlib.Topology.MetricSpace.ThickenedIndicator
+import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Topology.Metrizable.Basic
 import Mathlib.Topology.Metrizable.Uniformity
 import Mathlib.Topology.Metrizable.Urysohn

Mathlib/Analysis/Normed/Group/Pointwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yaël Dillies
 -/
 import Mathlib.Analysis.Normed.Group.Basic
-import Mathlib.Topology.MetricSpace.HausdorffDistance
+import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Topology.MetricSpace.IsometricSMul
 
 #align_import analysis.normed.group.pointwise from "leanprover-community/mathlib"@"c8f305514e0d47dfaa710f5a52f0d21b588e6328"

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -8,7 +8,7 @@ import Mathlib.MeasureTheory.Function.AEMeasurableSequence
 import Mathlib.MeasureTheory.Group.Arithmetic
 import Mathlib.MeasureTheory.Order.Lattice
 import Mathlib.Topology.Instances.EReal
-import Mathlib.Topology.MetricSpace.HausdorffDistance
+import Mathlib.Topology.MetricSpace.Thickening
 import Mathlib.Topology.GDelta
 import Mathlib.Topology.Order.Lattice
 import Mathlib.Topology.Semicontinuous

Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

@@ -5,7 +5,7 @@ Authors: Kalle Kytölä
 -/
 import Mathlib.Data.ENNReal.Basic
 import Mathlib.Topology.ContinuousFunction.Bounded
-import Mathlib.Topology.MetricSpace.HausdorffDistance
+import Mathlib.Topology.MetricSpace.Thickening
 
 #align_import topology.metric_space.thickened_indicator from "leanprover-community/mathlib"@"f2ce6086713c78a7f880485f7917ea547a215982"
 

scripts/style-exceptions.txt

@@ -164,7 +164,6 @@ Mathlib/Topology/Category/Profinite/Nobeling.lean : line 1 : ERR_NUM_LIN : 2000
 Mathlib/Topology/Constructions.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1731 lines, try to split it up
 Mathlib/Topology/ContinuousFunction/Bounded.lean : line 1 : ERR_NUM_LIN : 1800 file contains 1649 lines, try to split it up
 Mathlib/Topology/Instances/ENNReal.lean : line 1 : ERR_NUM_LIN : 1900 file contains 1713 lines, try to split it up
-Mathlib/Topology/MetricSpace/HausdorffDistance.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1543 lines, try to split it up
 Mathlib/Topology/MetricSpace/PseudoMetric.lean : line 1 : ERR_NUM_LIN : 2200 file contains 2098 lines, try to split it up
 Mathlib/Topology/Order/Basic.lean : line 1 : ERR_NUM_LIN : 3100 file contains 2983 lines, try to split it up
 Mathlib/Topology/PartialHomeomorph.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1513 lines, try to split it up