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
    • One or more equations did not get rendered due to their size.
    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) :
      @[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) :
          @[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]