Documentation

Mathlib.Data.List.Cycle

Cycles of a list #

Lists have an equivalence relation of whether they are rotational permutations of one another. This relation is defined as IsRotated.

Based on this, we define the quotient of lists by the rotation relation, called Cycle.

We also define a representation of concrete cycles, available when viewing them in a goal state or via #eval, when over representable types. For example, the cycle (2 1 4 3) will be shown as c[2, 1, 4, 3]. Two equal cycles may be printed differently if their internal representation is different.

def List.nextOr {α : Type u_1} [DecidableEq α] :
List αααα

Return the z such that x :: z :: _ appears in xs, or default if there is no such z.

Equations
  • [].nextOr x✝ x = x
  • [head].nextOr x✝ x = x
  • (y :: z :: xs).nextOr x✝ x = if x✝ = y then z else (z :: xs).nextOr x✝ x
Instances For
    @[simp]
    theorem List.nextOr_nil {α : Type u_1} [DecidableEq α] (x : α) (d : α) :
    [].nextOr x d = d
    @[simp]
    theorem List.nextOr_singleton {α : Type u_1} [DecidableEq α] (x : α) (y : α) (d : α) :
    [y].nextOr x d = d
    @[simp]
    theorem List.nextOr_self_cons_cons {α : Type u_1} [DecidableEq α] (xs : List α) (x : α) (y : α) (d : α) :
    (x :: y :: xs).nextOr x d = y
    theorem List.nextOr_cons_of_ne {α : Type u_1} [DecidableEq α] (xs : List α) (y : α) (x : α) (d : α) (h : x y) :
    (y :: xs).nextOr x d = xs.nextOr x d
    theorem List.nextOr_eq_nextOr_of_mem_of_ne {α : Type u_1} [DecidableEq α] (xs : List α) (x : α) (d : α) (d' : α) (x_mem : x xs) (x_ne : x xs.getLast ) :
    xs.nextOr x d = xs.nextOr x d'

    nextOr does not depend on the default value, if the next value appears.

    theorem List.mem_of_nextOr_ne {α : Type u_1} [DecidableEq α] {xs : List α} {x : α} {d : α} (h : xs.nextOr x d d) :
    x xs
    theorem List.nextOr_concat {α : Type u_1} [DecidableEq α] {xs : List α} {x : α} (d : α) (h : xxs) :
    (xs ++ [x]).nextOr x d = d
    theorem List.nextOr_mem {α : Type u_1} [DecidableEq α] {xs : List α} {x : α} {d : α} (hd : d xs) :
    xs.nextOr x d xs
    def List.next {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : x l) :
    α

    Given an element x : α of l : List α such that x ∈ l, get the next element of l. This works from head to tail, (including a check for last element) so it will match on first hit, ignoring later duplicates.

    For example:

    • next [1, 2, 3] 2 _ = 3
    • next [1, 2, 3] 3 _ = 1
    • next [1, 2, 3, 2, 4] 2 _ = 3
    • next [1, 2, 3, 2] 2 _ = 3
    • next [1, 1, 2, 3, 2] 1 _ = 1
    Equations
    • l.next x h = l.nextOr x (l.get 0, )
    Instances For
      def List.prev {α : Type u_1} [DecidableEq α] (l : List α) (x : α) :
      x lα

      Given an element x : α of l : List α such that x ∈ l, get the previous element of l. This works from head to tail, (including a check for last element) so it will match on first hit, ignoring later duplicates.

      • prev [1, 2, 3] 2 _ = 1
      • prev [1, 2, 3] 1 _ = 3
      • prev [1, 2, 3, 2, 4] 2 _ = 1
      • prev [1, 2, 3, 4, 2] 2 _ = 1
      • prev [1, 1, 2] 1 _ = 2
      Equations
      • [].prev x x_1 = .elim
      • [y].prev x x_1 = y
      • (y :: z :: xs).prev x x_1 = if hx : x = y then (z :: xs).getLast else if x = z then y else (z :: xs).prev x
      Instances For
        @[simp]
        theorem List.next_singleton {α : Type u_1} [DecidableEq α] (x : α) (y : α) (h : x [y]) :
        [y].next x h = y
        @[simp]
        theorem List.prev_singleton {α : Type u_1} [DecidableEq α] (x : α) (y : α) (h : x [y]) :
        [y].prev x h = y
        theorem List.next_cons_cons_eq' {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hx : x = y) :
        (y :: z :: l).next x h = z
        @[simp]
        theorem List.next_cons_cons_eq {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (z : α) (h : x x :: z :: l) :
        (x :: z :: l).next x h = z
        theorem List.next_ne_head_ne_getLast {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : x l) (y : α) (h : x y :: l) (hy : x y) (hx : x (y :: l).getLast ) :
        (y :: l).next x h = l.next x
        theorem List.next_cons_concat {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) (hy : x y) (hx : xl) (h : optParam (x y :: l ++ [x]) ) :
        (y :: l ++ [x]).next x h = y
        theorem List.next_getLast_cons {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : x l) (y : α) (h : x y :: l) (hy : x y) (hx : x = (y :: l).getLast ) (hl : l.Nodup) :
        (y :: l).next x h = y
        theorem List.prev_getLast_cons' {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) (hxy : x y :: l) (hx : x = y) :
        (y :: l).prev x hxy = (y :: l).getLast
        @[simp]
        theorem List.prev_getLast_cons {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : x x :: l) :
        (x :: l).prev x h = (x :: l).getLast
        theorem List.prev_cons_cons_eq' {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hx : x = y) :
        (y :: z :: l).prev x h = (z :: l).getLast
        theorem List.prev_cons_cons_eq {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (z : α) (h : x x :: z :: l) :
        (x :: z :: l).prev x h = (z :: l).getLast
        theorem List.prev_cons_cons_of_ne' {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hy : x y) (hz : x = z) :
        (y :: z :: l).prev x h = y
        theorem List.prev_cons_cons_of_ne {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) (h : x y :: x :: l) (hy : x y) :
        (y :: x :: l).prev x h = y
        theorem List.prev_ne_cons_cons {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (y : α) (z : α) (h : x y :: z :: l) (hy : x y) (hz : x z) :
        (y :: z :: l).prev x h = (z :: l).prev x
        theorem List.next_mem {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : x l) :
        l.next x h l
        theorem List.prev_mem {α : Type u_1} [DecidableEq α] (l : List α) (x : α) (h : x l) :
        l.prev x h l
        theorem List.next_get {α : Type u_1} [DecidableEq α] (l : List α) (_h : l.Nodup) (i : Fin l.length) :
        l.next (l.get i) = l.get (i + 1) % l.length,
        @[deprecated List.next_get]
        theorem List.next_nthLe {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (n : ) (hn : n < l.length) :
        l.next (l.nthLe n hn) = l.nthLe ((n + 1) % l.length)
        theorem List.prev_nthLe {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (n : ) (hn : n < l.length) :
        l.prev (l.nthLe n hn) = l.nthLe ((n + (l.length - 1)) % l.length)
        theorem List.pmap_next_eq_rotate_one {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) :
        List.pmap l.next l = l.rotate 1
        theorem List.pmap_prev_eq_rotate_length_sub_one {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) :
        List.pmap l.prev l = l.rotate (l.length - 1)
        theorem List.prev_next {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (x : α) (hx : x l) :
        l.prev (l.next x hx) = x
        theorem List.next_prev {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (x : α) (hx : x l) :
        l.next (l.prev x hx) = x
        theorem List.prev_reverse_eq_next {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (x : α) (hx : x l) :
        l.reverse.prev x = l.next x hx
        theorem List.next_reverse_eq_prev {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (x : α) (hx : x l) :
        l.reverse.next x = l.prev x hx
        theorem List.isRotated_next_eq {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} (h : l ~r l') (hn : l.Nodup) {x : α} (hx : x l) :
        l.next x hx = l'.next x
        theorem List.isRotated_prev_eq {α : Type u_1} [DecidableEq α] {l : List α} {l' : List α} (h : l ~r l') (hn : l.Nodup) {x : α} (hx : x l) :
        l.prev x hx = l'.prev x
        def Cycle (α : Type u_1) :
        Type u_1

        Cycle α is the quotient of List α by cyclic permutation. Duplicates are allowed.

        Equations
        Instances For
          def Cycle.ofList {α : Type u_1} :
          List αCycle α

          The coercion from List α to Cycle α

          Equations
          Instances For
            instance Cycle.instCoeList {α : Type u_1} :
            Coe (List α) (Cycle α)
            Equations
            • Cycle.instCoeList = { coe := Cycle.ofList }
            @[simp]
            theorem Cycle.coe_eq_coe {α : Type u_1} {l₁ : List α} {l₂ : List α} :
            l₁ = l₂ l₁ ~r l₂
            @[simp]
            theorem Cycle.mk_eq_coe {α : Type u_1} (l : List α) :
            Quot.mk Setoid.r l = l
            @[simp]
            theorem Cycle.mk''_eq_coe {α : Type u_1} (l : List α) :
            theorem Cycle.coe_cons_eq_coe_append {α : Type u_1} (l : List α) (a : α) :
            (a :: l) = (l ++ [a])
            def Cycle.nil {α : Type u_1} :

            The unique empty cycle.

            Equations
            • Cycle.nil = []
            Instances For
              @[simp]
              theorem Cycle.coe_nil {α : Type u_1} :
              [] = Cycle.nil
              @[simp]
              theorem Cycle.coe_eq_nil {α : Type u_1} (l : List α) :
              l = Cycle.nil l = []

              For consistency with EmptyCollection (List α).

              Equations
              • Cycle.instEmptyCollection = { emptyCollection := Cycle.nil }
              @[simp]
              theorem Cycle.empty_eq {α : Type u_1} :
              = Cycle.nil
              instance Cycle.instInhabited {α : Type u_1} :
              Equations
              • Cycle.instInhabited = { default := Cycle.nil }
              theorem Cycle.induction_on {α : Type u_1} {C : Cycle αProp} (s : Cycle α) (H0 : C Cycle.nil) (HI : ∀ (a : α) (l : List α), C lC (a :: l)) :
              C s

              An induction principle for Cycle. Use as induction s.

              def Cycle.Mem {α : Type u_1} (a : α) (s : Cycle α) :

              For x : α, s : Cycle α, x ∈ s indicates that x occurs at least once in s.

              Equations
              Instances For
                instance Cycle.instMembership {α : Type u_1} :
                Equations
                • Cycle.instMembership = { mem := Cycle.Mem }
                @[simp]
                theorem Cycle.mem_coe_iff {α : Type u_1} {a : α} {l : List α} :
                a l a l
                @[simp]
                theorem Cycle.not_mem_nil {α : Type u_1} (a : α) :
                aCycle.nil
                instance Cycle.instDecidableEq {α : Type u_1} [DecidableEq α] :
                Equations
                instance Cycle.instDecidableMemOfDecidableEq {α : Type u_1} [DecidableEq α] (x : α) (s : Cycle α) :
                Equations
                def Cycle.reverse {α : Type u_1} (s : Cycle α) :

                Reverse a s : Cycle α by reversing the underlying List.

                Equations
                Instances For
                  @[simp]
                  theorem Cycle.reverse_coe {α : Type u_1} (l : List α) :
                  (l).reverse = l.reverse
                  @[simp]
                  theorem Cycle.mem_reverse_iff {α : Type u_1} {a : α} {s : Cycle α} :
                  a s.reverse a s
                  @[simp]
                  theorem Cycle.reverse_reverse {α : Type u_1} (s : Cycle α) :
                  s.reverse.reverse = s
                  @[simp]
                  theorem Cycle.reverse_nil {α : Type u_1} :
                  Cycle.nil.reverse = Cycle.nil
                  def Cycle.length {α : Type u_1} (s : Cycle α) :

                  The length of the s : Cycle α, which is the number of elements, counting duplicates.

                  Equations
                  Instances For
                    @[simp]
                    theorem Cycle.length_coe {α : Type u_1} (l : List α) :
                    (l).length = l.length
                    @[simp]
                    theorem Cycle.length_nil {α : Type u_1} :
                    Cycle.nil.length = 0
                    @[simp]
                    theorem Cycle.length_reverse {α : Type u_1} (s : Cycle α) :
                    s.reverse.length = s.length
                    def Cycle.Subsingleton {α : Type u_1} (s : Cycle α) :

                    A s : Cycle α that is at most one element.

                    Equations
                    • s.Subsingleton = (s.length 1)
                    Instances For
                      theorem Cycle.subsingleton_nil {α : Type u_1} :
                      Cycle.nil.Subsingleton
                      theorem Cycle.length_subsingleton_iff {α : Type u_1} {s : Cycle α} :
                      s.Subsingleton s.length 1
                      @[simp]
                      theorem Cycle.subsingleton_reverse_iff {α : Type u_1} {s : Cycle α} :
                      s.reverse.Subsingleton s.Subsingleton
                      theorem Cycle.Subsingleton.congr {α : Type u_1} {s : Cycle α} (h : s.Subsingleton) ⦃x : α (_hx : x s) ⦃y : α (_hy : y s) :
                      x = y
                      def Cycle.Nontrivial {α : Type u_1} (s : Cycle α) :

                      A s : Cycle α that is made up of at least two unique elements.

                      Equations
                      Instances For
                        @[simp]
                        theorem Cycle.nontrivial_coe_nodup_iff {α : Type u_1} {l : List α} (hl : l.Nodup) :
                        (l).Nontrivial 2 l.length
                        @[simp]
                        theorem Cycle.nontrivial_reverse_iff {α : Type u_1} {s : Cycle α} :
                        s.reverse.Nontrivial s.Nontrivial
                        theorem Cycle.length_nontrivial {α : Type u_1} {s : Cycle α} (h : s.Nontrivial) :
                        2 s.length
                        def Cycle.Nodup {α : Type u_1} (s : Cycle α) :

                        The s : Cycle α contains no duplicates.

                        Equations
                        Instances For
                          @[simp]
                          theorem Cycle.nodup_nil {α : Type u_1} :
                          Cycle.nil.Nodup
                          @[simp]
                          theorem Cycle.nodup_coe_iff {α : Type u_1} {l : List α} :
                          (l).Nodup l.Nodup
                          @[simp]
                          theorem Cycle.nodup_reverse_iff {α : Type u_1} {s : Cycle α} :
                          s.reverse.Nodup s.Nodup
                          theorem Cycle.Subsingleton.nodup {α : Type u_1} {s : Cycle α} (h : s.Subsingleton) :
                          s.Nodup
                          theorem Cycle.Nodup.nontrivial_iff {α : Type u_1} {s : Cycle α} (h : s.Nodup) :
                          s.Nontrivial ¬s.Subsingleton
                          def Cycle.toMultiset {α : Type u_1} (s : Cycle α) :

                          The s : Cycle α as a Multiset α.

                          Equations
                          Instances For
                            @[simp]
                            theorem Cycle.coe_toMultiset {α : Type u_1} (l : List α) :
                            (l).toMultiset = l
                            @[simp]
                            theorem Cycle.nil_toMultiset {α : Type u_1} :
                            Cycle.nil.toMultiset = 0
                            @[simp]
                            theorem Cycle.card_toMultiset {α : Type u_1} (s : Cycle α) :
                            Multiset.card s.toMultiset = s.length
                            @[simp]
                            theorem Cycle.toMultiset_eq_nil {α : Type u_1} {s : Cycle α} :
                            s.toMultiset = 0 s = Cycle.nil
                            def Cycle.map {α : Type u_1} {β : Type u_2} (f : αβ) :
                            Cycle αCycle β

                            The lift of list.map.

                            Equations
                            Instances For
                              @[simp]
                              theorem Cycle.map_nil {α : Type u_1} {β : Type u_2} (f : αβ) :
                              Cycle.map f Cycle.nil = Cycle.nil
                              @[simp]
                              theorem Cycle.map_coe {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                              Cycle.map f l = (List.map f l)
                              @[simp]
                              theorem Cycle.map_eq_nil {α : Type u_1} {β : Type u_2} (f : αβ) (s : Cycle α) :
                              Cycle.map f s = Cycle.nil s = Cycle.nil
                              @[simp]
                              theorem Cycle.mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {b : β} {s : Cycle α} :
                              b Cycle.map f s as, f a = b
                              def Cycle.lists {α : Type u_1} (s : Cycle α) :

                              The Multiset of lists that can make the cycle.

                              Equations
                              Instances For
                                @[simp]
                                theorem Cycle.lists_coe {α : Type u_1} (l : List α) :
                                (l).lists = l.cyclicPermutations
                                @[simp]
                                theorem Cycle.mem_lists_iff_coe_eq {α : Type u_1} {s : Cycle α} {l : List α} :
                                l s.lists l = s
                                @[simp]
                                theorem Cycle.lists_nil {α : Type u_1} :
                                Cycle.nil.lists = [[]]
                                @[irreducible]
                                def Cycle.decidableNontrivialCoe {α : Type u_1} [DecidableEq α] (l : List α) :
                                Decidable (l).Nontrivial

                                Auxiliary decidability algorithm for lists that contain at least two unique elements.

                                Equations
                                Instances For
                                  instance Cycle.instDecidableNontrivial {α : Type u_1} [DecidableEq α] {s : Cycle α} :
                                  Decidable s.Nontrivial
                                  Equations
                                  instance Cycle.instDecidableNodup {α : Type u_1} [DecidableEq α] {s : Cycle α} :
                                  Decidable s.Nodup
                                  Equations
                                  instance Cycle.fintypeNodupCycle {α : Type u_1} [DecidableEq α] [Fintype α] :
                                  Fintype { s : Cycle α // s.Nodup }
                                  Equations
                                  instance Cycle.fintypeNodupNontrivialCycle {α : Type u_1} [DecidableEq α] [Fintype α] :
                                  Fintype { s : Cycle α // s.Nodup s.Nontrivial }
                                  Equations
                                  def Cycle.toFinset {α : Type u_1} [DecidableEq α] (s : Cycle α) :

                                  The s : Cycle α as a Finset α.

                                  Equations
                                  • s.toFinset = s.toMultiset.toFinset
                                  Instances For
                                    @[simp]
                                    theorem Cycle.toFinset_toMultiset {α : Type u_1} [DecidableEq α] (s : Cycle α) :
                                    s.toMultiset.toFinset = s.toFinset
                                    @[simp]
                                    theorem Cycle.coe_toFinset {α : Type u_1} [DecidableEq α] (l : List α) :
                                    (l).toFinset = l.toFinset
                                    @[simp]
                                    theorem Cycle.nil_toFinset {α : Type u_1} [DecidableEq α] :
                                    Cycle.nil.toFinset =
                                    @[simp]
                                    theorem Cycle.toFinset_eq_nil {α : Type u_1} [DecidableEq α] {s : Cycle α} :
                                    s.toFinset = s = Cycle.nil
                                    def Cycle.next {α : Type u_1} [DecidableEq α] (s : Cycle α) (_hs : s.Nodup) (x : α) (_hx : x s) :
                                    α

                                    Given a s : Cycle α such that Nodup s, retrieve the next element after x ∈ s.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def Cycle.prev {α : Type u_1} [DecidableEq α] (s : Cycle α) (_hs : s.Nodup) (x : α) (_hx : x s) :
                                      α

                                      Given a s : Cycle α such that Nodup s, retrieve the previous element before x ∈ s.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem Cycle.prev_reverse_eq_next {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x s) :
                                        s.reverse.prev x = s.next hs x hx
                                        @[simp]
                                        theorem Cycle.prev_reverse_eq_next' {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.reverse.Nodup) (x : α) (hx : x s.reverse) :
                                        s.reverse.prev hs x hx = s.next x
                                        theorem Cycle.next_reverse_eq_prev {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x s) :
                                        s.reverse.next x = s.prev hs x hx
                                        @[simp]
                                        theorem Cycle.next_reverse_eq_prev' {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.reverse.Nodup) (x : α) (hx : x s.reverse) :
                                        s.reverse.next hs x hx = s.prev x
                                        @[simp]
                                        theorem Cycle.next_mem {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x s) :
                                        s.next hs x hx s
                                        theorem Cycle.prev_mem {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x s) :
                                        s.prev hs x hx s
                                        @[simp]
                                        theorem Cycle.prev_next {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x s) :
                                        s.prev hs (s.next hs x hx) = x
                                        @[simp]
                                        theorem Cycle.next_prev {α : Type u_1} [DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x s) :
                                        s.next hs (s.prev hs x hx) = x
                                        unsafe instance Cycle.instRepr {α : Type u_1} [Repr α] :
                                        Repr (Cycle α)

                                        We define a representation of concrete cycles, available when viewing them in a goal state or via #eval, when over representable types. For example, the cycle (2 1 4 3) will be shown as c[2, 1, 4, 3]. Two equal cycles may be printed differently if their internal representation is different.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        def Cycle.Chain {α : Type u_1} (r : ααProp) (c : Cycle α) :

                                        chain R s means that R holds between adjacent elements of s.

                                        chain R ([a, b, c] : Cycle α) ↔ R a b ∧ R b c ∧ R c a

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Cycle.Chain.nil {α : Type u_1} (r : ααProp) :
                                          Cycle.Chain r Cycle.nil
                                          @[simp]
                                          theorem Cycle.chain_coe_cons {α : Type u_1} (r : ααProp) (a : α) (l : List α) :
                                          Cycle.Chain r (a :: l) List.Chain r a (l ++ [a])
                                          theorem Cycle.chain_singleton {α : Type u_1} (r : ααProp) (a : α) :
                                          Cycle.Chain r [a] r a a
                                          theorem Cycle.chain_ne_nil {α : Type u_1} (r : ααProp) {l : List α} (hl : l []) :
                                          Cycle.Chain r l List.Chain r (l.getLast hl) l
                                          theorem Cycle.chain_map {α : Type u_1} {β : Type u_2} {r : ααProp} (f : βα) {s : Cycle β} :
                                          Cycle.Chain r (Cycle.map f s) Cycle.Chain (fun (a b : β) => r (f a) (f b)) s
                                          theorem Cycle.chain_range_succ (r : Prop) (n : ) :
                                          Cycle.Chain r (List.range n.succ) r n 0 m < n, r m m.succ
                                          theorem Cycle.Chain.imp {α : Type u_1} {s : Cycle α} {r₁ : ααProp} {r₂ : ααProp} (H : ∀ (a b : α), r₁ a br₂ a b) (p : Cycle.Chain r₁ s) :
                                          theorem Cycle.chain_mono {α : Type u_1} :
                                          Monotone Cycle.Chain

                                          As a function from a relation to a predicate, chain is monotonic.

                                          theorem Cycle.chain_of_pairwise {α : Type u_1} {r : ααProp} {s : Cycle α} :
                                          (as, bs, r a b)Cycle.Chain r s
                                          theorem Cycle.chain_iff_pairwise {α : Type u_1} {r : ααProp} {s : Cycle α} [IsTrans α r] :
                                          Cycle.Chain r s as, bs, r a b
                                          theorem Cycle.Chain.eq_nil_of_irrefl {α : Type u_1} {r : ααProp} {s : Cycle α} [IsTrans α r] [IsIrrefl α r] (h : Cycle.Chain r s) :
                                          s = Cycle.nil
                                          theorem Cycle.Chain.eq_nil_of_well_founded {α : Type u_1} {r : ααProp} {s : Cycle α} [IsWellFounded α r] (h : Cycle.Chain r s) :
                                          s = Cycle.nil
                                          theorem Cycle.forall_eq_of_chain {α : Type u_1} {r : ααProp} {s : Cycle α} [IsTrans α r] [IsAntisymm α r] (hs : Cycle.Chain r s) {a : α} {b : α} (ha : a s) (hb : b s) :
                                          a = b