instInvolutiveNegElemSphereOfNat — Mathlib

English

On the sphere of radius r in a normed additive group E, the antipodal map v ↦ −v is an involution, i.e., −(−v) = v for all v on the sphere.

Русский

На сфере радиуса r в нормированной аддитивной группе E отображение antipodal v ↦ −v является инволюцией: −(−v) = v для всех v на сфере.

LaTeX

$$$\text{for all } v \in \mathsf{sphere}(0,r): \; -(-v) = v$$$

Lean4

/-- We equip the sphere, in a seminormed group, with a formal operation of negation, namely the
antipodal map. -/
instance : InvolutiveNeg (sphere (0 : E) r)
    where
  neg := Subtype.map Neg.neg fun w => by simp
  neg_neg x := Subtype.ext <| neg_neg x.1

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