English
If f: X → Y is an embedding and its range is Y \ {y}, then OnePoint X is homeomorphic to Y.
Русский
Если отображение f: X → Y — вложение, и его образ является Y \ {y}, то OnePoint X гомеоморфно Y.
LaTeX
$$$\\text{OnePoint}(X) \\cong_{\\mathrm{top}} Y$ given $f$ embedding and $\\operatorname{range}(f) = Y \\setminus \\{y\\}$.$$
Lean4
/-- 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
| infty => simp
| coe p =>
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⟩
