Documentation

Mathlib.Order.RelSeries

Series of a relation #

If r is a relation on α then a relation series of length n is a series a_0, a_1, ..., a_n such that r a_i a_{i+1} for all i < n

structure RelSeries {α : Type u_1} (r : Rel α α) :
Type u_1

Let r be a relation on α, a relation series of r of length n is a series a_0, a_1, ..., a_n such that r a_i a_{i+1} for all i < n

  • length :

    The number of inequalities in the series

  • toFun : Fin (self.length + 1)α

    The underlying function of a relation series

  • step : ∀ (i : Fin self.length), r (self.toFun i.castSucc) (self.toFun i.succ)

    Adjacent elements are related

Instances For
instance RelSeries.instCoeFunForallFinHAddNatLengthOfNat {α : Type u_1} (r : Rel α α) :
CoeFun (RelSeries r) fun (x : RelSeries r) => Fin (x.length + 1)α
Equations
def RelSeries.singleton {α : Type u_1} (r : Rel α α) (a : α) :

For any type α, each term of α gives a relation series with the right most index to be 0.

Equations
@[simp]
theorem RelSeries.singleton_length {α : Type u_1} (r : Rel α α) (a : α) :
(RelSeries.singleton r a).length = 0
@[simp]
theorem RelSeries.singleton_toFun {α : Type u_1} (r : Rel α α) (a : α) (x✝ : Fin (0 + 1)) :
(RelSeries.singleton r a).toFun x✝ = a
instance RelSeries.instIsEmpty {α : Type u_1} (r : Rel α α) [IsEmpty α] :
Equations
  • =
instance RelSeries.instInhabited {α : Type u_1} (r : Rel α α) [Inhabited α] :
Equations
instance RelSeries.instNonempty {α : Type u_1} (r : Rel α α) [Nonempty α] :
Equations
  • =
theorem RelSeries.ext {α : Type u_1} {r : Rel α α} {x y : RelSeries r} (length_eq : x.length = y.length) (toFun_eq : x.toFun = y.toFun Fin.cast ) :
x = y
theorem RelSeries.rel_of_lt {α : Type u_1} {r : Rel α α} [IsTrans α r] (x : RelSeries r) {i j : Fin (x.length + 1)} (h : i < j) :
r (x.toFun i) (x.toFun j)
theorem RelSeries.rel_or_eq_of_le {α : Type u_1} {r : Rel α α} [IsTrans α r] (x : RelSeries r) {i j : Fin (x.length + 1)} (h : i j) :
r (x.toFun i) (x.toFun j) x.toFun i = x.toFun j
def RelSeries.ofLE {α : Type u_1} {r : Rel α α} (x : RelSeries r) {s : Rel α α} (h : r s) :

Given two relations r, s on α such that r ≤ s, any relation series of r induces a relation series of s

Equations
  • x.ofLE h = { length := x.length, toFun := x.toFun, step := }
