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 : SetRel α α) : 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) : (self.toFun i.castSucc, self.toFun i.succ) ∈ r

  Adjacent elements are related

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

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

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

@[simp]

theorem RelSeries.singleton_length {α : Type u_1} (r : SetRel α α) (a : α) : (singleton r a).length = 0

@[simp]

theorem RelSeries.singleton_toFun {α : Type u_1} (r : SetRel α α) (a : α) (x✝ : Fin (0 + 1)) : (singleton r a).toFun x✝ = a

instance RelSeries.instIsEmpty {α : Type u_1} (r : SetRel α α) [IsEmpty α] : IsEmpty (RelSeries r)

instance RelSeries.instInhabited {α : Type u_1} (r : SetRel α α) [Inhabited α] : Inhabited (RelSeries r)

instance RelSeries.instNonempty {α : Type u_1} (r : SetRel α α) [Nonempty α] : Nonempty (RelSeries r)

theorem RelSeries.ext {α : Type u_1} {r : SetRel α α} {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 : SetRel α α} [r.IsTrans] (x : RelSeries r) {i j : Fin (x.length + 1)} (h : i < j) : (x.toFun i, x.toFun j) ∈ r

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

def RelSeries.ofLE {α : Type u_1} {r : SetRel α α} (x : RelSeries r) {s : SetRel α α} (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

@[simp]

theorem RelSeries.ofLE_toFun {α : Type u_1} {r : SetRel α α} (x : RelSeries r) {s : SetRel α α} (h : r ≤ s) (a✝ : Fin (x.length + 1)) : (x.ofLE h).toFun a✝ = x.toFun a✝

@[simp]

theorem RelSeries.ofLE_length {α : Type u_1} {r : SetRel α α} (x : RelSeries r) {s : SetRel α α} (h : r ≤ s) : (x.ofLE h).length = x.length

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

def RelSeries.toList {α : Type u_1} {r : SetRel α α} (x : RelSeries r) : List α

Every relation series gives a list

@[simp]

theorem RelSeries.length_toList {α : Type u_1} {r : SetRel α α} (x : RelSeries r) : x.toList.length = x.length + 1

@[simp]

theorem RelSeries.toList_singleton {α : Type u_1} {r : SetRel α α} (x : α) : (singleton r x).toList = [x]

theorem RelSeries.toList_chain' {α : Type u_1} {r : SetRel α α} (x : RelSeries r) : List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) x.toList

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

def RelSeries.fromListChain' {α : Type u_1} {r : SetRel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) x) : RelSeries r

Every nonempty list satisfying the chain condition gives a relation series

@[simp]

theorem RelSeries.fromListChain'_toFun {α : Type u_1} {r : SetRel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) x) (i : Fin (x.length - 1 + 1)) : (fromListChain' x x_ne_nil hx).toFun i = x[Fin.cast ⋯ i]

@[simp]

theorem RelSeries.fromListChain'_length {α : Type u_1} {r : SetRel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) x) : (fromListChain' x x_ne_nil hx).length = x.length - 1

def RelSeries.Equiv {α : Type u_1} {r : SetRel α α} : RelSeries r ≃ ↑{x : List α | x ≠ [] ∧ List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) x}

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

theorem RelSeries.toList_injective {α : Type u_1} {r : SetRel α α} : Function.Injective toList

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

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.

theorem SetRel.finiteDimensional_iff {α : Type u_1} (r : SetRel α α) : r.FiniteDimensional ↔ ∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length ≤ x.length

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

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.

theorem SetRel.infiniteDimensional_iff {α : Type u_1} (r : SetRel α α) : r.InfiniteDimensional ↔ ∀ (n : ℕ), ∃ (x : RelSeries r), x.length = n

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

The longest relational series when a relation is finite dimensional

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

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

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

@[simp]

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

theorem RelSeries.nonempty_of_infiniteDimensional {α : Type u_1} {r : SetRel α α} [r.InfiniteDimensional] : Nonempty α

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

theorem RelSeries.nonempty_of_finiteDimensional {α : Type u_1} {r : SetRel α α} [r.FiniteDimensional] : Nonempty α

instance RelSeries.membership {α : Type u_1} {r : SetRel α α} : Membership α (RelSeries r)

theorem RelSeries.mem_def {α : Type u_1} {r : SetRel α α} {s : RelSeries r} {x : α} : x ∈ s ↔ x ∈ Set.range s.toFun

