Documentation

Mathlib.Analysis.NormedSpace.BallAction

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.

instance mulActionClosedBallBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
instance continuousSMul_closedBall_ball {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
  • =
instance mulActionClosedBallClosedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
Equations
  • =
instance mulActionSphereBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
instance continuousSMul_sphere_ball {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
  • =
instance mulActionSphereClosedBall {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
Equations
  • =
instance mulActionSphereSphere {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
instance continuousSMul_sphere_sphere {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {r : } :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
instance isScalarTower_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] :
Equations
  • =
instance isScalarTower_closedBall_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
instance instSMulCommClass_sphere_ball_ball {𝕜 : Type u_1} {𝕜' : Type u_2} [NormedField 𝕜] [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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] :
Equations
  • =
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