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.

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

• instInvolutiveNegElemSphereOfNat = InvolutiveNeg.mk ⋯

@[simp]

theorem coe_neg_sphere {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.sphere 0 r)) : ↑(-v) = -↑v

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

Equations

• ⋯ = ⋯

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

• instInvolutiveNegElemBallOfNat = InvolutiveNeg.mk ⋯

@[simp]

theorem coe_neg_ball {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.ball 0 r)) : ↑(-v) = -↑v

instance instContinuousNegElemBallOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} : ContinuousNeg ↑(Metric.ball 0 r)

Equations

• ⋯ = ⋯

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

• instInvolutiveNegElemClosedBallOfNat = InvolutiveNeg.mk ⋯

@[simp]

theorem coe_neg_closedBall {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.closedBall 0 r)) : ↑(-v) = -↑v

instance instContinuousNegElemClosedBallOfNat {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} : ContinuousNeg ↑(Metric.closedBall 0 r)

Equations

• ⋯ = ⋯