English
The symmetrized stereographic projection stereographic' has a closed-form expression for its inverse: ((stereographic' n v).symm x) equals a combination of the projection basis U and the vector v, with the norm of U.symm x appearing in a quadratic form and involving 4.
Русский
Обратное отображение stereographic' имеет явную форму: (stereographic' n v).symm x выражается через базис U и вектор v с квадратичными членами, зависящими от ||U.symm x|| и числа 4.
LaTeX
$$$((\\text{stereographic'}\\ n\\ v).\\text{symm}\\ x) = \\text{(виражённая формула через } U \\text{ и } v)$$$
Lean4
/-- Variant of the stereographic projection, for the sphere in an `n + 1`-dimensional inner product
space `E`. This version has codomain the Euclidean space of dimension `n`, and is obtained by
composing the original stereographic projection (`stereographic`) with an arbitrary linear isometry
from `(ℝ ∙ v)ᗮ` to the Euclidean space. -/
def stereographic' (n : ℕ) [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
OpenPartialHomeomorph (sphere (0 : E) 1) (EuclideanSpace ℝ (Fin n)) :=
stereographic (norm_eq_of_mem_sphere v) ≫ₕ
(OrthonormalBasis.fromOrthogonalSpanSingleton n
(ne_zero_of_mem_unit_sphere v)).repr.toHomeomorph.toOpenPartialHomeomorph
