instInvolutiveNegElemBallOfNat — Mathlib

English

The antipodal negation of a point in the ball, when viewed in E, equals the ordinary negation in E.

Русский

Антиподная карта внутри шара при встраивании в E совпадает с обычным отрицанием в E.

LaTeX

$$$\iota(-v) = -\iota(v)\quad\text{для } v\in \mathsf{ball}(0,r)$$$

Lean4

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

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