Lexicographic order on a sigma type #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the lexicographic order on Σₗ' i, α i. a is less than b if its summand is
strictly less than the summand of b or they are in the same summand and a is less than b
there.
Notation #
Σₗ' i, α i: Sigma type equipped with the lexicographic order. A 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.sigma.order: Lexicographic order onΣₗ i, α i. Basically a twin of this file.data.prod.lex: Lexicographic order onα × β.
TODO #
Define the disjoint order on Σ' i, α i, where x ≤ y only if x.fst = y.fst.
Prove that a sigma type is a no_max_order, no_min_order, densely_ordered when its summands
are.
@[protected, instance]
def
psigma.lex.preorder
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)] :
Equations
- psigma.lex.preorder = {le := has_le.le psigma.lex.has_le, lt := has_lt.lt psigma.lex.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
@[protected, instance]
def
psigma.lex.partial_order
{ι : Type u_1}
{α : ι → Type u_2}
[partial_order ι]
[Π (i : ι), partial_order (α i)] :
partial_order (Σₗ' (i : ι), α i)
Dictionary / lexicographic partial_order for dependent pairs.
Equations
- psigma.lex.partial_order = {le := preorder.le psigma.lex.preorder, lt := preorder.lt psigma.lex.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
def
psigma.lex.linear_order
{ι : Type u_1}
{α : ι → Type u_2}
[linear_order ι]
[Π (i : ι), linear_order (α i)] :
linear_order (Σₗ' (i : ι), α i)
Dictionary / lexicographic linear_order for pairs.
Equations
- psigma.lex.linear_order = {le := partial_order.le psigma.lex.partial_order, lt := partial_order.lt psigma.lex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := psigma.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 := psigma.decidable_eq (λ (a : ι) (a_1 b : α a), eq.decidable a_1 b), decidable_lt := psigma.lex.decidable has_lt.lt (λ (i : ι), has_lt.lt) (λ (i : ι) (a b : (λ (i : ι), (λ (i : ι), (λ (i : ι), α i) i) i) i), has_lt.lt.decidable a b), max := max_default (λ (a b : Σₗ' (i : ι), α i), psigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) a b), max_def := _, min := min_default (λ (a b : Σₗ' (i : ι), α i), psigma.lex.decidable has_lt.lt (λ (i : ι), has_le.le) a b), min_def := _}
@[protected, instance]
def
psigma.lex.order_bot
{ι : Type u_1}
{α : ι → Type u_2}
[partial_order ι]
[order_bot ι]
[Π (i : ι), preorder (α i)]
[order_bot (α ⊥)] :
The lexicographical linear order on a sigma type.
@[protected, instance]
def
psigma.lex.order_top
{ι : Type u_1}
{α : ι → Type u_2}
[partial_order ι]
[order_top ι]
[Π (i : ι), preorder (α i)]
[order_top (α ⊤)] :
The lexicographical linear order on a sigma type.
@[protected, instance]
def
psigma.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
- psigma.lex.bounded_order = {top := order_top.top psigma.lex.order_top, le_top := _, bot := order_bot.bot psigma.lex.order_bot, bot_le := _}
@[protected, instance]
def
psigma.lex.densely_ordered
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[densely_ordered ι]
[∀ (i : ι), nonempty (α i)]
[Π (i : ι), preorder (α i)]
[∀ (i : ι), densely_ordered (α i)] :
densely_ordered (Σₗ' (i : ι), α i)
@[protected, instance]
def
psigma.lex.densely_ordered_of_no_max_order
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)]
[∀ (i : ι), densely_ordered (α i)]
[∀ (i : ι), no_max_order (α i)] :
densely_ordered (Σₗ' (i : ι), α i)
@[protected, instance]
def
psigma.lex.densely_ordered_of_no_min_order
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)]
[∀ (i : ι), densely_ordered (α i)]
[∀ (i : ι), no_min_order (α i)] :
densely_ordered (Σₗ' (i : ι), α i)
@[protected, instance]
def
psigma.lex.no_max_order_of_nonempty
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)]
[no_max_order ι]
[∀ (i : ι), nonempty (α i)] :
no_max_order (Σₗ' (i : ι), α i)
@[protected, instance]
def
psigma.lex.no_min_order_of_nonempty
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)]
[no_max_order ι]
[∀ (i : ι), nonempty (α i)] :
no_max_order (Σₗ' (i : ι), α i)
@[protected, instance]
def
psigma.lex.no_max_order
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)]
[∀ (i : ι), no_max_order (α i)] :
no_max_order (Σₗ' (i : ι), α i)
@[protected, instance]
def
psigma.lex.no_min_order
{ι : Type u_1}
{α : ι → Type u_2}
[preorder ι]
[Π (i : ι), preorder (α i)]
[∀ (i : ι), no_min_order (α i)] :
no_min_order (Σₗ' (i : ι), α i)