Multiplicative actions of/on balls and spheres

Let E be a normed vector space over a normed field 𝕜. In this file we define the following multiplicative actions.

• The closed unit ball in 𝕜 acts on open balls and closed balls centered at 0 in E.
• The unit sphere in 𝕜 acts on open balls, closed balls, and spheres centered at 0 in E.

@[instance_reducible]

instance instSMulElemClosedBallOfNatRealBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

• instSMulElemClosedBallOfNatRealBall = { smul := fun (c : ↑(Metric.closedBall 0 1)) (x : ↑(Metric.ball 0 r)) => ⟨↑c • ↑x, ⋯⟩ }

@[instance_reducible]

instance mulActionClosedBallBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

Equations

• mulActionClosedBallBall = { toSMul := instSMulElemClosedBallOfNatRealBall, mul_smul := ⋯, one_smul := ⋯ }

instance continuousSMul_closedBall_ball {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

@[instance_reducible]

instance instSMulElemClosedBallOfNatReal {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

• instSMulElemClosedBallOfNatReal = { smul := fun (c : ↑(Metric.closedBall 0 1)) (x : ↑(Metric.closedBall 0 r)) => ⟨↑c • ↑x, ⋯⟩ }

@[instance_reducible]

instance mulActionClosedBallClosedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

Equations

• mulActionClosedBallClosedBall = { toSMul := instSMulElemClosedBallOfNatReal, mul_smul := ⋯, one_smul := ⋯ }

instance continuousSMul_closedBall_closedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

@[instance_reducible]

instance instSMulElemSphereOfNatRealBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

Equations

• instSMulElemSphereOfNatRealBall = { smul := fun (c : ↑(Metric.sphere 0 1)) (x : ↑(Metric.ball 0 r)) => Set.inclusion ⋯ c • x }

@[instance_reducible]

instance mulActionSphereBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

Equations

• mulActionSphereBall = { toSMul := instSMulElemSphereOfNatRealBall, mul_smul := ⋯, one_smul := ⋯ }

instance continuousSMul_sphere_ball {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

@[instance_reducible]

instance instSMulElemSphereOfNatRealClosedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

Equations

• instSMulElemSphereOfNatRealClosedBall = { smul := fun (c : ↑(Metric.sphere 0 1)) (x : ↑(Metric.closedBall 0 r)) => Set.inclusion ⋯ c • x }

@[instance_reducible]

instance mulActionSphereClosedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

Equations

• mulActionSphereClosedBall = { toSMul := instSMulElemSphereOfNatRealClosedBall, mul_smul := ⋯, one_smul := ⋯ }

instance continuousSMul_sphere_closedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

@[instance_reducible]

instance instSMulElemSphereOfNatReal {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : SMul ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

Equations

• instSMulElemSphereOfNatReal = { smul := fun (c : ↑(Metric.sphere 0 1)) (x : ↑(Metric.sphere 0 r)) => ⟨↑c • ↑x, ⋯⟩ }

@[instance_reducible]

instance mulActionSphereSphere {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : MulAction ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

Equations

• mulActionSphereSphere = { toSMul := instSMulElemSphereOfNatReal, mul_smul := ⋯, one_smul := ⋯ }

instance continuousSMul_sphere_sphere {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ} : ContinuousSMul ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

instance isScalarTower_closedBall_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

instance isScalarTower_closedBall_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

instance isScalarTower_sphere_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

instance isScalarTower_sphere_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

instance isScalarTower_sphere_sphere_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

instance isScalarTower_sphere_sphere_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

instance isScalarTower_sphere_sphere_sphere {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

instance isScalarTower_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] : IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)

instance isScalarTower_closedBall_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] : IsScalarTower ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)

instance instSMulCommClass_closedBall_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

instance instSMulCommClass_closedBall_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

instance instSMulCommClass_sphere_closedBall_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)

instance instSMulCommClass_sphere_closedBall_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)

instance instSMulCommClass_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.ball 0 1) ↑(Metric.ball 0 1)

instance instSMulCommClass_sphere_sphere_closedBall {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.closedBall 0 r)

instance instSMulCommClass_sphere_sphere_ball {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)

instance instSMulCommClass_sphere_sphere_sphere {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedField 𝕜'] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {r : ℝ} [SMulCommClass 𝕜 𝕜' E] : SMulCommClass ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)

theorem ne_neg_of_mem_sphere (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 0 r)) : x ≠ -x

theorem ne_neg_of_mem_unit_sphere (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CharZero 𝕜] (x : ↑(Metric.sphere 0 1)) : x ≠ -x