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 := (_ : Fin 0 → r a a) }

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

Equations

• (_ : IsEmpty (RelSeries r)) = (_ : IsEmpty (RelSeries r))

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

• (_ : Nonempty (RelSeries r)) = (_ : 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 (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 := (_ : ∀ (x_1 : Fin x.length), s (x.toFun (Fin.castSucc x_1)) (x.toFun (Fin.succ x_1))) }

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

Equations

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

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 (_ : ∃ (x : RelSeries r), ∀ (y : RelSeries r), y.length ≤ x.length)

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 (_ : ∃ (x : RelSeries r), x.length = n)

@[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 r p q connect).length = p.length + q.length + 1

@[simp]

theorem RelSeries.append_toFun {α : Type u_1} (r : Rel α α) (p : RelSeries r) (q : RelSeries r) (connect : r (RelSeries.last r p) (RelSeries.head r q)) : ∀ (a : Fin (p.length + q.length + 1 + 1)), (RelSeries.append r p q connect).toFun a = (Fin.append p.toFun q.toFun ∘ Fin.cast (_ : p.length + q.length + 1 + 1 = p.length + 1 + (q.length + 1))) a

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

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

@[simp]

theorem RelSeries.map_toFun {α : 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)) : ∀ (a : Fin (p.length + 1)), (RelSeries.map r s p f hf).toFun a = (f ∘ p.toFun) a

@[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 r s 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 r s p f hf = { length := p.length, toFun := f ∘ p.toFun, step := (_ : ∀ (x : Fin p.length), s (f (p.toFun (Fin.castSucc x))) (f (p.toFun (Fin.succ x)))) }

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

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

@[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 := (_ : ∀ (i : Fin length), toFun (Fin.castSucc i) < toFun (Fin.succ i)) }

@[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) (_ : StrictMono (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 (_ : ∃ (a : α), f a = p.toFun i)

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

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