English
There exists a manifold structure on the interval [0,1] regarded as a Euclidean half-space model, i.e., the endpoint-interval inherits a smooth manifold structure.
Русский
Существует манифолд-структура на интервале [0,1], рассматриваемом как модель евклидовой полуплоскости, т.е. концовый интервал наследует гладкую структуру манифольда.
LaTeX
$$IsManifold\ (modelWithCornersEuclideanHalfSpace 1)\ (Set.Icc 0 1).Elem$$
Lean4
/-- Auxiliary function for the construction of the reverse direction of the stereographic
projection. This is a map from the orthogonal complement of a unit vector `v` in an inner product
space `E` to `E`; we will later prove that it takes values in the unit sphere.
For most purposes, use `stereoInvFun`, not `stereoInvFunAux`. -/
def stereoInvFunAux (w : E) : E :=
(‖w‖ ^ 2 + 4)⁻¹ • ((4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v)
