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 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 = MulAction.mk ⋯ ⋯

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 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 = MulAction.mk ⋯ ⋯

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 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 = MulAction.mk ⋯ ⋯

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 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 = MulAction.mk ⋯ ⋯

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 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 = MulAction.mk ⋯ ⋯

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