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

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

instance RelSeries.instCoeFunForallFinHAddNatLengthOfNat {α : Type u_1} (r : Rel α α) :
CoeFun () fun (x : ) => Fin (x.length + 1)α
Equations
• = { coe := RelSeries.toFun }
@[simp]
theorem RelSeries.singleton_toFun {α : Type u_1} (r : Rel α α) (a : α) :
∀ (x : Fin (0 + 1)), ().toFun x = a
@[simp]
theorem RelSeries.singleton_length {α : Type u_1} (r : Rel α α) (a : α) :
().length = 0
def RelSeries.singleton {α : Type u_1} (r : Rel α α) (a : α) :

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

Equations
• = { length := 0, toFun := fun (x : Fin (0 + 1)) => a, step := }
Instances For
instance RelSeries.instIsEmpty {α : Type u_1} (r : Rel α α) [] :
Equations
• =
instance RelSeries.instInhabited {α : Type u_1} (r : Rel α α) [] :
Equations
instance RelSeries.instNonempty {α : Type u_1} (r : Rel α α) [] :
Equations
• =
theorem RelSeries.ext {α : Type u_1} {r : Rel α α} {x : } {y : } (length_eq : x.length = y.length) (toFun_eq : x.toFun = y.toFun ) :
x = y
theorem RelSeries.rel_of_lt {α : Type u_1} {r : Rel α α} [IsTrans α r] (x : ) {i : Fin (x.length + 1)} {j : Fin (x.length + 1)} (h : i < j) :
r (x.toFun i) (x.toFun j)
theorem RelSeries.rel_or_eq_of_le {α : Type u_1} {r : Rel α α} [IsTrans α r] (x : ) {i : Fin (x.length + 1)} {j : Fin (x.length + 1)} (h : i j) :
r (x.toFun i) (x.toFun j) x.toFun i = x.toFun j
@[simp]
theorem RelSeries.ofLE_toFun {α : Type u_1} {r : Rel α α} (x : ) {s : Rel α α} (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 : Rel α α} (x : ) {s : Rel α α} (h : r s) :
(x.ofLE h).length = x.length
def RelSeries.ofLE {α : Type u_1} {r : Rel α α} (x : ) {s : Rel α α} (h : r s) :

Given two relations r, s on α such that r ≤ s, any relation series of r induces a relation series of s

Equations
• x.ofLE h = { length := x.length, toFun := x.toFun, step := }
Instances For
theorem RelSeries.coe_ofLE {α : Type u_1} {r : Rel α α} (x : ) {s : Rel α α} (h : r s) :
(x.ofLE h).toFun = x.toFun
def RelSeries.toList {α : Type u_1} {r : Rel α α} (x : ) :
List α

Every relation series gives a list

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

Every nonempty list satisfying the chain condition gives a relation series

Equations
Instances For
def RelSeries.Equiv {α : Type u_1} {r : Rel α α} :
{x : List α | 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.
Instances For
class Rel.FiniteDimensional {α : Type u_1} (r : Rel α α) :

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 : ), ∀ (y : ), y.length x.length

A relation r is said to be finite dimensional iff there is a relation series of r with the maximum length.

Instances
theorem Rel.FiniteDimensional.exists_longest_relSeries {α : Type u_1} {r : Rel α α} [self : r.FiniteDimensional] :
∃ (x : ), ∀ (y : ), y.length x.length

A relation r is said to be finite dimensional iff there is a relation series of r with the maximum length.

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

A relation r is said to be infinite dimensional iff there exists relation series of arbitrary length.

• exists_relSeries_with_length : ∀ (n : ), ∃ (x : ), x.length = n

A relation r is said to be infinite dimensional iff there exists relation series of arbitrary length.

Instances
theorem Rel.InfiniteDimensional.exists_relSeries_with_length {α : Type u_1} {r : Rel α α} [self : r.InfiniteDimensional] (n : ) :
∃ (x : ), 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] :

The longest relational series when a relation is finite dimensional

