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.partial_order
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
[Π (a : ι), partial_order (β a)] :
partial_order (pilex ι β)
Equations
- pilex.partial_order = have lt_not_symm : ∀ {x y : pilex ι β}, ¬(x < y ∧ y < x), from pilex.partial_order._proof_5, {le := λ (x y : pilex ι β), x < y ∨ x = y, lt := has_lt.lt pilex.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected]
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
- pilex.linear_order wf = {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 := _, le_total := _, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le)}
@[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 := _, gsmul := add_comm_group.gsmul pi.add_comm_group, gsmul_zero' := _, gsmul_succ' := _, gsmul_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 := _}