Successor and predecessor limits #
We define the predicate Order.IsSuccPrelimit for "successor pre-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.IsPredPrelimit analogously, and prove basic results.
TODO #
For some applications, it's desirable to exclude the case where an element is minimal. A future PR
will introduce IsSuccLimit for this usage.
The plan is to eventually replace Ordinal.IsLimit and Cardinal.IsLimit with the common
predicate Order.IsSuccLimit.
Successor limits #
A successor pre-limit is a value that doesn't cover any other.
It's so named because in a successor order, a successor pre-limit can't be the successor of anything smaller.
For some applications, it's desirable to exclude the case where an element is minimal. A future PR
will introduce IsSuccLimit for this usage.
Equations
- Order.IsSuccPrelimit a = ∀ (b : α), ¬b ⋖ a
Instances For
@[deprecated Order.IsSuccPrelimit]
Alias of Order.IsSuccPrelimit.
A successor pre-limit is a value that doesn't cover any other.
It's so named because in a successor order, a successor pre-limit can't be the successor of anything smaller.
For some applications, it's desirable to exclude the case where an element is minimal. A future PR
will introduce IsSuccLimit for this usage.
Equations
Instances For
theorem
Order.not_isSuccPrelimit_iff_exists_covBy
{α : Type u_1}
[LT α]
(a : α)
:
¬Order.IsSuccPrelimit a ↔ ∃ (b : α), b ⋖ a
@[deprecated Order.not_isSuccPrelimit_iff_exists_covBy]
theorem
Order.not_isSuccLimit_iff_exists_covBy
{α : Type u_1}
[LT α]
(a : α)
:
¬Order.IsSuccPrelimit a ↔ ∃ (b : α), b ⋖ a
@[simp]
@[deprecated Order.isSuccPrelimit_of_dense]
Alias of Order.isSuccPrelimit_of_dense.
@[deprecated IsMin.isSuccPrelimit]
Alias of IsMin.isSuccPrelimit.
@[deprecated Order.isSuccPrelimit_bot]
Alias of Order.isSuccPrelimit_bot.
theorem
Order.IsSuccPrelimit.isMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
(h : Order.IsSuccPrelimit (Order.succ a))
:
IsMax a
@[deprecated Order.IsSuccPrelimit.isMax]
theorem
Order.IsSuccLimit.isMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
(h : Order.IsSuccPrelimit (Order.succ a))
:
IsMax a
Alias of Order.IsSuccPrelimit.isMax.
theorem
Order.IsSuccPrelimit.succ_ne
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[NoMaxOrder α]
(h : Order.IsSuccPrelimit a)
(b : α)
:
Order.succ b ≠ a
@[deprecated Order.IsSuccPrelimit.succ_ne]
theorem
Order.IsSuccLimit.succ_ne
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[NoMaxOrder α]
(h : Order.IsSuccPrelimit a)
(b : α)
:
Order.succ b ≠ a
Alias of Order.IsSuccPrelimit.succ_ne.
@[simp]
theorem
Order.not_isSuccPrelimit_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
@[deprecated Order.not_isSuccPrelimit_succ]
theorem
Order.not_isSuccLimit_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
Alias of Order.not_isSuccPrelimit_succ.
theorem
Order.IsSuccPrelimit.isMin_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
(h : Order.IsSuccPrelimit a)
:
IsMin a
@[deprecated Order.IsSuccPrelimit.isMin_of_noMax]
theorem
Order.IsSuccLimit.isMin_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
(h : Order.IsSuccPrelimit a)
:
IsMin a
Alias of Order.IsSuccPrelimit.isMin_of_noMax.
@[simp]
theorem
Order.isSuccPrelimit_iff_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
:
@[deprecated Order.isSuccPrelimit_iff_of_noMax]
theorem
Order.isSuccLimit_iff_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
:
Alias of Order.isSuccPrelimit_iff_of_noMax.
theorem
Order.not_isSuccPrelimit_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMinOrder α]
[NoMaxOrder α]
:
@[deprecated Order.not_isSuccPrelimit_of_noMax]
theorem
Order.not_isSuccLimit_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMinOrder α]
[NoMaxOrder α]
:
Alias of Order.not_isSuccPrelimit_of_noMax.
theorem
Order.isSuccPrelimit_of_succ_ne
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
(h : ∀ (b : α), Order.succ b ≠ a)
:
@[deprecated Order.isSuccPrelimit_of_succ_ne]
theorem
Order.isSuccLimit_of_succ_ne
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
(h : ∀ (b : α), Order.succ b ≠ a)
:
Alias of Order.isSuccPrelimit_of_succ_ne.
theorem
Order.not_isSuccPrelimit_iff
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
:
¬Order.IsSuccPrelimit a ↔ ∃ (b : α), ¬IsMax b ∧ Order.succ b = a
@[deprecated Order.not_isSuccPrelimit_iff]
theorem
Order.not_isSuccLimit_iff
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
:
¬Order.IsSuccPrelimit a ↔ ∃ (b : α), ¬IsMax b ∧ Order.succ b = a
Alias of Order.not_isSuccPrelimit_iff.
theorem
Order.mem_range_succ_of_not_isSuccPrelimit
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
(h : ¬Order.IsSuccPrelimit a)
:
See not_isSuccPrelimit_iff for a version that states that a is a successor of a value other
than itself.
@[deprecated Order.mem_range_succ_of_not_isSuccPrelimit]
theorem
Order.mem_range_succ_of_not_isSuccLimit
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
(h : ¬Order.IsSuccPrelimit a)
:
Alias of Order.mem_range_succ_of_not_isSuccPrelimit.
See not_isSuccPrelimit_iff for a version that states that a is a successor of a value other
than itself.
theorem
Order.mem_range_succ_or_isSuccPrelimit
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
(a : α)
:
a ∈ Set.range Order.succ ∨ Order.IsSuccPrelimit a
@[deprecated Order.mem_range_succ_or_isSuccPrelimit]
theorem
Order.mem_range_succ_or_isSuccLimit
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
(a : α)
:
a ∈ Set.range Order.succ ∨ Order.IsSuccPrelimit a
Alias of Order.mem_range_succ_or_isSuccPrelimit.
theorem
Order.isSuccPrelimit_of_succ_lt
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{b : α}
(H : ∀ a < b, Order.succ a < b)
:
@[deprecated Order.isSuccPrelimit_of_succ_lt]
theorem
Order.isSuccLimit_of_succ_lt
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{b : α}
(H : ∀ a < b, Order.succ a < b)
:
Alias of Order.isSuccPrelimit_of_succ_lt.
theorem
Order.IsSuccPrelimit.succ_lt
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
{b : α}
(hb : Order.IsSuccPrelimit b)
(ha : a < b)
:
Order.succ a < b
@[deprecated Order.IsSuccPrelimit.succ_lt]
theorem
Order.IsSuccLimit.succ_lt
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
{b : α}
(hb : Order.IsSuccPrelimit b)
(ha : a < b)
:
Order.succ a < b
Alias of Order.IsSuccPrelimit.succ_lt.
theorem
Order.IsSuccPrelimit.succ_lt_iff
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
{b : α}
(hb : Order.IsSuccPrelimit b)
:
Order.succ a < b ↔ a < b
@[deprecated Order.IsSuccPrelimit.succ_lt_iff]
theorem
Order.IsSuccLimit.succ_lt_iff
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
{b : α}
(hb : Order.IsSuccPrelimit b)
:
Order.succ a < b ↔ a < b
Alias of Order.IsSuccPrelimit.succ_lt_iff.
theorem
Order.isSuccPrelimit_iff_succ_lt
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{b : α}
:
Order.IsSuccPrelimit b ↔ ∀ a < b, Order.succ a < b
@[deprecated Order.isSuccPrelimit_iff_succ_lt]
theorem
Order.isSuccLimit_iff_succ_lt
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{b : α}
:
Order.IsSuccPrelimit b ↔ ∀ a < b, Order.succ a < b
Alias of Order.isSuccPrelimit_iff_succ_lt.
theorem
Order.isSuccPrelimit_iff_succ_ne
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[NoMaxOrder α]
:
Order.IsSuccPrelimit a ↔ ∀ (b : α), Order.succ b ≠ a
@[deprecated Order.isSuccPrelimit_iff_succ_ne]
theorem
Order.isSuccLimit_iff_succ_ne
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[NoMaxOrder α]
:
Order.IsSuccPrelimit a ↔ ∀ (b : α), Order.succ b ≠ a
Alias of Order.isSuccPrelimit_iff_succ_ne.
theorem
Order.not_isSuccPrelimit_iff'
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[NoMaxOrder α]
:
¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ
@[deprecated Order.not_isSuccPrelimit_iff']
theorem
Order.not_isSuccLimit_iff'
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[NoMaxOrder α]
:
¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ
Alias of Order.not_isSuccPrelimit_iff'.
theorem
Order.IsSuccPrelimit.isMin
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[IsSuccArchimedean α]
(h : Order.IsSuccPrelimit a)
:
IsMin a
@[deprecated Order.IsSuccPrelimit.isMin]
theorem
Order.IsSuccLimit.isMin
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[IsSuccArchimedean α]
(h : Order.IsSuccPrelimit a)
:
IsMin a
Alias of Order.IsSuccPrelimit.isMin.
@[simp]
theorem
Order.isSuccPrelimit_iff
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[IsSuccArchimedean α]
:
@[deprecated Order.isSuccPrelimit_iff]
theorem
Order.isSuccLimit_iff
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[IsSuccArchimedean α]
:
Alias of Order.isSuccPrelimit_iff.
theorem
Order.not_isSuccPrelimit
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[IsSuccArchimedean α]
[NoMinOrder α]
:
@[deprecated Order.not_isSuccPrelimit]
theorem
Order.not_isSuccLimit
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
{a : α}
[IsSuccArchimedean α]
[NoMinOrder α]
:
Alias of Order.not_isSuccPrelimit.
Predecessor limits #
A successor pre-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.
For some applications, it's desirable to exclude the case where an element is maximal. A future PR
will introduce IsPredLimit for this usage.
Equations
- Order.IsPredPrelimit a = ∀ (b : α), ¬a ⋖ b
Instances For
@[deprecated Order.IsPredPrelimit]
Alias of Order.IsPredPrelimit.
A successor pre-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.
For some applications, it's desirable to exclude the case where an element is maximal. A future PR
will introduce IsPredLimit for this usage.
Equations
Instances For
theorem
Order.not_isPredPrelimit_iff_exists_covBy
{α : Type u_1}
[LT α]
(a : α)
:
¬Order.IsPredPrelimit a ↔ ∃ (b : α), a ⋖ b
@[deprecated Order.not_isPredPrelimit_iff_exists_covBy]
theorem
Order.not_isPredLimit_iff_exists_covBy
{α : Type u_1}
[LT α]
(a : α)
:
¬Order.IsPredPrelimit a ↔ ∃ (b : α), a ⋖ b
@[deprecated Order.isPredPrelimit_of_dense]
Alias of Order.isPredPrelimit_of_dense.
@[simp]
theorem
Order.isSuccPrelimit_toDual_iff
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsSuccPrelimit (OrderDual.toDual a) ↔ Order.IsPredPrelimit a
@[deprecated Order.isSuccPrelimit_toDual_iff]
theorem
Order.isSuccLimit_toDual_iff
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsSuccPrelimit (OrderDual.toDual a) ↔ Order.IsPredPrelimit a
Alias of Order.isSuccPrelimit_toDual_iff.
@[simp]
theorem
Order.isPredPrelimit_toDual_iff
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsPredPrelimit (OrderDual.toDual a) ↔ Order.IsSuccPrelimit a
@[deprecated Order.isPredPrelimit_toDual_iff]
theorem
Order.isPredLimit_toDual_iff
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsPredPrelimit (OrderDual.toDual a) ↔ Order.IsSuccPrelimit a
Alias of Order.isPredPrelimit_toDual_iff.
theorem
Order.IsPredPrelimit.dual
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsPredPrelimit a → Order.IsSuccPrelimit (OrderDual.toDual a)
Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.
theorem
Order.IsSuccPrelimit.dual
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsSuccPrelimit a → Order.IsPredPrelimit (OrderDual.toDual a)
Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.
@[deprecated Order.IsPredPrelimit.dual]
theorem
Order.isPredLimit.dual
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsPredPrelimit a → Order.IsSuccPrelimit (OrderDual.toDual a)
Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.
Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.
@[deprecated Order.IsSuccPrelimit.dual]
theorem
Order.isSuccLimit.dual
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsSuccPrelimit a → Order.IsPredPrelimit (OrderDual.toDual a)
Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.
Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.
@[deprecated IsMax.isPredPrelimit]
Alias of IsMax.isPredPrelimit.
@[deprecated Order.isPredPrelimit_top]
Alias of Order.isPredPrelimit_top.
theorem
Order.IsPredPrelimit.isMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
(h : Order.IsPredPrelimit (Order.pred a))
:
IsMin a
@[deprecated Order.IsPredPrelimit.isMin]
theorem
Order.IsPredLimit.isMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
(h : Order.IsPredPrelimit (Order.pred a))
:
IsMin a
Alias of Order.IsPredPrelimit.isMin.
theorem
Order.IsPredPrelimit.pred_ne
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[NoMinOrder α]
(h : Order.IsPredPrelimit a)
(b : α)
:
Order.pred b ≠ a
@[deprecated Order.IsPredPrelimit.pred_ne]
theorem
Order.IsPredLimit.pred_ne
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[NoMinOrder α]
(h : Order.IsPredPrelimit a)
(b : α)
:
Order.pred b ≠ a
Alias of Order.IsPredPrelimit.pred_ne.
@[simp]
theorem
Order.not_isPredPrelimit_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
@[deprecated Order.not_isPredPrelimit_pred]
theorem
Order.not_isPredLimit_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
Alias of Order.not_isPredPrelimit_pred.
theorem
Order.IsPredPrelimit.isMax_of_noMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
(h : Order.IsPredPrelimit a)
:
IsMax a
@[deprecated Order.IsPredPrelimit.isMax_of_noMin]
theorem
Order.IsPredLimit.isMax_of_noMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
(h : Order.IsPredPrelimit a)
:
IsMax a
Alias of Order.IsPredPrelimit.isMax_of_noMin.
@[simp]
theorem
Order.isPredPrelimit_iff_of_noMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
:
@[deprecated Order.isPredPrelimit_iff_of_noMin]
theorem
Order.isPredLimit_iff_of_noMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
:
Alias of Order.isPredPrelimit_iff_of_noMin.
theorem
Order.not_isPredPrelimit_of_noMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
[NoMaxOrder α]
:
@[deprecated Order.not_isPredPrelimit_of_noMin]
theorem
Order.not_isPredLimit_of_noMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
[NoMaxOrder α]
:
Alias of Order.not_isPredPrelimit_of_noMin.
theorem
Order.isPredPrelimit_of_pred_ne
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
(h : ∀ (b : α), Order.pred b ≠ a)
:
@[deprecated Order.isPredPrelimit_of_pred_ne]
theorem
Order.isPredLimit_of_pred_ne
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
(h : ∀ (b : α), Order.pred b ≠ a)
:
Alias of Order.isPredPrelimit_of_pred_ne.
theorem
Order.not_isPredPrelimit_iff
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
:
¬Order.IsPredPrelimit a ↔ ∃ (b : α), ¬IsMin b ∧ Order.pred b = a
@[deprecated Order.not_isPredPrelimit_iff]
theorem
Order.not_isPredLimit_iff
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
:
¬Order.IsPredPrelimit a ↔ ∃ (b : α), ¬IsMin b ∧ Order.pred b = a
Alias of Order.not_isPredPrelimit_iff.
theorem
Order.mem_range_pred_of_not_isPredPrelimit
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
(h : ¬Order.IsPredPrelimit a)
:
See not_isPredPrelimit_iff for a version that states that a is a successor of a value other
than itself.
@[deprecated Order.mem_range_pred_of_not_isPredPrelimit]
theorem
Order.mem_range_pred_of_not_isPredLimit
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
(h : ¬Order.IsPredPrelimit a)
:
Alias of Order.mem_range_pred_of_not_isPredPrelimit.
See not_isPredPrelimit_iff for a version that states that a is a successor of a value other
than itself.
theorem
Order.mem_range_pred_or_isPredPrelimit
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
(a : α)
:
a ∈ Set.range Order.pred ∨ Order.IsPredPrelimit a
@[deprecated Order.mem_range_pred_or_isPredPrelimit]
theorem
Order.mem_range_pred_or_isPredLimit
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
(a : α)
:
a ∈ Set.range Order.pred ∨ Order.IsPredPrelimit a
Alias of Order.mem_range_pred_or_isPredPrelimit.
theorem
Order.isPredPrelimit_of_pred_lt
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{b : α}
(H : ∀ a > b, Order.pred a < b)
:
@[deprecated Order.isPredPrelimit_of_pred_lt]
theorem
Order.isPredLimit_of_pred_lt
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{b : α}
(H : ∀ a > b, Order.pred a < b)
:
Alias of Order.isPredPrelimit_of_pred_lt.
theorem
Order.IsPredPrelimit.lt_pred
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
{b : α}
(h : Order.IsPredPrelimit a)
:
a < b → a < Order.pred b
@[deprecated Order.IsPredPrelimit.lt_pred]
theorem
Order.IsPredLimit.lt_pred
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
{b : α}
(h : Order.IsPredPrelimit a)
:
a < b → a < Order.pred b
Alias of Order.IsPredPrelimit.lt_pred.
theorem
Order.IsPredPrelimit.lt_pred_iff
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
{b : α}
(h : Order.IsPredPrelimit a)
:
a < Order.pred b ↔ a < b
@[deprecated Order.IsPredPrelimit.lt_pred_iff]
theorem
Order.IsPredLimit.lt_pred_iff
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
{b : α}
(h : Order.IsPredPrelimit a)
:
a < Order.pred b ↔ a < b
Alias of Order.IsPredPrelimit.lt_pred_iff.
theorem
Order.isPredPrelimit_iff_lt_pred
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
:
Order.IsPredPrelimit a ↔ ∀ ⦃b : α⦄, a < b → a < Order.pred b
@[deprecated Order.isPredPrelimit_iff_lt_pred]
theorem
Order.isPredLimit_iff_lt_pred
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
:
Order.IsPredPrelimit a ↔ ∀ ⦃b : α⦄, a < b → a < Order.pred b
Alias of Order.isPredPrelimit_iff_lt_pred.
theorem
Order.IsPredPrelimit.isMax
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
[IsPredArchimedean α]
(h : Order.IsPredPrelimit a)
:
IsMax a
@[deprecated Order.IsPredPrelimit.isMax]
theorem
Order.IsPredLimit.isMax
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
[IsPredArchimedean α]
(h : Order.IsPredPrelimit a)
:
IsMax a
Alias of Order.IsPredPrelimit.isMax.
@[simp]
theorem
Order.isPredPrelimit_iff
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
[IsPredArchimedean α]
:
@[deprecated Order.isPredPrelimit_iff]
theorem
Order.isPredLimit_iff
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
[IsPredArchimedean α]
:
Alias of Order.isPredPrelimit_iff.
theorem
Order.not_isPredPrelimit
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
[IsPredArchimedean α]
[NoMaxOrder α]
:
@[deprecated Order.not_isPredPrelimit]
theorem
Order.not_isPredLimit
{α : Type u_1}
[PartialOrder α]
[PredOrder α]
{a : α}
[IsPredArchimedean α]
[NoMaxOrder α]
:
Alias of Order.not_isPredPrelimit.
Induction principles #
noncomputable def
Order.isSuccPrelimitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
(b : α)
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
:
C b
A value can be built by building it on successors and successor limits.
Equations
- Order.isSuccPrelimitRecOn b hs hl = if hb : Order.IsSuccPrelimit b then hl b hb else let_fun H := ⋯; ⋯.mpr (hs (Classical.choose ⋯) ⋯)
Instances For
@[deprecated Order.isSuccPrelimitRecOn]
def
Order.isSuccLimitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
(b : α)
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
:
C b
Alias of Order.isSuccPrelimitRecOn.
A value can be built by building it on successors and successor limits.
Instances For
theorem
Order.isSuccPrelimitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[SuccOrder α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
(hb : Order.IsSuccPrelimit b)
:
Order.isSuccPrelimitRecOn b hs hl = hl b hb
@[deprecated Order.isSuccPrelimitRecOn_limit]
theorem
Order.isSuccLimitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[SuccOrder α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
(hb : Order.IsSuccPrelimit b)
:
Order.isSuccPrelimitRecOn b hs hl = hl b hb
Alias of Order.isSuccPrelimitRecOn_limit.
theorem
Order.isSuccPrelimitRecOn_succ'
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[LinearOrder α]
[SuccOrder α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
(hb : ¬IsMax b)
:
Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b hb
@[deprecated Order.isSuccPrelimitRecOn_succ']
theorem
Order.isSuccLimitRecOn_succ'
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[LinearOrder α]
[SuccOrder α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
(hb : ¬IsMax b)
:
Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b hb
Alias of Order.isSuccPrelimitRecOn_succ'.
@[simp]
theorem
Order.isSuccPrelimitRecOn_succ
{α : Type u_1}
{C : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
(b : α)
:
Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b ⋯
@[deprecated Order.isSuccPrelimitRecOn_succ]
theorem
Order.isSuccLimitRecOn_succ
{α : Type u_1}
{C : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
[NoMaxOrder α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
(b : α)
:
Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b ⋯
Alias of Order.isSuccPrelimitRecOn_succ.
noncomputable def
Order.isPredPrelimitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
(b : α)
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
:
C b
A value can be built by building it on predecessors and predecessor limits.
Equations
- Order.isPredPrelimitRecOn b hs hl = Order.isSuccPrelimitRecOn b hs fun (x : αᵒᵈ) (ha : Order.IsSuccPrelimit x) => hl x ⋯
Instances For
@[deprecated Order.isPredPrelimitRecOn]
def
Order.isPredLimitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
(b : α)
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
:
C b
Alias of Order.isPredPrelimitRecOn.
A value can be built by building it on predecessors and predecessor limits.
Instances For
theorem
Order.isPredPrelimitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
(hb : Order.IsPredPrelimit b)
:
Order.isPredPrelimitRecOn b hs hl = hl b hb
@[deprecated Order.isPredPrelimitRecOn_limit]
theorem
Order.isPredLimitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
(hb : Order.IsPredPrelimit b)
:
Order.isPredPrelimitRecOn b hs hl = hl b hb
Alias of Order.isPredPrelimitRecOn_limit.
theorem
Order.isPredPrelimitRecOn_pred'
{α : Type u_1}
{C : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
{b : α}
(hb : ¬IsMin b)
:
Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b hb
@[deprecated Order.isPredPrelimitRecOn_pred']
theorem
Order.isPredLimitRecOn_pred'
{α : Type u_1}
{C : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
{b : α}
(hb : ¬IsMin b)
:
Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b hb
Alias of Order.isPredPrelimitRecOn_pred'.
@[simp]
theorem
Order.isPredPrelimitRecOn_pred
{α : Type u_1}
{C : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
[NoMinOrder α]
(b : α)
:
Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b ⋯
@[deprecated Order.isPredPrelimitRecOn_pred]
theorem
Order.isPredLimitRecOn_pred
{α : Type u_1}
{C : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
[NoMinOrder α]
(b : α)
:
Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b ⋯
Alias of Order.isPredPrelimitRecOn_pred.
noncomputable def
SuccOrder.prelimitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(b : α)
(hs : (a : α) → ¬IsMax a → C a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a)
:
C b
Recursion principle on a well-founded partial SuccOrder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated SuccOrder.prelimitRecOn]
def
SuccOrder.limitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(b : α)
(hs : (a : α) → ¬IsMax a → C a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a)
:
C b
Alias of SuccOrder.prelimitRecOn.
Recursion principle on a well-founded partial SuccOrder.
Instances For
@[simp]
theorem
SuccOrder.prelimitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(hs : (a : α) → ¬IsMax a → C a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a)
(hb : Order.IsSuccPrelimit b)
:
SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl
@[deprecated SuccOrder.prelimitRecOn_limit]
theorem
SuccOrder.limitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(hs : (a : α) → ¬IsMax a → C a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a)
(hb : Order.IsSuccPrelimit b)
:
SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl
Alias of SuccOrder.prelimitRecOn_limit.
@[simp]
theorem
SuccOrder.prelimitRecOn_succ
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[LinearOrder α]
[SuccOrder α]
[WellFoundedLT α]
(hs : (a : α) → ¬IsMax a → C a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a)
(hb : ¬IsMax b)
:
SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b hb (SuccOrder.prelimitRecOn b hs hl)
@[deprecated SuccOrder.prelimitRecOn_succ]
theorem
SuccOrder.limitRecOn_succ
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[LinearOrder α]
[SuccOrder α]
[WellFoundedLT α]
(hs : (a : α) → ¬IsMax a → C a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a)
(hb : ¬IsMax b)
:
SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b hb (SuccOrder.prelimitRecOn b hs hl)
Alias of SuccOrder.prelimitRecOn_succ.
noncomputable def
PredOrder.prelimitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(b : α)
(hp : (a : α) → ¬IsMin a → C a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a)
:
C b
Recursion principle on a well-founded partial PredOrder.
Equations
- PredOrder.prelimitRecOn b hp hl = SuccOrder.prelimitRecOn b hp fun (a : αᵒᵈ) (ha : Order.IsSuccPrelimit a) => hl a ⋯
Instances For
@[deprecated PredOrder.prelimitRecOn]
def
PredOrder.limitRecOn
{α : Type u_1}
{C : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(b : α)
(hp : (a : α) → ¬IsMin a → C a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a)
:
C b
Alias of PredOrder.prelimitRecOn.
Recursion principle on a well-founded partial PredOrder.
Instances For
@[simp]
theorem
PredOrder.prelimitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(hp : (a : α) → ¬IsMin a → C a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a)
(hb : Order.IsPredPrelimit b)
:
PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl
@[deprecated PredOrder.prelimitRecOn_limit]
theorem
PredOrder.limitRecOn_limit
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(hp : (a : α) → ¬IsMin a → C a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a)
(hb : Order.IsPredPrelimit b)
:
PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl
Alias of PredOrder.prelimitRecOn_limit.
@[simp]
theorem
PredOrder.prelimitRecOn_pred
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[LinearOrder α]
[PredOrder α]
[WellFoundedGT α]
(hp : (a : α) → ¬IsMin a → C a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a)
(hb : ¬IsMin b)
:
PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b hb (PredOrder.prelimitRecOn b hp hl)
@[deprecated PredOrder.prelimitRecOn_pred]
theorem
PredOrder.limitRecOn_pred
{α : Type u_1}
{C : α → Sort u_2}
{b : α}
[LinearOrder α]
[PredOrder α]
[WellFoundedGT α]
(hp : (a : α) → ¬IsMin a → C a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a)
(hb : ¬IsMin b)
:
PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b hb (PredOrder.prelimitRecOn b hp hl)
Alias of PredOrder.prelimitRecOn_pred.