# 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 : α) :
∃ (b : α), b a
@[simp]
theorem Order.isSuccLimit_of_dense {α : Type u_1} [LT α] [] (a : α) :
theorem IsMin.isSuccLimit {α : Type u_1} [] {a : α} :
theorem Order.isSuccLimit_bot {α : Type u_1} [] [] :
theorem Order.IsSuccLimit.isMax {α : Type u_1} [] {a : α} [] (h : ) :
theorem Order.not_isSuccLimit_succ_of_not_isMax {α : Type u_1} [] {a : α} [] (ha : ¬) :
theorem Order.IsSuccLimit.succ_ne {α : Type u_1} [] {a : α} [] [] (h : ) (b : α) :
a
@[simp]
theorem Order.not_isSuccLimit_succ {α : Type u_1} [] [] [] (a : α) :
theorem Order.IsSuccLimit.isMin_of_noMax {α : Type u_1} [] {a : α} [] [] (h : ) :
@[simp]
theorem Order.isSuccLimit_iff_of_noMax {α : Type u_1} [] {a : α} [] [] :
theorem Order.not_isSuccLimit_of_noMax {α : Type u_1} [] {a : α} [] [] [] :
theorem Order.isSuccLimit_of_succ_ne {α : Type u_1} [] [] {a : α} (h : ∀ (b : α), a) :
theorem Order.not_isSuccLimit_iff {α : Type u_1} [] [] {a : α} :
∃ (b : α), ¬ = a
theorem Order.mem_range_succ_of_not_isSuccLimit {α : Type u_1} [] [] {a : α} (h : ) :
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} [] [] {b : α} (H : a < b, < b) :
theorem Order.IsSuccLimit.succ_lt {α : Type u_1} [] [] {a : α} {b : α} (hb : ) (ha : a < b) :
< b
theorem Order.IsSuccLimit.succ_lt_iff {α : Type u_1} [] [] {a : α} {b : α} (hb : ) :
< b a < b
theorem Order.isSuccLimit_iff_succ_lt {α : Type u_1} [] [] {b : α} :
a < b, < b
noncomputable def Order.isSuccLimitRecOn {α : Type u_1} [] [] {C : αSort u_2} (b : α) (hs : (a : α) → ¬C ()) (hl : (a : α) → C a) :
C b

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

Equations
• = if hb : then hl b hb else let_fun H := ; .mpr (hs () )
Instances For
theorem Order.isSuccLimitRecOn_limit {α : Type u_1} [] [] {b : α} {C : αSort u_2} (hs : (a : α) → ¬C ()) (hl : (a : α) → C a) (hb : ) :
= hl b hb
theorem Order.isSuccLimitRecOn_succ' {α : Type u_1} [] [] {C : αSort u_2} (hs : (a : α) → ¬C ()) (hl : (a : α) → C a) {b : α} (hb : ¬) :
Order.isSuccLimitRecOn () hs hl = hs b hb
noncomputable def SuccOrder.limitRecOn {α : Type u_1} [] [] (a : α) {C : αSort u_2} [] (H_succ : (a : α) → ¬C aC ()) (H_lim : (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} [] [] {a : α} {C : αSort u_2} [] (H_succ : (a : α) → ¬C aC ()) (H_lim : (a : α) → ((b : α) → b < aC b)C a) (ha : ¬) :
SuccOrder.limitRecOn () H_succ H_lim = H_succ a ha (SuccOrder.limitRecOn a H_succ H_lim)
@[simp]
theorem SuccOrder.limitRecOn_limit {α : Type u_1} [] [] {a : α} {C : αSort u_2} [] (H_succ : (a : α) → ¬C aC ()) (H_lim : (a : α) → ((b : α) → b < aC b)C a) (ha : ) :
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} [] [] {C : αSort u_2} [] (hs : (a : α) → ¬C ()) (hl : (a : α) → C a) (b : α) :
Order.isSuccLimitRecOn () hs hl = hs b
theorem Order.isSuccLimit_iff_succ_ne {α : Type u_1} [] [] {a : α} [] :
∀ (b : α), a
theorem Order.not_isSuccLimit_iff' {α : Type u_1} [] [] {a : α} [] :
a Set.range Order.succ
theorem Order.IsSuccLimit.isMin {α : Type u_1} [] [] {a : α} (h : ) :
@[simp]
theorem Order.isSuccLimit_iff {α : Type u_1} [] [] {a : α} :
theorem Order.not_isSuccLimit {α : Type u_1} [] [] {a : α} [] :

