English
The function stereoToFun v is ContDiffOn on the set where innerSL v x ≠ 1; more precisely, it is differentiable on that domain.
Русский
Функция stereoToFun v гладкая на множестве, где innerSL v x ≠ 1; точнее,' её гладкость/дифференцируемость сохраняется на этой области.
LaTeX
$$ContDiffOn\ Real n\ (stereoToFun v)\ (setOf x => Ne (innerSL Reals v x) 1)$$
Lean4
/-- Stereographic projection, forward direction. This is a map from an inner product space `E` to
the orthogonal complement of an element `v` of `E`. It is smooth away from the affine hyperplane
through `v` parallel to the orthogonal complement. It restricts on the sphere to the stereographic
projection. -/
def stereoToFun (x : E) : (ℝ ∙ v)ᗮ :=
(2 / ((1 : ℝ) - innerSL ℝ v x)) • (ℝ ∙ v)ᗮ.orthogonalProjection x
