Theorems · Theorem · global analysis

stereoToFun_apply

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (x : E),
  stereoToFun v x = (2 / (1 - ((innerSL ℝ) v) x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto x

Defined in

Mathlib.Geometry.Manifold.Instances.Sphere

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpace