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 : α) : 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

• Order.IsSuccLimit a = ∀ (b : α), ¬b ⋖ a

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 : α) : Order.IsSuccLimit a

theorem IsMin.isSuccLimit {α : Type u_1} [Preorder α] {a : α} : IsMin a → Order.IsSuccLimit a

theorem Order.isSuccLimit_bot {α : Type u_1} [Preorder α] [OrderBot α] : Order.IsSuccLimit ⊥

theorem Order.IsSuccLimit.isMax {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] (h : Order.IsSuccLimit (Order.succ a)) : IsMax a

theorem Order.not_isSuccLimit_succ_of_not_isMax {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] (ha : ¬IsMax a) : ¬Order.IsSuccLimit (Order.succ a)

theorem Order.IsSuccLimit.succ_ne {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] [NoMaxOrder α] (h : Order.IsSuccLimit a) (b : α) : Order.succ b ≠ a

@[simp]

theorem Order.not_isSuccLimit_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) : ¬Order.IsSuccLimit (Order.succ a)

theorem Order.IsSuccLimit.isMin_of_noMax {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] (h : Order.IsSuccLimit a) : IsMin a

@[simp]

theorem Order.isSuccLimit_iff_of_noMax {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] : Order.IsSuccLimit a ↔ IsMin a

theorem Order.not_isSuccLimit_of_noMax {α : Type u_1} [Preorder α] {a : α} [SuccOrder α] [IsSuccArchimedean α] [NoMinOrder α] [NoMaxOrder α] : ¬Order.IsSuccLimit a

theorem Order.isSuccLimit_of_succ_ne {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} (h : ∀ (b : α), Order.succ b ≠ a) : Order.IsSuccLimit a

theorem Order.not_isSuccLimit_iff {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} : ¬Order.IsSuccLimit a ↔ ∃ (b : α), ¬IsMax b ∧ Order.succ b = 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) : Order.IsSuccLimit b

theorem Order.IsSuccLimit.succ_lt {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {b : α} (hb : Order.IsSuccLimit b) (ha : a < b) : Order.succ 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 : α} : Order.IsSuccLimit b ↔ ∀ a < b, Order.succ a < b

noncomputable def Order.isSuccLimitRecOn {α : Type u_1} [PartialOrder α] [SuccOrder α] {C : α → Sort u_2} (b : α) (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) : C b

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

Equations

• Order.isSuccLimitRecOn b hs hl = if hb : Order.IsSuccLimit b then hl b hb else let_fun H := ⋯; ⋯.mpr (hs (Classical.choose ⋯) ⋯)

theorem Order.isSuccLimitRecOn_limit {α : Type u_1} [PartialOrder α] [SuccOrder α] {b : α} {C : α → Sort u_2} (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C 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 a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) {b : α} (hb : ¬IsMax b) : Order.isSuccLimitRecOn (Order.succ b) hs hl = hs b hb

