Documentation

Mathlib.Order.RelSeries

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

Instances For
    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
    @[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 : α) :

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

    Equations
    Instances For
      instance RelSeries.instIsEmpty {α : Type u_1} (r : Rel α α) [IsEmpty α] :
      Equations
      • =
      instance RelSeries.instInhabited {α : Type u_1} (r : Rel α α) [Inhabited α] :
      Equations
      instance RelSeries.instNonempty {α : Type u_1} (r : Rel α α) [Nonempty α] :
      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) :

      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 : RelSeries r) {s : Rel α α} (h : r s) :
        (x.ofLE h).toFun = x.toFun
        def RelSeries.toList {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
        List α

        Every relation series gives a list

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

          Every nonempty list satisfying the chain condition gives a relation series

          Equations
          Instances For
            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.
            Instances For
              theorem RelSeries.toList_injective {α : Type u_1} {r : Rel α α} :
              Function.Injective RelSeries.toList
              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 : 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.

              Instances
                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 α α) :

                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.

                Instances
                  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] :

                  The longest relational series when a relation is finite dimensional

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

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

                    Equations
                    Instances For
                      @[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] :

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

                      instance RelSeries.membership {α : Type u_1} {r : Rel α α} :
                      Equations
                      theorem RelSeries.mem_def {α : Type u_1} {r : Rel α α} {s : RelSeries r} {x : α} :
                      x s x Set.range s.toFun
                      @[simp]
                      theorem RelSeries.mem_toList {α : Type u_1} {r : Rel α α} {s : RelSeries r} {x : α} :
                      x s.toList x s
                      theorem RelSeries.subsingleton_of_length_eq_zero {α : Type u_1} {r : Rel α α} {s : RelSeries r} (hs : s.length = 0) :
                      {x : α | x s}.Subsingleton
                      theorem RelSeries.length_ne_zero_of_nontrivial {α : Type u_1} {r : Rel α α} {s : RelSeries r} (h : {x : α | x s}.Nontrivial) :
                      s.length 0
                      theorem RelSeries.length_pos_of_nontrivial {α : Type u_1} {r : Rel α α} {s : RelSeries r} (h : {x : α | x s}.Nontrivial) :
                      0 < s.length
                      theorem RelSeries.length_ne_zero {α : Type u_1} {r : Rel α α} {s : RelSeries r} (irrefl : Irreflexive r) :
                      s.length 0 {x : α | x s}.Nontrivial
                      theorem RelSeries.length_pos {α : Type u_1} {r : Rel α α} {s : RelSeries r} (irrefl : Irreflexive r) :
                      0 < s.length {x : α | x s}.Nontrivial
                      theorem RelSeries.length_eq_zero {α : Type u_1} {r : Rel α α} {s : RelSeries r} (irrefl : Irreflexive r) :
                      s.length = 0 {x : α | x s}.Subsingleton
                      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
                      • x.head = x.toFun 0
                      Instances For
                        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
                        Instances For
                          theorem RelSeries.apply_last {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
                          x.toFun (Fin.last x.length) = x.last
                          theorem RelSeries.head_mem {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
                          x.head x
                          theorem RelSeries.last_mem {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
                          x.last x
                          @[simp]
                          theorem RelSeries.append_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (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 : RelSeries r) (q : RelSeries r) (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 Fin.cast , step := }
                          Instances For
                            theorem RelSeries.append_apply_left {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (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 : RelSeries r) (q : RelSeries r) (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 : RelSeries r) (q : RelSeries r) (connect : r p.last q.head) :
                            (p.append q connect).head = p.head
                            @[simp]
                            theorem RelSeries.last_append {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (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 : 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) :

                            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 : RelSeries r) (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 : 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
                              @[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
                              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)) :

                              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 : 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 := }
                                Instances For
                                  @[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 p.head) :
                                  (p.cons newHead rel).length = p.length + 1
                                  def RelSeries.cons {α : Type u_1} {r : Rel α α} (p : RelSeries r) (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 : RelSeries r) (newHead : α) (rel : r newHead p.head) :
                                    (p.cons newHead rel).head = newHead
                                    @[simp]
                                    theorem RelSeries.last_cons {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newHead : α) (rel : r newHead p.head) :
                                    (p.cons newHead rel).last = p.last
                                    @[simp]
                                    theorem RelSeries.snoc_length {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
                                    (p.snoc newLast rel).length = p.length + 1
                                    def RelSeries.snoc {α : Type u_1} {r : Rel α α} (p : RelSeries r) (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 : RelSeries r) (newLast : α) (rel : r p.last newLast) :
                                      (p.snoc newLast rel).head = p.head
                                      @[simp]
                                      theorem RelSeries.last_snoc {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
                                      (p.snoc newLast rel).last = newLast
                                      @[simp]
                                      theorem RelSeries.last_snoc' {α : Type u_1} {r : Rel α α} (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
                                      (p.snoc newLast rel).toFun (Fin.last (p.length + 1)) = newLast
                                      @[simp]
                                      theorem RelSeries.snoc_castSucc {α : Type u_1} {r : Rel α α} (s : RelSeries r) (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 : RelSeries r} {newLast : α} {rel : r p.last newLast} {x : α} :
                                      x p.snoc newLast rel x p x = newLast
                                      @[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
                                      @[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
                                      def RelSeries.tail {α : Type u_1} {r : Rel α α} (p : RelSeries r) (len_pos : p.length 0) :

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

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem RelSeries.head_tail {α : Type u_1} {r : Rel α α} (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 : Rel α α} (p : RelSeries r) (len_pos : p.length 0) :
                                        (p.tail len_pos).last = p.last
                                        @[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) :

                                        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 : RelSeries r) :
                                          p.eraseLast.head = p.head
                                          @[simp]
                                          theorem RelSeries.last_eraseLast {α : Type u_1} {r : Rel α α} (p : RelSeries r) :
                                          p.eraseLast.last = p.toFun p.length.pred,
                                          @[simp]
                                          theorem RelSeries.smash_toFun {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (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 : RelSeries r) (q : RelSeries r) (connect : p.last = q.head) :
                                          (p.smash q connect).length = p.length + q.length
                                          def RelSeries.smash {α : Type u_1} {r : Rel α α} (p : RelSeries r) (q : RelSeries r) (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 : RelSeries r} {q : RelSeries r} (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 : RelSeries r} {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 : Rel α α} {p : RelSeries r} {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 : Rel α α} {p : RelSeries r} {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 : Rel α α} {p : RelSeries r} {q : RelSeries r} (h : p.last = q.head) :
                                            (p.smash q h).head = p.head
                                            @[simp]
                                            theorem RelSeries.last_smash {α : Type u_1} {r : Rel α α} {p : RelSeries r} {q : RelSeries r} (h : p.last = q.head) :
                                            (p.smash q h).last = q.last
                                            @[reducible, inline]
                                            abbrev FiniteDimensionalOrder (γ : Type u_3) [Preorder γ] :

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

                                            Equations
                                            Instances For
                                              Equations
                                              • =
                                              @[reducible, inline]
                                              abbrev InfiniteDimensionalOrder (γ : Type u_3) [Preorder γ] :

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

                                              Equations
                                              Instances For
                                                @[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
                                                Instances For
                                                  noncomputable def LTSeries.longestOf (α : Type u_1) [Preorder α] [FiniteDimensionalOrder α] :

                                                  The longest <-series when a type is finite dimensional

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

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

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

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

                                                      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} [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) :

                                                        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} [Preorder α] [Preorder β] (p : LTSeries β) (f : αβ) (comap : ∀ ⦃x y : α⦄, f x < f yx < 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 yx < 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 yx < y) (surjective : Function.Surjective f) :

                                                          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
                                                            theorem infiniteDimensionalOrder_of_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : αβ) (hf : StrictMono f) [InfiniteDimensionalOrder α] :

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