mathlib3 documentation

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]
structure has_lipschitz_add (β : Type u_2) [pseudo_metric_space β] [add_monoid β] :
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) [pseudo_metric_space β] [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
noncomputable def has_lipschitz_add.C (β : Type u_2) [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] :

The Lipschitz constant of an add_monoid β satisfying has_lipschitz_add

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

The Lipschitz constant of a monoid β satisfying has_lipschitz_mul

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[class]
structure has_bounded_smul (α : Type u_1) (β : Type u_2) [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_smul α β] :
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} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_smul α β] [has_bounded_smul α β] (x : α) (y₁ y₂ : β) :
has_dist.dist (x y₁) (x y₂) has_dist.dist x 0 * has_dist.dist y₁ y₂
theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_smul α β] [has_bounded_smul α β] (x₁ x₂ : α) (y : β) :
has_dist.dist (x₁ y) (x₂ y) has_dist.dist x₁ x₂ * has_dist.dist y 0
@[protected, instance]

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

@[protected, instance]
@[protected, instance]

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

@[protected, instance]