# mathlib3documentation

order.succ_pred.limit

# Successor and predecessor limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the predicate order.is_succ_limit 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.is_pred_limit analogously, and prove basic results.

## Todo #

The plan is to eventually replace ordinal.is_limit and cardinal.is_limit with the common predicate order.is_succ_limit.

### Successor limits #

def order.is_succ_limit {α : Type u_1} [has_lt α] (a : α) :
Prop

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
theorem order.not_is_succ_limit_iff_exists_covby {α : Type u_1} [has_lt α] (a : α) :
(b : α), b a
@[simp]
theorem order.is_succ_limit_of_dense {α : Type u_1} [has_lt α] (a : α) :
@[protected]
theorem is_min.is_succ_limit {α : Type u_1} [preorder α] {a : α} :
theorem order.is_succ_limit_bot {α : Type u_1} [preorder α] [order_bot α] :
@[protected]
theorem order.is_succ_limit.is_max {α : Type u_1} [preorder α] {a : α} [succ_order α] (h : order.is_succ_limit (order.succ a)) :
theorem order.not_is_succ_limit_succ_of_not_is_max {α : Type u_1} [preorder α] {a : α} [succ_order α] (ha : ¬) :
theorem order.is_succ_limit.succ_ne {α : Type u_1} [preorder α] {a : α} [succ_order α] [no_max_order α] (h : order.is_succ_limit a) (b : α) :
a
@[simp]
theorem order.not_is_succ_limit_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
@[simp]
theorem order.is_succ_limit_iff_of_no_max {α : Type u_1} [preorder α] {a : α} [succ_order α] [no_max_order α] :
theorem order.not_is_succ_limit_of_no_max {α : Type u_1} [preorder α] {a : α} [succ_order α] [no_min_order α] [no_max_order α] :
theorem order.is_succ_limit_of_succ_ne {α : Type u_1} [succ_order α] {a : α} (h : (b : α), a) :
theorem order.not_is_succ_limit_iff {α : Type u_1} [succ_order α] {a : α} :
(b : α), ¬ = a
theorem order.mem_range_succ_of_not_is_succ_limit {α : Type u_1} [succ_order α] {a : α} (h : ¬) :

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

theorem order.is_succ_limit_of_succ_lt {α : Type u_1} [succ_order α] {b : α} (H : (a : α), a < b < b) :
theorem order.is_succ_limit.succ_lt {α : Type u_1} [succ_order α] {a b : α} (hb : order.is_succ_limit b) (ha : a < b) :
< b
theorem order.is_succ_limit.succ_lt_iff {α : Type u_1} [succ_order α] {a b : α} (hb : order.is_succ_limit b) :
< b a < b
theorem order.is_succ_limit_iff_succ_lt {α : Type u_1} [succ_order α] {b : α} :
(a : α), a < b < b
noncomputable def order.is_succ_limit_rec_on {α : Type u_1} [succ_order α] {C : α Sort u_2} (b : α) (hs : Π (a : α), ¬ C (order.succ a)) (hl : Π (a : α), C a) :
C b

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

