mathlib documentation

order.succ_pred.limit

Successor and predecessor limits #

We define the predicate order.is_succ_limit for "successor limits", values that aren't successors, except possibly of themselves. 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} [preorder α] [succ_order α] (a : α) :
Prop

A successor limit is a value that isn't a successor, except possibly of itself.

Equations
@[protected]
theorem order.is_succ_limit.is_max {α : Type u_1} {a : α} [preorder α] [succ_order α] (h : order.is_succ_limit (order.succ a)) :
@[protected]
theorem is_min.is_succ_limit {α : Type u_1} {a : α} [preorder α] [succ_order α] (h : is_min a) :
theorem order.is_succ_limit_of_succ_ne {α : Type u_1} {a : α} [preorder α] [succ_order α] (h : ∀ (b : α), order.succ b a) :
theorem order.not_is_succ_limit_iff {α : Type u_1} {a : α} [preorder α] [succ_order α] :

See order.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} {b : α} [preorder α] [succ_order α] (H : ∀ (a : α), a < border.succ a < b) :
noncomputable def order.is_succ_limit_rec_on {α : Type u_1} [preorder α] [succ_order α] {C : α → Sort u_2} (b : α) (hs : Π (a : α), ¬is_max aC (order.succ a)) (hl : Π (a : α), order.is_succ_limit aC a) :
C b

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

Note that you need a partial order for data built using this to behave nicely on successors.

Equations
theorem order.is_succ_limit_rec_on_limit {α : Type u_1} {b : α} [preorder α] [succ_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_max aC (order.succ a)) (hl : Π (a : α), order.is_succ_limit aC a) (hb : order.is_succ_limit b) :
theorem order.is_succ_limit.succ_ne {α : Type u_1} {a : α} [preorder α] [succ_order α] [no_max_order α] (h : order.is_succ_limit a) (b : α) :
@[simp]
theorem order.not_is_succ_limit_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
theorem order.is_succ_limit_iff_succ_ne {α : Type u_1} {a : α} [preorder α] [succ_order α] [no_max_order α] :
@[simp]
theorem order.is_succ_limit.succ_lt {α : Type u_1} {a b : α} [partial_order α] [succ_order α] (hb : order.is_succ_limit b) (ha : a < b) :
theorem order.is_succ_limit.succ_lt_iff {α : Type u_1} {a b : α} [partial_order α] [succ_order α] (hb : order.is_succ_limit b) :
order.succ a < b a < b
theorem order.is_succ_limit_iff_succ_lt {α : Type u_1} {b : α} [partial_order α] [succ_order α] :
order.is_succ_limit b ∀ (a : α), a < border.succ a < b
theorem order.is_succ_limit_rec_on_succ' {α : Type u_1} [partial_order α] [succ_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_max aC (order.succ a)) (hl : Π (a : α), order.is_succ_limit aC a) {b : α} (hb : ¬is_max b) :
@[simp]
theorem order.is_succ_limit_rec_on_succ {α : Type u_1} [partial_order α] [succ_order α] [no_max_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_max aC (order.succ a)) (hl : Π (a : α), order.is_succ_limit aC a) (b : α) :
@[protected]
theorem order.is_succ_limit.is_min {α : Type u_1} {a : α} [partial_order α] [succ_order α] [is_succ_archimedean α] (h : order.is_succ_limit a) :
@[simp]
theorem order.is_succ_limit_iff {α : Type u_1} {a : α} [partial_order α] [succ_order α] [is_succ_archimedean α] :

Predecessor limits #

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

A predecessor limit is a value that isn't a predecessor, except possibly of itself.

Equations
@[protected]
theorem order.is_pred_limit.is_min {α : Type u_1} {a : α} [preorder α] [pred_order α] (h : order.is_pred_limit (order.pred a)) :
@[protected]
theorem is_max.is_pred_limit {α : Type u_1} {a : α} [preorder α] [pred_order α] :
theorem order.is_pred_limit_of_pred_ne {α : Type u_1} {a : α} [preorder α] [pred_order α] (h : ∀ (b : α), order.pred b a) :
theorem order.not_is_pred_limit_iff {α : Type u_1} {a : α} [preorder α] [pred_order α] :

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

theorem order.is_pred_limit_of_lt_pred {α : Type u_1} {a : α} [preorder α] [pred_order α] :
(∀ (b : α), b > aa < order.pred b)order.is_pred_limit a
noncomputable def order.is_pred_limit_rec_on {α : Type u_1} [preorder α] [pred_order α] {C : α → Sort u_2} (b : α) (hs : Π (a : α), ¬is_min aC (order.pred a)) (hl : Π (a : α), order.is_pred_limit aC a) :
C b

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

Note that you need a partial order for data built using this to behave nicely on successors.

Equations
theorem order.is_pred_limit_rec_on_limit {α : Type u_1} {b : α} [preorder α] [pred_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_min aC (order.pred a)) (hl : Π (a : α), order.is_pred_limit aC a) (hb : order.is_pred_limit b) :
theorem order.is_pred_limit.pred_ne {α : Type u_1} {a : α} [preorder α] [pred_order α] [no_min_order α] (h : order.is_pred_limit a) (b : α) :
@[simp]
theorem order.not_is_pred_limit_pred {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
theorem order.is_pred_limit_iff_pred_ne {α : Type u_1} {a : α} [preorder α] [pred_order α] [no_min_order α] :
@[protected]
@[simp]
theorem order.is_pred_limit.lt_pred {α : Type u_1} {a b : α} [partial_order α] [pred_order α] (ha : order.is_pred_limit a) :
a < ba < order.pred b
theorem order.is_pred_limit.lt_pred_iff {α : Type u_1} {a b : α} [partial_order α] [pred_order α] (ha : order.is_pred_limit a) :
a < order.pred b a < b
theorem order.is_pred_limit_iff_lt_pred {α : Type u_1} {a : α} [partial_order α] [pred_order α] :
order.is_pred_limit a ∀ (b : α), b > aa < order.pred b
theorem order.is_pred_limit_rec_on_pred' {α : Type u_1} [partial_order α] [pred_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_min aC (order.pred a)) (hl : Π (a : α), order.is_pred_limit aC a) {b : α} (hb : ¬is_min b) :
@[simp]
theorem order.is_pred_limit_rec_on_pred {α : Type u_1} [partial_order α] [pred_order α] [no_min_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_min aC (order.pred a)) (hl : Π (a : α), order.is_pred_limit aC a) (b : α) :
@[protected]
theorem order.is_pred_limit.is_max {α : Type u_1} {a : α} [partial_order α] [pred_order α] [is_pred_archimedean α] :
@[simp]
theorem order.is_pred_limit_iff {α : Type u_1} {a : α} [partial_order α] [pred_order α] [is_pred_archimedean α] :