@[simp]

theorem RelSeries.mem_toList {α : Type u_1} {r : SetRel α α} {s : RelSeries r} {x : α} : x ∈ s.toList ↔ x ∈ s

theorem RelSeries.subsingleton_of_length_eq_zero {α : Type u_1} {r : SetRel α α} {s : RelSeries r} (hs : s.length = 0) : {x : α | x ∈ s}.Subsingleton

theorem RelSeries.length_ne_zero_of_nontrivial {α : Type u_1} {r : SetRel α α} {s : RelSeries r} (h : {x : α | x ∈ s}.Nontrivial) : s.length ≠ 0

theorem RelSeries.length_pos_of_nontrivial {α : Type u_1} {r : SetRel α α} {s : RelSeries r} (h : {x : α | x ∈ s}.Nontrivial) : 0 < s.length

theorem RelSeries.length_ne_zero {α : Type u_1} {r : SetRel α α} {s : RelSeries r} [r.IsIrrefl] : s.length ≠ 0 ↔ {x : α | x ∈ s}.Nontrivial

theorem RelSeries.length_pos {α : Type u_1} {r : SetRel α α} {s : RelSeries r} [r.IsIrrefl] : 0 < s.length ↔ {x : α | x ∈ s}.Nontrivial

theorem RelSeries.length_eq_zero {α : Type u_1} {r : SetRel α α} {s : RelSeries r} [r.IsIrrefl] : s.length = 0 ↔ {x : α | x ∈ s}.Subsingleton

