# mathlibdocumentation

analysis.normed_space.ordered

# Ordered normed spaces #

In this file, we define classes for fields and groups that are both normed and ordered. These are mostly useful to avoid diamonds during type class inference.

@[class]
structure normed_linear_ordered_group (α : Type u_1) :
Type u_1
• to_has_norm :
• to_metric_space :
• dist_eq : ∀ (x y : α), dist x y = x - y

A normed_linear_ordered_group is an additive group that is both a normed_group and a linear_ordered_add_comm_group. This class is necessary to avoid diamonds.

Instances
@[instance]
Equations
@[class]
structure normed_linear_ordered_field (α : Type u_1) :
Type u_1
• to_linear_ordered_field :
• to_has_norm :
• to_metric_space :
• dist_eq : ∀ (x y : α), dist x y = x - y
• norm_mul' : ∀ (a b : α), a * b = a * b

A normed_linear_ordered_field is a field that is both a normed_field and a linear_ordered_field. This class is necessary to avoid diamonds.

Instances
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations