English
The stereographic inverse stereoInvFun v is a ContDiff map: it is continuously differentiable with respect to its input variables.
Русский
Стереографическая обратная карта stereoInvFun v является непрерывно дифференцируемой: она имеет непрерывную первую производную и т. д. по входу.
LaTeX
$$$\\operatorname{ContDiff}_{\\mathbb{R}}\\; m\\; (\\text{stereoInvFun } v) \\quad (m\\text{ произвольного типа})$$$
Lean4
/-- Stereographic projection, reverse direction. This is a map from the orthogonal complement of a
unit vector `v` in an inner product space `E` to the unit sphere in `E`. -/
def stereoInvFun (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) : sphere (0 : E) 1 :=
⟨stereoInvFunAux v (w : E), stereoInvFunAux_mem hv w.2⟩
