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_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∥
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
@[protected, instance]
def
normed_linear_ordered_group.to_normed_add_comm_group
(α : Type u_1)
[normed_linear_ordered_group α] :
Equations
- normed_linear_ordered_group.to_normed_add_comm_group α = {to_has_norm := normed_linear_ordered_group.to_has_norm _inst_1, to_add_comm_group := ordered_add_comm_group.to_add_comm_group α (linear_ordered_add_comm_group.to_ordered_add_comm_group α), to_metric_space := normed_linear_ordered_group.to_metric_space _inst_1, dist_eq := _}
@[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∥
- norm_mul' : ∀ (a b : α), ∥a * b∥ = ∥a∥ * ∥b∥
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
- 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]
def
normed_linear_ordered_field.to_normed_linear_ordered_group
(α : Type u_1)
[normed_linear_ordered_field α] :
Equations
- normed_linear_ordered_field.to_normed_linear_ordered_group α = {to_linear_ordered_add_comm_group := linear_ordered_ring.to_linear_ordered_add_comm_group (linear_ordered_comm_ring.to_linear_ordered_ring α), to_has_norm := normed_linear_ordered_field.to_has_norm _inst_1, to_metric_space := normed_linear_ordered_field.to_metric_space _inst_1, dist_eq := _}
@[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 := normed_field.to_has_norm real.normed_field, to_metric_space := real.metric_space, dist_eq := real.normed_linear_ordered_field._proof_1, norm_mul' := real.normed_linear_ordered_field._proof_2}