Lexicographic order on Pi types #
This file defines the lexicographic relation for Pi types of partial orders and linear orders. We
also provide a pilex analog of pi.ordered_comm_group (see algebra.order.pi).
def
pi.lex
{ι : Type u_1}
{β : ι → Type u_2}
(r : ι → ι → Prop)
(s : Π {i : ι}, β i → β i → Prop)
(x y : Π (i : ι), β i) :
Prop
The lexicographic relation on Π i : ι, β i, where ι is ordered by r,
and each β i is ordered by s.
@[protected, instance]
Equations
- pilex.inhabited = pilex.inhabited._proof_1.mpr (pi.inhabited ι)
@[protected, instance]
def
pilex.is_strict_order
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
[Π (a : ι), partial_order (β a)] :
is_strict_order (pilex ι β) has_lt.lt
@[protected, instance]
def
pilex.partial_order
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
[Π (a : ι), partial_order (β a)] :
partial_order (pilex ι β)
Equations
@[protected]
theorem
pilex.is_strict_total_order'
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
(wf : well_founded has_lt.lt)
[Π (a : ι), linear_order (β a)] :
@[protected]
noncomputable
def
pilex.linear_order
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
(wf : well_founded has_lt.lt)
[Π (a : ι), linear_order (β a)] :
linear_order (pilex ι β)
pilex is a linear order if the original order is well-founded.
This cannot be an instance, since it depends on the well-foundedness of <.
Equations
theorem
pilex.le_of_forall_le
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
(wf : well_founded has_lt.lt)
[Π (a : ι), linear_order (β a)]
{a b : pilex ι β}
(h : ∀ (i : ι), a i ≤ b i) :
a ≤ b
@[protected, instance]
def
pilex.ordered_add_comm_group
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
[Π (a : ι), ordered_add_comm_group (β a)] :
ordered_add_comm_group (pilex ι β)
Equations
- pilex.ordered_add_comm_group = {add := add_comm_group.add pi.add_comm_group, add_assoc := _, zero := add_comm_group.zero pi.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul pi.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg pi.add_comm_group, sub := add_comm_group.sub pi.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul pi.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le pilex.partial_order, lt := partial_order.lt pilex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
@[protected, instance]
def
pilex.ordered_comm_group
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
[Π (a : ι), ordered_comm_group (β a)] :
ordered_comm_group (pilex ι β)
Equations
- pilex.ordered_comm_group = {mul := comm_group.mul pi.comm_group, mul_assoc := _, one := comm_group.one pi.comm_group, one_mul := _, mul_one := _, npow := comm_group.npow pi.comm_group, npow_zero' := _, npow_succ' := _, inv := comm_group.inv pi.comm_group, div := comm_group.div pi.comm_group, div_eq_mul_inv := _, zpow := comm_group.zpow pi.comm_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := partial_order.le pilex.partial_order, lt := partial_order.lt pilex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}