Equations
• = .choose
Instances For
theorem RelSeries.length_le_length_longestOf {α : Type u_1} (r : Rel α α) [r.FiniteDimensional] (x : ) :
x.length .length
noncomputable def RelSeries.withLength {α : Type u_1} (r : Rel α α) [r.InfiniteDimensional] (n : ) :

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

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

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

instance RelSeries.membership {α : Type u_1} {r : Rel α α} :
Equations
• RelSeries.membership = { mem := fun (x : α) (x_1 : ) => x Set.range x_1.toFun }
theorem RelSeries.mem_def {α : Type u_1} {r : Rel α α} {s : } {x : α} :
x s x Set.range s.toFun
@[simp]
theorem RelSeries.mem_toList {α : Type u_1} {r : Rel α α} {s : } {x : α} :
x s.toList x s
theorem RelSeries.subsingleton_of_length_eq_zero {α : Type u_1} {r : Rel α α} {s : } (hs : s.length = 0) :
{x : α | x s}.Subsingleton
theorem RelSeries.length_ne_zero_of_nontrivial {α : Type u_1} {r : Rel α α} {s : } (h : {x : α | x s}.Nontrivial) :
s.length 0
theorem RelSeries.length_pos_of_nontrivial {α : Type u_1} {r : Rel α α} {s : } (h : {x : α | x s}.Nontrivial) :
0 < s.length
theorem RelSeries.length_ne_zero {α : Type u_1} {r : Rel α α} {s : } (irrefl : ) :
s.length 0 {x : α | x s}.Nontrivial
theorem RelSeries.length_pos {α : Type u_1} {r : Rel α α} {s : } (irrefl : ) :
0 < s.length {x : α | x s}.Nontrivial
theorem RelSeries.length_eq_zero {α : Type u_1} {r : Rel α α} {s : } (irrefl : ) :
s.length = 0 {x : α | x s}.Subsingleton
def RelSeries.head {α : Type u_1} {r : Rel α α} (x : ) :
α

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
Instances For
def RelSeries.last {α : Type u_1} {r : Rel α α} (x : ) :
α

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
Instances For
theorem RelSeries.head_mem {α : Type u_1} {r : Rel α α} (x : ) :
theorem RelSeries.last_mem {α : Type u_1} {r : Rel α α} (x : ) :
x.last x
@[simp]
theorem RelSeries.append_length {α : Type u_1} {r : Rel α α} (p : ) (q : ) (connect : r p.last q.head) :
(p.append q connect).length = p.length + q.length + 1
def RelSeries.append {α : Type u_1} {r : Rel α α} (p : ) (q : ) (connect : r p.last q.head) :

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 , step := }
Instances For
theorem RelSeries.append_apply_left {α : Type u_1} {r : Rel α α} (p : ) (q : ) (connect : r p.last q.head) (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 : ) (q : ) (connect : r p.last q.head) (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 : ) (q : ) (connect : r p.last q.head) :
@[simp]
theorem RelSeries.last_append {α : Type u_1} {r : Rel α α} (p : ) (q : ) (connect : r p.last q.head) :
(p.append q connect).last = q.last
@[simp]
theorem RelSeries.map_length {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : ) (f : r →r s) :
(p.map f).length = p.length
def RelSeries.map {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : ) (f : r →r 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 := }
Instances For
@[simp]
theorem RelSeries.map_apply {α : Type u_1} {r : Rel α α} {β : Type u_2} {s : Rel β β} (p : ) (f : r →r s) (i : Fin (p.length + 1)) :
(p.map f).toFun i = f (p.toFun i)
@[simp]
theorem RelSeries.insertNth_length {α : Type u_1} {r : Rel α α} (p : ) (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
@[simp]
theorem RelSeries.insertNth_toFun {α : Type u_1} {r : Rel α α} (p : ) (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
def RelSeries.insertNth {α : Type u_1} {r : Rel α α} (p : ) (i : Fin p.length) (a : α) (prev_connect : r (p.toFun i.castSucc) a) (connect_next : r a (p.toFun i.succ)) :

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 := }
Instances For
@[simp]
theorem RelSeries.reverse_length {α : Type u_1} {r : Rel α α} (p : ) :
p.reverse.length = p.length
def RelSeries.reverse {α : Type u_1} {r : Rel α α} (p : ) :
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 := }
Instances For
@[simp]
theorem RelSeries.reverse_apply {α : Type u_1} {r : Rel α α} (p : ) (i : Fin (p.length + 1)) :
p.reverse.toFun i = p.toFun i.rev
@[simp]
theorem RelSeries.cons_length {α : Type u_1} {r : Rel α α} (p : ) (newHead : α) (rel : r newHead p.head) :
(p.cons newHead rel).length = p.length + 1
def RelSeries.cons {α : Type u_1} {r : Rel α α} (p : ) (newHead : α) (rel : r newHead p.head) :

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
Instances For
@[simp]
theorem RelSeries.head_cons {α : Type u_1} {r : Rel α α} (p : ) (newHead : α) (rel : r newHead p.head) :
@[simp]
theorem RelSeries.last_cons {α : Type u_1} {r : Rel α α} (p : ) (newHead : α) (rel : r newHead p.head) :
@[simp]
theorem RelSeries.snoc_length {α : Type u_1} {r : Rel α α} (p : ) (newLast : α) (rel : r p.last newLast) :
(p.snoc newLast rel).length = p.length + 1
def RelSeries.snoc {α : Type u_1} {r : Rel α α} (p : ) (newLast : α) (rel : r p.last newLast) :

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.

