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))
:
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))
:
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))
:
instance
instContinuousNegElemClosedBallOfNat
{E : Type u_1}
[i : SeminormedAddCommGroup E]
{r : ℝ}
:
ContinuousNeg ↑(Metric.closedBall 0 r)
Equations
- ⋯ = ⋯