onePointHyperplaneHomeoUnitSphere

English

Elliptic elements have no fixed points on OnePoint(K); i.e., for all c ∈ OnePoint(K), g • c ≠ c.

Русский

Эллиптические элементы не имеют фиксированных точек на OnePoint(K); для любого c ∈ OnePoint(K) выполняется g • c ≠ c.

LaTeX

$$$g$ IsElliptic $\\Rightarrow$ ∀ $c$, $g\\cdot c \\neq c$.$$

Lean4

/-- A homeomorphism from the one-point compactification of a hyperplane in Euclidean space to the
sphere. -/
def onePointHyperplaneHomeoUnitSphere {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    {v : E} (hv : ‖v‖ = 1) : OnePoint (ℝ ∙ v)ᗮ ≃ₜ sphere (0 : E) 1 :=
  OnePoint.equivOfIsEmbeddingOfRangeEq _ _ (isOpenEmbedding_stereographic_symm hv).toIsEmbedding
    (range_stereographic_symm hv)

Похожие утверждения