stereographic_apply — Mathlib

English

For hv with ‖v‖ = 1 and x on the sphere, the stereographic projection is given by a scalar multiple of the orthogonal projection: stereographic hv x = (2 / (1 − ⟨v, x⟩)) · P⊥(x).

Русский

При ‖v‖=1 и x на сфере стереографическая проекция задаётся как кратное скалярному проекции: stereographic hv x = (2/(1−⟨v,x⟩))·Proj⊥(x).

LaTeX

$$$\\text{stereographic } hv \\; x = \\dfrac{2}{1 - \\langle v, x\\rangle} \\cdot ((\\mathbb{R}\\cdot v)^{\\perp}\\!\\text{ projections } x)$$$

Lean4

theorem stereographic_apply (hv : ‖v‖ = 1) (x : sphere (0 : E) 1) :
    stereographic hv x = (2 / ((1 : ℝ) - ⟪v, x⟫)) • (ℝ ∙ v)ᗮ.orthogonalProjection x :=
  rfl

Похожие утверждения