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 #
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
Instances For
theorem
Order.not_isSuccLimit_iff_exists_covBy
{α : Type u_1}
[LT α]
(a : α)
:
¬Order.IsSuccLimit a ↔ ∃ (b : α), b ⋖ a
@[simp]
theorem
Order.IsSuccLimit.isMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
(h : Order.IsSuccLimit (Order.succ a))
:
IsMax 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 : α)
:
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 α]
:
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 : α}
:
¬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)
:
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)
:
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 := ⋯; Eq.mpr ⋯ (hs (Classical.choose ⋯) ⋯)
Instances For
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
@[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 α]
:
Predecessor limits #
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
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 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
Order.IsPredLimit.isMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
(h : Order.IsPredLimit (Order.pred a))
:
IsMin 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 : α)
:
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 α]
:
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 : α}
:
¬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)
:
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 < 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 ⋯
Instances For
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
@[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 α]
: