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.
For some applications, it is desirable to exclude minimal elements from being successor limits, or
maximal elements from being predecessor limits. As such, we also provide Order.IsSuccLimit and
Order.IsPredLimit, which exclude these cases.
TODO #
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
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.
A successor limit is a value that isn't minimal and 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.
This previously allowed the element to be minimal. This usage is now covered by IsSuccPrelimit.
Equations
- Order.IsSuccLimit a = (¬IsMin a ∧ Order.IsSuccPrelimit a)
Instances For
theorem
Order.IsSuccLimit.isSuccPrelimit
{α : Type u_1}
[Preorder α]
{a : α}
(h : Order.IsSuccLimit a)
:
theorem
Order.IsSuccPrelimit.isSuccLimit_of_not_isMin
{α : Type u_1}
[Preorder α]
{a : α}
(h : Order.IsSuccPrelimit a)
(ha : ¬IsMin a)
:
theorem
Order.IsSuccPrelimit.isSuccLimit
{α : Type u_1}
[Preorder α]
{a : α}
[NoMinOrder α]
(h : Order.IsSuccPrelimit a)
:
theorem
Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin
{α : Type u_1}
[Preorder α]
{a : α}
(h : ¬IsMin a)
:
@[deprecated IsMin.isSuccPrelimit]
Alias of IsMin.isSuccPrelimit.
theorem
Order.IsSuccLimit.ne_bot
{α : Type u_1}
[Preorder α]
{a : α}
[OrderBot α]
(h : Order.IsSuccLimit a)
:
@[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
theorem
Order.IsSuccLimit.isMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
(h : Order.IsSuccLimit (Order.succ a))
:
IsMax a
theorem
Order.IsSuccPrelimit.succ_ne
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[NoMaxOrder α]
(h : Order.IsSuccPrelimit a)
(b : α)
:
Order.succ b ≠ 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_isSuccPrelimit_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
@[simp]
theorem
Order.not_isSuccLimit_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
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.
@[simp]
theorem
Order.not_isSuccLimit_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
:
theorem
Order.not_isSuccPrelimit_of_noMax
{α : Type u_1}
[Preorder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
[NoMinOrder α]
:
theorem
Order.isSuccLimit_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
[OrderBot α]
:
Order.IsSuccLimit a ↔ a ≠ ⊥ ∧ Order.IsSuccPrelimit a
theorem
Order.isSuccPrelimit_of_succ_ne
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
(h : ∀ (b : α), Order.succ b ≠ a)
:
@[deprecated Order.isSuccPrelimit_of_succ_ne]
theorem
Order.isSuccLimit_of_succ_ne
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
(h : ∀ (b : α), Order.succ b ≠ a)
:
Alias of Order.isSuccPrelimit_of_succ_ne.
theorem
Order.not_isSuccPrelimit_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
:
¬Order.IsSuccPrelimit a ↔ ∃ (b : α), ¬IsMax b ∧ Order.succ b = a
theorem
Order.mem_range_succ_of_not_isSuccPrelimit
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
(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 α]
{a : α}
[SuccOrder α]
(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 α]
{b : α}
[SuccOrder α]
(H : ∀ a < b, Order.succ a < b)
:
@[deprecated Order.isSuccPrelimit_of_succ_lt]
theorem
Order.isSuccLimit_of_succ_lt
{α : Type u_1}
[PartialOrder α]
{b : α}
[SuccOrder α]
(H : ∀ a < b, Order.succ a < b)
:
Alias of Order.isSuccPrelimit_of_succ_lt.
theorem
Order.IsSuccPrelimit.succ_lt
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[SuccOrder α]
(hb : Order.IsSuccPrelimit b)
(ha : a < b)
:
Order.succ a < b
theorem
Order.IsSuccLimit.succ_lt
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[SuccOrder α]
(hb : Order.IsSuccLimit b)
(ha : a < b)
:
Order.succ a < b
theorem
Order.IsSuccPrelimit.succ_lt_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[SuccOrder α]
(hb : Order.IsSuccPrelimit b)
:
Order.succ a < b ↔ a < b
theorem
Order.IsSuccLimit.succ_lt_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[SuccOrder α]
(hb : Order.IsSuccLimit b)
:
Order.succ a < b ↔ a < b
theorem
Order.isSuccPrelimit_iff_succ_lt
{α : Type u_1}
[PartialOrder α]
{b : α}
[SuccOrder α]
:
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 α]
{b : α}
[SuccOrder α]
:
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 α]
{a : α}
[SuccOrder α]
[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 α]
{a : α}
[SuccOrder α]
[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 α]
{a : α}
[SuccOrder α]
[NoMaxOrder α]
:
¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ
@[deprecated Order.not_isSuccPrelimit_iff']
theorem
Order.not_isSuccLimit_iff'
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
[NoMaxOrder α]
:
¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ
Alias of Order.not_isSuccPrelimit_iff'.
theorem
Order.IsSuccPrelimit.isMin
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
(h : Order.IsSuccPrelimit a)
:
IsMin a
@[simp]
theorem
Order.isSuccPrelimit_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
:
@[simp]
theorem
Order.not_isSuccLimit
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
:
theorem
Order.not_isSuccPrelimit
{α : Type u_1}
[PartialOrder α]
{a : α}
[SuccOrder α]
[IsSuccArchimedean α]
[NoMinOrder α]
:
Predecessor limits #
A predecessor pre-limit is a value that isn't covered by any other.
It's so named because in a predecessor order, a predecessor pre-limit can't be the predecessor of anything smaller.
For some applications, it's desirable to exclude maximal elements from this definition. For that,
see IsPredLimit.
Equations
- Order.IsPredPrelimit a = ∀ (b : α), ¬a ⋖ b
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
@[simp]
theorem
Order.isPredPrelimit_toDual_iff
{α : Type u_1}
[LT α]
{a : α}
:
Order.IsPredPrelimit (OrderDual.toDual a) ↔ Order.IsSuccPrelimit a
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.
A predecessor limit is a value that isn't maximal and doesn't cover any other.
It's so named because in a predecessor order, a predecessor limit can't be the predecessor of anything larger.
This previously allowed the element to be maximal. This usage is now covered by IsPredPreLimit.
Equations
- Order.IsPredLimit a = (¬IsMax a ∧ Order.IsPredPrelimit a)
Instances For
theorem
Order.IsPredLimit.isPredPrelimit
{α : Type u_1}
[Preorder α]
{a : α}
(h : Order.IsPredLimit a)
:
@[simp]
theorem
Order.isSuccLimit_toDual_iff
{α : Type u_1}
[Preorder α]
{a : α}
:
Order.IsSuccLimit (OrderDual.toDual a) ↔ Order.IsPredLimit a
@[simp]
theorem
Order.isPredLimit_toDual_iff
{α : Type u_1}
[Preorder α]
{a : α}
:
Order.IsPredLimit (OrderDual.toDual a) ↔ Order.IsSuccLimit a
theorem
Order.IsPredLimit.dual
{α : Type u_1}
[Preorder α]
{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}
[Preorder α]
{a : α}
:
Order.IsSuccLimit a → Order.IsPredLimit (OrderDual.toDual a)
Alias of the reverse direction of Order.isPredLimit_toDual_iff.
theorem
Order.IsPredPrelimit.isPredLimit_of_not_isMax
{α : Type u_1}
[Preorder α]
{a : α}
(h : Order.IsPredPrelimit a)
(ha : ¬IsMax a)
:
theorem
Order.IsPredPrelimit.isPredLimit
{α : Type u_1}
[Preorder α]
{a : α}
[NoMaxOrder α]
(h : Order.IsPredPrelimit a)
:
theorem
Order.isPredPrelimit_iff_isPredLimit_of_not_isMax
{α : Type u_1}
[Preorder α]
{a : α}
(h : ¬IsMax a)
:
@[deprecated IsMax.isPredPrelimit]
Alias of IsMax.isPredPrelimit.
@[deprecated Order.isPredPrelimit_top]
Alias of Order.isPredPrelimit_top.
theorem
Order.IsPredLimit.ne_top
{α : Type u_1}
[Preorder α]
{a : α}
[OrderTop α]
(h : Order.IsPredLimit a)
:
theorem
Order.not_isPredLimit_of_not_isPredPrelimit
{α : Type u_1}
[Preorder α]
{a : α}
(h : ¬Order.IsPredPrelimit a)
:
theorem
Order.IsPredPrelimit.isMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
(h : Order.IsPredPrelimit (Order.pred a))
:
IsMin a
theorem
Order.IsPredLimit.isMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
(h : Order.IsPredLimit (Order.pred a))
:
IsMin a
theorem
Order.IsPredPrelimit.pred_ne
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[NoMinOrder α]
(h : Order.IsPredPrelimit a)
(b : α)
:
Order.pred b ≠ 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_isPredPrelimit_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
@[simp]
theorem
Order.not_isPredLimit_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
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 α]
:
@[simp]
theorem
Order.not_isPredLimit_of_noMin
{α : Type u_1}
[Preorder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
:
theorem
Order.isPredLimit_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
[OrderTop α]
:
Order.IsPredLimit a ↔ a ≠ ⊤ ∧ Order.IsPredPrelimit a
theorem
Order.isPredPrelimit_of_pred_ne
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
(h : ∀ (b : α), Order.pred b ≠ a)
:
@[deprecated Order.isPredPrelimit_of_pred_ne]
theorem
Order.isPredLimit_of_pred_ne
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
(h : ∀ (b : α), Order.pred b ≠ a)
:
Alias of Order.isPredPrelimit_of_pred_ne.
theorem
Order.not_isPredPrelimit_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
:
¬Order.IsPredPrelimit a ↔ ∃ (b : α), ¬IsMin b ∧ Order.pred b = a
theorem
Order.mem_range_pred_of_not_isPredPrelimit
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
(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 α]
{a : α}
[PredOrder α]
(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 α]
{a : α}
[PredOrder α]
(H : ∀ b > a, a < Order.pred b)
:
@[deprecated Order.isPredPrelimit_of_pred_lt]
theorem
Order.isPredLimit_of_pred_lt
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
(H : ∀ b > a, a < Order.pred b)
:
Alias of Order.isPredPrelimit_of_pred_lt.
theorem
Order.IsPredPrelimit.lt_pred
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[PredOrder α]
(ha : Order.IsPredPrelimit a)
(hb : a < b)
:
a < Order.pred b
theorem
Order.IsPredLimit.lt_pred
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[PredOrder α]
(ha : Order.IsPredLimit a)
(hb : a < b)
:
a < Order.pred b
theorem
Order.IsPredPrelimit.lt_pred_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[PredOrder α]
(ha : Order.IsPredPrelimit a)
:
a < Order.pred b ↔ a < b
theorem
Order.IsPredLimit.lt_pred_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
{b : α}
[PredOrder α]
(ha : Order.IsPredLimit a)
:
a < Order.pred b ↔ a < b
theorem
Order.isPredPrelimit_iff_lt_pred
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
:
Order.IsPredPrelimit a ↔ ∀ b > a, a < Order.pred b
@[deprecated Order.isPredPrelimit_iff_lt_pred]
theorem
Order.isPredLimit_iff_lt_pred
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
:
Order.IsPredPrelimit a ↔ ∀ b > a, a < Order.pred b
Alias of Order.isPredPrelimit_iff_lt_pred.
theorem
Order.isPredPrelimit_iff_pred_ne
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
[NoMinOrder α]
:
Order.IsPredPrelimit a ↔ ∀ (b : α), Order.pred b ≠ a
theorem
Order.not_isPredPrelimit_iff'
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
[NoMinOrder α]
:
¬Order.IsPredPrelimit a ↔ a ∈ Set.range Order.pred
theorem
Order.IsPredPrelimit.isMax
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
(h : Order.IsPredPrelimit a)
:
IsMax a
@[deprecated Order.IsPredPrelimit.isMax]
theorem
Order.IsPredLimit.isMax
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
(h : Order.IsPredPrelimit a)
:
IsMax a
Alias of Order.IsPredPrelimit.isMax.
@[simp]
theorem
Order.isPredPrelimit_iff
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
:
@[simp]
theorem
Order.not_isPredLimit
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
:
theorem
Order.not_isPredPrelimit
{α : Type u_1}
[PartialOrder α]
{a : α}
[PredOrder α]
[IsPredArchimedean α]
[NoMaxOrder α]
:
Induction principles #
noncomputable def
Order.isSuccPrelimitRecOn
{α : 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)
:
C b
A value can be built by building it on successors and successor pre-limits.
Equations
- Order.isSuccPrelimitRecOn b hs hl = if hb : Order.IsSuccPrelimit b then hl b hb else cast ⋯ (hs (Classical.choose ⋯) ⋯)
Instances For
@[deprecated Order.isSuccPrelimitRecOn]
def
Order.isSuccLimitRecOn
{α : 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)
:
C b
Alias of Order.isSuccPrelimitRecOn.
A value can be built by building it on successors and successor pre-limits.
Instances For
@[simp]
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 α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
[NoMaxOrder α]
(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 α]
(hs : (a : α) → ¬IsMax a → C (Order.succ a))
(hl : (a : α) → Order.IsSuccPrelimit a → C a)
[NoMaxOrder α]
(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}
(b : α)
[PartialOrder α]
[PredOrder α]
(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 pre-limits.
Equations
- Order.isPredPrelimitRecOn b hs hl = Order.isSuccPrelimitRecOn b hs fun (a : αᵒᵈ) (ha : Order.IsSuccPrelimit a) => hl a ⋯
Instances For
@[deprecated Order.isPredPrelimitRecOn]
def
Order.isPredLimitRecOn
{α : 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)
:
C b
Alias of Order.isPredPrelimitRecOn.
A value can be built by building it on predecessors and predecessor pre-limits.
Instances For
@[simp]
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}
{b : α}
[LinearOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
(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}
{b : α}
[LinearOrder α]
[PredOrder α]
(hs : (a : α) → ¬IsMin a → C (Order.pred a))
(hl : (a : α) → Order.IsPredPrelimit a → C a)
(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}
(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)
:
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}
(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)
:
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.
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)
@[simp]
theorem
SuccOrder.prelimitRecOn_succ
{α : Type u_1}
{C : α → Sort u_2}
[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)
[NoMaxOrder α]
(b : α)
:
SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b ⋯ (SuccOrder.prelimitRecOn b hs hl)
@[deprecated SuccOrder.prelimitRecOn_succ]
theorem
SuccOrder.limitRecOn_succ
{α : Type u_1}
{C : α → Sort u_2}
[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)
[NoMaxOrder α]
(b : α)
:
SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b ⋯ (SuccOrder.prelimitRecOn b hs hl)
Alias of SuccOrder.prelimitRecOn_succ.
noncomputable def
PredOrder.prelimitRecOn
{α : 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)
:
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}
(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)
:
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.
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)
@[simp]
theorem
PredOrder.prelimitRecOn_pred
{α : Type u_1}
{C : α → Sort u_2}
[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)
[NoMinOrder α]
(b : α)
:
PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b ⋯ (PredOrder.prelimitRecOn b hp hl)
@[deprecated PredOrder.prelimitRecOn_pred]
theorem
PredOrder.limitRecOn_pred
{α : Type u_1}
{C : α → Sort u_2}
[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)
[NoMinOrder α]
(b : α)
:
PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b ⋯ (PredOrder.prelimitRecOn b hp hl)
Alias of PredOrder.prelimitRecOn_pred.