Equations
Instances For
@[simp]
theorem RelSeries.head_snoc {α : Type u_1} {r : Rel α α} (p : ) (newLast : α) (rel : r p.last newLast) :
@[simp]
theorem RelSeries.last_snoc {α : Type u_1} {r : Rel α α} (p : ) (newLast : α) (rel : r p.last newLast) :
(p.snoc newLast rel).last = newLast
@[simp]
theorem RelSeries.snoc_castSucc {α : Type u_1} {r : Rel α α} (s : ) (a : α) (connect : r s.last a) (i : Fin (s.length + 1)) :
(s.snoc a connect).toFun i.castSucc = s.toFun i
theorem RelSeries.mem_snoc {α : Type u_1} {r : Rel α α} {p : } {newLast : α} {rel : r p.last newLast} {x : α} :
x p.snoc newLast rel x p x = newLast
@[simp]
theorem RelSeries.tail_toFun {α : Type u_1} {r : Rel α α} (p : ) (len_pos : p.length 0) :
∀ (a : Fin (p.length - 1 + 1)), (p.tail len_pos).toFun a = (Fin.tail p.toFun ) a
@[simp]
theorem RelSeries.tail_length {α : Type u_1} {r : Rel α α} (p : ) (len_pos : p.length 0) :
(p.tail len_pos).length = p.length - 1
def RelSeries.tail {α : Type u_1} {r : Rel α α} (p : ) (len_pos : p.length 0) :

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 , step := }
Instances For
@[simp]
theorem RelSeries.head_tail {α : Type u_1} {r : Rel α α} (p : ) (len_pos : p.length 0) :
@[simp]
theorem RelSeries.last_tail {α : Type u_1} {r : Rel α α} (p : ) (len_pos : p.length 0) :
(p.tail len_pos).last = p.last
@[simp]
theorem RelSeries.eraseLast_toFun {α : Type u_1} {r : Rel α α} (p : ) (i : Fin (p.length - 1 + 1)) :
p.eraseLast.toFun i = p.toFun i,
@[simp]
theorem RelSeries.eraseLast_length {α : Type u_1} {r : Rel α α} (p : ) :
p.eraseLast.length = p.length - 1
def RelSeries.eraseLast {α : Type u_1} {r : Rel α α} (p : ) :

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 := }
Instances For
@[simp]
theorem RelSeries.head_eraseLast {α : Type u_1} {r : Rel α α} (p : ) :
@[simp]
theorem RelSeries.last_eraseLast {α : Type u_1} {r : Rel α α} (p : ) :
p.eraseLast.last = p.toFun p.length.pred,
@[simp]
theorem RelSeries.smash_toFun {α : Type u_1} {r : Rel α α} (p : ) (q : ) (connect : p.last = q.head) (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 : ) (q : ) (connect : p.last = q.head) :
(p.smash q connect).length = p.length + q.length
def RelSeries.smash {α : Type u_1} {r : Rel α α} (p : ) (q : ) (connect : p.last = q.head) :

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.
Instances For
theorem RelSeries.smash_castAdd {α : Type u_1} {r : Rel α α} {p : } {q : } (connect : p.last = q.head) (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 : } {q : } (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 : Rel α α} {p : } {q : } (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 : Rel α α} {p : } {q : } (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 : Rel α α} {p : } {q : } (h : p.last = q.head) :
@[simp]
theorem RelSeries.last_smash {α : Type u_1} {r : Rel α α} {p : } {q : } (h : p.last = q.head) :
(p.smash q h).last = q.last
@[reducible, inline]
abbrev FiniteDimensionalOrder (γ : Type u_3) [] :

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

