Theorems · Definition · global analysis

stereoToFun

{E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → (v : E) → E → ↥(ℝ ∙ v)ᗮ

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.

Defined in

Mathlib.Geometry.Manifold.Instances.Sphere

Cited by

7 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpace