# 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
• 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 () ()

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

Instances For
CoeFun () fun x => Fin (x.length + 1)α
@[simp]
theorem RelSeries.singleton_length {α : Type u_1} (r : Rel α α) (a : α) :
().length = 0
@[simp]
theorem RelSeries.singleton_toFun {α : Type u_1} (r : Rel α α) (a : α) :
∀ (x : Fin (0 + 1)), = a
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.

Instances For
instance RelSeries.instIsEmptyRelSeries {α : Type u_1} (r : Rel α α) [] :
instance RelSeries.instInhabitedRelSeries {α : Type u_1} (r : Rel α α) [] :
instance RelSeries.instNonemptyRelSeries {α : Type u_1} (r : Rel α α) [] :
theorem RelSeries.ext {α : Type u_1} {r : Rel α α} {x : } {y : } (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 : ) {i : Fin (x.length + 1)} {j : Fin (x.length + 1)} (h : i < j) :
r () ()
theorem RelSeries.rel_or_eq_of_le {α : Type u_1} {r : Rel α α} [IsTrans α r] (x : ) {i : Fin (x.length + 1)} {j : Fin (x.length + 1)} (h : i j) :
r () () =
@[simp]
theorem RelSeries.ofLE_length {α : Type u_1} {r : Rel α α} (x : ) {s : Rel α α} (h : r s) :
().length = x.length
@[simp]
theorem RelSeries.ofLE_toFun {α : Type u_1} {r : Rel α α} (x : ) {s : Rel α α} (h : r s) :
∀ (a : Fin (x.length + 1)), =
def RelSeries.ofLE {α : Type u_1} {r : Rel α α} (x : ) {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

Instances For
theorem RelSeries.coe_ofLE {α : Type u_1} {r : Rel α α} (x : ) {s : Rel α α} (h : r s) :
().toFun = x.toFun
@[inline, reducible]
abbrev RelSeries.toList {α : Type u_1} {r : Rel α α} (x : ) :
List α

Every relation series gives a list

Instances For
theorem RelSeries.toList_chain' {α : Type u_1} {r : Rel α α} (x : ) :
theorem RelSeries.toList_ne_empty {α : Type u_1} {r : Rel α α} (x : ) :
@[simp]
theorem RelSeries.fromListChain'_toFun {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_empty : x []) (hx : ) :
∀ (a : Fin ( + 1)), RelSeries.toFun (RelSeries.fromListChain' x x_ne_empty hx) a = (List.get x Fin.cast (_ : Nat.succ () = )) a
@[simp]
theorem RelSeries.fromListChain'_length {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_empty : x []) (hx : ) :
(RelSeries.fromListChain' x x_ne_empty hx).length =
def RelSeries.fromListChain' {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_empty : x []) (hx : ) :

Every nonempty list satisfying the chain condition gives a relation series

Instances For
def RelSeries.Equiv {α : Type u_1} {r : Rel α α} :
{x | x [] }

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

Instances For
class Rel.FiniteDimensional {α : Type u_1} (r : Rel α α) :
• exists_longest_relSeries : x, ∀ (y : ), 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.

Instances
class Rel.InfiniteDimensional {α : Type u_1} (r : Rel α α) :
• 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.

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

The longest relational series when a relation is finite dimensional

Instances For
theorem RelSeries.length_le_length_longestOf {α : Type u_1} (r : Rel α α) (x : ) :
x.length ().length
noncomputable def RelSeries.withLength {α : Type u_1} (r : Rel α α) (n : ) :

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

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

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

@[inline, reducible]
abbrev FiniteDimensionalOrder (γ : Type u_1) [] :

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

Instances For
@[inline, reducible]
abbrev InfiniteDimensionalOrder (γ : Type u_1) [] :

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

Instances For
@[inline, reducible]
abbrev LTSeries (α : Type u_1) [] :
Type u_1

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

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

The longest <-series when a type is finite dimensional

Instances For
noncomputable def LTSeries.withLength (α : Type u_1) [] (n : ) :

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

Instances For
@[simp]
theorem LTSeries.length_withLength (α : Type u_1) [] (n : ) :
().length = n

if α is infinite dimensional, then α is nonempty.

theorem LTSeries.longestOf_is_longest {α : Type u_1} [] (x : ) :
x.length ().length
theorem LTSeries.longestOf_len_unique {α : Type u_1} [] (p : ) (is_longest : ∀ (q : ), q.length p.length) :
p.length = ().length
theorem LTSeries.strictMono {α : Type u_1} [] (x : ) :
StrictMono x.toFun
theorem LTSeries.monotone {α : Type u_1} [] (x : ) :
Monotone x.toFun