Documentation

Mathlib.Order.SuccPred.Limit

Successor and predecessor limits #

We define the predicate Order.IsSuccLimit for "successor 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.IsPredLimit analogously, and prove basic results.

TODO #

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

Successor limits #

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

A successor limit is a value that 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.

Equations
Instances For
    theorem Order.not_isSuccLimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
    ¬Order.IsSuccLimit a ∃ (b : α), b a
    @[simp]
    theorem Order.isSuccLimit_of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) :
    theorem IsMin.isSuccLimit {α : Type u_1} [Preorder α] {a : α} :
    theorem Order.IsSuccLimit.isMax {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] (h : Order.IsSuccLimit (Order.succ a)) :
    theorem Order.IsSuccLimit.succ_ne {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] [NoMaxOrder α] (h : Order.IsSuccLimit a) (b : α) :
    @[simp]
    theorem Order.isSuccLimit_of_succ_ne {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} (h : ∀ (b : α), Order.succ b a) :
    theorem Order.not_isSuccLimit_iff {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} :
    theorem Order.mem_range_succ_of_not_isSuccLimit {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} (h : ¬Order.IsSuccLimit a) :
    a Set.range Order.succ

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

    theorem Order.isSuccLimit_of_succ_lt {α : Type u_1} [PartialOrder α] [SuccOrder α] {b : α} (H : a < b, Order.succ a < b) :
    theorem Order.IsSuccLimit.succ_lt {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {b : α} (hb : Order.IsSuccLimit b) (ha : a < b) :
    theorem Order.IsSuccLimit.succ_lt_iff {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {b : α} (hb : Order.IsSuccLimit b) :
    Order.succ a < b a < b
    theorem Order.isSuccLimit_iff_succ_lt {α : Type u_1} [PartialOrder α] [SuccOrder α] {b : α} :
    noncomputable def Order.isSuccLimitRecOn {α : Type u_1} [PartialOrder α] [SuccOrder α] {C : αSort u_2} (b : α) (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) :
    C b

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

    Equations
    Instances For
      theorem Order.isSuccLimitRecOn_limit {α : Type u_1} [PartialOrder α] [SuccOrder α] {b : α} {C : αSort u_2} (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) (hb : Order.IsSuccLimit b) :
      Order.isSuccLimitRecOn b hs hl = hl b hb
      theorem Order.isSuccLimitRecOn_succ' {α : Type u_1} [PartialOrder α] [SuccOrder α] {C : αSort u_2} (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) {b : α} (hb : ¬IsMax b) :
      noncomputable def SuccOrder.limitRecOn {α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) {C : αSort u_2} [WellFoundedLT α] (H_succ : (a : α) → ¬IsMax aC aC (Order.succ a)) (H_lim : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) :
      C a

      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.limitRecOn_succ {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {C : αSort u_2} [WellFoundedLT α] (H_succ : (a : α) → ¬IsMax aC aC (Order.succ a)) (H_lim : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) (ha : ¬IsMax a) :
        SuccOrder.limitRecOn (Order.succ a) H_succ H_lim = H_succ a ha (SuccOrder.limitRecOn a H_succ H_lim)
        @[simp]
        theorem SuccOrder.limitRecOn_limit {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {C : αSort u_2} [WellFoundedLT α] (H_succ : (a : α) → ¬IsMax aC aC (Order.succ a)) (H_lim : (a : α) → Order.IsSuccLimit a((b : α) → b < aC b)C a) (ha : Order.IsSuccLimit a) :
        SuccOrder.limitRecOn a H_succ H_lim = H_lim a ha fun (x : α) (x_1 : x < a) => SuccOrder.limitRecOn x H_succ H_lim
        @[simp]
        theorem Order.isSuccLimitRecOn_succ {α : Type u_1} [PartialOrder α] [SuccOrder α] {C : αSort u_2} [NoMaxOrder α] (hs : (a : α) → ¬IsMax aC (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit aC a) (b : α) :
        theorem Order.isSuccLimit_iff_succ_ne {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [NoMaxOrder α] :
        Order.IsSuccLimit a ∀ (b : α), Order.succ b a
        @[simp]

        Predecessor limits #

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

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

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

        Equations
        Instances For
          theorem Order.not_isPredLimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
          ¬Order.IsPredLimit a ∃ (b : α), a b
          @[simp]
          theorem Order.isSuccLimit_toDual_iff {α : Type u_1} [LT α] {a : α} :
          Order.IsSuccLimit (OrderDual.toDual a) Order.IsPredLimit a
          @[simp]
          theorem Order.isPredLimit_toDual_iff {α : Type u_1} [LT α] {a : α} :
          Order.IsPredLimit (OrderDual.toDual a) Order.IsSuccLimit a
          theorem Order.isPredLimit.dual {α : Type u_1} [LT α] {a : α} :
          Order.IsPredLimit aOrder.IsSuccLimit (OrderDual.toDual a)

          Alias of the reverse direction of Order.isSuccLimit_toDual_iff.

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

          Alias of the reverse direction of Order.isPredLimit_toDual_iff.

          theorem IsMax.isPredLimit {α : Type u_1} [Preorder α] {a : α} :
          theorem Order.IsPredLimit.isMin {α : Type u_1} [Preorder α] {a : α} [PredOrder α] (h : Order.IsPredLimit (Order.pred a)) :
          theorem Order.IsPredLimit.pred_ne {α : Type u_1} [Preorder α] {a : α} [PredOrder α] [NoMinOrder α] (h : Order.IsPredLimit a) (b : α) :
          @[simp]
          theorem Order.isPredLimit_of_pred_ne {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} (h : ∀ (b : α), Order.pred b a) :
          theorem Order.not_isPredLimit_iff {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} :
          theorem Order.mem_range_pred_of_not_isPredLimit {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} (h : ¬Order.IsPredLimit a) :
          a Set.range Order.pred

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

          theorem Order.isPredLimit_of_pred_lt {α : Type u_1} [PartialOrder α] [PredOrder α] {b : α} (H : a > b, Order.pred a < b) :
          theorem Order.IsPredLimit.lt_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {b : α} (h : Order.IsPredLimit a) :
          a < ba < Order.pred b
          theorem Order.IsPredLimit.lt_pred_iff {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {b : α} (h : Order.IsPredLimit a) :
          a < Order.pred b a < b
          theorem Order.isPredLimit_iff_lt_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} :
          Order.IsPredLimit a ∀ ⦃b : α⦄, a < ba < Order.pred b
          noncomputable def Order.isPredLimitRecOn {α : Type u_1} [PartialOrder α] [PredOrder α] {C : αSort u_2} (b : α) (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) :
          C b

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

          Equations
          Instances For
            theorem Order.isPredLimitRecOn_limit {α : Type u_1} [PartialOrder α] [PredOrder α] {b : α} {C : αSort u_2} (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) (hb : Order.IsPredLimit b) :
            Order.isPredLimitRecOn b hs hl = hl b hb
            theorem Order.isPredLimitRecOn_pred' {α : Type u_1} [PartialOrder α] [PredOrder α] {C : αSort u_2} (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) {b : α} (hb : ¬IsMin b) :
            noncomputable def PredOrder.limitRecOn {α : Type u_1} [PartialOrder α] [PredOrder α] (a : α) {C : αSort u_2} [WellFoundedGT α] (H_pred : (a : α) → ¬IsMin aC aC (Order.pred a)) (H_lim : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) :
            C a

            Recursion principle on a well-founded partial PredOrder.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem PredOrder.limitRecOn_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {C : αSort u_2} [WellFoundedGT α] (H_pred : (a : α) → ¬IsMin aC aC (Order.pred a)) (H_lim : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) (ha : ¬IsMin a) :
              PredOrder.limitRecOn (Order.pred a) H_pred H_lim = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
              @[simp]
              theorem PredOrder.limitRecOn_limit {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {C : αSort u_2} [WellFoundedGT α] (H_pred : (a : α) → ¬IsMin aC aC (Order.pred a)) (H_lim : (a : α) → Order.IsPredLimit a((b : α) → b > aC b)C a) (ha : Order.IsPredLimit a) :
              PredOrder.limitRecOn a H_pred H_lim = H_lim a ha fun (x : α) (x_1 : x > a) => PredOrder.limitRecOn x H_pred H_lim
              @[simp]
              theorem Order.isPredLimitRecOn_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {C : αSort u_2} [NoMinOrder α] (hs : (a : α) → ¬IsMin aC (Order.pred a)) (hl : (a : α) → Order.IsPredLimit aC a) (b : α) :
              @[simp]