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 (Fin.castSucc i)) (self.toFun (Fin.succ i))

  Adjacent elements are related

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

Equations

• RelSeries.instCoeFunRelSeriesForAllFinHAddNatInstHAddInstAddNatLengthOfNat r = { coe := RelSeries.toFun }

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

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.

Equations

• RelSeries.singleton r a = { length := 0, toFun := fun (x : Fin (0 + 1)) => a, step := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• RelSeries.instInhabitedRelSeries r = { default := RelSeries.singleton r default }

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

Equations

• ⋯ = ⋯

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 = 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 (x.toFun i) (x.toFun 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 (x.toFun i) (x.toFun j) ∨ x.toFun i = x.toFun 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.ofLE x h).toFun a = x.toFun 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

Equations

• RelSeries.ofLE x h = { length := x.length, toFun := x.toFun, step := ⋯ }

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

Equations

• RelSeries.toList x = List.ofFn x.toFun

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.fromListChain' x x_ne_empty hx).toFun a = (List.get x ∘ Fin.cast ⋯) 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

Equations

• RelSeries.fromListChain' x x_ne_empty hx = { length := Nat.pred (List.length x), toFun := List.get x ∘ Fin.cast ⋯, step := ⋯ }

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.

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

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

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

The longest relational series when a relation is finite dimensional

Equations

• RelSeries.longestOf r = Exists.choose ⋯

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

Equations

• RelSeries.withLength r n = Exists.choose ⋯

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

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

Equations

• RelSeries.membership r = { mem := fun (x : α) (x_1 : RelSeries r) => x ∈ Set.range x_1.toFun }

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

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

• RelSeries.head r x = 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

• RelSeries.last r x = x.toFun (Fin.last x.length)

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

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

@[simp]

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

def RelSeries.append {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (connect : r (RelSeries.last r p) (RelSeries.head r q)) : 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ₘ.

Equations

• RelSeries.append p q connect = { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }

theorem RelSeries.append_apply_left {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (connect : r (RelSeries.last r p) (RelSeries.head r q)) (i : Fin (p.length + 1)) : (RelSeries.append p 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 : RelSeries r) (q : RelSeries r) (connect : r (RelSeries.last r p) (RelSeries.head r q)) (i : Fin (q.length + 1)) : (RelSeries.append p q connect).toFun (↑↑(Fin.natAdd p.length i) + 1) = q.toFun i

@[simp]

theorem RelSeries.head_append {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (connect : r (RelSeries.last r p) (RelSeries.head r q)) : RelSeries.head r (RelSeries.append p q connect) = RelSeries.head r p

@[simp]

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

@[simp]

theorem RelSeries.map_length {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : α → β) (hf : ∀ ⦃x y : α⦄, r x y → s (f x) (f y)) : (RelSeries.map p f hf).length = p.length

def RelSeries.map {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : α → β) (hf : ∀ ⦃x y : α⦄, r x y → s (f x) (f y)) : 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ₙ

Equations

• RelSeries.map p f hf = { length := p.length, toFun := f ∘ p.toFun, step := ⋯ }

@[simp]

theorem RelSeries.map_apply {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : RelSeries r) (f : α → β) (hf : ∀ ⦃x y : α⦄, r x y → s (f x) (f y)) (i : Fin (p.length + 1)) : (RelSeries.map p f hf).toFun i = f (p.toFun i)

@[simp]

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

@[simp]

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

def RelSeries.insertNth {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin p.length) (a : α) (prev_connect : r (p.toFun (Fin.castSucc i)) a) (connect_next : r a (p.toFun (Fin.succ i))) : 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

Equations

• RelSeries.insertNth p i a prev_connect connect_next = { length := p.length + 1, toFun := Fin.insertNth (Fin.castSucc (Fin.succ i)) a p.toFun, step := ⋯ }

@[simp]

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

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

• RelSeries.reverse p = { length := p.length, toFun := p.toFun ∘ Fin.rev, step := ⋯ }

@[simp]

theorem RelSeries.reverse_apply {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : (RelSeries.reverse p).toFun i = p.toFun (Fin.rev i)

@[simp]

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

def RelSeries.cons {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newHead : α) (rel : r newHead (RelSeries.head r p)) : 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ₙ.

Equations

• RelSeries.cons p newHead rel = RelSeries.append (RelSeries.singleton r newHead) p rel

@[simp]

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

@[simp]

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

@[simp]

theorem RelSeries.tail_toFun {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length ≠ 0) : ∀ (a : Fin (p.length - 1 + 1)), (RelSeries.tail p 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) : (RelSeries.tail p len_pos).length = p.length - 1

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

Equations

• RelSeries.tail p len_pos = { length := p.length - 1, toFun := Fin.tail p.toFun ∘ Fin.cast ⋯, step := ⋯ }

@[simp]

theorem RelSeries.head_tail {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length ≠ 0) : RelSeries.head r (RelSeries.tail p len_pos) = p.toFun 1

@[simp]

theorem RelSeries.last_tail {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length ≠ 0) : RelSeries.last r (RelSeries.tail p len_pos) = RelSeries.last r p

@[simp]

theorem RelSeries.eraseLast_toFun {α : Type u_1} {r : Rel α α} (p : RelSeries r) (i : Fin (p.length - 1 + 1)) : (RelSeries.eraseLast p).toFun i = p.toFun { val := ↑i, isLt := ⋯ }

@[simp]

theorem RelSeries.eraseLast_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) : (RelSeries.eraseLast p).length = p.length - 1

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

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

Equations

• RelSeries.eraseLast p = { length := p.length - 1, toFun := fun (i : Fin (p.length - 1 + 1)) => p.toFun { val := ↑i, isLt := ⋯ }, step := ⋯ }

@[simp]

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

@[simp]

theorem RelSeries.last_eraseLast {α : Type u_1} {r : Rel α α} (p : RelSeries r) : RelSeries.last r (RelSeries.eraseLast p) = p.toFun { val := Nat.pred p.length, isLt := ⋯ }

@[simp]

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

@[simp]

theorem RelSeries.smash_toFun {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (connect : RelSeries.last r p = RelSeries.head r q) (i : Fin (p.length + q.length + 1)) : (RelSeries.smash p q connect).toFun i = if H : ↑i < p.length then p.toFun { val := ↑i, isLt := ⋯ } else q.toFun { val := ↑i - p.length, isLt := ⋯ }

def RelSeries.smash {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (connect : RelSeries.last r p = RelSeries.head r q) : 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.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

theorem RelSeries.smash_succ_natAdd {α : Type u_1} {r : Rel α α} {p : RelSeries r} {q : RelSeries r} (h : RelSeries.last r p = RelSeries.head r q) (i : Fin q.length) : (RelSeries.smash p q h).toFun (Fin.succ (Fin.natAdd p.length i)) = q.toFun (Fin.succ i)

@[simp]

theorem RelSeries.head_smash {α : Type u_1} {r : Rel α α} {p : RelSeries r} {q : RelSeries r} (h : RelSeries.last r p = RelSeries.head r q) : RelSeries.head r (RelSeries.smash p q h) = RelSeries.head r p

@[simp]

theorem RelSeries.last_smash {α : Type u_1} {r : Rel α α} {p : RelSeries r} {q : RelSeries r} (h : RelSeries.last r p = RelSeries.head r q) : RelSeries.last r (RelSeries.smash p q h) = RelSeries.last r q

@[inline, reducible]

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

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

Equations

• FiniteDimensionalOrder γ = Rel.FiniteDimensional fun (x x_1 : γ) => x < x_1

@[inline, reducible]

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

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

Equations

• InfiniteDimensionalOrder γ = Rel.InfiniteDimensional fun (x x_1 : γ) => x < x_1

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

Equations

• LTSeries α = RelSeries fun (x x_1 : α) => x < x_1

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

The longest <-series when a type is finite dimensional

Equations

• LTSeries.longestOf α = RelSeries.longestOf fun (x x_1 : α) => x < x_1

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

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

Equations

• LTSeries.withLength α n = RelSeries.withLength (fun (x x_1 : α) => x < x_1) n

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

@[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.mk {α : Type u_1} [Preorder α] (length : ℕ) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun) : LTSeries α

An alternative constructor of LTSeries from a strictly monotone function.

Equations

• LTSeries.mk length toFun strictMono = { length := length, toFun := toFun, step := ⋯ }

@[simp]

theorem LTSeries.map_length {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries α) (f : α → β) (hf : StrictMono f) : (LTSeries.map p 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)), (LTSeries.map p f hf).toFun a = f (p.toFun a)

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ₙ

Equations

• LTSeries.map p f hf = LTSeries.mk p.length (f ∘ p.toFun) ⋯

@[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)) : (LTSeries.comap p f comap surjective).toFun i = Exists.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) : (LTSeries.comap p f comap surjective).length = p.length

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

Equations

• LTSeries.comap p f comap surjective = LTSeries.mk p.length (fun (i : Fin (p.length + 1)) => Exists.choose ⋯) ⋯