Orders on a sigma type #
This file defines two orders on a sigma type:
- The disjoint sum of orders.
a
is lessb
iffa
andb
are in the same summand anda
is less thanb
there. - The lexicographical order.
a
is less thanb
if its summand is strictly less than the summand ofb
or they are in the same summand anda
is less thanb
there.
We make the disjoint sum of orders the default set of instances. The lexicographic order goes on a type synonym.
Notation #
_root_.Lex (Sigma α)
: 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 #
Upgrade Equiv.sigma_congr_left
, Equiv.sigma_congr
, Equiv.sigma_assoc
,
Equiv.sigma_prod_of_equiv
, Equiv.sigma_equiv_prod
, ... to order isomorphisms.
- fiber: ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LE (α i)] (i : ι) (a b : α i), a ≤ b → Sigma.le { fst := i, snd := a } { fst := i, snd := b }
Disjoint sum of orders. ⟨i, a⟩ ≤ ⟨j, b⟩
iff i = j
and a ≤ b
.
Instances For
- fiber: ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → LT (α i)] (i : ι) (a b : α i), a < b → Sigma.lt { fst := i, snd := a } { fst := i, snd := b }
Disjoint sum of orders. ⟨i, a⟩ < ⟨j, b⟩
iff i = j
and a < b
.
Instances For
The notation Σₗ i, α i
refers to a sigma type equipped with the lexicographic order.
Instances For
The lexicographical partial order on a sigma type.
The lexicographical linear order on a sigma type.
The lexicographical linear order on a sigma type.
The lexicographical linear order on a sigma type.
The lexicographical linear order on a sigma type.