stereoInvFun_apply — Mathlib

English

For hv with ‖v‖ = 1 and w in the orthogonal complement of v, the stereographic inverse has an explicit formula in E: (stereoInvFun hv w) = (‖w‖^2 + 4)^{-1} · (4 w + (‖w‖^2 − 4) v).

Русский

При hv, удовлетворяющем ‖v‖ = 1, и любом w ∈ (ℝ·v)⊥, явное выражение stereoInvFun hv w в пространстве E задаётся формулой (‖w‖^2 + 4)^{-1} · (4 w + (‖w‖^2 − 4) v).

LaTeX

$$$\\bigl(\\text{stereoInvFun } hv \\; w \\bigr) = (\\|w\\|^2 + 4)^{-1} \\cdot \\bigl( 4 w + (\\|w\\|^2 - 4) v \\bigr) \\quad (hv: \\|v\\| = 1,\\ w \\in (\\mathbb{R} \\cdot v)^{\\perp})$$$

Lean4

@[simp]
theorem stereoInvFun_apply (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) :
    (stereoInvFun hv w : E) = (‖w‖ ^ 2 + 4)⁻¹ • ((4 : ℝ) • w + (‖w‖ ^ 2 - 4) • v) :=
  rfl

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