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

• length : ℕ

  The number of inequalities in the series

• toFun : Fin (s.length + 1) → α

  The underlying function of a relation series

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

  Adjacent elements are related

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

instance RelSeries.instCoeFunRelSeriesForAllFinHAddNatInstHAddInstAddNatLengthOfNat {α : Type u_1} (r : Rel α α) : CoeFun (RelSeries r) fun x => Fin (x.length + 1) → α

@[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.toFun (RelSeries.singleton r a) x = a

def RelSeries.singleton {α : Type u_1} (r : Rel α α) (a : α) : RelSeries r

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

instance RelSeries.instIsEmptyRelSeries {α : Type u_1} (r : Rel α α) [IsEmpty α] : IsEmpty (RelSeries r)

instance RelSeries.instInhabitedRelSeries {α : Type u_1} (r : Rel α α) [Inhabited α] : Inhabited (RelSeries r)

instance RelSeries.instNonemptyRelSeries {α : Type u_1} (r : Rel α α) [Nonempty α] : Nonempty (RelSeries r)

theorem RelSeries.ext {α : Type u_1} {r : Rel α α} {x : RelSeries r} {y : RelSeries r} (length_eq : x.length = y.length) (toFun_eq : x.toFun = y.toFun ∘ Fin.cast (_ : x.length + 1 = y.length + 1)) : x = y

theorem RelSeries.rel_of_lt {α : Type u_1} {r : Rel α α} [IsTrans α r] (x : RelSeries r) {i : Fin (x.length + 1)} {j : Fin (x.length + 1)} (h : i < j) : r (RelSeries.toFun x i) (RelSeries.toFun x j)

theorem RelSeries.rel_or_eq_of_le {α : Type u_1} {r : Rel α α} [IsTrans α r] (x : RelSeries r) {i : Fin (x.length + 1)} {j : Fin (x.length + 1)} (h : i ≤ j) : r (RelSeries.toFun x i) (RelSeries.toFun x j) ∨ RelSeries.toFun x i = RelSeries.toFun x j

@[simp]

theorem RelSeries.ofLE_length {α : Type u_1} {r : Rel α α} (x : RelSeries r) {s : Rel α α} (h : r ≤ s) : (RelSeries.ofLE x 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)), RelSeries.toFun (RelSeries.ofLE x h) a = RelSeries.toFun x a

def RelSeries.ofLE {α : Type u_1} {r : Rel α α} (x : RelSeries r) {s : Rel α α} (h : r ≤ s) : RelSeries s

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

theorem RelSeries.coe_ofLE {α : Type u_1} {r : Rel α α} (x : RelSeries r) {s : Rel α α} (h : r ≤ s) : (RelSeries.ofLE x h).toFun = x.toFun

@[inline, reducible]

abbrev RelSeries.toList {α : Type u_1} {r : Rel α α} (x : RelSeries r) : List α

Every relation series gives a list

theorem RelSeries.toList_chain' {α : Type u_1} {r : Rel α α} (x : RelSeries r) : List.Chain' r (RelSeries.toList x)

theorem RelSeries.toList_ne_empty {α : Type u_1} {r : Rel α α} (x : RelSeries r) : RelSeries.toList x ≠ []

@[simp]

theorem RelSeries.fromListChain'_toFun {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_empty : x ≠ []) (hx : List.Chain' r x) : ∀ (a : Fin (Nat.pred (List.length x) + 1)), RelSeries.toFun (RelSeries.fromListChain' x x_ne_empty hx) a = (List.get x ∘ Fin.cast (_ : Nat.succ (Nat.pred (List.length x)) = List.length x)) a

@[simp]

theorem RelSeries.fromListChain'_length {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_empty : x ≠ []) (hx : List.Chain' r x) : (RelSeries.fromListChain' x x_ne_empty hx).length = Nat.pred (List.length x)

def RelSeries.fromListChain' {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_empty : x ≠ []) (hx : List.Chain' r x) : RelSeries r

Every nonempty list satisfying the chain condition gives a relation series

def RelSeries.Equiv {α : Type u_1} {r : Rel α α} : RelSeries r ≃ ↑{x | x ≠ [] ∧ List.Chain' r x}

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

class Rel.FiniteDimensional {α : Type u_1} (r : Rel α α) : Prop

• exists_longest_relSeries : ∃ x, ∀ (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.

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

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

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

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

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

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

The longest relational series when a relation is finite dimensional

theorem RelSeries.length_le_length_longestOf {α : Type u_1} (r : Rel α α) [Rel.FiniteDimensional r] (x : RelSeries r) : x.length ≤ (RelSeries.longestOf r).length

noncomputable def RelSeries.withLength {α : Type u_1} (r : Rel α α) [Rel.InfiniteDimensional r] (n : ℕ) : RelSeries r

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

@[simp]

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

theorem RelSeries.nonempty_of_infiniteDimensional {α : Type u_1} (r : Rel α α) [Rel.InfiniteDimensional r] : Nonempty α

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

@[inline, reducible]

abbrev FiniteDimensionalOrder (γ : Type u_1) [Preorder γ] : Prop

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

@[inline, reducible]

abbrev InfiniteDimensionalOrder (γ : Type u_1) [Preorder γ] : Prop

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

@[inline, reducible]

abbrev LTSeries (α : Type u_1) [Preorder α] : Type u_1

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

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

The longest <-series when a type is finite dimensional

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

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

@[simp]

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

theorem LTSeries.nonempty_of_infiniteDimensionalType (α : Type u_1) [Preorder α] [InfiniteDimensionalOrder α] : Nonempty α

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