ne_neg_of_mem_sphere — Mathlib

English

If the radius r is nonzero, then no element x of the sphere is its own negation, i.e., x ≠ -x whenever r ≠ 0.

Русский

Если радиус r не равен нулю, ни один элемент сферы не совпадает с его отрицанием: x ≠ -x при r ≠ 0.

LaTeX

$$$(r\neq 0)\Rightarrow\forall x\in S(0,r),\ x\neq -x,$ where $S(0,r)=\{x: E:\|x\|=r\}$$$

Lean4

theorem ne_neg_of_mem_sphere {r : ℝ} (hr : r ≠ 0) (x : sphere (0 : E) r) : x ≠ -x := fun h =>
  ne_zero_of_mem_sphere hr x ((self_eq_neg 𝕜 _).mp (by (conv_lhs => rw [h]); rfl))

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