Documentation

Mathlib.Order.SuccPred.Limit

Successor and predecessor limits #

We define the predicate Order.IsSuccPrelimit for "successor pre-limits", values that don't cover any others. They are so named since they can't be the successors of anything smaller. We define Order.IsPredPrelimit analogously, and prove basic results.

For some applications, it is desirable to exclude minimal elements from being successor limits, or maximal elements from being predecessor limits. As such, we also provide Order.IsSuccLimit and Order.IsPredLimit, which exclude these cases.

TODO #

The plan is to eventually replace Ordinal.IsLimit and Cardinal.IsLimit with the common predicate Order.IsSuccLimit.

Successor limits #

def Order.IsSuccPrelimit {α : Type u_1} [LT α] (a : α) :

A successor pre-limit is a value that doesn't cover any other.

It's so named because in a successor order, a successor pre-limit can't be the successor of anything smaller.

Use IsSuccLimit if you want to exclude the case of a minimal element.

Equations
Instances For
    theorem Order.not_isSuccPrelimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
    ¬Order.IsSuccPrelimit a ∃ (b : α), b a
    @[deprecated Order.not_isSuccPrelimit_iff_exists_covBy]
    theorem Order.not_isSuccLimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
    ¬Order.IsSuccPrelimit a ∃ (b : α), b a

    Alias of Order.not_isSuccPrelimit_iff_exists_covBy.

    @[simp]
    @[deprecated Order.isSuccPrelimit_of_dense]
    theorem Order.isSuccLimit_of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) :

    Alias of Order.isSuccPrelimit_of_dense.

    def Order.IsSuccLimit {α : Type u_1} [Preorder α] (a : α) :

    A successor limit is a value that isn't minimal and doesn't cover any other.

    It's so named because in a successor order, a successor limit can't be the successor of anything smaller.

    This previously allowed the element to be minimal. This usage is now covered by IsSuccPrelimit.

    Equations
    Instances For
      theorem Order.IsSuccLimit.not_isMin {α : Type u_1} {a : α} [Preorder α] (h : Order.IsSuccLimit a) :
      theorem IsMin.not_isSuccLimit {α : Type u_1} {a : α} [Preorder α] (h : IsMin a) :
      theorem IsMin.isSuccPrelimit {α : Type u_1} {a : α} [Preorder α] :
      @[deprecated IsMin.isSuccPrelimit]
      theorem IsMin.isSuccLimit {α : Type u_1} {a : α} [Preorder α] :

      Alias of IsMin.isSuccPrelimit.

      theorem Order.IsSuccLimit.ne_bot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] (h : Order.IsSuccLimit a) :
      @[deprecated Order.isSuccPrelimit_bot]

      Alias of Order.isSuccPrelimit_bot.

      theorem Order.IsSuccLimit.isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : Order.IsSuccLimit (Order.succ a)) :
      theorem Order.IsSuccPrelimit.succ_ne {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : Order.IsSuccPrelimit a) (b : α) :
      theorem Order.IsSuccLimit.succ_ne {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : Order.IsSuccLimit a) (b : α) :
      @[simp]
      @[deprecated Order.IsSuccPrelimit.isMin_of_noMax]

      Alias of Order.IsSuccPrelimit.isMin_of_noMax.

      @[deprecated Order.isSuccPrelimit_iff_of_noMax]

      Alias of Order.isSuccPrelimit_iff_of_noMax.

      theorem Order.isSuccPrelimit_of_succ_ne {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ∀ (b : α), Order.succ b a) :
      @[deprecated Order.isSuccPrelimit_of_succ_ne]
      theorem Order.isSuccLimit_of_succ_ne {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ∀ (b : α), Order.succ b a) :

      Alias of Order.isSuccPrelimit_of_succ_ne.

      theorem Order.not_isSuccPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] :

      See not_isSuccPrelimit_iff for a version that states that a is a successor of a value other than itself.

      @[deprecated Order.mem_range_succ_of_not_isSuccPrelimit]
      theorem Order.mem_range_succ_of_not_isSuccLimit {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ¬Order.IsSuccPrelimit a) :
      a Set.range Order.succ

      Alias of Order.mem_range_succ_of_not_isSuccPrelimit.


      See not_isSuccPrelimit_iff for a version that states that a is a successor of a value other than itself.

      @[deprecated Order.mem_range_succ_or_isSuccPrelimit]

      Alias of Order.mem_range_succ_or_isSuccPrelimit.

      theorem Order.isSuccPrelimit_of_succ_lt {α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] (H : a < b, Order.succ a < b) :
      @[deprecated Order.isSuccPrelimit_of_succ_lt]
      theorem Order.isSuccLimit_of_succ_lt {α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] (H : a < b, Order.succ a < b) :

      Alias of Order.isSuccPrelimit_of_succ_lt.

      theorem Order.IsSuccPrelimit.succ_lt {α : Type u_1} {a : α} {b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccPrelimit b) (ha : a < b) :
      theorem Order.IsSuccLimit.succ_lt {α : Type u_1} {a : α} {b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) (ha : a < b) :
      theorem Order.IsSuccPrelimit.succ_lt_iff {α : Type u_1} {a : α} {b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccPrelimit b) :
      Order.succ a < b a < b
      theorem Order.IsSuccLimit.succ_lt_iff {α : Type u_1} {a : α} {b : α} [PartialOrder α] [SuccOrder α] (hb : Order.IsSuccLimit b) :
      Order.succ a < b a < b
      @[deprecated Order.isSuccPrelimit_iff_succ_lt]
      theorem Order.isSuccLimit_iff_succ_lt {α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] :

      Alias of Order.isSuccPrelimit_iff_succ_lt.

      @[deprecated Order.isSuccPrelimit_iff_succ_ne]
      theorem Order.isSuccLimit_iff_succ_ne {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] :

      Alias of Order.isSuccPrelimit_iff_succ_ne.

      @[deprecated Order.not_isSuccPrelimit_iff']
      theorem Order.not_isSuccLimit_iff' {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] :

      Alias of Order.not_isSuccPrelimit_iff'.

      @[simp]
      theorem Order.IsSuccPrelimit.le_iff_forall_le {α : Type u_1} {a : α} {b : α} [LinearOrder α] (h : Order.IsSuccPrelimit a) :
      a b c < a, c b
      theorem Order.IsSuccPrelimit.lt_iff_exists_lt {α : Type u_1} {a : α} {b : α} [LinearOrder α] (h : Order.IsSuccPrelimit b) :
      a < b c < b, a < c

      Predecessor limits #

      def Order.IsPredPrelimit {α : Type u_1} [LT α] (a : α) :

      A predecessor pre-limit is a value that isn't covered by any other.

      It's so named because in a predecessor order, a predecessor pre-limit can't be the predecessor of anything smaller.

      Use IsPredLimit to exclude the case of a maximal element.

      Equations
      Instances For
        theorem Order.not_isPredPrelimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
        ¬Order.IsPredPrelimit a ∃ (b : α), a b
        @[deprecated Order.not_isPredPrelimit_iff_exists_covBy]
        theorem Order.not_isPredLimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
        ¬Order.IsPredPrelimit a ∃ (b : α), a b

        Alias of Order.not_isPredPrelimit_iff_exists_covBy.

        @[deprecated Order.isPredPrelimit_of_dense]
        theorem Order.isPredLimit_of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) :

        Alias of Order.isPredPrelimit_of_dense.

        @[simp]
        theorem Order.isSuccPrelimit_toDual_iff {α : Type u_1} {a : α} [LT α] :
        @[simp]
        theorem Order.isPredPrelimit_toDual_iff {α : Type u_1} {a : α} [LT α] :
        theorem Order.IsPredPrelimit.dual {α : Type u_1} {a : α} [LT α] :
        Order.IsPredPrelimit aOrder.IsSuccPrelimit (OrderDual.toDual a)

        Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.

        theorem Order.IsSuccPrelimit.dual {α : Type u_1} {a : α} [LT α] :
        Order.IsSuccPrelimit aOrder.IsPredPrelimit (OrderDual.toDual a)

        Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.

        @[deprecated Order.IsPredPrelimit.dual]
        theorem Order.isPredLimit.dual {α : Type u_1} {a : α} [LT α] :
        Order.IsPredPrelimit aOrder.IsSuccPrelimit (OrderDual.toDual a)

        Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.


        Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.

        @[deprecated Order.IsSuccPrelimit.dual]
        theorem Order.isSuccLimit.dual {α : Type u_1} {a : α} [LT α] :
        Order.IsSuccPrelimit aOrder.IsPredPrelimit (OrderDual.toDual a)

        Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.


        Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.

        def Order.IsPredLimit {α : Type u_1} [Preorder α] (a : α) :

        A predecessor limit is a value that isn't maximal and doesn't cover any other.

        It's so named because in a predecessor order, a predecessor limit can't be the predecessor of anything larger.

        This previously allowed the element to be maximal. This usage is now covered by IsPredPreLimit.

        Equations
        Instances For
          theorem Order.IsPredLimit.not_isMax {α : Type u_1} {a : α} [Preorder α] (h : Order.IsPredLimit a) :
          @[simp]
          theorem Order.isSuccLimit_toDual_iff {α : Type u_1} {a : α} [Preorder α] :
          Order.IsSuccLimit (OrderDual.toDual a) Order.IsPredLimit a
          @[simp]
          theorem Order.isPredLimit_toDual_iff {α : Type u_1} {a : α} [Preorder α] :
          Order.IsPredLimit (OrderDual.toDual a) Order.IsSuccLimit a
          theorem Order.IsPredLimit.dual {α : Type u_1} {a : α} [Preorder α] :
          Order.IsPredLimit aOrder.IsSuccLimit (OrderDual.toDual a)

          Alias of the reverse direction of Order.isSuccLimit_toDual_iff.

          theorem Order.IsSuccLimit.dual {α : Type u_1} {a : α} [Preorder α] :
          Order.IsSuccLimit aOrder.IsPredLimit (OrderDual.toDual a)

          Alias of the reverse direction of Order.isPredLimit_toDual_iff.

          theorem IsMax.not_isPredLimit {α : Type u_1} {a : α} [Preorder α] (h : IsMax a) :
          theorem IsMax.isPredPrelimit {α : Type u_1} {a : α} [Preorder α] :
          @[deprecated IsMax.isPredPrelimit]
          theorem IsMax.isPredLimit {α : Type u_1} {a : α} [Preorder α] :

          Alias of IsMax.isPredPrelimit.

          @[deprecated Order.isPredPrelimit_top]

          Alias of Order.isPredPrelimit_top.

          theorem Order.IsPredLimit.ne_top {α : Type u_1} {a : α} [Preorder α] [OrderTop α] (h : Order.IsPredLimit a) :
          theorem Order.IsPredLimit.isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (h : Order.IsPredLimit (Order.pred a)) :
          theorem Order.IsPredPrelimit.pred_ne {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [NoMinOrder α] (h : Order.IsPredPrelimit a) (b : α) :
          theorem Order.IsPredLimit.pred_ne {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [NoMinOrder α] (h : Order.IsPredLimit a) (b : α) :
          @[simp]
          @[deprecated Order.IsPredPrelimit.isMax_of_noMin]

          Alias of Order.IsPredPrelimit.isMax_of_noMin.

          @[deprecated Order.isPredPrelimit_iff_of_noMin]

          Alias of Order.isPredPrelimit_iff_of_noMin.

          theorem Order.isPredPrelimit_of_pred_ne {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (h : ∀ (b : α), Order.pred b a) :
          @[deprecated Order.isPredPrelimit_of_pred_ne]
          theorem Order.isPredLimit_of_pred_ne {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (h : ∀ (b : α), Order.pred b a) :

          Alias of Order.isPredPrelimit_of_pred_ne.

          theorem Order.not_isPredPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] :

          See not_isPredPrelimit_iff for a version that states that a is a successor of a value other than itself.

          @[deprecated Order.mem_range_pred_of_not_isPredPrelimit]
          theorem Order.mem_range_pred_of_not_isPredLimit {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (h : ¬Order.IsPredPrelimit a) :
          a Set.range Order.pred

          Alias of Order.mem_range_pred_of_not_isPredPrelimit.


          See not_isPredPrelimit_iff for a version that states that a is a successor of a value other than itself.

          @[deprecated Order.mem_range_pred_or_isPredPrelimit]

          Alias of Order.mem_range_pred_or_isPredPrelimit.

          theorem Order.isPredPrelimit_of_pred_lt {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (H : b > a, a < Order.pred b) :
          @[deprecated Order.isPredPrelimit_of_pred_lt]
          theorem Order.isPredLimit_of_pred_lt {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (H : b > a, a < Order.pred b) :

          Alias of Order.isPredPrelimit_of_pred_lt.

          theorem Order.IsPredPrelimit.lt_pred {α : Type u_1} {a : α} {b : α} [PartialOrder α] [PredOrder α] (ha : Order.IsPredPrelimit a) (hb : a < b) :
          theorem Order.IsPredLimit.lt_pred {α : Type u_1} {a : α} {b : α} [PartialOrder α] [PredOrder α] (ha : Order.IsPredLimit a) (hb : a < b) :
          theorem Order.IsPredPrelimit.lt_pred_iff {α : Type u_1} {a : α} {b : α} [PartialOrder α] [PredOrder α] (ha : Order.IsPredPrelimit a) :
          a < Order.pred b a < b
          theorem Order.IsPredLimit.lt_pred_iff {α : Type u_1} {a : α} {b : α} [PartialOrder α] [PredOrder α] (ha : Order.IsPredLimit a) :
          a < Order.pred b a < b
          @[deprecated Order.isPredPrelimit_iff_lt_pred]
          theorem Order.isPredLimit_iff_lt_pred {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] :

          Alias of Order.isPredPrelimit_iff_lt_pred.

          @[deprecated Order.IsPredPrelimit.isMax]
          theorem Order.IsPredLimit.isMax {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (h : Order.IsPredPrelimit a) :

          Alias of Order.IsPredPrelimit.isMax.

          @[simp]
          theorem Order.IsPredPrelimit.le_iff_forall_le {α : Type u_1} {a : α} {b : α} [LinearOrder α] (h : Order.IsPredPrelimit a) :
          b a ∀ ⦃c : α⦄, a < cb c
          theorem Order.IsPredPrelimit.lt_iff_exists_lt {α : Type u_1} {a : α} {b : α} [LinearOrder α] (h : Order.IsPredPrelimit b) :
          b < a ∃ (c : α), b < c c < a

          Induction principles #

          noncomputable def Order.isSuccPrelimitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) :
          C b

          A value can be built by building it on successors and successor pre-limits.

          Equations
          Instances For
            theorem Order.isSuccPrelimitRecOn_of_isSuccPrelimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) (hb : Order.IsSuccPrelimit b) :
            @[deprecated Order.isSuccPrelimitRecOn_of_isSuccPrelimit]
            theorem Order.isSuccLimitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) (hb : Order.IsSuccPrelimit b) :

            Alias of Order.isSuccPrelimitRecOn_of_isSuccPrelimit.

            @[deprecated Order.isSuccPrelimitRecOn_of_isSuccPrelimit]
            theorem Order.isSuccPrelimitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) (hb : Order.IsSuccPrelimit b) :

            Alias of Order.isSuccPrelimitRecOn_of_isSuccPrelimit.

            theorem Order.isSuccPrelimitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) (hb : ¬IsMax b) :
            @[deprecated Order.isSuccPrelimitRecOn_succ_of_not_isMax]
            theorem Order.isSuccLimitRecOn_succ' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) (hb : ¬IsMax b) :

            Alias of Order.isSuccPrelimitRecOn_succ_of_not_isMax.

            @[deprecated Order.isSuccPrelimitRecOn_succ_of_not_isMax]
            theorem Order.isSuccPrelimitRecOn_succ' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) (hb : ¬IsMax b) :

            Alias of Order.isSuccPrelimitRecOn_succ_of_not_isMax.

            @[simp]
            theorem Order.isSuccPrelimitRecOn_succ {α : Type u_1} {C : αSort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit aC a) [NoMaxOrder α] (b : α) :
            noncomputable def Order.isPredPrelimitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) :
            C b

            A value can be built by building it on predecessors and predecessor pre-limits.

            Equations
            Instances For
              theorem Order.isPredPrelimitRecOn_of_isPredPrelimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) (hb : Order.IsPredPrelimit b) :
              @[deprecated Order.isPredPrelimitRecOn_of_isPredPrelimit]
              theorem Order.isPredLimitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) (hb : Order.IsPredPrelimit b) :

              Alias of Order.isPredPrelimitRecOn_of_isPredPrelimit.

              @[deprecated Order.isPredPrelimitRecOn_of_isPredPrelimit]
              theorem Order.isPredPrelimitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) (hb : Order.IsPredPrelimit b) :

              Alias of Order.isPredPrelimitRecOn_of_isPredPrelimit.

              theorem Order.isPredPrelimitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) (hb : ¬IsMin b) :
              @[deprecated Order.isPredPrelimitRecOn_pred_of_not_isMin]
              theorem Order.isPredLimitRecOn_pred' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) (hb : ¬IsMin b) :

              Alias of Order.isPredPrelimitRecOn_pred_of_not_isMin.

              @[deprecated Order.isPredPrelimitRecOn_pred_of_not_isMin]
              theorem Order.isPredPrelimitRecOn_pred' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) (hb : ¬IsMin b) :

              Alias of Order.isPredPrelimitRecOn_pred_of_not_isMin.

              @[simp]
              theorem Order.isPredPrelimitRecOn_pred {α : Type u_1} {C : αSort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit aC a) [NoMinOrder α] (b : α) :
              noncomputable def Order.isSuccLimitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [SuccOrder α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) :
              C b

              A value can be built by building it on minimal elements, successors, and successor limits.

              Equations
              Instances For
                @[simp]
                theorem Order.isSuccLimitRecOn_of_isSuccLimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) (hb : Order.IsSuccLimit b) :
                Order.isSuccLimitRecOn b hm hs hl = hl b hb
                theorem Order.isSuccLimitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) (hb : ¬IsMax b) :
                Order.isSuccLimitRecOn (Order.succ b) hm hs hl = hs b hb
                @[simp]
                theorem Order.isSuccLimitRecOn_succ {α : Type u_1} {C : αSort u_2} [LinearOrder α] [SuccOrder α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) [NoMaxOrder α] (b : α) :
                Order.isSuccLimitRecOn (Order.succ b) hm hs hl = hs b
                theorem Order.isSuccLimitRecOn_of_isMin {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) (hb : IsMin b) :
                Order.isSuccLimitRecOn b hm hs hl = hm b hb
                noncomputable def Order.isPredLimitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [PredOrder α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) :
                C b

                A value can be built by building it on maximal elements, predecessors, and predecessor limits.

                Equations
                Instances For
                  @[simp]
                  theorem Order.isPredLimitRecOn_of_isPredLimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) (hb : Order.IsPredLimit b) :
                  Order.isPredLimitRecOn b hm hs hl = hl b hb
                  theorem Order.isPredLimitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) (hb : ¬IsMin b) :
                  Order.isPredLimitRecOn (Order.pred b) hm hs hl = hs b hb
                  @[simp]
                  theorem Order.isPredLimitRecOn_pred {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) [NoMinOrder α] :
                  Order.isPredLimitRecOn (Order.pred b) hm hs hl = hs b
                  theorem Order.isPredLimitRecOn_of_isMax {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) (hb : IsMax b) :
                  Order.isPredLimitRecOn b hm hs hl = hm b hb
                  noncomputable def SuccOrder.prelimitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) :
                  C b

                  Recursion principle on a well-founded partial SuccOrder.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem SuccOrder.prelimitRecOn_of_isSuccPrelimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) (hb : Order.IsSuccPrelimit b) :
                    SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl
                    @[deprecated SuccOrder.prelimitRecOn_of_isSuccPrelimit]
                    theorem SuccOrder.limitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) (hb : Order.IsSuccPrelimit b) :
                    SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl

                    Alias of SuccOrder.prelimitRecOn_of_isSuccPrelimit.

                    @[deprecated SuccOrder.prelimitRecOn_of_isSuccPrelimit]
                    theorem SuccOrder.prelimitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) (hb : Order.IsSuccPrelimit b) :
                    SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl

                    Alias of SuccOrder.prelimitRecOn_of_isSuccPrelimit.

                    theorem SuccOrder.prelimitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) (hb : ¬IsMax b) :
                    @[deprecated SuccOrder.prelimitRecOn_succ_of_not_isMax]
                    theorem SuccOrder.limitRecOn_succ' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) (hb : ¬IsMax b) :

                    Alias of SuccOrder.prelimitRecOn_succ_of_not_isMax.

                    @[deprecated SuccOrder.prelimitRecOn_succ_of_not_isMax]
                    theorem SuccOrder.prelimitRecOn_succ' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) (hb : ¬IsMax b) :

                    Alias of SuccOrder.prelimitRecOn_succ_of_not_isMax.

                    @[simp]
                    theorem SuccOrder.prelimitRecOn_succ {α : Type u_1} {C : αSort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a((b : α) → b < aC b)C a) [NoMaxOrder α] (b : α) :
                    noncomputable def SuccOrder.limitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) :
                    C b

                    Recursion principle on a well-founded partial SuccOrder, separating out the case of a minimal element.

                    Equations
                    Instances For
                      @[simp]
                      theorem SuccOrder.limitRecOn_isMin {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) (hb : IsMin b) :
                      SuccOrder.limitRecOn b hm hs hl = hm b hb
                      @[simp]
                      theorem SuccOrder.limitRecOn_of_isSuccLimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) (hb : Order.IsSuccLimit b) :
                      SuccOrder.limitRecOn b hm hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.limitRecOn x hm hs hl
                      theorem SuccOrder.limitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) (hb : ¬IsMax b) :
                      SuccOrder.limitRecOn (Order.succ b) hm hs hl = hs b hb (SuccOrder.limitRecOn b hm hs hl)
                      @[simp]
                      theorem SuccOrder.limitRecOn_succ {α : Type u_1} {C : αSort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin aC a) (hs : (a : α) → ¬IsMax aC aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) [NoMaxOrder α] (b : α) :
                      SuccOrder.limitRecOn (Order.succ b) hm hs hl = hs b (SuccOrder.limitRecOn b hm hs hl)
                      noncomputable def PredOrder.prelimitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) :
                      C b

                      Recursion principle on a well-founded partial PredOrder.

                      Equations
                      Instances For
                        @[simp]
                        theorem PredOrder.prelimitRecOn_of_isPredPrelimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) (hb : Order.IsPredPrelimit b) :
                        PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl
                        @[deprecated PredOrder.prelimitRecOn_of_isPredPrelimit]
                        theorem PredOrder.limitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) (hb : Order.IsPredPrelimit b) :
                        PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl

                        Alias of PredOrder.prelimitRecOn_of_isPredPrelimit.

                        @[deprecated PredOrder.prelimitRecOn_of_isPredPrelimit]
                        theorem PredOrder.prelimitRecOn_limit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) (hb : Order.IsPredPrelimit b) :
                        PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl

                        Alias of PredOrder.prelimitRecOn_of_isPredPrelimit.

                        theorem PredOrder.prelimitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) (hb : ¬IsMin b) :
                        @[deprecated PredOrder.prelimitRecOn_pred_of_not_isMin]
                        theorem PredOrder.limitRecOn_pred' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) (hb : ¬IsMin b) :

                        Alias of PredOrder.prelimitRecOn_pred_of_not_isMin.

                        @[deprecated PredOrder.prelimitRecOn_pred_of_not_isMin]
                        theorem PredOrder.prelimitRecOn_pred' {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) (hb : ¬IsMin b) :

                        Alias of PredOrder.prelimitRecOn_pred_of_not_isMin.

                        @[simp]
                        theorem PredOrder.prelimitRecOn_pred {α : Type u_1} {C : αSort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a((b : α) → b > aC b)C a) [NoMinOrder α] (b : α) :
                        noncomputable def PredOrder.limitRecOn {α : Type u_1} (b : α) {C : αSort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) :
                        C b

                        Recursion principle on a well-founded partial PredOrder, separating out the case of a maximal element.

                        Equations
                        Instances For
                          @[simp]
                          theorem PredOrder.limitRecOn_isMax {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) (hb : IsMax b) :
                          PredOrder.limitRecOn b hm hs hl = hm b hb
                          @[simp]
                          theorem PredOrder.limitRecOn_of_isPredLimit {α : Type u_1} {b : α} {C : αSort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) (hb : Order.IsPredLimit b) :
                          PredOrder.limitRecOn b hm hs hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.limitRecOn x hm hs hl
                          theorem PredOrder.limitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : αSort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) (hb : ¬IsMin b) :
                          PredOrder.limitRecOn (Order.pred b) hm hs hl = hs b hb (PredOrder.limitRecOn b hm hs hl)
                          @[simp]
                          theorem PredOrder.limitRecOn_pred {α : Type u_1} {C : αSort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax aC a) (hs : (a : α) → ¬IsMin aC aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) [NoMinOrder α] (b : α) :
                          PredOrder.limitRecOn (Order.pred b) hm hs hl = hs b (PredOrder.limitRecOn b hm hs hl)