@[protected, instance]
def
lex.decidable_eq
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β] :
decidable_eq (lex α β)
Equations
@[protected, instance]
Equations
@[protected, instance]
Dictionary / lexicographic preorder for pairs.
Equations
- lex_preorder = {le := has_le.le lex_has_le, lt := has_lt.lt lex_has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
@[protected, instance]
def
lex_partial_order
{α : Type u}
{β : Type v}
[partial_order α]
[partial_order β] :
partial_order (lex α β)
Dictionary / lexicographic partial_order for pairs.
Equations
- lex_partial_order = {le := preorder.le lex_preorder, lt := preorder.lt lex_preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
def
lex_linear_order
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β] :
linear_order (lex α β)
Dictionary / lexicographic linear_order for pairs.
Equations
- lex_linear_order = {le := partial_order.le lex_partial_order, lt := partial_order.lt lex_partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := id (λ (a b : lex α β), prod.cases_on a (λ (a₁ : α) (b₁ : β), prod.cases_on b (λ (a₂ : α) (b₂ : β), (linear_order.decidable_le a₁ a₂).cases_on (λ (a_lt : ¬a₁ ≤ a₂), is_false _) (λ (a_le : a₁ ≤ a₂), dite (a₁ = a₂) (λ (h : a₁ = a₂), _.mpr ((linear_order.decidable_le b₁ b₂).cases_on (λ (b_lt : ¬b₁ ≤ b₂), is_false _) (λ (b_le : b₁ ≤ b₂), is_true _))) (λ (h : ¬a₁ = a₂), is_true _))))), decidable_eq := decidable_eq_of_decidable_le (id (λ (a b : lex α β), prod.cases_on a (λ (a₁ : α) (b₁ : β), prod.cases_on b (λ (a₂ : α) (b₂ : β), (linear_order.decidable_le a₁ a₂).cases_on (λ (a_lt : ¬a₁ ≤ a₂), is_false _) (λ (a_le : a₁ ≤ a₂), dite (a₁ = a₂) (λ (h : a₁ = a₂), _.mpr ((linear_order.decidable_le b₁ b₂).cases_on (λ (b_lt : ¬b₁ ≤ b₂), is_false _) (λ (b_le : b₁ ≤ b₂), is_true _))) (λ (h : ¬a₁ = a₂), is_true _)))))), decidable_lt := decidable_lt_of_decidable_le (id (λ (a b : lex α β), prod.cases_on a (λ (a₁ : α) (b₁ : β), prod.cases_on b (λ (a₂ : α) (b₂ : β), (linear_order.decidable_le a₁ a₂).cases_on (λ (a_lt : ¬a₁ ≤ a₂), is_false _) (λ (a_le : a₁ ≤ a₂), dite (a₁ = a₂) (λ (h : a₁ = a₂), _.mpr ((linear_order.decidable_le b₁ b₂).cases_on (λ (b_lt : ¬b₁ ≤ b₂), is_false _) (λ (b_le : b₁ ≤ b₂), is_true _))) (λ (h : ¬a₁ = a₂), is_true _))))))}
@[protected, instance]
def
dlex_has_le
{α : Type u}
{Z : α → Type v}
[preorder α]
[Π (a : α), preorder (Z a)] :
has_le (Σ' (a : α), Z a)
Dictionary / lexicographic ordering on dependent pairs.
The 'pointwise' partial order prod.has_le doesn't make
sense for dependent pairs, so it's safe to mark these as
instances here.
Equations
- dlex_has_le = {le := psigma.lex has_lt.lt (λ (a : α), has_le.le)}
@[protected, instance]
def
dlex_has_lt
{α : Type u}
{Z : α → Type v}
[preorder α]
[Π (a : α), preorder (Z a)] :
has_lt (Σ' (a : α), Z a)
Equations
- dlex_has_lt = {lt := psigma.lex has_lt.lt (λ (a : α), has_lt.lt)}
@[protected, instance]
def
dlex_preorder
{α : Type u}
{Z : α → Type v}
[preorder α]
[Π (a : α), preorder (Z a)] :
preorder (Σ' (a : α), Z a)
Dictionary / lexicographic preorder on dependent pairs.
Equations
- dlex_preorder = {le := has_le.le dlex_has_le, lt := has_lt.lt dlex_has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
@[protected, instance]
def
dlex_partial_order
{α : Type u}
{Z : α → Type v}
[partial_order α]
[Π (a : α), partial_order (Z a)] :
partial_order (Σ' (a : α), Z a)
Dictionary / lexicographic partial_order for dependent pairs.
Equations
- dlex_partial_order = {le := preorder.le dlex_preorder, lt := preorder.lt dlex_preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
@[protected, instance]
def
dlex_linear_order
{α : Type u}
{Z : α → Type v}
[linear_order α]
[Π (a : α), linear_order (Z a)] :
linear_order (Σ' (a : α), Z a)
Dictionary / lexicographic linear_order for pairs.
Equations
- dlex_linear_order = {le := partial_order.le dlex_partial_order, lt := partial_order.lt dlex_partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := id (λ (a b : Σ' (a : α), Z a), a.cases_on (λ (a₁ : α) (b₁ : Z a₁), b.cases_on (λ (a₂ : α) (b₂ : Z a₂), (linear_order.decidable_le a₁ a₂).cases_on (λ (a_lt : ¬a₁ ≤ a₂), is_false _) (λ (a_le : a₁ ≤ a₂), dite (a₁ = a₂) (λ (h : a₁ = a₂), eq.rec (λ (b₂ : Z a₁) (a_le : a₁ ≤ a₁), (linear_order.decidable_le b₁ b₂).cases_on (λ (b_lt : ¬b₁ ≤ b₂), is_false _) (λ (b_le : b₁ ≤ b₂), is_true _)) h b₂ a_le) (λ (h : ¬a₁ = a₂), is_true _))))), decidable_eq := decidable_eq_of_decidable_le (id (λ (a b : Σ' (a : α), Z a), a.cases_on (λ (a₁ : α) (b₁ : Z a₁), b.cases_on (λ (a₂ : α) (b₂ : Z a₂), (linear_order.decidable_le a₁ a₂).cases_on (λ (a_lt : ¬a₁ ≤ a₂), is_false _) (λ (a_le : a₁ ≤ a₂), dite (a₁ = a₂) (λ (h : a₁ = a₂), eq.rec (λ (b₂ : Z a₁) (a_le : a₁ ≤ a₁), (linear_order.decidable_le b₁ b₂).cases_on (λ (b_lt : ¬b₁ ≤ b₂), is_false _) (λ (b_le : b₁ ≤ b₂), is_true _)) h b₂ a_le) (λ (h : ¬a₁ = a₂), is_true _)))))), decidable_lt := decidable_lt_of_decidable_le (id (λ (a b : Σ' (a : α), Z a), a.cases_on (λ (a₁ : α) (b₁ : Z a₁), b.cases_on (λ (a₂ : α) (b₂ : Z a₂), (linear_order.decidable_le a₁ a₂).cases_on (λ (a_lt : ¬a₁ ≤ a₂), is_false _) (λ (a_le : a₁ ≤ a₂), dite (a₁ = a₂) (λ (h : a₁ = a₂), eq.rec (λ (b₂ : Z a₁) (a_le : a₁ ≤ a₁), (linear_order.decidable_le b₁ b₂).cases_on (λ (b_lt : ¬b₁ ≤ b₂), is_false _) (λ (b_le : b₁ ≤ b₂), is_true _)) h b₂ a_le) (λ (h : ¬a₁ = a₂), is_true _))))))}