Equations
Instances For
instance FiniteDimensionalOrder.ofUnique (γ : Type u_3) [] [] :
Equations
• =
@[reducible, inline]
abbrev InfiniteDimensionalOrder (γ : Type u_3) [] :

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

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

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

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

The longest <-series when a type is finite dimensional

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

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

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

if α is infinite dimensional, then α is nonempty.

theorem LTSeries.longestOf_is_longest {α : Type u_1} [] (x : ) :
x.length .length
theorem LTSeries.longestOf_len_unique {α : Type u_1} [] (p : ) (is_longest : ∀ (q : ), q.length p.length) :
p.length = .length
theorem LTSeries.strictMono {α : Type u_1} [] (x : ) :
StrictMono x.toFun
theorem LTSeries.monotone {α : Type u_1} [] (x : ) :
Monotone x.toFun
@[simp]
theorem LTSeries.mk_toFun {α : Type u_1} [] (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} [] (length : ) (toFun : Fin (length + 1)α) (strictMono : StrictMono toFun) :
(LTSeries.mk length toFun strictMono).length = length
def LTSeries.mk {α : Type u_1} [] (length : ) (toFun : Fin (length + 1)α) (strictMono : StrictMono toFun) :

An alternative constructor of LTSeries from a strictly monotone function.

Equations
• LTSeries.mk length toFun strictMono = { length := length, toFun := toFun, step := }
Instances For
@[simp]
theorem LTSeries.map_toFun {α : Type u_1} {β : Type u_2} [] [] (p : ) (f : αβ) (hf : ) :
∀ (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} [] [] (p : ) (f : αβ) (hf : ) :
(p.map f hf).length = p.length
def LTSeries.map {α : Type u_1} {β : Type u_2} [] [] (p : ) (f : αβ) (hf : ) :

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
Instances For
@[simp]
theorem LTSeries.comap_toFun {α : Type u_1} {β : Type u_2} [] [] (p : ) (f : αβ) (comap : ∀ ⦃x y : α⦄, f x < f yx < y) (surjective : ) (i : Fin (p.length + 1)) :
(p.comap f comap surjective).toFun i = .choose
@[simp]
theorem LTSeries.comap_length {α : Type u_1} {β : Type u_2} [] [] (p : ) (f : αβ) (comap : ∀ ⦃x y : α⦄, f x < f yx < y) (surjective : ) :
(p.comap f comap surjective).length = p.length
noncomputable def LTSeries.comap {α : Type u_1} {β : Type u_2} [] [] (p : ) (f : αβ) (comap : ∀ ⦃x y : α⦄, f x < f yx < y) (surjective : ) :

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)
Instances For