noncomputable def SuccOrder.limitRecOn {α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) {C : α → Sort u_2} [WellFoundedLT α] (H_succ : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (H_lim : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C 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.

@[simp]

theorem SuccOrder.limitRecOn_succ {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} {C : α → Sort u_2} [WellFoundedLT α] (H_succ : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (H_lim : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C 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 a → C a → C (Order.succ a)) (H_lim : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C 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 a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) (b : α) : Order.isSuccLimitRecOn (Order.succ b) hs hl = hs b ⋯

theorem Order.isSuccLimit_iff_succ_ne {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [NoMaxOrder α] : Order.IsSuccLimit a ↔ ∀ (b : α), Order.succ b ≠ a

theorem Order.not_isSuccLimit_iff' {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [NoMaxOrder α] : ¬Order.IsSuccLimit a ↔ a ∈ Set.range Order.succ

theorem Order.IsSuccLimit.isMin {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [IsSuccArchimedean α] (h : Order.IsSuccLimit a) : IsMin a

@[simp]

theorem Order.isSuccLimit_iff {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [IsSuccArchimedean α] : Order.IsSuccLimit a ↔ IsMin a

theorem Order.not_isSuccLimit {α : Type u_1} [PartialOrder α] [SuccOrder α] {a : α} [IsSuccArchimedean α] [NoMinOrder α] : ¬Order.IsSuccLimit a

Predecessor limits

def Order.IsPredLimit {α : Type u_1} [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

• Order.IsPredLimit a = ∀ (b : α), ¬a ⋖ b

theorem Order.not_isPredLimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) : ¬Order.IsPredLimit a ↔ ∃ (b : α), a ⋖ b

theorem Order.isPredLimit_of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) : Order.IsPredLimit a

@[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 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.IsSuccLimit a → Order.IsPredLimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isPredLimit_toDual_iff.

theorem IsMax.isPredLimit {α : Type u_1} [Preorder α] {a : α} : IsMax a → Order.IsPredLimit a

theorem Order.isPredLimit_top {α : Type u_1} [Preorder α] [OrderTop α] : Order.IsPredLimit ⊤

theorem Order.IsPredLimit.isMin {α : Type u_1} [Preorder α] {a : α} [PredOrder α] (h : Order.IsPredLimit (Order.pred a)) : IsMin a

theorem Order.not_isPredLimit_pred_of_not_isMin {α : Type u_1} [Preorder α] {a : α} [PredOrder α] (ha : ¬IsMin a) : ¬Order.IsPredLimit (Order.pred a)

theorem Order.IsPredLimit.pred_ne {α : Type u_1} [Preorder α] {a : α} [PredOrder α] [NoMinOrder α] (h : Order.IsPredLimit a) (b : α) : Order.pred b ≠ a

@[simp]

theorem Order.not_isPredLimit_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) : ¬Order.IsPredLimit (Order.pred a)

theorem Order.IsPredLimit.isMax_of_noMin {α : Type u_1} [Preorder α] {a : α} [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] (h : Order.IsPredLimit a) : IsMax a

@[simp]

theorem Order.isPredLimit_iff_of_noMin {α : Type u_1} [Preorder α] {a : α} [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] : Order.IsPredLimit a ↔ IsMax a

theorem Order.not_isPredLimit_of_noMin {α : Type u_1} [Preorder α] {a : α} [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] [NoMaxOrder α] : ¬Order.IsPredLimit a

theorem Order.isPredLimit_of_pred_ne {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} (h : ∀ (b : α), Order.pred b ≠ a) : Order.IsPredLimit a

theorem Order.not_isPredLimit_iff {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} : ¬Order.IsPredLimit a ↔ ∃ (b : α), ¬IsMin b ∧ Order.pred b = 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) : Order.IsPredLimit b

theorem Order.IsPredLimit.lt_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {b : α} (h : Order.IsPredLimit a) : a < b → a < 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 < b → a < Order.pred b

noncomputable def Order.isPredLimitRecOn {α : Type u_1} [PartialOrder α] [PredOrder α] {C : α → Sort u_2} (b : α) (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) : C b

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

Equations

• Order.isPredLimitRecOn b hs hl = Order.isSuccLimitRecOn b hs fun (x : αᵒᵈ) (ha : Order.IsSuccLimit x) => hl x ⋯

theorem Order.isPredLimitRecOn_limit {α : Type u_1} [PartialOrder α] [PredOrder α] {b : α} {C : α → Sort u_2} (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C 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 a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) {b : α} (hb : ¬IsMin b) : Order.isPredLimitRecOn (Order.pred b) hs hl = hs b hb

noncomputable def PredOrder.limitRecOn {α : Type u_1} [PartialOrder α] [PredOrder α] (a : α) {C : α → Sort u_2} [WellFoundedGT α] (H_pred : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (H_lim : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C 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.

@[simp]

theorem PredOrder.limitRecOn_pred {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} {C : α → Sort u_2} [WellFoundedGT α] (H_pred : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (H_lim : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C 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 a → C a → C (Order.pred a)) (H_lim : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C 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 a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) (b : α) : Order.isPredLimitRecOn (Order.pred b) hs hl = hs b ⋯

theorem Order.IsPredLimit.isMax {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} [IsPredArchimedean α] (h : Order.IsPredLimit a) : IsMax a

@[simp]

theorem Order.isPredLimit_iff {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} [IsPredArchimedean α] : Order.IsPredLimit a ↔ IsMax a

theorem Order.not_isPredLimit {α : Type u_1} [PartialOrder α] [PredOrder α] {a : α} [IsPredArchimedean α] [NoMaxOrder α] : ¬Order.IsPredLimit a