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

Instances For
    instance RelSeries.instCoeFunRelSeriesForAllFinHAddNatInstHAddInstAddNatLengthOfNat {α : Type u_1} (r : Rel α α) :
    CoeFun (RelSeries r) fun x => Fin (x.length + 1)α
    @[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.toFun (RelSeries.singleton r a) x = a
    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.

    Instances For
      instance RelSeries.instIsEmptyRelSeries {α : Type u_1} (r : Rel α α) [IsEmpty α] :
      instance RelSeries.instNonemptyRelSeries {α : Type u_1} (r : Rel α α) [Nonempty α] :
      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) :
      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) :
      @[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.toFun (RelSeries.ofLE x h) a = RelSeries.toFun x 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

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

        Instances For
          theorem RelSeries.toList_chain' {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
          theorem RelSeries.toList_ne_empty {α : Type u_1} {r : Rel α α} (x : RelSeries r) :
          @[simp]
          theorem RelSeries.fromListChain'_toFun {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_empty : x []) (hx : List.Chain' r x) :
          @[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) :

          Every nonempty list satisfying the chain condition gives a relation series

          Instances For
            def RelSeries.Equiv {α : Type u_1} {r : Rel α α} :
            RelSeries r {x | x [] List.Chain' r x}

            Relation series of r and nonempty list of α satisfying r-chain condition bijectively corresponds to each other.

            Instances For
              class Rel.FiniteDimensional {α : Type u_1} (r : Rel α α) :
              • exists_longest_relSeries : x, ∀ (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.

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

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

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

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

                  The longest relational series when a relation is finite dimensional

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

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

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

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

                      @[inline, reducible]
                      abbrev FiniteDimensionalOrder (γ : Type u_1) [Preorder γ] :

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

                      Instances For
                        @[inline, reducible]
                        abbrev InfiniteDimensionalOrder (γ : Type u_1) [Preorder γ] :

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

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

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

                            The longest <-series when a type is finite dimensional

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

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

                              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