feat: add a uniqueness result for one-point compactification (#18411)

Mathlib/Topology/Compactification/OnePoint.lean

@@ -43,7 +43,7 @@ In this section we define `OnePoint X` to be the disjoint union of `X` and `∞`
 -/
 
 
-variable {X : Type*}
+variable {X Y : Type*}
 
 /-- The OnePoint extension of an arbitrary topological space `X` -/
 def OnePoint (X : Type*) :=
@@ -67,6 +67,11 @@ scoped notation "∞" => OnePoint.infty
 /-- Coercion from `X` to `OnePoint X`. -/
 @[coe, match_pattern] def some : X → OnePoint X := Option.some
 
+@[simp]
+lemma some_eq_iff (x₁ x₂ : X) : (some x₁ = some x₂) ↔ (x₁ = x₂) := by
+  rw [iff_eq_eq]
+  exact Option.some.injEq x₁ x₂
+
 instance : CoeTC X (OnePoint X) := ⟨some⟩
 
 instance : Inhabited (OnePoint X) := ⟨∞⟩
@@ -107,6 +112,13 @@ protected def rec {C : OnePoint X → Sort*} (h₁ : C ∞) (h₂ : ∀ x : X, C
   | ∞ => h₁
   | (x : X) => h₂ x
 
+/-- An elimination principle for `OnePoint`. -/
+@[inline] protected def elim : OnePoint X → Y → (X → Y) → Y := Option.elim
+
+@[simp] theorem elim_infty (y : Y) (f : X → Y) : ∞.elim y f = y := rfl
+
+@[simp] theorem elim_some (y : Y) (f : X → Y) (x : X) : (some x).elim y f = f x := rfl
+
 theorem isCompl_range_coe_infty : IsCompl (range ((↑) : X → OnePoint X)) {∞} :=
   isCompl_range_some_none X
 
@@ -540,6 +552,51 @@ instance (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
       rw [OnePoint.isOpen_iff_of_not_mem]
       exacts [isOpen_discrete _, (Option.some_ne_none val).symm]
 
+section Uniqueness
+
+variable [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
+  (y : Y) (f : X → Y) (hf : IsEmbedding f) (hy : range f = {y}ᶜ)
+
+open scoped Classical in
+/-- If `f` embeds `X` into a compact Hausdorff space `Y`, and has exactly one point outside its
+range, then `(Y, f)` is the one-point compactification of `X`. -/
+noncomputable def equivOfIsEmbeddingOfRangeEq :
+    OnePoint X ≃ₜ Y :=
+  have _i := hf.t2Space
+  have : Tendsto f (coclosedCompact X) (𝓝 y) := by
+    rw [coclosedCompact_eq_cocompact, hasBasis_cocompact.tendsto_left_iff]
+    intro N hN
+    obtain ⟨U, hU₁, hU₂, hU₃⟩ := mem_nhds_iff.mp hN
+    refine ⟨f⁻¹' Uᶜ, ?_, by simpa using (mapsTo_preimage f U).mono_right hU₁⟩
+    rw [hf.isCompact_iff, image_preimage_eq_iff.mpr (by simpa [hy])]
+    exact (isClosed_compl_iff.mpr hU₂).isCompact
+  let e : OnePoint X ≃ Y :=
+    { toFun := fun p ↦ p.elim y f
+      invFun := fun q ↦ if hq : q = y then ∞ else ↑(show q ∈ range f from by simpa [hy]).choose
+      left_inv := fun p ↦ by
+        induction' p using OnePoint.rec with p
+        · simp
+        · have hp : f p ≠ y := by simpa [hy] using mem_range_self (f := f) p
+          simpa [hp] using hf.injective (mem_range_self p).choose_spec
+      right_inv := fun q ↦ by
+        rcases eq_or_ne q y with rfl | hq
+        · simp
+        · have hq' : q ∈ range f := by simpa [hy]
+          simpa [hq] using hq'.choose_spec }
+  Continuous.homeoOfEquivCompactToT2 <| (continuous_iff e).mpr ⟨this, hf.continuous⟩
+
+@[simp]
+lemma equivOfIsEmbeddingOfRangeEq_apply_coe (x : X) :
+    equivOfIsEmbeddingOfRangeEq y f hf hy x = f x :=
+  rfl
+
+@[simp]
+lemma equivOfIsEmbeddingOfRangeEq_apply_infty :
+    equivOfIsEmbeddingOfRangeEq y f hf hy ∞ = y :=
+  rfl
+
+end Uniqueness
+
 end OnePoint
 
 /-- A concrete counterexample shows that `Continuous.homeoOfEquivCompactToT2`