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
instInvolutiveNegElemSphereToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup
{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
- One or more equations did not get rendered due to their size.
@[simp]
theorem
coe_neg_sphere
{E : Type u_1}
[i : SeminormedAddCommGroup E]
{r : ℝ}
(v : ↑(Metric.sphere 0 r))
:
instance
instContinuousNegElemSphereToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpaceToNegInstInvolutiveNegElemSphereToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup
{E : Type u_1}
[i : SeminormedAddCommGroup E]
{r : ℝ}
:
ContinuousNeg ↑(Metric.sphere 0 r)
Equations
- (_ : ContinuousNeg ↑(Metric.sphere 0 r)) = (_ : ContinuousNeg ↑(Metric.sphere 0 r))
instance
instInvolutiveNegElemBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup
{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
- One or more equations did not get rendered due to their size.
@[simp]
theorem
coe_neg_ball
{E : Type u_1}
[i : SeminormedAddCommGroup E]
{r : ℝ}
(v : ↑(Metric.ball 0 r))
:
instance
instContinuousNegElemBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpaceToNegInstInvolutiveNegElemBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup
{E : Type u_1}
[i : SeminormedAddCommGroup E]
{r : ℝ}
:
ContinuousNeg ↑(Metric.ball 0 r)
Equations
- (_ : ContinuousNeg ↑(Metric.ball 0 r)) = (_ : ContinuousNeg ↑(Metric.ball 0 r))
instance
instInvolutiveNegElemClosedBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup
{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
- One or more equations did not get rendered due to their size.
@[simp]
theorem
coe_neg_closedBall
{E : Type u_1}
[i : SeminormedAddCommGroup E]
{r : ℝ}
(v : ↑(Metric.closedBall 0 r))
:
instance
instContinuousNegElemClosedBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpaceToNegInstInvolutiveNegElemClosedBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup
{E : Type u_1}
[i : SeminormedAddCommGroup E]
{r : ℝ}
:
ContinuousNeg ↑(Metric.closedBall 0 r)
Equations
- (_ : ContinuousNeg ↑(Metric.closedBall 0 r)) = (_ : ContinuousNeg ↑(Metric.closedBall 0 r))