mathlib documentation

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

A normed_linear_ordered_group is an additive group that is both a normed_add_comm_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
@[class]
structure normed_linear_ordered_field (α : Type u_1) :
Type u_1

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