stereographic_source — Mathlib

English

For hv with ‖v‖ = 1, the stereographic projection stereographic hv is surjective onto the whole orthogonal complement; every point of (ℝ·v)⊥ is attained by stereographic hv from some point on the sphere.

Русский

При ‖v‖=1 стереографическая проекция также сюръективна на все пространство (ℝ·v)⊥; любой член этого подпространства достигается образом sterographic hv.

LaTeX

$$$\\operatorname{Surjective}(\\text{stereographic } hv)$$$

Lean4

@[simp]
theorem stereographic_source (hv : ‖v‖ = 1) : (stereographic hv).source = {⟨v, by simp [hv]⟩}ᶜ :=
  rfl

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