mathlib3 documentation

data.dfinsupp.lex

Lexicographic order on finitely supported dependent functions #

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

This file defines the lexicographic order on dfinsupp.

@[protected]

def dfinsupp.lex {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] (r : ι → ι → Prop) (s : Π (i : ι), α i → α i → Prop) (x y : Π₀ (i : ι), α i) :

Prop

dfinsupp.lex r s is the lexicographic relation on Π₀ i, α i, where ι is ordered by r, and α i is ordered by s i. The type synonym lex (Π₀ i, α i) has an order given by dfinsupp.lex (<) (λ i, (<)).

Equations

dfinsupp.lex r s x y = pi.lex r s ⇑x ⇑y

theorem pi.lex_eq_dfinsupp_lex {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} (a b : Π₀ (i : ι), α i) :

pi.lex r s ⇑a ⇑b = dfinsupp.lex r s a b

theorem dfinsupp.lex_def {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} {a b : Π₀ (i : ι), α i} :

dfinsupp.lex r s a b ↔ ∃ (j : ι), (∀ (d : ι), r d j → ⇑a d = ⇑b d) ∧ s j (⇑a j) (⇑b j)

@[protected, instance]

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

has_lt (lex (Π₀ (i : ι), α i))

Equations

dfinsupp.lex.has_lt = {lt := λ (f g : lex (Π₀ (i : ι), α i)), dfinsupp.lex has_lt.lt (λ (i : ι), has_lt.lt) (⇑of_lex f) (⇑of_lex g)}

theorem dfinsupp.lex_lt_of_lt_of_preorder {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), preorder (α i)] (r : ι → ι → Prop) [is_strict_order ι r] {x y : Π₀ (i : ι), α i} (hlt : x < y) :

∃ (i : ι), (∀ (j : ι), r j i → ⇑x j ≤ ⇑y j ∧ ⇑y j ≤ ⇑x j) ∧ ⇑x i < ⇑y i

theorem dfinsupp.lex_lt_of_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), partial_order (α i)] (r : ι → ι → Prop) [is_strict_order ι r] {x y : Π₀ (i : ι), α i} (hlt : x < y) :

pi.lex r (λ (i : ι), has_lt.lt) ⇑x ⇑y

@[protected, instance]

def dfinsupp.lex.is_strict_order {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] :

is_strict_order (lex (Π₀ (i : ι), α i)) has_lt.lt

@[protected, instance]

def dfinsupp.lex.partial_order {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] :

partial_order (lex (Π₀ (i : ι), α i))

The partial order on dfinsupps obtained by the lexicographic ordering. See dfinsupp.lex.linear_order for a proof that this partial order is in fact linear.

Equations

dfinsupp.lex.partial_order = partial_order.lift (λ (x : lex (Π₀ (i : ι), α i)), ⇑to_lex ⇑(⇑of_lex x)) dfinsupp.lex.partial_order._proof_1

@[protected, instance, irreducible]

def dfinsupp.lex.decidable_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), linear_order (α i)] :

decidable_rel has_le.le

Equations

dfinsupp.lex.decidable_le = lt_trichotomy_rec (λ (f g : Π₀ (i : ι), α i) (h : ⇑to_lex f < ⇑to_lex g), decidable.is_true _) (λ (f g : Π₀ (i : ι), α i) (h : ⇑to_lex f = ⇑to_lex g), decidable.is_true _) (λ (f g : Π₀ (i : ι), α i) (h : ⇑to_lex g < ⇑to_lex f), decidable.is_false _)

@[protected, instance, irreducible]

def dfinsupp.lex.decidable_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), linear_order (α i)] :

decidable_rel has_lt.lt

Equations

dfinsupp.lex.decidable_lt = lt_trichotomy_rec (λ (f g : Π₀ (i : ι), α i) (h : ⇑to_lex f < ⇑to_lex g), decidable.is_true h) (λ (f g : Π₀ (i : ι), α i) (h : ⇑to_lex f = ⇑to_lex g), decidable.is_false _) (λ (f g : Π₀ (i : ι), α i) (h : ⇑to_lex g < ⇑to_lex f), decidable.is_false _)

@[protected, instance]

def dfinsupp.lex.linear_order {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), linear_order (α i)] :

linear_order (lex (Π₀ (i : ι), α i))

The linear order on dfinsupps obtained by the lexicographic ordering.

Equations

dfinsupp.lex.linear_order = {le := partial_order.le dfinsupp.lex.partial_order, lt := partial_order.lt dfinsupp.lex.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : lex (Π₀ (i : ι), α i)), dfinsupp.lex.decidable_le a b, decidable_eq := λ (a b : lex (Π₀ (i : ι), α i)), dfinsupp.decidable_eq a b, decidable_lt := λ (a b : lex (Π₀ (i : ι), α i)), dfinsupp.lex.decidable_lt a b, max := max_default (λ (a b : lex (Π₀ (i : ι), α i)), dfinsupp.lex.decidable_le a b), max_def := _, min := min_default (λ (a b : lex (Π₀ (i : ι), α i)), dfinsupp.lex.decidable_le a b), min_def := _}

theorem dfinsupp.to_lex_monotone {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] :

monotone ⇑to_lex

theorem dfinsupp.lt_of_forall_lt_of_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_zero (α i)] [linear_order ι] [Π (i : ι), partial_order (α i)] (a b : lex (Π₀ (i : ι), α i)) (i : ι) :

(∀ (j : ι), j < i → ⇑(⇑of_lex a) j = ⇑(⇑of_lex b) j) → ⇑(⇑of_lex a) i < ⇑(⇑of_lex b) i → a < b

We are about to sneak in a hypothesis that might appear to be too strong. We assume covariant_class with strict inequality < also when proving the one with the weak inequality ≤. This is actually necessary: addition on lex (Π₀ i, α i) may fail to be monotone, when it is "just" monotone on α i.

@[protected, instance]

def dfinsupp.lex.covariant_class_lt_left {ι : Type u_1} {α : ι → Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [∀ (i : ι), covariant_class (α i) (α i) has_add.add has_lt.lt] :

covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) has_add.add has_lt.lt

@[protected, instance]

def dfinsupp.lex.covariant_class_le_left {ι : Type u_1} {α : ι → Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [∀ (i : ι), covariant_class (α i) (α i) has_add.add has_lt.lt] :

covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) has_add.add has_le.le

@[protected, instance]

def dfinsupp.lex.covariant_class_lt_right {ι : Type u_1} {α : ι → Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [∀ (i : ι), covariant_class (α i) (α i) (function.swap has_add.add) has_lt.lt] :

covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) (function.swap has_add.add) has_lt.lt

@[protected, instance]

def dfinsupp.lex.covariant_class_le_right {ι : Type u_1} {α : ι → Type u_2} [linear_order ι] [Π (i : ι), add_monoid (α i)] [Π (i : ι), linear_order (α i)] [∀ (i : ι), covariant_class (α i) (α i) (function.swap has_add.add) has_lt.lt] :

covariant_class (lex (Π₀ (i : ι), α i)) (lex (Π₀ (i : ι), α i)) (function.swap has_add.add) has_le.le