mathlib documentation

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]
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
@[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

The Lipschitz constant of a monoid β satisfying has_lipschitz_mul

Equations
theorem lipschitz_with_lipschitz_const_add {β : Type u_2} [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] (p q : β × β) :
dist (p.fst + p.snd) (q.fst + q.snd) ((has_lipschitz_add.C β)) * dist p q
theorem lipschitz_with_lipschitz_const_mul {β : Type u_2} [pseudo_metric_space β] [monoid β] [has_lipschitz_mul β] (p q : β × β) :
dist ((p.fst) * p.snd) ((q.fst) * q.snd) ((has_lipschitz_mul.C β)) * dist p q
@[class]
structure has_bounded_smul (α : Type u_1) (β : Type u_2) [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_scalar α β] :
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} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_scalar α β] [has_bounded_smul α β] (x : α) (y₁ y₂ : β) :
dist (x y₁) (x y₂) (dist x 0) * dist y₁ y₂
theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_scalar α β] [has_bounded_smul α β] (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} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_scalar α β] [has_bounded_smul α β] :

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