# mathlib3documentation

topology.metric_space.algebra

# Compatibility of algebraic operations with metric space structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 of this typeclass
@[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 of this typeclass

The Lipschitz constant of an add_monoid β satisfying has_lipschitz_add

Equations
noncomputable 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 : β × β) :
has_dist.dist (p.fst + p.snd) (q.fst + q.snd)
theorem lipschitz_with_lipschitz_const_mul {β : Type u_2} [monoid β] (p q : β × β) :
has_dist.dist (p.fst * p.snd) (q.fst * q.snd)
@[protected, instance]
@[protected, instance]
@[protected, instance]
def submonoid.has_lipschitz_mul {β : Type u_2} [monoid β] (s : submonoid β) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def mul_opposite.has_lipschitz_mul {β : Type u_2} [monoid β]  :
@[protected, instance]
@[protected, instance]
@[class]
structure has_bounded_smul (α : Type u_1) (β : Type u_2) [has_zero α] [has_zero β] [ β] :
Prop

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 of this typeclass
theorem dist_smul_pair {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] [ β] (x : α) (y₁ y₂ : β) :
has_dist.dist (x y₁) (x y₂) * y₂
theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] [ β] (x₁ x₂ : α) (y : β) :
has_dist.dist (x₁ y) (x₂ y) x₂ *
@[protected, 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.

@[protected, instance]
@[protected, instance]
@[protected, instance]
def has_bounded_smul.op {α : Type u_1} {β : Type u_2} [has_zero α] [has_zero β] [ β] [ β] [ β] [ β] :

If a scalar is central, then its right action is bounded when its left action is.

@[protected, instance]