mathlib documentation

analysis.normed.order.basic

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_ordered_add_group (α : Type u_2) :
Type u_2

A normed_ordered_add_group is an additive group that is both a normed_add_comm_group and an ordered_add_comm_group. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

Instances of this typeclass
Instances of other typeclasses for normed_ordered_add_group
  • normed_ordered_add_group.has_sizeof_inst
@[class]
structure normed_ordered_group (α : Type u_2) :
Type u_2

A normed_ordered_group is a group that is both a normed_comm_group and an ordered_comm_group. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

Instances of this typeclass
Instances of other typeclasses for normed_ordered_group
  • normed_ordered_group.has_sizeof_inst
@[class]
structure normed_linear_ordered_add_group (α : Type u_2) :
Type u_2

A normed_linear_ordered_add_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 caused by both classes carrying their own group structure.

Instances of this typeclass
Instances of other typeclasses for normed_linear_ordered_add_group
  • normed_linear_ordered_add_group.has_sizeof_inst
@[class]
structure normed_linear_ordered_group (α : Type u_2) :
Type u_2

A normed_linear_ordered_group is a group that is both a normed_comm_group and a linear_ordered_comm_group. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

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_2) :
Type u_2

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]
Equations