@[instance]
Equations
- pilex.inhabited = pilex.inhabited._proof_1.mpr (pi.inhabited ι)
@[instance]
def
pilex.partial_order
{ι : Type u_1}
{β : ι → Type u_2}
[linear_order ι]
[Π (a : ι), partial_order (β a)] :
partial_order (pilex ι β)
Equations
- pilex.partial_order = let I : decidable_linear_order ι := classical.DLO ι in 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 := _}
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 := _}
@[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 := _, neg := add_comm_group.neg pi.add_comm_group, 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 := _}