English
For hv with ‖v‖ = 1 and w ∈ (ℝ·v)⊥, stereoInvFun hv w is never equal to the north pole on the sphere; i.e., stereoInvFun hv w ≠ ⟨v,hv⟩.
Русский
При ‖v‖ = 1 и w ∈ (ℝ·v)⊥ отображение stereo InvFun hv w не равно северной полю на сфере.
LaTeX
$$$\\text{stereoInvFun } hv w \\neq \\bigl(\\langle v, \\cdot \\rangle, \\text{hv} \\bigr)\\;$$$
Lean4
theorem stereoInvFun_ne_north_pole (hv : ‖v‖ = 1) (w : (ℝ ∙ v)ᗮ) :
stereoInvFun hv w ≠ (⟨v, by simp [hv]⟩ : sphere (0 : E) 1) :=
by
refine Subtype.coe_ne_coe.1 ?_
rw [← inner_lt_one_iff_real_of_norm_one _ hv]
· have hw : ⟪v, w⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
have hw' : (‖(w : E)‖ ^ 2 + 4)⁻¹ * (‖(w : E)‖ ^ 2 - 4) < 1 :=
by
rw [inv_mul_lt_iff₀']
· linarith
positivity
simpa [real_inner_comm, inner_add_right, inner_smul_right, real_inner_self_eq_norm_mul_norm, hw, hv] using hw'
· simpa using stereoInvFunAux_mem hv w.2
