mathlib3 documentation

analysis.normed.order.basic

Ordered normed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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