Orders on a sigma type #
This file defines two orders on a sigma type:
- The disjoint sum of orders.
ais lessbiffaandbare in the same summand andais less thanbthere. - The lexicographical order.
ais less thanbif its summand is strictly less than the summand ofbor they are in the same summand andais less thanbthere.
We make the disjoint sum of orders the default set of instances. The lexicographic order goes on a type synonym.
Notation #
Σₗ i, α i: Sigma type equipped with the lexicographic order. Type synonym ofΣ i, α i.
See also #
Related files are:
data.finset.colex: Colexicographic order on finite sets.data.list.lex: Lexicographic order on lists.data.pi.lex: Lexicographic order onΠₗ i, α i.data.psigma.order: Lexicographic order onΣₗ' i, α i. Basically a twin of this file.data.prod.lex: Lexicographic order onα × β.
TODO #
Prove that a sigma type is a no_max_order, no_min_order, densely_ordered when its summands
are.
Upgrade equiv.sigma_congr_left, equiv.sigma_congr, equiv.sigma_assoc,
equiv.sigma_prod_of_equiv, equiv.sigma_equiv_prod, ... to order isomorphisms.
@[protected, instance]
def
sigma.has_le
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_le (α i)] :
has_le (Σ (i : ι), α i)
Equations
- sigma.has_le = {le := sigma.le (λ (i : ι), _inst_1 i)}
@[protected, instance]
def
sigma.has_lt
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), has_lt (α i)] :
has_lt (Σ (i : ι), α i)
Equations
- sigma.has_lt = {lt := sigma.lt (λ (i : ι), _inst_1 i)}
@[protected, instance]
def
sigma.preorder
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), preorder (α i)] :
preorder (Σ (i : ι), α i)
Equations
- sigma.preorder = {le := has_le.le sigma.has_le, lt := has_lt.lt sigma.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
@[protected, instance]
def
sigma.partial_order
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), partial_order (α i)] :
partial_order (Σ (i : ι), α i)
Equations
- sigma.partial_order = {le := preorder.le sigma.preorder, lt := preorder.lt sigma.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
def
sigma.lex.preorder
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)] :
preorder (Σₗ (i : ι), α i)
The lexicographical preorder on a sigma type.
Equations
- sigma.lex.preorder = {le := has_le.le sigma.lex.has_le, lt := has_lt.lt sigma.lex.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
@[protected, instance]
def
sigma.lex.partial_order
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), partial_order (α i)] :
partial_order (Σₗ (i : ι), α i)
The lexicographical partial order on a sigma type.
Equations
- sigma.lex.partial_order = {le := preorder.le sigma.lex.preorder, lt := preorder.lt sigma.lex.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
def
sigma.lex.linear_order
{ι : Type u_1}
{α : ι → Type u_2}
[linear_order ι]
[Π (i : ι), linear_order (α i)] :
linear_order (Σₗ (i : ι), α i)
The lexicographical linear order on a sigma type.
Equations
- sigma.lex.linear_order = {le := partial_order.le sigma.lex.partial_order, lt := partial_order.lt sigma.lex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := sigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) (λ (i : ι) (a b : (λ (i : ι), (λ (i : ι), (λ (i : ι), α i) i) i) i), has_le.le.decidable a b), decidable_eq := sigma.decidable_eq (λ (a : ι) (a_1 b : α a), eq.decidable a_1 b), decidable_lt := decidable_lt_of_decidable_le (sigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le)), max := max_default (λ (a b : Σₗ (i : ι), α i), sigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) a b), max_def := _, min := min_default (λ (a b : Σₗ (i : ι), α i), sigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) a b), min_def := _}
@[protected, instance]
def
sigma.lex.order_bot
{ι : Type u_1}
{α : ι → Type u_2}
[partial_order ι]
[order_bot ι]
[Π (i : ι), preorder (α i)]
[order_bot (α ⊥)] :
order_bot (Σₗ (i : ι), α i)
The lexicographical linear order on a sigma type.
@[protected, instance]
def
sigma.lex.order_top
{ι : Type u_1}
{α : ι → Type u_2}
[partial_order ι]
[order_top ι]
[Π (i : ι), preorder (α i)]
[order_top (α ⊤)] :
order_top (Σₗ (i : ι), α i)
The lexicographical linear order on a sigma type.
@[protected, instance]
def
sigma.lex.bounded_order
{ι : Type u_1}
{α : ι → Type u_2}
[partial_order ι]
[bounded_order ι]
[Π (i : ι), preorder (α i)]
[order_bot (α ⊥)]
[order_top (α ⊤)] :
bounded_order (Σₗ (i : ι), α i)
The lexicographical linear order on a sigma type.
Equations
- sigma.lex.bounded_order = {top := order_top.top sigma.lex.order_top, le_top := _, bot := order_bot.bot sigma.lex.order_bot, bot_le := _}