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

theorem RelSeries.step {α : Type u_1} {r : Rel α α} (self : RelSeries r) (i : Fin self.length) : r (self.toFun i.castSucc) (self.toFun i.succ)

Adjacent elements are related

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

Equations

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

@[simp]

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

@[simp]

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

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.instIsEmpty {α : Type u_1} (r : Rel α α) [IsEmpty α] : IsEmpty (RelSeries r)

Equations

• ⋯ = ⋯

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

Equations

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

instance RelSeries.instNonempty {α : 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) : (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

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

• x.ofLE 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) : (x.ofLE h).toFun = x.toFun

@[reducible, inline]

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

Every relation series gives a list

Equations

• x.toList = List.ofFn x.toFun

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

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

@[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 = x.length.pred

@[simp]

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

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 := x.length.pred, toFun := x.get ∘ 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.

theorem Rel.FiniteDimensional.exists_longest_relSeries {α : Type u_1} {r : Rel α α} [self : r.FiniteDimensional] : ∃ (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.

theorem Rel.InfiniteDimensional.exists_relSeries_with_length {α : Type u_1} {r : Rel α α} [self : r.InfiniteDimensional] (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 α α) [r.FiniteDimensional] : RelSeries r

The longest relational series when a relation is finite dimensional

Equations

• RelSeries.longestOf r = ⋯.choose

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 : ℕ) : RelSeries r

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

Equations

• RelSeries.withLength r n = ⋯.choose

@[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] : 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)) : (p.append 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

• p.append 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)) : (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 : RelSeries r) (q : RelSeries r) (connect : r (RelSeries.last r p) (RelSeries.head r q)) (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 : RelSeries r) (q : RelSeries r) (connect : r (RelSeries.last r p) (RelSeries.head r q)) : RelSeries.head r (p.append 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 (p.append 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 : r →r s) : (p.map f).length = p.length

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

Equations

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

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

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

@[simp]

theorem RelSeries.reverse_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) : p.reverse.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

• p.reverse = { 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)) : p.reverse.toFun i = p.toFun i.rev

@[simp]

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

• p.cons newHead rel = (RelSeries.singleton r newHead).append 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 (p.cons 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 (p.cons 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)), (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

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

• p.tail 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 (p.tail 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 (p.tail len_pos) = RelSeries.last r p

@[simp]

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

@[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, ⋯⟩

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

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

@[simp]

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

@[simp]

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

@[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)) : (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 : RelSeries r) (q : RelSeries r) (connect : RelSeries.last r p = RelSeries.head r q) : (p.smash q connect).length = p.length + q.length

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) : (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 : RelSeries r} {q : RelSeries r} (h : RelSeries.last r p = RelSeries.head r q) (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 : RelSeries r} {q : RelSeries r} (h : RelSeries.last r p = RelSeries.head r q) (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 : RelSeries r} {q : RelSeries r} (h : RelSeries.last r p = RelSeries.head r q) (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 : RelSeries r} {q : RelSeries r} (h : RelSeries.last r p = RelSeries.head r q) : RelSeries.head r (p.smash 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 (p.smash q h) = RelSeries.last r q

@[reducible, inline]

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

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

Equations

• ⋯ = ⋯

@[reducible, inline]

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

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

• 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_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

@[simp]

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

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_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

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

• p.map 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)) : (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

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

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