Documentation

Mathlib.Analysis.Normed.Group.BallSphere

Negation on spheres and balls #

In this file we define InvolutiveNeg and ContinuousNeg instances for spheres, open balls, and closed balls in a semi normed group.

source
instance instInvolutiveNegElemSphereOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
InvolutiveNeg ↑(Metric.sphere 0 r)

We equip the sphere, in a seminormed group, with a formal operation of negation, namely the antipodal map.

Equations
    source
    @[simp]
    theorem coe_neg_sphere {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.sphere 0 r)) :
    ↑(-v) = -↑v
    source
    instance instContinuousNegElemSphereOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
    ContinuousNeg ↑(Metric.sphere 0 r)
    source
    instance instInvolutiveNegElemBallOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
    InvolutiveNeg ↑(Metric.ball 0 r)

    We equip the ball, in a seminormed group, with a formal operation of negation, namely the antipodal map.

    Equations
      source
      @[simp]
      theorem coe_neg_ball {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.ball 0 r)) :
      ↑(-v) = -↑v
      source
      instance instContinuousNegElemBallOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
      ContinuousNeg ↑(Metric.ball 0 r)
      source
      instance instInvolutiveNegElemClosedBallOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
      InvolutiveNeg ↑(Metric.closedBall 0 r)

      We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the antipodal map.

      Equations
        source
        @[simp]
        theorem coe_neg_closedBall {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.closedBall 0 r)) :
        ↑(-v) = -↑v
        source
        instance instContinuousNegElemClosedBallOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
        ContinuousNeg ↑(Metric.closedBall 0 r)