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 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
  • instInvolutiveNegElemSphereToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup = InvolutiveNeg.mk ⋯
source
@[simp]
theorem coe_neg_sphere {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.sphere 0 r)) :
↑(-v) = -↑v
source
instance instContinuousNegElemSphereToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpaceToNegInstInvolutiveNegElemSphereToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
ContinuousNeg ↑(Metric.sphere 0 r)
Equations
  • ⋯ = ⋯
source
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
  • instInvolutiveNegElemBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup = InvolutiveNeg.mk ⋯
source
@[simp]
theorem coe_neg_ball {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.ball 0 r)) :
↑(-v) = -↑v
source
instance instContinuousNegElemBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpaceToNegInstInvolutiveNegElemBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
ContinuousNeg ↑(Metric.ball 0 r)
Equations
  • ⋯ = ⋯
source
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
  • instInvolutiveNegElemClosedBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup = InvolutiveNeg.mk ⋯
source
@[simp]
theorem coe_neg_closedBall {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} (v : ↑(Metric.closedBall 0 r)) :
↑(-v) = -↑v
source
instance instContinuousNegElemClosedBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroupInstTopologicalSpaceSubtypeMemSetInstMembershipSetToTopologicalSpaceToUniformSpaceToNegInstInvolutiveNegElemClosedBallToPseudoMetricSpaceOfNatToOfNat0ToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToAddCommGroup {E : Type u_1} [i : SeminormedAddCommGroup E] {r : ℝ} :
ContinuousNeg ↑(Metric.closedBall 0 r)
Equations
  • ⋯ = ⋯