stereographic_apply_neg — Mathlib

English

For v ∈ sphere and the vector -v, the stereographic projection sends the negative pole to 0 on the target, i.e., stereographic (norm_eq_of_mem_sphere (-v)) (-v) = 0.

Русский

Для v на сфере и вектора −v стереографическая проекция отправляет северный полюс на ноль: stereographic (norm_eq_of_mem_sphere (−v)) (−v) = 0.

LaTeX

$$$\\text{stereographic}(\\text{norm\_eq\_of\_mem\_sphere }(-v))(-v) = 0$$$

Lean4

@[simp]
theorem stereographic_apply_neg (v : sphere (0 : E) 1) : stereographic (norm_eq_of_mem_sphere v) (-v) = 0 := by
  simp [stereographic_apply, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero]

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