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 : α), = 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 of this typeclass
Instances of other typeclasses for normed_linear_ordered_group
• normed_linear_ordered_group.has_sizeof_inst
@[protected, 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 : α), = 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 of this typeclass
Instances of other typeclasses for normed_linear_ordered_field
• normed_linear_ordered_field.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def rat.normed_linear_ordered_field  :
Equations
@[protected, instance]
noncomputable def real.normed_linear_ordered_field  :
Equations