English
The stereographic projection stereographic hv is the open partial homeomorphism from the unit sphere to the orthogonal complement (ℝ∙v)⊥ with hv: ‖v‖ = 1; toFun and invFun are stereoToFun v and stereoInvFun hv respectively.
Русский
Стереографическая проекция stereographic hv задаёт отображение сферы на ортогональное дополнение (ℝ·v)⊥; отображение строится через stereoToFun и stereoInvFun hv.
LaTeX
$$$\\text{stereographic } hv : \\text{sphere} \\to (\\mathbb{R}\\cdot v)^{\\perp}$$$
Lean4
/-- Stereographic projection from the unit sphere in `E`, centred at a unit vector `v` in `E`;
this is the version as an open partial homeomorphism. -/
def stereographic (hv : ‖v‖ = 1) : OpenPartialHomeomorph (sphere (0 : E) 1) (ℝ ∙ v)ᗮ
where
toFun := stereoToFun v ∘ (↑)
invFun := stereoInvFun hv
source := {⟨v, by simp [hv]⟩}ᶜ
target := Set.univ
map_source' := by simp
map_target' {w} _ := fun h => (stereoInvFun_ne_north_pole hv w) (Set.eq_of_mem_singleton h)
left_inv' x
hx :=
stereo_left_inv hv fun h =>
hx
(by
rw [← h] at hv
apply Subtype.ext
dsimp
exact h)
right_inv' w _ := stereo_right_inv hv w
open_source := isOpen_compl_singleton
open_target := isOpen_univ
continuousOn_toFun :=
continuousOn_stereoToFun.comp continuous_subtype_val.continuousOn fun w h =>
by
dsimp
exact h ∘ Subtype.ext ∘ Eq.symm ∘ (inner_eq_one_iff_of_norm_one hv (by simp)).mp
continuousOn_invFun := (continuous_stereoInvFun hv).continuousOn