stereographic_neg_apply — Mathlib

English

If x is a point on the unit sphere with opposite sign, stereographic hv (norm_eq_of_mem_sphere (−x)) x = 0; this is the negation compatibility of stereo projection.

Русский

Если x лежит на единичной сфере, stereographic proj^{-1} от −x дает 0; совместимость с отрицанием.

LaTeX

$$$\\text{stereographic\_neg\_apply} (x) : stereographic (norm\_eq\_of\_mem\_sphere(-x)) x = 0$$$

Lean4

@[simp]
theorem stereographic_neg_apply (v : sphere (0 : E) 1) : stereographic (norm_eq_of_mem_sphere (-v)) v = 0 :=
  by
  convert stereographic_apply_neg (-v)
  ext1
  simp

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