instInvolutiveNegElemClosedBallOfNat

English

The antipodal map on the closed ball is well-defined and negation is consistent with ambient negation.

Русский

Антиподная карта на замкнутом шаре корректна и согласуется с внешним отрицанием.

LaTeX

$$$\operatorname{dist}\,(-v,0) = \operatorname{dist}(v,0)$ by symmetry$$

Lean4

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

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