Equations
• hl = (λ (hb : , hl b hb) (λ (hb : , _.mpr (hs _))
theorem order.is_succ_limit_rec_on_limit {α : Type u_1} [succ_order α] {b : α} {C : α Sort u_2} (hs : Π (a : α), ¬ C (order.succ a)) (hl : Π (a : α), C a) (hb : order.is_succ_limit b) :
hl = hl b hb
theorem order.is_succ_limit_rec_on_succ' {α : Type u_1} [succ_order α] {C : α Sort u_2} (hs : Π (a : α), ¬ C (order.succ a)) (hl : Π (a : α), C a) {b : α} (hb : ¬) :
hl = hs b hb
@[simp]
theorem order.is_succ_limit_rec_on_succ {α : Type u_1} [succ_order α] {C : α Sort u_2} [no_max_order α] (hs : Π (a : α), ¬ C (order.succ a)) (hl : Π (a : α), C a) (b : α) :
hl = hs b _
theorem order.is_succ_limit_iff_succ_ne {α : Type u_1} [succ_order α] {a : α} [no_max_order α] :
(b : α), a
theorem order.not_is_succ_limit_iff' {α : Type u_1} [succ_order α] {a : α} [no_max_order α] :
@[protected]
theorem order.is_succ_limit.is_min {α : Type u_1} [succ_order α] {a : α} (h : order.is_succ_limit a) :
@[simp]
theorem order.is_succ_limit_iff {α : Type u_1} [succ_order α] {a : α}  :
theorem order.not_is_succ_limit {α : Type u_1} [succ_order α] {a : α} [no_min_order α] :

### Predecessor limits #

def order.is_pred_limit {α : Type u_1} [has_lt α] (a : α) :
Prop

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
theorem order.not_is_pred_limit_iff_exists_covby {α : Type u_1} [has_lt α] (a : α) :
(b : α), a b
theorem order.is_pred_limit_of_dense {α : Type u_1} [has_lt α] (a : α) :
@[simp]
theorem order.is_succ_limit_to_dual_iff {α : Type u_1} [has_lt α] {a : α} :
@[simp]
theorem order.is_pred_limit_to_dual_iff {α : Type u_1} [has_lt α] {a : α} :
theorem order.is_pred_limit.dual {α : Type u_1} [has_lt α] {a : α} :

Alias of the reverse direction of order.is_succ_limit_to_dual_iff.

theorem order.is_succ_limit.dual {α : Type u_1} [has_lt α] {a : α} :

Alias of the reverse direction of order.is_pred_limit_to_dual_iff.

@[protected]
theorem is_max.is_pred_limit {α : Type u_1} [preorder α] {a : α} :
theorem order.is_pred_limit_top {α : Type u_1} [preorder α] [order_top α] :
@[protected]
theorem order.is_pred_limit.is_min {α : Type u_1} [preorder α] {a : α} [pred_order α] (h : order.is_pred_limit (order.pred a)) :
theorem order.not_is_pred_limit_pred_of_not_is_min {α : Type u_1} [preorder α] {a : α} [pred_order α] (ha : ¬) :
theorem order.is_pred_limit.pred_ne {α : Type u_1} [preorder α] {a : α} [pred_order α] [no_min_order α] (h : order.is_pred_limit a) (b : α) :
a
@[simp]
theorem order.not_is_pred_limit_pred {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
@[protected]
theorem order.is_pred_limit.is_max_of_no_min {α : Type u_1} [preorder α] {a : α} [pred_order α] [no_min_order α] (h : order.is_pred_limit a) :
@[simp]
theorem order.is_pred_limit_iff_of_no_min {α : Type u_1} [preorder α] {a : α} [pred_order α] [no_min_order α] :
theorem order.not_is_pred_limit_of_no_min {α : Type u_1} [preorder α] {a : α} [pred_order α] [no_min_order α] [no_max_order α] :
theorem order.is_pred_limit_of_pred_ne {α : Type u_1} [pred_order α] {a : α} (h : (b : α), a) :
theorem order.not_is_pred_limit_iff {α : Type u_1} [pred_order α] {a : α} :
(b : α), ¬ = a
theorem order.mem_range_pred_of_not_is_pred_limit {α : Type u_1} [pred_order α] {a : α} (h : ¬) :

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

theorem order.is_pred_limit_of_pred_lt {α : Type u_1} [pred_order α] {b : α} (H : (a : α), a > b < b) :
theorem order.is_pred_limit.lt_pred {α : Type u_1} [pred_order α] {a b : α} (h : order.is_pred_limit a) :
a < b a <
theorem order.is_pred_limit.lt_pred_iff {α : Type u_1} [pred_order α] {a b : α} (h : order.is_pred_limit a) :
a < a < b
theorem order.is_pred_limit_iff_lt_pred {α : Type u_1} [pred_order α] {a : α} :
⦃b : α⦄, a < b a <
noncomputable def order.is_pred_limit_rec_on {α : Type u_1} [pred_order α] {C : α Sort u_2} (b : α) (hs : Π (a : α), ¬ C (order.pred a)) (hl : Π (a : α), C a) :
C b

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

Equations
• hl = (λ (a : αᵒᵈ) (ha : , hl _)
theorem order.is_pred_limit_rec_on_limit {α : Type u_1} [pred_order α] {b : α} {C : α Sort u_2} (hs : Π (a : α), ¬ C (order.pred a)) (hl : Π (a : α), C a) (hb : order.is_pred_limit b) :
hl = hl b hb
theorem order.is_pred_limit_rec_on_pred' {α : Type u_1} [pred_order α] {C : α Sort u_2} (hs : Π (a : α), ¬ C (order.pred a)) (hl : Π (a : α), C a) {b : α} (hb : ¬) :
hl = hs b hb
@[simp]
theorem order.is_pred_limit_rec_on_pred {α : Type u_1} [pred_order α] {C : α Sort u_2} [no_min_order α] (hs : Π (a : α), ¬ C (order.pred a)) (hl : Π (a : α), C a) (b : α) :
hl = hs b _
@[protected]
theorem order.is_pred_limit.is_max {α : Type u_1} [pred_order α] {a : α} (h : order.is_pred_limit a) :
@[simp]
theorem order.is_pred_limit_iff {α : Type u_1} [pred_order α] {a : α}  :
theorem order.not_is_pred_limit {α : Type u_1} [pred_order α] {a : α} [no_max_order α] :