@[simp]
theorem RelSeries.ofLE_length {α : Type u_1} {r : Rel α α} (x : RelSeries r) {s : Rel α α} (h : r s) :
(x.ofLE h).length = x.length
@[simp]
theorem RelSeries.ofLE_toFun {α : Type u_1} {r : Rel α α} (x : RelSeries r) {s : Rel α α} (h : r s) (a✝ : Fin (x.length + 1)) :
(x.ofLE h).toFun a✝ = x.toFun a✝
theorem RelSeries.coe_ofLE {α : Type u_1} {r : Rel α α} (x : RelSeries r) {s : Rel α α} (h : r s) :
(x.ofLE h).toFun = x.toFun
def RelSeries.toList {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
List α

Every relation series gives a list

Equations
@[simp]
theorem RelSeries.length_toList {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
x.toList.length = x.length + 1
theorem RelSeries.toList_chain' {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
List.Chain' r x.toList
theorem RelSeries.toList_ne_nil {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
x.toList []
def RelSeries.fromListChain' {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_nil : x []) (hx : List.Chain' r x) :

Every nonempty list satisfying the chain condition gives a relation series

Equations
@[simp]
theorem RelSeries.fromListChain'_length {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_nil : x []) (hx : List.Chain' r x) :
(RelSeries.fromListChain' x x_ne_nil hx).length = x.length - 1
@[simp]
theorem RelSeries.fromListChain'_toFun {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_nil : x []) (hx : List.Chain' r x) (i : Fin (x.length - 1 + 1)) :
(RelSeries.fromListChain' x x_ne_nil hx).toFun i = x[Fin.cast i]
def RelSeries.Equiv {α : Type u_1} {r : Rel α α} :
RelSeries r {x : List α | x [] List.Chain' r x}

Relation series of r and nonempty list of α satisfying r-chain condition bijectively corresponds to each other.

Equations
  • One or more equations did not get rendered due to their size.
theorem RelSeries.toList_injective {α : Type u_1} {r : Rel α α} :
Function.Injective RelSeries.toList
class Rel.FiniteDimensional {α : Type u_1} (r : Rel α α) :

A relation r is said to be finite dimensional iff there is a relation series of r with the maximum length.

  • exists_longest_relSeries : ∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length x.length

    A relation r is said to be finite dimensional iff there is a relation series of r with the maximum length.

Instances
class Rel.InfiniteDimensional {α : Type u_1} (r : Rel α α) :

A relation r is said to be infinite dimensional iff there exists relation series of arbitrary length.

  • exists_relSeries_with_length : ∀ (n : ), ∃ (x : RelSeries r), x.length = n

    A relation r is said to be infinite dimensional iff there exists relation series of arbitrary length.

Instances
    noncomputable def RelSeries.longestOf {α : Type u_1} (r : Rel α α) [r.FiniteDimensional] :

    The longest relational series when a relation is finite dimensional

    Equations
    theorem RelSeries.length_le_length_longestOf {α : Type u_1} (r : Rel α α) [r.FiniteDimensional] (x : RelSeries r) :
    x.length (RelSeries.longestOf r).length
    noncomputable def RelSeries.withLength {α : Type u_1} (r : Rel α α) [r.InfiniteDimensional] (n : ) :

    A relation series with length n if the relation is infinite dimensional

    Equations
    @[simp]
    theorem RelSeries.length_withLength {α : Type u_1} (r : Rel α α) [r.InfiniteDimensional] (n : ) :
    (RelSeries.withLength r n).length = n
    theorem RelSeries.nonempty_of_infiniteDimensional {α : Type u_1} {r : Rel α α} [r.InfiniteDimensional] :

    If a relation on α is infinite dimensional, then α is nonempty.

    instance RelSeries.membership {α : Type u_1} {r : Rel α α} :
    Equations
    theorem RelSeries.mem_def {α : Type u_1} {r : Rel α α} {s : RelSeries r} {x : α} :
    x s x Set.range s.toFun
    @[simp]
    theorem RelSeries.mem_toList {α : Type u_1} {r : Rel α α} {s : RelSeries r} {x : α} :
    x s.toList x s
    theorem RelSeries.subsingleton_of_length_eq_zero {α : Type u_1} {r : Rel α α} {s : RelSeries r} (hs : s.length = 0) :
    {x : α | x s}.Subsingleton
    theorem RelSeries.length_ne_zero_of_nontrivial {α : Type u_1} {r : Rel α α} {s : RelSeries r} (h : {x : α | x s}.Nontrivial) :
    s.length 0
    theorem RelSeries.length_pos_of_nontrivial {α : Type u_1} {r : Rel α α} {s : RelSeries r} (h : {x : α | x s}.Nontrivial) :
    0 < s.length
    theorem RelSeries.length_ne_zero {α : Type u_1} {r : Rel α α} {s : RelSeries r} (irrefl : Irreflexive r) :
    s.length 0 {x : α | x s}.Nontrivial
    theorem RelSeries.length_pos {α : Type u_1} {r : Rel α α} {s : RelSeries r} (irrefl : Irreflexive r) :
    0 < s.length {x : α | x s}.Nontrivial
    theorem RelSeries.length_eq_zero {α : Type u_1} {r : Rel α α} {s : RelSeries r} (irrefl : Irreflexive r) :
    s.length = 0 {x : α | x s}.Subsingleton
    def RelSeries.head {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
    α

    Start of a series, i.e. for a₀ -r→ a₁ -r→ ... -r→ aₙ, its head is a₀.

    Since a relation series is assumed to be non-empty, this is well defined.

    Equations
    • x.head = x.toFun 0
    def RelSeries.last {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
    α

    End of a series, i.e. for a₀ -r→ a₁ -r→ ... -r→ aₙ, its last element is aₙ.

    Since a relation series is assumed to be non-empty, this is well defined.

    Equations
    theorem RelSeries.apply_last {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
    x.toFun (Fin.last x.length) = x.last
    theorem RelSeries.head_mem {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
    x.head x
    theorem RelSeries.last_mem {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
    x.last x
    @[simp]
    theorem RelSeries.head_singleton {α : Type u_1} {r : Rel α α} (x : α) :
    (RelSeries.singleton r x).head = x
    @[simp]
    theorem RelSeries.last_singleton {α : Type u_1} {r : Rel α α} (x : α) :
    (RelSeries.singleton r x).last = x
    def RelSeries.append {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : r p.last q.head) :

    If a₀ -r→ a₁ -r→ ... -r→ aₙ and b₀ -r→ b₁ -r→ ... -r→ bₘ are two strict series such that r aₙ b₀, then there is a chain of length n + m + 1 given by a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ b₀ -r→ b₁ -r→ ... -r→ bₘ.

    Equations
    • p.append q connect = { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun Fin.cast , step := }
    @[simp]
    theorem RelSeries.append_length {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : r p.last q.head) :
    (p.append q connect).length = p.length + q.length + 1
    theorem RelSeries.append_apply_left {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : r p.last q.head) (i : Fin (p.length + 1)) :
    (p.append q connect).toFun (Fin.cast (Fin.castAdd (q.length + 1) i)) = p.toFun i
    theorem RelSeries.append_apply_right {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : r p.last q.head) (i : Fin (q.length + 1)) :
    (p.append q connect).toFun ((Fin.natAdd p.length i) + 1) = q.toFun i
    @[simp]
    theorem RelSeries.head_append {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : r p.last q.head) :
    (p.append q connect).head = p.head
    @[simp]
    theorem RelSeries.last_append {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : r p.last q.head) :
    (p.append q connect).last = q.last
    def RelSeries.map {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : r →r s) :

    For two types α, β and relation on them r, s, if f : α → β preserves relation r, then an r-series can be pushed out to an s-series by a₀ -r→ a₁ -r→ ... -r→ aₙ ↦ f a₀ -s→ f a₁ -s→ ... -s→ f aₙ

    Equations
    • p.map f = { length := p.length, toFun := f.toFun p.toFun, step := }
    @[simp]
    theorem RelSeries.map_length {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : r →r s) :
    (p.map f).length = p.length
    @[simp]
    theorem RelSeries.map_apply {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : r →r s) (i : Fin (p.length + 1)) :
    (p.map f).toFun i = f (p.toFun i)
    @[simp]
    theorem RelSeries.head_map {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : r →r s) :
    (p.map f).head = f p.head
    @[simp]
    theorem RelSeries.last_map {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : r →r s) :
    (p.map f).last = f p.last
    def RelSeries.insertNth {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : r (p.toFun i.castSucc) a) (connect_next : r a (p.toFun i.succ)) :

    If a₀ -r→ a₁ -r→ ... -r→ aₙ is an r-series and a is such that aᵢ -r→ a -r→ a_ᵢ₊₁, then a₀ -r→ a₁ -r→ ... -r→ aᵢ -r→ a -r→ aᵢ₊₁ -r→ ... -r→ aₙ is another r-series

    Equations
    • p.insertNth i a prev_connect connect_next = { length := p.length + 1, toFun := i.succ.castSucc.insertNth a p.toFun, step := }
    @[simp]
    theorem RelSeries.insertNth_toFun {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : r (p.toFun i.castSucc) a) (connect_next : r a (p.toFun i.succ)) (j : Fin (p.length + 1 + 1)) :
    (p.insertNth i a prev_connect connect_next).toFun j = i.succ.castSucc.insertNth a p.toFun j
    @[simp]
    theorem RelSeries.insertNth_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : r (p.toFun i.castSucc) a) (connect_next : r a (p.toFun i.succ)) :
    (p.insertNth i a prev_connect connect_next).length = p.length + 1
    def RelSeries.reverse {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    RelSeries fun (a b : α) => r b a

    A relation series a₀ -r→ a₁ -r→ ... -r→ aₙ of r gives a relation series of the reverse of r by reversing the series aₙ ←r- aₙ₋₁ ←r- ... ←r- a₁ ←r- a₀.

    Equations
    • p.reverse = { length := p.length, toFun := p.toFun Fin.rev, step := }
    @[simp]
    theorem RelSeries.reverse_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    p.reverse.length = p.length
    @[simp]
    theorem RelSeries.reverse_apply {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :
    p.reverse.toFun i = p.toFun i.rev
    @[simp]
    theorem RelSeries.last_reverse {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    p.reverse.last = p.head
    @[simp]
    theorem RelSeries.head_reverse {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    p.reverse.head = p.last
    @[simp]
    theorem RelSeries.reverse_reverse {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    p.reverse.reverse = p
    def RelSeries.cons {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newHead : α) (rel : r newHead p.head) :

    Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ and an a such that a₀ -r→ a holds, there is a series of length n+1: a -r→ a₀ -r→ a₁ -r→ ... -r→ aₙ.

    Equations
    @[simp]
    theorem RelSeries.cons_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newHead : α) (rel : r newHead p.head) :
    (p.cons newHead rel).length = p.length + 1
    @[simp]
    theorem RelSeries.head_cons {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newHead : α) (rel : r newHead p.head) :
    (p.cons newHead rel).head = newHead
    @[simp]
    theorem RelSeries.last_cons {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newHead : α) (rel : r newHead p.head) :
    (p.cons newHead rel).last = p.last
    def RelSeries.snoc {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :

    Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ and an a such that aₙ -r→ a holds, there is a series of length n+1: a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a.

    Equations
    @[simp]
    theorem RelSeries.snoc_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
    (p.snoc newLast rel).length = p.length + 1
    @[simp]
    theorem RelSeries.head_snoc {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
    (p.snoc newLast rel).head = p.head
    @[simp]
    theorem RelSeries.last_snoc {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
    (p.snoc newLast rel).last = newLast
    @[simp]
    theorem RelSeries.last_snoc' {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
    (p.snoc newLast rel).toFun (Fin.last (p.length + 1)) = newLast
    @[simp]
    theorem RelSeries.snoc_castSucc {α : Type u_1} {r : Rel α α} (s : RelSeries r) (a : α) (connect : r s.last a) (i : Fin (s.length + 1)) :
    (s.snoc a connect).toFun i.castSucc = s.toFun i
    theorem RelSeries.mem_snoc {α : Type u_1} {r : Rel α α} {p : RelSeries r} {newLast : α} {rel : r p.last newLast} {x : α} :
    x p.snoc newLast rel x p x = newLast
    def RelSeries.tail {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length 0) :

    If a series a₀ -r→ a₁ -r→ ... has positive length, then a₁ -r→ ... is another series

    Equations
    @[simp]
    theorem RelSeries.tail_toFun {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length 0) (a✝ : Fin (p.length - 1 + 1)) :
    (p.tail len_pos).toFun a✝ = (Fin.tail p.toFun Fin.cast ) a✝
    @[simp]
    theorem RelSeries.tail_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length 0) :
    (p.tail len_pos).length = p.length - 1
    @[simp]
    theorem RelSeries.head_tail {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length 0) :
    (p.tail len_pos).head = p.toFun 1
    @[simp]
    theorem RelSeries.last_tail {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length 0) :
    (p.tail len_pos).last = p.last
    def RelSeries.eraseLast {α : Type u_1} {r : Rel α α} (p : RelSeries r) :

    If a series a₀ -r→ a₁ -r→ ... -r→ aₙ, then a₀ -r→ a₁ -r→ ... -r→ aₙ₋₁ is another series

    Equations
    • p.eraseLast = { length := p.length - 1, toFun := fun (i : Fin (p.length - 1 + 1)) => p.toFun i, , step := }
    @[simp]
    theorem RelSeries.eraseLast_toFun {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length - 1 + 1)) :
    p.eraseLast.toFun i = p.toFun i,
    @[simp]
    theorem RelSeries.eraseLast_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    p.eraseLast.length = p.length - 1
    @[simp]
    theorem RelSeries.head_eraseLast {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    p.eraseLast.head = p.head
    @[simp]
    theorem RelSeries.last_eraseLast {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
    p.eraseLast.last = p.toFun p.length.pred,
    theorem RelSeries.eraseLast_last_rel_last {α : Type u_1} {r : Rel α α} (p : RelSeries r) (h : p.length 0) :
    r p.eraseLast.last p.last

    In a non-trivial series p, the last element of p.eraseLast is related to p.last

    def RelSeries.smash {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : p.last = q.head) :

    Given two series of the form a₀ -r→ ... -r→ X and X -r→ b ---> ..., then a₀ -r→ ... -r→ X -r→ b ... is another series obtained by combining the given two.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem RelSeries.smash_toFun {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : p.last = q.head) (i : Fin (p.length + q.length + 1)) :
    (p.smash q connect).toFun i = if H : i < p.length then p.toFun i, else q.toFun i - p.length,
    @[simp]
    theorem RelSeries.smash_length {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (connect : p.last = q.head) :
    (p.smash q connect).length = p.length + q.length
    theorem RelSeries.smash_castAdd {α : Type u_1} {r : Rel α α} {p q : RelSeries r} (connect : p.last = q.head) (i : Fin p.length) :
    (p.smash q connect).toFun (Fin.castAdd q.length i).castSucc = p.toFun i.castSucc
    theorem RelSeries.smash_succ_castAdd {α : Type u_1} {r : Rel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin p.length) :
    (p.smash q h).toFun (Fin.castAdd q.length i).succ = p.toFun i.succ
    theorem RelSeries.smash_natAdd {α : Type u_1} {r : Rel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) :
    (p.smash q h).toFun (Fin.natAdd p.length i).castSucc = q.toFun i.castSucc
    theorem RelSeries.smash_succ_natAdd {α : Type u_1} {r : Rel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) :
    (p.smash q h).toFun (Fin.natAdd p.length i).succ = q.toFun i.succ
    @[simp]
    theorem RelSeries.head_smash {α : Type u_1} {r : Rel α α} {p q : RelSeries r} (h : p.last = q.head) :
    (p.smash q h).head = p.head
    @[simp]
    theorem RelSeries.last_smash {α : Type u_1} {r : Rel α α} {p q : RelSeries r} (h : p.last = q.head) :
    (p.smash q h).last = q.last
    def RelSeries.take {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :

    Given the series a₀ -r→ … -r→ aᵢ -r→ … -r→ aₙ, the series a₀ -r→ … -r→ aᵢ.

    Equations
    • p.take i = { length := i, toFun := fun (x : Fin (i + 1)) => match x with | j, h => p.toFun j, , step := }
    @[simp]
    theorem RelSeries.take_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.take i).length = i
    @[simp]
    theorem RelSeries.head_take {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.take i).head = p.head
    @[simp]
    theorem RelSeries.last_take {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.take i).last = p.toFun i
    def RelSeries.drop {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :

    Given the series a₀ -r→ … -r→ aᵢ -r→ … -r→ aₙ, the series aᵢ₊₁ -r→ … -r→ aᵢ.

    Equations
    • p.drop i = { length := p.length - i, toFun := fun (x : Fin (p.length - i + 1)) => match x with | j, h => p.toFun j + i, , step := }
    @[simp]
    theorem RelSeries.drop_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.drop i).length = p.length - i
    @[simp]
    theorem RelSeries.head_drop {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.drop i).head = p.toFun i
    @[simp]
    theorem RelSeries.last_drop {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) :
    (p.drop i).last = p.last
    @[reducible, inline]
    abbrev FiniteDimensionalOrder (γ : Type u_3) [Preorder γ] :

    A type is finite dimensional if its LTSeries has bounded length.

    Equations
    Equations
    • =
    @[reducible, inline]
    abbrev InfiniteDimensionalOrder (γ : Type u_3) [Preorder γ] :

    A type is infinite dimensional if it has LTSeries of at least arbitrary length

    Equations
    @[reducible, inline]
    abbrev LTSeries (α : Type u_1) [Preorder α] :
    Type u_1

    If α is a preorder, a LTSeries is a relation series of the less than relation.

    Equations
    Instances For
    noncomputable def LTSeries.longestOf (α : Type u_1) [Preorder α] [FiniteDimensionalOrder α] :

    The longest <-series when a type is finite dimensional

    Equations
    noncomputable def LTSeries.withLength (α : Type u_1) [Preorder α] [InfiniteDimensionalOrder α] (n : ) :

    A <-series with length n if the relation is infinite dimensional

    Equations
    @[simp]
    theorem LTSeries.length_withLength (α : Type u_1) [Preorder α] [InfiniteDimensionalOrder α] (n : ) :
    (LTSeries.withLength α n).length = n

    if α is infinite dimensional, then α is nonempty.

    theorem LTSeries.longestOf_is_longest {α : Type u_1} [Preorder α] [FiniteDimensionalOrder α] (x : LTSeries α) :
    x.length (LTSeries.longestOf α).length
    theorem LTSeries.longestOf_len_unique {α : Type u_1} [Preorder α] [FiniteDimensionalOrder α] (p : LTSeries α) (is_longest : ∀ (q : LTSeries α), q.length p.length) :
    p.length = (LTSeries.longestOf α).length
    theorem LTSeries.strictMono {α : Type u_1} [Preorder α] (x : LTSeries α) :
    StrictMono x.toFun
    theorem LTSeries.monotone {α : Type u_1} [Preorder α] (x : LTSeries α) :
    Monotone x.toFun
    def LTSeries.mk {α : Type u_1} [Preorder α] (length : ) (toFun : Fin (length + 1)α) (strictMono : StrictMono toFun) :

    An alternative constructor of LTSeries from a strictly monotone function.

    Equations
    • LTSeries.mk length toFun strictMono = { length := length, toFun := toFun, step := }
    @[simp]
    theorem LTSeries.mk_length {α : Type u_1} [Preorder α] (length : ) (toFun : Fin (length + 1)α) (strictMono : StrictMono toFun) :
    (LTSeries.mk length toFun strictMono).length = length
    @[simp]
    theorem LTSeries.mk_toFun {α : Type u_1} [Preorder α] (length : ) (toFun : Fin (length + 1)α) (strictMono : StrictMono toFun) (a✝ : Fin (length + 1)) :
    (LTSeries.mk length toFun strictMono).toFun a✝ = toFun a✝
    def LTSeries.injStrictMono {α : Type u_1} [Preorder α] (n : ) :
    { f : (l : Fin n) × (Fin (l + 1)α) // StrictMono f.snd } LTSeries α

    An injection from the type of strictly monotone functions with limited length to LTSeries.

    Equations
    def LTSeries.map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : αβ) (hf : StrictMono f) :

    For two preorders α, β, if f : α → β is strictly monotonic, then a strict chain of α can be pushed out to a strict chain of β by a₀ < a₁ < ... < aₙ ↦ f a₀ < f a₁ < ... < f aₙ

    Equations
    @[simp]
    theorem LTSeries.map_length {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : αβ) (hf : StrictMono f) :
    (p.map f hf).length = p.length
    @[simp]
    theorem LTSeries.map_toFun {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : αβ) (hf : StrictMono f) (a✝ : Fin (p.length + 1)) :
    (p.map f hf).toFun a✝ = f (p.toFun a✝)
    @[simp]
    theorem LTSeries.head_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : αβ) (hf : StrictMono f) :
    RelSeries.head (p.map f hf) = f (RelSeries.head p)
    @[simp]
    theorem LTSeries.last_map {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : αβ) (hf : StrictMono f) :
    RelSeries.last (p.map f hf) = f (RelSeries.last p)
    noncomputable def LTSeries.comap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : αβ) (comap : ∀ ⦃x y : α⦄, f x < f yx < y) (surjective : Function.Surjective f) :

    For two preorders α, β, if f : α → β is surjective and strictly comonotonic, then a strict series of β can be pulled back to a strict chain of α by b₀ < b₁ < ... < bₙ ↦ f⁻¹ b₀ < f⁻¹ b₁ < ... < f⁻¹ bₙ where f⁻¹ bᵢ is an arbitrary element in the preimage of f⁻¹ {bᵢ}.

    Equations
    • p.comap f comap surjective = LTSeries.mk p.length (fun (i : Fin (p.length + 1)) => .choose)
    @[simp]
    theorem LTSeries.comap_length {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : αβ) (comap : ∀ ⦃x y : α⦄, f x < f yx < y) (surjective : Function.Surjective f) :
    (p.comap f comap surjective).length = p.length
    @[simp]
    theorem LTSeries.comap_toFun {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : αβ) (comap : ∀ ⦃x y : α⦄, f x < f yx < y) (surjective : Function.Surjective f) (i : Fin (p.length + 1)) :
    (p.comap f comap surjective).toFun i = .choose

    The strict series 0 < … < n in .

    Equations
    @[simp]
    theorem LTSeries.length_range (n : ) :
    (LTSeries.range n).length = n
    @[simp]
    theorem LTSeries.range_apply (n : ) (i : Fin (n + 1)) :
    (LTSeries.range n).toFun i = i
    theorem LTSeries.apply_add_index_le_apply_add_index_nat (p : LTSeries ) (i j : Fin (p.length + 1)) (hij : i j) :
    p.toFun i + j p.toFun j + i

    In ℕ, two entries in an LTSeries differ by at least the difference of their indices. (Expressed in a way that avoids subtraction).

    theorem LTSeries.apply_add_index_le_apply_add_index_int (p : LTSeries ) (i j : Fin (p.length + 1)) (hij : i j) :
    p.toFun i + j p.toFun j + i

    In ℤ, two entries in an LTSeries differ by at least the difference of their indices. (Expressed in a way that avoids subtraction).

    In ℕ, the head and tail of an LTSeries differ at least by the length of the series

    In ℤ, the head and tail of an LTSeries differ at least by the length of the series

    theorem LTSeries.length_lt_card {α : Type u_1} [Preorder α] [Fintype α] (s : LTSeries α) :
    s.length < Fintype.card α
    instance LTSeries.instFintypeOfDecidableRelLt {α : Type u_1} [Preorder α] [Fintype α] [DecidableRel fun (x1 x2 : α) => x1 < x2] :
    Equations
    theorem infiniteDimensionalOrder_of_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : αβ) (hf : StrictMono f) [InfiniteDimensionalOrder α] :

    If f : α → β is a strictly monotonic function and α is an infinite dimensional type then so is β.