# mathlibdocumentation

topology.metric_space.algebra

# Compatibility of algebraic operations with metric space structures #

In this file we define mixin typeclasses has_lipschitz_mul, has_lipschitz_add, has_bounded_smul expressing compatibility of multiplication, addition and scalar-multiplication operations with an underlying metric space structure. The intended use case is to abstract certain properties shared by normed groups and by R≥0.

## Implementation notes #

We deduce a has_continuous_mul instance from has_lipschitz_mul, etc. In principle there should be an intermediate typeclass for uniform spaces, but the algebraic hierarchy there (see uniform_group) is structured differently.

@[class]
Prop

Class has_lipschitz_add M says that the addition (+) : X × X → X is Lipschitz jointly in the two arguments.

Instances
@[class]
structure has_lipschitz_mul (β : Type u_2) [monoid β] :
Prop

Class has_lipschitz_mul M says that the multiplication (*) : X × X → X is Lipschitz jointly in the two arguments.

Instances

The Lipschitz constant of an add_monoid β satisfying has_lipschitz_add

Equations
def has_lipschitz_mul.C (β : Type u_2) [monoid β]  :

The Lipschitz constant of a monoid β satisfying has_lipschitz_mul

Equations
theorem lipschitz_with_lipschitz_const_mul_edist {β : Type u_2} [monoid β]  :
(λ (p : β × β), (p.fst) * p.snd)
(λ (p : β × β), p.fst + p.snd)
theorem lipschitz_with_lipschitz_const_add {β : Type u_2} [add_monoid β] (p q : β × β) :
dist (p.fst + p.snd) (q.fst + q.snd) ( * dist p q
theorem lipschitz_with_lipschitz_const_mul {β : Type u_2} [monoid β] (p q : β × β) :
dist ((p.fst) * p.snd) ((q.fst) * q.snd) ( * dist p q
@[instance]
@[instance]
def has_lipschitz_mul.has_continuous_mul {β : Type u_2} [monoid β]  :
@[instance]
def submonoid.has_lipschitz_mul {β : Type u_2} [monoid β] (s : submonoid β) :
@[instance]
@[instance]
@[instance]
@[class]
structure has_bounded_smul (α : Type u_1) (β : Type u_2) [has_zero α] [has_zero β] [ β] :
Prop
• dist_smul_pair' : ∀ (x : α) (y₁ y₂ : β), dist (x y₁) (x y₂) (dist x 0) * dist y₁ y₂
• dist_pair_smul' : ∀ (x₁ x₂ : α) (y : β), dist (x₁ y) (x₂ y) (dist x₁ x₂) * dist y 0

Mixin typeclass on a scalar action of a metric space α on a metric space β both with distinguished points 0, requiring compatibility of the action in the sense that dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂ and dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0.

Instances
theorem dist_smul_pair {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] [ β] (x : α) (y₁ y₂ : β) :
dist (x y₁) (x y₂) (dist x 0) * dist y₁ y₂
theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] [ β] (x₁ x₂ : α) (y : β) :
dist (x₁ y) (x₂ y) (dist x₁ x₂) * dist y 0
@[instance]
def has_bounded_smul.has_continuous_smul {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] [ β] :

The typeclass has_bounded_smul on a metric-space scalar action implies continuity of the action.

@[instance]
@[instance]