def RelSeries.head {α : Type u_1} {r : SetRel α α} (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.

def RelSeries.last {α : Type u_1} {r : SetRel α α} (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.

theorem RelSeries.apply_zero {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.toFun 0 = p.head

theorem RelSeries.apply_last {α : Type u_1} {r : SetRel α α} (x : RelSeries r) : x.toFun (Fin.last x.length) = x.last

theorem RelSeries.head_mem {α : Type u_1} {r : SetRel α α} (x : RelSeries r) : x.head ∈ x

theorem RelSeries.last_mem {α : Type u_1} {r : SetRel α α} (x : RelSeries r) : x.last ∈ x

@[simp]

theorem RelSeries.head_singleton {α : Type u_1} {r : SetRel α α} (x : α) : (singleton r x).head = x

@[simp]

theorem RelSeries.last_singleton {α : Type u_1} {r : SetRel α α} (x : α) : (singleton r x).last = x

@[simp]

theorem RelSeries.head_toList {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.toList.head ⋯ = p.head

@[simp]

theorem RelSeries.toList_getElem_eq_apply {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : p.toList[↑i] = p.toFun i

theorem RelSeries.toList_getElem_eq_apply_of_lt_length {α : Type u_1} {r : SetRel α α} {p : RelSeries r} {i : ℕ} (hi : i < p.length + 1) : p.toList[i] = p.toFun ⟨i, hi⟩

@[simp]

theorem RelSeries.toList_getElem_zero_eq_head {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.toList[0] = p.head

@[simp]

theorem RelSeries.toList_fromListChain' {α : Type u_1} {r : SetRel α α} (l : List α) (l_ne_nil : l ≠ []) (hl : List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) l) : (fromListChain' l l_ne_nil hl).toList = l

@[simp]

theorem RelSeries.head_fromListChain' {α : Type u_1} {r : SetRel α α} (l : List α) (l_ne_nil : l ≠ []) (hl : List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) l) : (fromListChain' l l_ne_nil hl).head = l.head l_ne_nil

@[simp]

theorem RelSeries.getLast_toList {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.toList.getLast ⋯ = p.last

def RelSeries.append {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) : RelSeries r

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ₘ.

@[simp]

theorem RelSeries.append_length {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) : (p.append q connect).length = p.length + q.length + 1

theorem RelSeries.append_apply_left {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) (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 : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) (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 : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) : (p.append q connect).head = p.head

@[simp]

theorem RelSeries.last_append {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) : (p.append q connect).last = q.last

theorem RelSeries.append_assoc {α : Type u_1} {r : SetRel α α} (p q w : RelSeries r) (hpq : (p.last, q.head) ∈ r) (hqw : (q.last, w.head) ∈ r) : (p.append q hpq).append w ⋯ = p.append (q.append w hqw) ⋯

@[simp]

theorem RelSeries.toList_append {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r) : (p.append q connect).toList = p.toList ++ q.toList

def RelSeries.map {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s) : RelSeries 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ₙ

@[simp]

theorem RelSeries.map_length {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s) : (p.map f).length = p.length

@[simp]

theorem RelSeries.map_apply {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s) (i : Fin (p.length + 1)) : (p.map f).toFun i = f (p.toFun i)

@[simp]

theorem RelSeries.head_map {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s) : (p.map f).head = f p.head

@[simp]

theorem RelSeries.last_map {α : Type u_1} {r : SetRel α α} {β : Type u_2} {s : SetRel β β} (p : RelSeries r) (f : r.Hom s) : (p.map f).last = f p.last

def RelSeries.insertNth {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : (p.toFun i.castSucc, a) ∈ r) (connect_next : (a, p.toFun i.succ) ∈ r) : RelSeries r

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

@[simp]

theorem RelSeries.insertNth_length {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : (p.toFun i.castSucc, a) ∈ r) (connect_next : (a, p.toFun i.succ) ∈ r) : (p.insertNth i a prev_connect connect_next).length = p.length + 1

@[simp]

theorem RelSeries.insertNth_toFun {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : (p.toFun i.castSucc, a) ∈ r) (connect_next : (a, p.toFun i.succ) ∈ r) (j : Fin (p.length + 1 + 1)) : (p.insertNth i a prev_connect connect_next).toFun j = i.succ.castSucc.insertNth a p.toFun j

def RelSeries.reverse {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : RelSeries r.inv

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₀.

@[simp]

theorem RelSeries.reverse_length {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.reverse.length = p.length

@[simp]

theorem RelSeries.reverse_apply {α : Type u_1} {r : SetRel α α} (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 : SetRel α α} (p : RelSeries r) : p.reverse.last = p.head

@[simp]

theorem RelSeries.head_reverse {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.reverse.head = p.last

@[simp]

theorem RelSeries.reverse_reverse {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.reverse.reverse = p

def RelSeries.cons {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r) : RelSeries r

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ₙ.

@[simp]

theorem RelSeries.cons_length {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r) : (p.cons newHead rel).length = p.length + 1

@[simp]

theorem RelSeries.head_cons {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r) : (p.cons newHead rel).head = newHead

@[simp]

theorem RelSeries.last_cons {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r) : (p.cons newHead rel).last = p.last

theorem RelSeries.cons_cast_succ {α : Type u_1} {r : SetRel α α} (s : RelSeries r) (a : α) (h : (a, s.head) ∈ r) (i : Fin (s.length + 1)) : (s.cons a h).toFun (Fin.cast ⋯ i.succ) = s.toFun i

@[simp]

theorem RelSeries.append_singleton_left {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (x : α) (hx : (x, p.head) ∈ r) : (singleton r x).append p hx = p.cons x hx

@[simp]

theorem RelSeries.toList_cons {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (x : α) (hx : (x, p.head) ∈ r) : (p.cons x hx).toList = x :: p.toList

theorem RelSeries.fromListChain'_cons {α : Type u_1} {r : SetRel α α} (l : List α) (l_ne_nil : l ≠ []) (hl : List.Chain' (fun (x1 x2 : α) => (x1, x2) ∈ r) l) (x : α) (hx : (x, l.head l_ne_nil) ∈ r) : fromListChain' (x :: l) ⋯ ⋯ = (fromListChain' l l_ne_nil hl).cons x ⋯

theorem RelSeries.append_cons {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} {x : α} (hx : (x, p.head) ∈ r) (hq : (p.last, q.head) ∈ r) : (p.cons x hx).append q ⋯ = (p.append q hq).cons x ⋯

def RelSeries.snoc {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r) : RelSeries r

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.

@[simp]

theorem RelSeries.snoc_length {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r) : (p.snoc newLast rel).length = p.length + 1

@[simp]

theorem RelSeries.head_snoc {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r) : (p.snoc newLast rel).head = p.head

@[simp]

theorem RelSeries.last_snoc {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r) : (p.snoc newLast rel).last = newLast

theorem RelSeries.snoc_cast_castSucc {α : Type u_1} {r : SetRel α α} (s : RelSeries r) (a : α) (h : (s.last, a) ∈ r) (i : Fin (s.length + 1)) : (s.snoc a h).toFun (Fin.cast ⋯ i.castSucc) = s.toFun i

@[simp]

theorem RelSeries.last_snoc' {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r) : (p.snoc newLast rel).toFun (Fin.last (p.length + 1)) = newLast

@[simp]

theorem RelSeries.snoc_castSucc {α : Type u_1} {r : SetRel α α} (s : RelSeries r) (a : α) (connect : (s.last, a) ∈ r) (i : Fin (s.length + 1)) : (s.snoc a connect).toFun i.castSucc = s.toFun i

theorem RelSeries.mem_snoc {α : Type u_1} {r : SetRel α α} {p : RelSeries r} {newLast : α} {rel : (p.last, newLast) ∈ r} {x : α} : x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast

def RelSeries.tail {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (len_pos : p.length ≠ 0) : RelSeries r

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

@[simp]

theorem RelSeries.tail_toFun {α : Type u_1} {r : SetRel α α} (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 : SetRel α α} (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 : SetRel α α} (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 : SetRel α α} (p : RelSeries r) (len_pos : p.length ≠ 0) : (p.tail len_pos).last = p.last

@[simp]

theorem RelSeries.toList_tail {α : Type u_1} {r : SetRel α α} {p : RelSeries r} (hp : p.length ≠ 0) : (p.tail hp).toList = p.toList.tail

@[simp]

theorem RelSeries.tail_cons {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (x : α) (hx : (x, p.head) ∈ r) : (p.cons x hx).tail ⋯ = p

theorem RelSeries.cons_self_tail {α : Type u_1} {r : SetRel α α} {p : RelSeries r} (hp : p.length ≠ 0) : (p.tail hp).cons p.head ⋯ = p

def RelSeries.inductionOn {α : Type u_1} {r : SetRel α α} (motive : RelSeries r → Sort u_3) (singleton : (x : α) → motive (singleton r x)) (cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)) (p : RelSeries r) : motive p

To show a proposition p for xs : RelSeries r it suffices to show it for all singletons and to show that when p holds for xs it also holds for xs prepended with one element.

Note: This can also be used to construct data, but it does not have good definitional properties, since (p.cons x hx).tail _ = p is not a definitional equality.

@[simp]

theorem RelSeries.toList_snoc {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r) : (p.snoc newLast rel).toList = p.toList ++ [newLast]

def RelSeries.eraseLast {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : RelSeries r

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

@[simp]

theorem RelSeries.eraseLast_toFun {α : Type u_1} {r : SetRel α α} (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 : SetRel α α} (p : RelSeries r) : p.eraseLast.length = p.length - 1

@[simp]

theorem RelSeries.head_eraseLast {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.eraseLast.head = p.head

@[simp]

theorem RelSeries.last_eraseLast {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.eraseLast.last = p.toFun ⟨p.length.pred, ⋯⟩

theorem RelSeries.eraseLast_last_rel_last {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (h : p.length ≠ 0) : (p.eraseLast.last, p.last) ∈ r

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

@[simp]

theorem RelSeries.toList_eraseLast {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (hp : p.length ≠ 0) : p.eraseLast.toList = p.toList.dropLast

theorem RelSeries.snoc_self_eraseLast {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (h : p.length ≠ 0) : p.eraseLast.snoc p.last ⋯ = p

def RelSeries.inductionOn' {α : Type u_1} {r : SetRel α α} (motive : RelSeries r → Sort u_3) (singleton : (x : α) → motive (singleton r x)) (snoc : (p : RelSeries r) → (x : α) → (hx : (p.last, x) ∈ r) → motive p → motive (p.snoc x hx)) (p : RelSeries r) : motive p

To show a proposition p for xs : RelSeries r it suffices to show it for all singletons and to show that when p holds for xs it also holds for xs appended with one element.

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

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.

@[simp]

theorem RelSeries.smash_length {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : p.last = q.head) : (p.smash q connect).length = p.length + q.length

theorem RelSeries.smash_castLE {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin (p.length + 1)) : (p.smash q h).toFun (Fin.castLE ⋯ i) = p.toFun i

theorem RelSeries.smash_castAdd {α : Type u_1} {r : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) (i : Fin p.length) : (p.smash q h).toFun (Fin.castAdd q.length i).castSucc = p.toFun i.castSucc

theorem RelSeries.smash_succ_castAdd {α : Type u_1} {r : SetRel α α} {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 : SetRel α α} {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 : SetRel α α} {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 : SetRel α α} {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 : SetRel α α} {p q : RelSeries r} (h : p.last = q.head) : (p.smash q h).last = q.last

def RelSeries.take {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : RelSeries r

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

@[simp]

theorem RelSeries.take_length {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : (p.take i).length = ↑i

@[simp]

theorem RelSeries.head_take {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : (p.take i).head = p.head

@[simp]

theorem RelSeries.last_take {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : (p.take i).last = p.toFun i

def RelSeries.drop {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : RelSeries r

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

@[simp]

theorem RelSeries.drop_length {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : (p.drop i).length = p.length - ↑i

@[simp]

theorem RelSeries.head_drop {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : (p.drop i).head = p.toFun i

@[simp]

theorem RelSeries.last_drop {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : (p.drop i).last = p.last

theorem SetRel.not_finiteDimensional_iff {α : Type u_1} {r : SetRel α α} [Nonempty α] : ¬r.FiniteDimensional ↔ r.InfiniteDimensional

theorem SetRel.not_infiniteDimensional_iff {α : Type u_1} {r : SetRel α α} [Nonempty α] : ¬r.InfiniteDimensional ↔ r.FiniteDimensional

theorem SetRel.finiteDimensional_or_infiniteDimensional {α : Type u_1} (r : SetRel α α) [Nonempty α] : r.FiniteDimensional ∨ r.InfiniteDimensional

instance SetRel.FiniteDimensional.inv {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional] : r.inv.FiniteDimensional

@[simp]

theorem SetRel.finiteDimensional_inv {α : Type u_1} {r : SetRel α α} : r.inv.FiniteDimensional ↔ r.FiniteDimensional

@[deprecated SetRel.finiteDimensional_inv (since := "2025-07-06")]

theorem SetRel.finiteDimensional_swap_iff {α : Type u_1} {r : SetRel α α} : r.inv.FiniteDimensional ↔ r.FiniteDimensional

Alias of SetRel.finiteDimensional_inv.

instance SetRel.InfiniteDimensional.inv {α : Type u_1} (r : SetRel α α) [r.InfiniteDimensional] : r.inv.InfiniteDimensional

@[simp]

theorem SetRel.infiniteDimensional_inv {α : Type u_1} {r : SetRel α α} : r.inv.InfiniteDimensional ↔ r.InfiniteDimensional

@[deprecated SetRel.infiniteDimensional_inv (since := "2025-07-06")]

theorem SetRel.infiniteDimensional_swap_iff {α : Type u_1} {r : SetRel α α} : r.inv.InfiniteDimensional ↔ r.InfiniteDimensional

Alias of SetRel.infiniteDimensional_inv.

theorem SetRel.IsWellFounded.inv_of_finiteDimensional {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional] : r.inv.IsWellFounded

@[deprecated SetRel.IsWellFounded.inv_of_finiteDimensional (since := "2025-07-06")]

theorem Rel.wellFounded_swap_of_finiteDimensional {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional] : r.inv.IsWellFounded

Alias of SetRel.IsWellFounded.inv_of_finiteDimensional.

theorem SetRel.IsWellFounded.of_finiteDimensional {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional] : r.IsWellFounded

@[deprecated SetRel.IsWellFounded.of_finiteDimensional (since := "2025-07-06")]

theorem SetRel.wellFounded_of_finiteDimensional {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional] : r.IsWellFounded

Alias of SetRel.IsWellFounded.of_finiteDimensional.

@[reducible, inline]

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

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

instance FiniteDimensionalOrder.ofUnique (γ : Type u_3) [Preorder γ] [Unique γ] : FiniteDimensionalOrder γ

@[reducible, inline]

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

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

@[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.

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_infiniteDimensionalOrder (α : Type u_1) [Preorder α] [InfiniteDimensionalOrder α] : Nonempty α

if α is infinite dimensional, then α is nonempty.

@[deprecated LTSeries.nonempty_of_infiniteDimensionalOrder (since := "2025-03-01")]

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

Alias of LTSeries.nonempty_of_infiniteDimensionalOrder.

---

if α is infinite dimensional, then α is nonempty.

theorem LTSeries.nonempty_of_finiteDimensionalOrder (α : Type u_1) [Preorder α] [FiniteDimensionalOrder α] : 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

theorem LTSeries.head_le {α : Type u_1} [Preorder α] (x : LTSeries α) (n : Fin (x.length + 1)) : RelSeries.head x ≤ x.toFun n

theorem LTSeries.head_le_last {α : Type u_1} [Preorder α] (x : LTSeries α) : RelSeries.head x ≤ RelSeries.last x

def LTSeries.mk {α : Type u_1} [Preorder α] (length : ℕ) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun) : LTSeries α

An alternative constructor of LTSeries from a strictly monotone function.

@[simp]

theorem LTSeries.mk_toFun {α : Type u_1} [Preorder α] (length : ℕ) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun) (a✝ : Fin (length + 1)) : (mk length toFun strictMono).toFun a✝ = toFun a✝

@[simp]

theorem LTSeries.mk_length {α : Type u_1} [Preorder α] (length : ℕ) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun) : (mk length toFun strictMono).length = length

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.

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

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ₙ

@[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.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.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 y → x < y) (surjective : Function.Surjective f) : LTSeries α

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ᵢ}.

@[simp]

theorem LTSeries.comap_toFun {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : α → β) (comap : ∀ ⦃x y : α⦄, f x < f y → x < y) (surjective : Function.Surjective f) (i : Fin (p.length + 1)) : (p.comap f comap surjective).toFun i = ⋯.choose

@[simp]

theorem LTSeries.comap_length {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : α → β) (comap : ∀ ⦃x y : α⦄, f x < f y → x < y) (surjective : Function.Surjective f) : (p.comap f comap surjective).length = p.length

def LTSeries.range (n : ℕ) : LTSeries ℕ

The strict series 0 < … < n in ℕ.

@[simp]

theorem LTSeries.length_range (n : ℕ) : (range n).length = n

@[simp]

theorem LTSeries.range_apply (n : ℕ) (i : Fin (n + 1)) : (range n).toFun i = ↑i

@[simp]

theorem LTSeries.head_range (n : ℕ) : RelSeries.head (range n) = 0

@[simp]

theorem LTSeries.last_range (n : ℕ) : RelSeries.last (range n) = n

theorem LTSeries.exists_relSeries_covBy {α : Type u_3} [PartialOrder α] [WellFoundedLT α] [WellFoundedGT α] (s : LTSeries α) : ∃ (t : RelSeries {(a, b) : α × α | a ⋖ b}) (i : Fin (s.length + 1) ↪ Fin (t.length + 1)), t.toFun ∘ ⇑i = s.toFun ∧ i 0 = 0 ∧ i (Fin.last s.length) = Fin.last t.length

Any LTSeries can be refined to a CovBy-RelSeries in a bidirectionally well-founded order.

theorem LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot {α : Type u_3} [PartialOrder α] [BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α] (s : LTSeries α) : ∃ (t : RelSeries {(a, b) : α × α | a ⋖ b}) (i : Fin (s.length + 1) ↪ Fin (t.length + 1)), t.toFun ∘ ⇑i = s.toFun ∧ t.head = ⊥ ∧ t.last = ⊤

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).

theorem LTSeries.head_add_length_le_nat (p : LTSeries ℕ) : RelSeries.head p + p.length ≤ RelSeries.last p

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

theorem LTSeries.head_add_length_le_int (p : LTSeries ℤ) : RelSeries.head p + ↑p.length ≤ RelSeries.last p

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.instFintypeOfDecidableLT {α : Type u_1} [Preorder α] [Fintype α] [DecidableLT α] : Fintype (LTSeries α)

theorem not_finiteDimensionalOrder_iff {α : Type u_1} [Preorder α] [Nonempty α] : ¬FiniteDimensionalOrder α ↔ InfiniteDimensionalOrder α

theorem not_infiniteDimensionalOrder_iff {α : Type u_1} [Preorder α] [Nonempty α] : ¬InfiniteDimensionalOrder α ↔ FiniteDimensionalOrder α

theorem finiteDimensionalOrder_or_infiniteDimensionalOrder (α : Type u_1) [Preorder α] [Nonempty α] : FiniteDimensionalOrder α ∨ InfiniteDimensionalOrder α

theorem infiniteDimensionalOrder_of_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → β) (hf : StrictMono f) [InfiniteDimensionalOrder α] : InfiniteDimensionalOrder β

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