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.

source
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
source
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)
Equations
source
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
  • One or more equations did not get rendered due to their size.
source
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)
Equations
source
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
source
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)
Equations
source
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
  • One or more equations did not get rendered due to their size.
source
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)
Equations
source
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
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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)
Equations
source
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
source
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