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_group and a linear_ordered_add_comm_group. This class is necessary to avoid diamonds.

Instances
@[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