English
There exists a homeomorphism between the one-point compactification of a real finite-dimensional vector space V and the unit sphere in a real Euclidean space of dimension card(ι)−1, provided finrank(V) + 1 = card(ι).
Русский
Существует гомеоморфизм между одноточечной компактфикацией конечномерного вещественного пространства V и единичной сферой в евклидовом пространстве той размерности, что равна card(ι)−1, при условии finrank(V) + 1 = card(ι).
LaTeX
$$$\\text{OnePoint}(V) \\simeq_t \\mathbb{S}^{m-1}$ where $m=\\operatorname{finrank}_{\\mathbb{R}} V + 1$ and $m = |\\iota|$. $$
Lean4
/-- A homeomorphism from the one-point compactification of a finite-dimensional real vector space to
the sphere. -/
def onePointEquivSphereOfFinrankEq {ι V : Type*} [Fintype ι] [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]
[TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [T2Space V]
(h : finrank ℝ V + 1 = Fintype.card ι) : OnePoint V ≃ₜ sphere (0 : EuclideanSpace ℝ ι) 1 := by
classical
have : Nonempty ι := Fintype.card_pos_iff.mp <| by cutsat
let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
have hv : ‖v‖ = 1 := by simp [v]
have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv
