Orders on a sigma type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines two orders on a sigma type:

The disjoint sum of orders. a is less b iff a and b are in the same summand and a is less than b there.
The lexicographical order. 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.

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.

TODO #

Upgrade equiv.sigma_congr_left, equiv.sigma_congr, equiv.sigma_assoc, equiv.sigma_prod_of_equiv, equiv.sigma_equiv_prod, ... to order isomorphisms.

Disjoint sum of orders on `sigma` #

source

inductive sigma.le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_le (α i)] (a b : Σ (i : ι), α i) :

Prop

fiber : ∀ {ι : Type u_1} {α : ι → Type u_2} [_inst_1 : Π (i : ι), has_le (α i)] (i : ι) (a b : α i), a ≤ b → ⟨i, a⟩.le ⟨i, b⟩

Disjoint sum of orders. ⟨i, a⟩ ≤ ⟨j, b⟩ iff i = j and a ≤ b.

source

inductive sigma.lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_lt (α i)] (a b : Σ (i : ι), α i) :

Prop

fiber : ∀ {ι : Type u_1} {α : ι → Type u_2} [_inst_1 : Π (i : ι), has_lt (α i)] (i : ι) (a b : α i), a < b → ⟨i, a⟩.lt ⟨i, b⟩

Disjoint sum of orders. ⟨i, a⟩ < ⟨j, b⟩ iff i = j and a < b.

source

@[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)}

source

@[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)}

source

@[simp]

theorem sigma.mk_le_mk_iff {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_le (α i)] {i : ι} {a b : α i} :

⟨i, a⟩ ≤ ⟨i, b⟩ ↔ a ≤ b

source

@[simp]

theorem sigma.mk_lt_mk_iff {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_lt (α i)] {i : ι} {a b : α i} :

⟨i, a⟩ < ⟨i, b⟩ ↔ a < b

source

theorem sigma.le_def {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_le (α i)] {a b : Σ (i : ι), α i} :

a ≤ b ↔ ∃ (h : a.fst = b.fst), eq.rec a.snd h ≤ b.snd

source

theorem sigma.lt_def {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_lt (α i)] {a b : Σ (i : ι), α i} :

a < b ↔ ∃ (h : a.fst = b.fst), eq.rec a.snd h < b.snd

source

@[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 := _}

source

@[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 := _}

source

@[protected, instance]

def sigma.densely_ordered {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), preorder (α i)] [∀ (i : ι), densely_ordered (α i)] :

densely_ordered (Σ (i : ι), α i)

Lexicographical order on `sigma` #

source

@[protected, instance]

def sigma.lex.has_le {ι : Type u_1} {α : ι → Type u_2} [has_lt ι] [Π (i : ι), has_le (α i)] :

has_le (Σₗ (i : ι), α i)

The lexicographical ≤ on a sigma type.

Equations

sigma.lex.has_le = {le := sigma.lex has_lt.lt (λ (i : ι), has_le.le)}

source

@[protected, instance]

def sigma.lex.has_lt {ι : Type u_1} {α : ι → Type u_2} [has_lt ι] [Π (i : ι), has_lt (α i)] :

has_lt (Σₗ (i : ι), α i)

The lexicographical < on a sigma type.

Equations

sigma.lex.has_lt = {lt := sigma.lex has_lt.lt (λ (i : ι), has_lt.lt)}

source

theorem sigma.lex.le_def {ι : Type u_1} {α : ι → Type u_2} [has_lt ι] [Π (i : ι), has_le (α i)] {a b : Σₗ (i : ι), α i} :

a ≤ b ↔ a.fst < b.fst ∨ ∃ (h : a.fst = b.fst), eq.rec a.snd h ≤ b.snd

source

theorem sigma.lex.lt_def {ι : Type u_1} {α : ι → Type u_2} [has_lt ι] [Π (i : ι), has_lt (α i)] {a b : Σₗ (i : ι), α i} :

a < b ↔ a.fst < b.fst ∨ ∃ (h : a.fst = b.fst), eq.rec a.snd h < b.snd

source

@[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 := _}

source

@[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 := _}

source

@[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 := _}

source

@[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.

Equations

sigma.lex.order_bot = {bot := ⟨⊥, ⊥⟩, bot_le := _}

source

@[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.

Equations

sigma.lex.order_top = {top := ⟨⊤, ⊤⟩, le_top := _}

source

@[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 := _}

source

@[protected, instance]

def sigma.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)

source

@[protected, instance]