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]
- to_ordered_add_comm_group : ordered_add_comm_group α
- to_has_norm : has_norm α
- to_metric_space : metric_space α
- dist_eq : (∀ (x y : α), has_dist.dist x y = ‖x - y‖) . "obviously"
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]
- to_ordered_comm_group : ordered_comm_group α
- to_has_norm : has_norm α
- to_metric_space : metric_space α
- dist_eq : (∀ (x y : α), has_dist.dist x y = ‖x / y‖) . "obviously"
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]
- to_linear_ordered_add_comm_group : linear_ordered_add_comm_group α
- to_has_norm : has_norm α
- to_metric_space : metric_space α
- dist_eq : (∀ (x y : α), has_dist.dist x y = ‖x - y‖) . "obviously"
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]
- to_linear_ordered_comm_group : linear_ordered_comm_group α
- to_has_norm : has_norm α
- to_metric_space : metric_space α
- dist_eq : (∀ (x y : α), has_dist.dist x y = ‖x / y‖) . "obviously"
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]
- to_linear_ordered_field : linear_ordered_field α
- to_has_norm : has_norm α
- to_metric_space : metric_space α
- dist_eq : (∀ (x y : α), has_dist.dist x y = ‖x - y‖) . "obviously"
- norm_mul' : ∀ (x y : α), ‖x * y‖ = ‖x‖ * ‖y‖
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]
@[protected, instance]
Equations
- normed_ordered_add_group.to_normed_add_comm_group = {to_has_norm := normed_ordered_add_group.to_has_norm _inst_1, to_add_comm_group := ordered_add_comm_group.to_add_comm_group α normed_ordered_add_group.to_ordered_add_comm_group, to_metric_space := normed_ordered_add_group.to_metric_space _inst_1, dist_eq := _}
@[protected, instance]
def
normed_linear_ordered_group.to_normed_ordered_group
{α : Type u_1}
[normed_linear_ordered_group α] :
Equations
- normed_linear_ordered_group.to_normed_ordered_group = {to_ordered_comm_group := linear_ordered_comm_group.to_ordered_comm_group α normed_linear_ordered_group.to_linear_ordered_comm_group, to_has_norm := normed_linear_ordered_group.to_has_norm _inst_1, to_metric_space := normed_linear_ordered_group.to_metric_space _inst_1, dist_eq := _}
@[protected, instance]
def
normed_linear_ordered_add_group.to_normed_ordered_add_group
{α : Type u_1}
[normed_linear_ordered_add_group α] :
Equations
- normed_linear_ordered_add_group.to_normed_ordered_add_group = {to_ordered_add_comm_group := linear_ordered_add_comm_group.to_ordered_add_comm_group α normed_linear_ordered_add_group.to_linear_ordered_add_comm_group, to_has_norm := normed_linear_ordered_add_group.to_has_norm _inst_1, to_metric_space := normed_linear_ordered_add_group.to_metric_space _inst_1, dist_eq := _}
@[protected, instance]
Equations
- normed_linear_ordered_field.to_normed_field α = {to_has_norm := normed_linear_ordered_field.to_has_norm _inst_1, to_field := linear_ordered_field.to_field α normed_linear_ordered_field.to_linear_ordered_field, to_metric_space := normed_linear_ordered_field.to_metric_space _inst_1, dist_eq := _, norm_mul' := _}
@[protected, instance]
Equations
- rat.normed_linear_ordered_field = {to_linear_ordered_field := rat.linear_ordered_field, to_has_norm := normed_field.to_has_norm rat.normed_field, to_metric_space := rat.metric_space, dist_eq := rat.normed_linear_ordered_field._proof_1, norm_mul' := rat.normed_linear_ordered_field._proof_2}
@[protected, instance]
Equations
- real.normed_linear_ordered_field = {to_linear_ordered_field := real.linear_ordered_field, to_has_norm := real.has_norm, to_metric_space := real.metric_space, dist_eq := real.normed_linear_ordered_field._proof_1, norm_mul' := real.normed_linear_ordered_field._proof_2}
@[protected, instance]
Equations
- order_dual.normed_ordered_group = {to_ordered_comm_group := {mul := comm_group.mul normed_comm_group.to_comm_group, mul_assoc := _, one := comm_group.one normed_comm_group.to_comm_group, one_mul := _, mul_one := _, npow := comm_group.npow normed_comm_group.to_comm_group, npow_zero' := _, npow_succ' := _, inv := comm_group.inv normed_comm_group.to_comm_group, div := comm_group.div normed_comm_group.to_comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow normed_comm_group.to_comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := ordered_comm_group.le order_dual.ordered_comm_group, lt := ordered_comm_group.lt order_dual.ordered_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}, to_has_norm := normed_comm_group.to_has_norm normed_ordered_group.to_normed_comm_group, to_metric_space := normed_comm_group.to_metric_space normed_ordered_group.to_normed_comm_group, dist_eq := _}
@[protected, instance]
Equations
- order_dual.normed_ordered_add_group = {to_ordered_add_comm_group := {add := add_comm_group.add normed_add_comm_group.to_add_comm_group, add_assoc := _, zero := add_comm_group.zero normed_add_comm_group.to_add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul normed_add_comm_group.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg normed_add_comm_group.to_add_comm_group, sub := add_comm_group.sub normed_add_comm_group.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul normed_add_comm_group.to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_add_comm_group.le order_dual.ordered_add_comm_group, lt := ordered_add_comm_group.lt order_dual.ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}, to_has_norm := normed_add_comm_group.to_has_norm normed_ordered_add_group.to_normed_add_comm_group, to_metric_space := normed_add_comm_group.to_metric_space normed_ordered_add_group.to_normed_add_comm_group, dist_eq := _}
@[protected, instance]
Equations
- order_dual.normed_linear_ordered_group = {to_linear_ordered_comm_group := {mul := ordered_comm_group.mul normed_ordered_group.to_ordered_comm_group, mul_assoc := _, one := ordered_comm_group.one normed_ordered_group.to_ordered_comm_group, one_mul := _, mul_one := _, npow := ordered_comm_group.npow normed_ordered_group.to_ordered_comm_group, npow_zero' := _, npow_succ' := _, inv := ordered_comm_group.inv normed_ordered_group.to_ordered_comm_group, div := ordered_comm_group.div normed_ordered_group.to_ordered_comm_group, div_eq_mul_inv := _, zpow := ordered_comm_group.zpow normed_ordered_group.to_ordered_comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := ordered_comm_group.le normed_ordered_group.to_ordered_comm_group, lt := ordered_comm_group.lt normed_ordered_group.to_ordered_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := linear_order.max (order_dual.linear_order α), max_def := _, min := linear_order.min (order_dual.linear_order α), min_def := _}, to_has_norm := normed_ordered_group.to_has_norm order_dual.normed_ordered_group, to_metric_space := normed_ordered_group.to_metric_space order_dual.normed_ordered_group, dist_eq := _}
@[protected, instance]
Equations
- order_dual.normed_linear_ordered_add_group = {to_linear_ordered_add_comm_group := {add := ordered_add_comm_group.add normed_ordered_add_group.to_ordered_add_comm_group, add_assoc := _, zero := ordered_add_comm_group.zero normed_ordered_add_group.to_ordered_add_comm_group, zero_add := _, add_zero := _, nsmul := ordered_add_comm_group.nsmul normed_ordered_add_group.to_ordered_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_add_comm_group.neg normed_ordered_add_group.to_ordered_add_comm_group, sub := ordered_add_comm_group.sub normed_ordered_add_group.to_ordered_add_comm_group, sub_eq_add_neg := _, zsmul := ordered_add_comm_group.zsmul normed_ordered_add_group.to_ordered_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := ordered_add_comm_group.le normed_ordered_add_group.to_ordered_add_comm_group, lt := ordered_add_comm_group.lt normed_ordered_add_group.to_ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max := linear_order.max (order_dual.linear_order α), max_def := _, min := linear_order.min (order_dual.linear_order α), min_def := _}, to_has_norm := normed_ordered_add_group.to_has_norm order_dual.normed_ordered_add_group, to_metric_space := normed_ordered_add_group.to_metric_space order_dual.normed_ordered_add_group, dist_eq := _}
@[protected, instance]
Equations
- additive.normed_ordered_add_group = {to_ordered_add_comm_group := additive.ordered_add_comm_group normed_ordered_group.to_ordered_comm_group, to_has_norm := normed_add_comm_group.to_has_norm additive.normed_add_comm_group, to_metric_space := normed_add_comm_group.to_metric_space additive.normed_add_comm_group, dist_eq := _}
@[protected, instance]
Equations
- multiplicative.normed_ordered_group = {to_ordered_comm_group := multiplicative.ordered_comm_group normed_ordered_add_group.to_ordered_add_comm_group, to_has_norm := normed_comm_group.to_has_norm multiplicative.normed_comm_group, to_metric_space := normed_comm_group.to_metric_space multiplicative.normed_comm_group, dist_eq := _}
@[protected, instance]
Equations
- additive.normed_linear_ordered_add_group = {to_linear_ordered_add_comm_group := additive.linear_ordered_add_comm_group normed_linear_ordered_group.to_linear_ordered_comm_group, to_has_norm := normed_add_comm_group.to_has_norm additive.normed_add_comm_group, to_metric_space := normed_add_comm_group.to_metric_space additive.normed_add_comm_group, dist_eq := _}
@[protected, instance]
Equations
- multiplicative.normed_linear_ordered_group = {to_linear_ordered_comm_group := multiplicative.linear_ordered_comm_group normed_linear_ordered_add_group.to_linear_ordered_add_comm_group, to_has_norm := normed_comm_group.to_has_norm multiplicative.normed_comm_group, to_metric_space := normed_comm_group.to_metric_space multiplicative.normed_comm_group, dist_eq := _}