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

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]

structure normed_ordered_group (α : Type u_2) :

Type u_2

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]

structure normed_linear_ordered_add_group (α : Type u_2) :

Type u_2

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]

structure normed_linear_ordered_group (α : Type u_2) :

Type u_2

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]

structure normed_linear_ordered_field (α : Type u_2) :

Type u_2

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]

def normed_ordered_group.to_normed_comm_group {α : Type u_1} [normed_ordered_group α] :

normed_comm_group α

Equations

normed_ordered_group.to_normed_comm_group = {to_has_norm := normed_ordered_group.to_has_norm _inst_1, to_comm_group := ordered_comm_group.to_comm_group α normed_ordered_group.to_ordered_comm_group, to_metric_space := normed_ordered_group.to_metric_space _inst_1, dist_eq := _}

@[protected, instance]

def normed_ordered_add_group.to_normed_add_comm_group {α : Type u_1} [normed_ordered_add_group α] :

normed_add_comm_group α

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 α] :

normed_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 α] :

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

def normed_linear_ordered_field.to_normed_field (α : Type u_1) [normed_linear_ordered_field α] :

normed_field α

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 rat.normed_linear_ordered_field :

normed_linear_ordered_field ℚ

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]

noncomputable def real.normed_linear_ordered_field :

normed_linear_ordered_field ℝ

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]

def order_dual.normed_ordered_group {α : Type u_1} [normed_ordered_group α] :

normed_ordered_group αᵒᵈ

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]

def order_dual.normed_ordered_add_group {α : Type u_1} [normed_ordered_add_group α] :

normed_ordered_add_group αᵒᵈ

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]

def order_dual.normed_linear_ordered_group {α : Type u_1} [normed_linear_ordered_group α] :

normed_linear_ordered_group αᵒᵈ

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]

def order_dual.normed_linear_ordered_add_group {α : Type u_1} [normed_linear_ordered_add_group α] :

normed_linear_ordered_add_group αᵒᵈ

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]

def additive.normed_ordered_add_group {α : Type u_1} [normed_ordered_group α] :

normed_ordered_add_group (additive α)

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]

def multiplicative.normed_ordered_group {α : Type u_1} [normed_ordered_add_group α] :

normed_ordered_group (multiplicative α)

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]

def additive.normed_linear_ordered_add_group {α : Type u_1} [normed_linear_ordered_group α] :

normed_linear_ordered_add_group (additive α)

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]

def multiplicative.normed_linear_ordered_group {α : Type u_1} [normed_linear_ordered_add_group α] :

normed_linear_ordered_group (multiplicative α)

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 := _}