stereographic — Mathlib

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

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