### 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 : α) :
∃ (b : α), a b
theorem Order.isPredLimit_of_dense {α : Type u_1} [LT α] [] (a : α) :
@[simp]
theorem Order.isSuccLimit_toDual_iff {α : Type u_1} [LT α] {a : α} :
Order.IsSuccLimit (OrderDual.toDual a)
@[simp]
theorem Order.isPredLimit_toDual_iff {α : Type u_1} [LT α] {a : α} :
Order.IsPredLimit (OrderDual.toDual a)
theorem Order.isPredLimit.dual {α : Type u_1} [LT α] {a : α} :
Order.IsSuccLimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isSuccLimit_toDual_iff.

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

Alias of the reverse direction of Order.isPredLimit_toDual_iff.

theorem IsMax.isPredLimit {α : Type u_1} [] {a : α} :
theorem Order.isPredLimit_top {α : Type u_1} [] [] :
theorem Order.IsPredLimit.isMin {α : Type u_1} [] {a : α} [] (h : ) :
theorem Order.not_isPredLimit_pred_of_not_isMin {α : Type u_1} [] {a : α} [] (ha : ¬) :
theorem Order.IsPredLimit.pred_ne {α : Type u_1} [] {a : α} [] [] (h : ) (b : α) :
a
@[simp]
theorem Order.not_isPredLimit_pred {α : Type u_1} [] [] [] (a : α) :
theorem Order.IsPredLimit.isMax_of_noMin {α : Type u_1} [] {a : α} [] [] (h : ) :
@[simp]
theorem Order.isPredLimit_iff_of_noMin {α : Type u_1} [] {a : α} [] [] :
theorem Order.not_isPredLimit_of_noMin {α : Type u_1} [] {a : α} [] [] [] :
theorem Order.isPredLimit_of_pred_ne {α : Type u_1} [] [] {a : α} (h : ∀ (b : α), a) :
theorem Order.not_isPredLimit_iff {α : Type u_1} [] [] {a : α} :
∃ (b : α), ¬ = a
theorem Order.mem_range_pred_of_not_isPredLimit {α : Type u_1} [] [] {a : α} (h : ) :
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} [] [] {b : α} (H : a > b, < b) :
theorem Order.IsPredLimit.lt_pred {α : Type u_1} [] [] {a : α} {b : α} (h : ) :
a < ba <
theorem Order.IsPredLimit.lt_pred_iff {α : Type u_1} [] [] {a : α} {b : α} (h : ) :
a < a < b
theorem Order.isPredLimit_iff_lt_pred {α : Type u_1} [] [] {a : α} :
∀ ⦃b : α⦄, a < ba <
noncomputable def Order.isPredLimitRecOn {α : Type u_1} [] [] {C : αSort u_2} (b : α) (hs : (a : α) → ¬C ()) (hl : (a : α) → C 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} [] [] {b : α} {C : αSort u_2} (hs : (a : α) → ¬C ()) (hl : (a : α) → C a) (hb : ) :
= hl b hb
theorem Order.isPredLimitRecOn_pred' {α : Type u_1} [] [] {C : αSort u_2} (hs : (a : α) → ¬C ()) (hl : (a : α) → C a) {b : α} (hb : ¬) :
Order.isPredLimitRecOn () hs hl = hs b hb
noncomputable def PredOrder.limitRecOn {α : Type u_1} [] [] (a : α) {C : αSort u_2} [] (H_pred : (a : α) → ¬C aC ()) (H_lim : (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} [] [] {a : α} {C : αSort u_2} [] (H_pred : (a : α) → ¬C aC ()) (H_lim : (a : α) → ((b : α) → b > aC b)C a) (ha : ¬) :
PredOrder.limitRecOn () H_pred H_lim = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
@[simp]
theorem PredOrder.limitRecOn_limit {α : Type u_1} [] [] {a : α} {C : αSort u_2} [] (H_pred : (a : α) → ¬C aC ()) (H_lim : (a : α) → ((b : α) → b > aC b)C a) (ha : ) :
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} [] [] {C : αSort u_2} [] (hs : (a : α) → ¬C ()) (hl : (a : α) → C a) (b : α) :
Order.isPredLimitRecOn () hs hl = hs b
theorem Order.IsPredLimit.isMax {α : Type u_1} [] [] {a : α} (h : ) :
@[simp]
theorem Order.isPredLimit_iff {α : Type u_1} [] [] {a : α} :
theorem Order.not_isPredLimit {α : Type u_1} [] [] {a : α} [] :