# Lemmas for BoundedSMul over normed additive groups #

Lemmas which hold only in NormedSpace α β are provided in another file.

Notably we prove that NonUnitalSeminormedRings have bounded actions by left- and right- multiplication. This allows downstream files to write general results about BoundedSMul, and then deduce const_mul and mul_const results as an immediate corollary.

theorem norm_smul_le {α : Type u_1} {β : Type u_2} [] [] (r : α) (x : β) :
theorem nnnorm_smul_le {α : Type u_1} {β : Type u_2} [] [] (r : α) (x : β) :
theorem dist_smul_le {α : Type u_1} {β : Type u_2} [] [] (s : α) (x : β) (y : β) :
dist (s x) (s y) s * dist x y
theorem nndist_smul_le {α : Type u_1} {β : Type u_2} [] [] (s : α) (x : β) (y : β) :
nndist (s x) (s y) s‖₊ * nndist x y
theorem lipschitzWith_smul {α : Type u_1} {β : Type u_2} [] [] (s : α) :
LipschitzWith s‖₊ fun (x : β) => s x
theorem edist_smul_le {α : Type u_1} {β : Type u_2} [] [] (s : α) (x : β) (y : β) :
edist (s x) (s y) s‖₊ edist x y

Left multiplication is bounded.

Equations
• =

Right multiplication is bounded.

Equations
• =
theorem BoundedSMul.of_norm_smul_le {α : Type u_1} {β : Type u_2} [] [Module α β] (h : ∀ (r : α) (x : β), r x r * x) :
theorem BoundedSMul.of_nnnorm_smul_le {α : Type u_1} {β : Type u_2} [] [Module α β] (h : ∀ (r : α) (x : β), r x‖₊ r‖₊ * x‖₊) :
theorem norm_smul {α : Type u_1} {β : Type u_2} [] [] (r : α) (x : β) :
theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [] [] (r : α) (x : β) :
theorem dist_smul₀ {α : Type u_1} {β : Type u_2} [Module α β] [] (s : α) (x : β) (y : β) :
dist (s x) (s y) = s * dist x y
theorem nndist_smul₀ {α : Type u_1} {β : Type u_2} [Module α β] [] (s : α) (x : β) (y : β) :
nndist (s x) (s y) = s‖₊ * nndist x y
theorem edist_smul₀ {α : Type u_1} {β : Type u_2} [Module α β] [] (s : α) (x : β) (y : β) :
edist (s x) (s y) = s‖₊ edist x y