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.
Use IsSuccLimit if you want to exclude the case of a minimal element.
Equations
- Order.IsSuccPrelimit a = ∀ (b : α), ¬b ⋖ a
@[simp]
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)
theorem
Order.IsSuccPrelimit.isSuccLimit_of_not_isMin
{α : Type u_1}
{a : α}
[Preorder α]
(h : IsSuccPrelimit a)
(ha : ¬IsMin a)
:
theorem
Order.IsSuccPrelimit.isSuccLimit
{α : Type u_1}
{a : α}
[Preorder α]
[NoMinOrder α]
(h : IsSuccPrelimit a)
:
theorem
Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin
{α : Type u_1}
{a : α}
[Preorder α]
(h : ¬IsMin a)
:
theorem
Order.IsSuccLimit.ne_bot
{α : Type u_1}
{a : α}
[Preorder α]
[OrderBot α]
(h : IsSuccLimit a)
:
theorem
Order.IsSuccPrelimit.isMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
(h : IsSuccPrelimit (succ a))
:
IsMax a
theorem
Order.IsSuccLimit.isMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
(h : IsSuccLimit (succ a))
:
IsMax a
theorem
Order.not_isSuccPrelimit_succ_of_not_isMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
(ha : ¬IsMax a)
:
¬IsSuccPrelimit (succ a)
theorem
Order.not_isSuccLimit_succ_of_not_isMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
(ha : ¬IsMax a)
:
¬IsSuccLimit (succ a)
noncomputable def
Order.IsSuccPrelimit.mid
{α : Type u_1}
[Preorder α]
{i j : α}
(hi : IsSuccPrelimit i)
(hj : j < i)
:
↑(Set.Ioo j i)
Given j < i with i a prelimit, IsSuccPrelimit.mid picks an arbitrary element strictly
between j and i.
Equations
- hi.mid hj = Classical.indefiniteDescription (Membership.mem (Set.Ioo j i)) ⋯
theorem
Order.IsSuccPrelimit.succ_ne
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(h : IsSuccPrelimit a)
(b : α)
:
theorem
Order.IsSuccLimit.succ_ne
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(h : IsSuccLimit a)
(b : α)
:
@[simp]
theorem
Order.not_isSuccPrelimit_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
¬IsSuccPrelimit (succ a)
@[simp]
theorem
Order.not_isSuccLimit_succ
{α : Type u_1}
[Preorder α]
[SuccOrder α]
[NoMaxOrder α]
(a : α)
:
¬IsSuccLimit (succ a)
theorem
Order.IsSuccPrelimit.isMin_of_noMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
(h : IsSuccPrelimit a)
:
IsMin a
@[simp]
theorem
Order.isSuccPrelimit_iff_of_noMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
:
@[simp]
theorem
Order.not_isSuccLimit_of_noMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
:
theorem
Order.not_isSuccPrelimit_of_noMax
{α : Type u_1}
{a : α}
[Preorder α]
[SuccOrder α]
[IsSuccArchimedean α]
[NoMaxOrder α]
[NoMinOrder α]
:
theorem
Order.IsSuccLimit.bot_lt
{α : Type u_1}
{a : α}
[PartialOrder α]
[OrderBot α]
(h : IsSuccLimit a)
:
theorem
Order.isSuccPrelimit_of_succ_ne
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
(h : ∀ (b : α), succ b ≠ a)
:
theorem
Order.mem_range_succ_of_not_isSuccPrelimit
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
(h : ¬IsSuccPrelimit a)
:
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 : α)
:
theorem
Order.isMin_or_mem_range_succ_or_isSuccLimit
{α : Type u_1}
[PartialOrder α]
[SuccOrder α]
(a : α)
:
theorem
Order.isSuccPrelimit_of_succ_lt
{α : Type u_1}
{b : α}
[PartialOrder α]
[SuccOrder α]
(H : ∀ a < b, succ a < b)
:
theorem
Order.IsSuccPrelimit.succ_lt
{α : Type u_1}
{a b : α}
[PartialOrder α]
[SuccOrder α]
(hb : IsSuccPrelimit b)
(ha : a < b)
:
theorem
Order.IsSuccLimit.succ_lt
{α : Type u_1}
{a b : α}
[PartialOrder α]
[SuccOrder α]
(hb : IsSuccLimit b)
(ha : a < b)
:
theorem
Order.IsSuccPrelimit.succ_lt_iff
{α : Type u_1}
{a b : α}
[PartialOrder α]
[SuccOrder α]
(hb : IsSuccPrelimit b)
:
theorem
Order.IsSuccLimit.succ_lt_iff
{α : Type u_1}
{a b : α}
[PartialOrder α]
[SuccOrder α]
(hb : IsSuccLimit b)
:
theorem
Order.isSuccPrelimit_iff_succ_ne
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
[NoMaxOrder α]
:
theorem
Order.not_isSuccPrelimit_iff'
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
[NoMaxOrder α]
:
theorem
Order.IsSuccPrelimit.isMin
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
[IsSuccArchimedean α]
(h : IsSuccPrelimit a)
:
IsMin a
@[simp]
theorem
Order.isSuccPrelimit_iff
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
[IsSuccArchimedean α]
:
@[simp]
theorem
Order.not_isSuccLimit
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
[IsSuccArchimedean α]
:
theorem
Order.not_isSuccPrelimit
{α : Type u_1}
{a : α}
[PartialOrder α]
[SuccOrder α]
[IsSuccArchimedean α]
[NoMinOrder α]
:
theorem
Order.IsSuccPrelimit.le_iff_forall_le
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsSuccPrelimit a)
:
theorem
Order.IsSuccLimit.le_iff_forall_le
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsSuccLimit a)
:
theorem
Order.IsSuccPrelimit.lt_iff_exists_lt
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsSuccPrelimit b)
:
theorem
Order.IsSuccLimit.lt_iff_exists_lt
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsSuccLimit b)
:
theorem
IsLUB.isSuccPrelimit_of_not_mem
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsLUB s a)
(ha : a ∉ s)
:
theorem
IsLUB.mem_of_not_isSuccPrelimit
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsLUB s a)
(ha : ¬Order.IsSuccPrelimit a)
:
theorem
IsLUB.isSuccLimit_of_not_mem
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsLUB s a)
(hs' : s.Nonempty)
(ha : a ∉ s)
:
theorem
IsLUB.mem_of_not_isSuccLimit
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsLUB s a)
(hs' : s.Nonempty)
(ha : ¬Order.IsSuccLimit a)
:
theorem
Order.IsSuccPrelimit.isLUB_Iio
{α : Type u_1}
{a : α}
[LinearOrder α]
(ha : IsSuccPrelimit a)
:
theorem
Order.IsSuccPrelimit.le_succ_iff
{α : Type u_1}
{a b : α}
[LinearOrder α]
[SuccOrder α]
(hb : IsSuccPrelimit b)
:
theorem
Order.IsSuccLimit.le_succ_iff
{α : Type u_1}
{a b : α}
[LinearOrder α]
[SuccOrder α]
(hb : IsSuccLimit b)
:
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.
Use IsPredLimit to exclude the case of a maximal element.
Equations
- Order.IsPredPrelimit a = ∀ (b : α), ¬a ⋖ b
@[simp]
@[simp]
@[simp]
Alias of the reverse direction of Order.isSuccPrelimit_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)
@[simp]
@[simp]
theorem
Order.IsPredLimit.dual
{α : Type u_1}
{a : α}
[Preorder α]
:
IsPredLimit a → IsSuccLimit (OrderDual.toDual a)
Alias of the reverse direction of Order.isSuccLimit_toDual_iff.
theorem
Order.IsSuccLimit.dual
{α : Type u_1}
{a : α}
[Preorder α]
:
IsSuccLimit a → IsPredLimit (OrderDual.toDual a)
Alias of the reverse direction of Order.isPredLimit_toDual_iff.
theorem
Order.IsPredPrelimit.isPredLimit_of_not_isMax
{α : Type u_1}
{a : α}
[Preorder α]
(h : IsPredPrelimit a)
(ha : ¬IsMax a)
:
theorem
Order.IsPredPrelimit.isPredLimit
{α : Type u_1}
{a : α}
[Preorder α]
[NoMaxOrder α]
(h : IsPredPrelimit a)
:
theorem
Order.isPredPrelimit_iff_isPredLimit_of_not_isMax
{α : Type u_1}
{a : α}
[Preorder α]
(h : ¬IsMax a)
:
theorem
Order.IsPredLimit.ne_top
{α : Type u_1}
{a : α}
[Preorder α]
[OrderTop α]
(h : IsPredLimit a)
:
theorem
Order.not_isPredLimit_of_not_isPredPrelimit
{α : Type u_1}
{a : α}
[Preorder α]
(h : ¬IsPredPrelimit a)
:
theorem
Order.IsPredPrelimit.isMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
(h : IsPredPrelimit (pred a))
:
IsMin a
theorem
Order.IsPredLimit.isMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
(h : IsPredLimit (pred a))
:
IsMin a
theorem
Order.not_isPredPrelimit_pred_of_not_isMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
(ha : ¬IsMin a)
:
¬IsPredPrelimit (pred a)
theorem
Order.not_isPredLimit_pred_of_not_isMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
(ha : ¬IsMin a)
:
¬IsPredLimit (pred a)
theorem
Order.IsPredPrelimit.pred_ne
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(h : IsPredPrelimit a)
(b : α)
:
theorem
Order.IsPredLimit.pred_ne
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(h : IsPredLimit a)
(b : α)
:
@[simp]
theorem
Order.not_isPredPrelimit_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
¬IsPredPrelimit (pred a)
@[simp]
theorem
Order.not_isPredLimit_pred
{α : Type u_1}
[Preorder α]
[PredOrder α]
[NoMinOrder α]
(a : α)
:
¬IsPredLimit (pred a)
theorem
Order.IsPredPrelimit.isMax_of_noMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
(h : IsPredPrelimit a)
:
IsMax a
@[simp]
theorem
Order.isPredPrelimit_iff_of_noMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
:
theorem
Order.not_isPredPrelimit_of_noMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
[NoMaxOrder α]
:
@[simp]
theorem
Order.not_isPredLimit_of_noMin
{α : Type u_1}
{a : α}
[Preorder α]
[PredOrder α]
[IsPredArchimedean α]
[NoMinOrder α]
:
theorem
Order.IsPredLimit.lt_top
{α : Type u_1}
{a : α}
[PartialOrder α]
[OrderTop α]
(h : IsPredLimit a)
:
theorem
Order.isPredPrelimit_of_pred_ne
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
(h : ∀ (b : α), pred b ≠ a)
:
theorem
Order.mem_range_pred_of_not_isPredPrelimit
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
(h : ¬IsPredPrelimit a)
:
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 : α)
:
theorem
Order.isPredPrelimit_of_pred_lt
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
(H : ∀ b > a, a < pred b)
:
theorem
Order.IsPredPrelimit.lt_pred
{α : Type u_1}
{a b : α}
[PartialOrder α]
[PredOrder α]
(ha : IsPredPrelimit a)
(hb : a < b)
:
theorem
Order.IsPredLimit.lt_pred
{α : Type u_1}
{a b : α}
[PartialOrder α]
[PredOrder α]
(ha : IsPredLimit a)
(hb : a < b)
:
theorem
Order.IsPredPrelimit.lt_pred_iff
{α : Type u_1}
{a b : α}
[PartialOrder α]
[PredOrder α]
(ha : IsPredPrelimit a)
:
theorem
Order.IsPredLimit.lt_pred_iff
{α : Type u_1}
{a b : α}
[PartialOrder α]
[PredOrder α]
(ha : IsPredLimit a)
:
theorem
Order.isPredPrelimit_iff_pred_ne
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
[NoMinOrder α]
:
theorem
Order.not_isPredPrelimit_iff'
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
[NoMinOrder α]
:
theorem
Order.IsPredPrelimit.isMax
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
[IsPredArchimedean α]
(h : IsPredPrelimit a)
:
IsMax a
@[simp]
theorem
Order.isPredPrelimit_iff
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
[IsPredArchimedean α]
:
@[simp]
theorem
Order.not_isPredLimit
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
[IsPredArchimedean α]
:
theorem
Order.not_isPredPrelimit
{α : Type u_1}
{a : α}
[PartialOrder α]
[PredOrder α]
[IsPredArchimedean α]
[NoMaxOrder α]
:
theorem
Order.IsPredPrelimit.le_iff_forall_le
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsPredPrelimit a)
:
theorem
Order.IsPredLimit.le_iff_forall_le
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsPredLimit a)
:
theorem
Order.IsPredPrelimit.lt_iff_exists_lt
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsPredPrelimit b)
:
theorem
Order.IsPredLimit.lt_iff_exists_lt
{α : Type u_1}
{a b : α}
[LinearOrder α]
(h : IsPredLimit b)
:
theorem
IsGLB.isPredPrelimit_of_not_mem
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsGLB s a)
(ha : a ∉ s)
:
theorem
IsGLB.mem_of_not_isPredPrelimit
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsGLB s a)
(ha : ¬Order.IsPredPrelimit a)
:
theorem
IsGLB.isPredLimit_of_not_mem
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsGLB s a)
(hs' : s.Nonempty)
(ha : a ∉ s)
:
theorem
IsGLB.mem_of_not_isPredLimit
{α : Type u_1}
{a : α}
[LinearOrder α]
{s : Set α}
(hs : IsGLB s a)
(hs' : s.Nonempty)
(ha : ¬Order.IsPredLimit a)
:
theorem
Order.IsPredPrelimit.isGLB_Ioi
{α : Type u_1}
{a : α}
[LinearOrder α]
(ha : IsPredPrelimit a)
:
theorem
Order.IsPredPrelimit.pred_le_iff
{α : Type u_1}
{a b : α}
[LinearOrder α]
[PredOrder α]
(hb : IsPredPrelimit b)
:
theorem
Order.IsPredLimit.pred_le_iff
{α : Type u_1}
{a b : α}
[LinearOrder α]
[PredOrder α]
(hb : IsPredLimit b)
:
Induction principles #
noncomputable def
Order.isSuccPrelimitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a)
:
motive b
A value can be built by building it on successors and successor pre-limits.
Equations
- Order.isSuccPrelimitRecOn b succ isSuccPrelimit = if hb : Order.IsSuccPrelimit b then isSuccPrelimit b hb else cast ⋯ (succ (Classical.choose ⋯) ⋯)
theorem
Order.isSuccPrelimitRecOn_of_isSuccPrelimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a)
(hb : IsSuccPrelimit b)
:
theorem
Order.isSuccPrelimitRecOn_succ_of_not_isMax
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a)
(hb : ¬IsMax b)
:
@[simp]
theorem
Order.isSuccPrelimitRecOn_succ
{α : Type u_1}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a)
[NoMaxOrder α]
(b : α)
:
noncomputable def
Order.isPredPrelimitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredPrelimit : (a : α) → IsPredPrelimit a → motive a)
:
motive b
A value can be built by building it on predecessors and predecessor pre-limits.
Equations
- Order.isPredPrelimitRecOn b pred isPredPrelimit = Order.isSuccPrelimitRecOn b pred fun (a : αᵒᵈ) (ha : Order.IsSuccPrelimit a) => isPredPrelimit a ⋯
theorem
Order.isPredPrelimitRecOn_of_isPredPrelimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredPrelimit : (a : α) → IsPredPrelimit a → motive a)
(hb : IsPredPrelimit b)
:
theorem
Order.isPredPrelimitRecOn_pred_of_not_isMin
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredPrelimit : (a : α) → IsPredPrelimit a → motive a)
(hb : ¬IsMin b)
:
@[simp]
theorem
Order.isPredPrelimitRecOn_pred
{α : Type u_1}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredPrelimit : (a : α) → IsPredPrelimit a → motive a)
[NoMinOrder α]
(b : α)
:
noncomputable def
Order.isSuccLimitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccLimit : (a : α) → IsSuccLimit a → motive a)
:
motive b
A value can be built by building it on minimal elements, successors, and successor limits.
Equations
- Order.isSuccLimitRecOn b isMin succ isSuccLimit = Order.isSuccPrelimitRecOn b succ fun (a : α) (ha : Order.IsSuccPrelimit a) => if h : IsMin a then isMin a h else isSuccLimit a ⋯
@[simp]
theorem
Order.isSuccLimitRecOn_of_isSuccLimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccLimit : (a : α) → IsSuccLimit a → motive a)
(hb : IsSuccLimit b)
:
theorem
Order.isSuccLimitRecOn_succ_of_not_isMax
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccLimit : (a : α) → IsSuccLimit a → motive a)
(hb : ¬IsMax b)
:
@[simp]
theorem
Order.isSuccLimitRecOn_succ
{α : Type u_1}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccLimit : (a : α) → IsSuccLimit a → motive a)
[NoMaxOrder α]
(b : α)
:
theorem
Order.isSuccLimitRecOn_of_isMin
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive (succ a))
(isSuccLimit : (a : α) → IsSuccLimit a → motive a)
(hb : IsMin b)
:
noncomputable def
Order.isPredLimitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredLimit : (a : α) → IsPredLimit a → motive a)
:
motive b
A value can be built by building it on maximal elements, predecessors, and predecessor limits.
Equations
- Order.isPredLimitRecOn b isMax pred isPredLimit = Order.isSuccLimitRecOn b isMax pred fun (a : αᵒᵈ) (ha : Order.IsSuccLimit a) => isPredLimit a ⋯
@[simp]
theorem
Order.isPredLimitRecOn_of_isPredLimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredLimit : (a : α) → IsPredLimit a → motive a)
(hb : IsPredLimit b)
:
theorem
Order.isPredLimitRecOn_pred_of_not_isMin
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredLimit : (a : α) → IsPredLimit a → motive a)
(hb : ¬IsMin b)
:
@[simp]
theorem
Order.isPredLimitRecOn_pred
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredLimit : (a : α) → IsPredLimit a → motive a)
[NoMinOrder α]
:
theorem
Order.isPredLimitRecOn_of_isMax
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive (pred a))
(isPredLimit : (a : α) → IsPredLimit a → motive a)
(hb : IsMax b)
:
noncomputable def
SuccOrder.prelimitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a)
:
motive b
Recursion principle on a well-founded partial SuccOrder.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
SuccOrder.prelimitRecOn_of_isSuccPrelimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a)
(hb : Order.IsSuccPrelimit b)
:
prelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb fun (x : α) (x_1 : x < b) => prelimitRecOn x succ isSuccPrelimit
theorem
SuccOrder.prelimitRecOn_succ_of_not_isMax
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
[WellFoundedLT α]
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a)
(hb : ¬IsMax b)
:
@[simp]
theorem
SuccOrder.prelimitRecOn_succ
{α : Type u_1}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
[WellFoundedLT α]
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a)
[NoMaxOrder α]
(b : α)
:
noncomputable def
SuccOrder.limitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a)
:
motive b
Recursion principle on a well-founded partial SuccOrder, separating out the case of a
minimal element.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
SuccOrder.limitRecOn_isMin
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a)
(hb : IsMin b)
:
@[simp]
theorem
SuccOrder.limitRecOn_of_isSuccLimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[SuccOrder α]
[WellFoundedLT α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a)
(hb : Order.IsSuccLimit b)
:
limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun (x : α) (x_1 : x < b) => limitRecOn x isMin succ isSuccLimit
theorem
SuccOrder.limitRecOn_succ_of_not_isMax
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
[WellFoundedLT α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a)
(hb : ¬IsMax b)
:
@[simp]
theorem
SuccOrder.limitRecOn_succ
{α : Type u_1}
{motive : α → Sort u_2}
[LinearOrder α]
[SuccOrder α]
[WellFoundedLT α]
(isMin : (a : α) → IsMin a → motive a)
(succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
(isSuccLimit : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a)
[NoMaxOrder α]
(b : α)
:
noncomputable def
PredOrder.prelimitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → motive b) → motive a)
:
motive b
Recursion principle on a well-founded partial PredOrder.
Equations
- PredOrder.prelimitRecOn b pred isPredPrelimit = SuccOrder.prelimitRecOn b pred fun (a : αᵒᵈ) (ha : Order.IsSuccPrelimit a) => isPredPrelimit a ⋯
@[simp]
theorem
PredOrder.prelimitRecOn_of_isPredPrelimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → motive b) → motive a)
(hb : Order.IsPredPrelimit b)
:
prelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb fun (x : α) (x_1 : x > b) => prelimitRecOn x pred isPredPrelimit
theorem
PredOrder.prelimitRecOn_pred_of_not_isMin
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
[WellFoundedGT α]
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → motive b) → motive a)
(hb : ¬IsMin b)
:
@[simp]
theorem
PredOrder.prelimitRecOn_pred
{α : Type u_1}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
[WellFoundedGT α]
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → motive b) → motive a)
[NoMinOrder α]
(b : α)
:
noncomputable def
PredOrder.limitRecOn
{α : Type u_1}
(b : α)
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → motive b) → motive a)
:
motive b
Recursion principle on a well-founded partial PredOrder, separating out the case of a
maximal element.
Equations
- PredOrder.limitRecOn b isMax pred isPredLimit = SuccOrder.limitRecOn b isMax pred fun (a : αᵒᵈ) (ha : Order.IsSuccLimit a) => isPredLimit a ⋯
@[simp]
theorem
PredOrder.limitRecOn_isMax
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → motive b) → motive a)
(hb : IsMax b)
:
@[simp]
theorem
PredOrder.limitRecOn_of_isPredLimit
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[PartialOrder α]
[PredOrder α]
[WellFoundedGT α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → motive b) → motive a)
(hb : Order.IsPredLimit b)
:
limitRecOn b isMax pred isPredLimit = isPredLimit b hb fun (x : α) (x_1 : x > b) => limitRecOn x isMax pred isPredLimit
theorem
PredOrder.limitRecOn_pred_of_not_isMin
{α : Type u_1}
{b : α}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
[WellFoundedGT α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → motive b) → motive a)
(hb : ¬IsMin b)
:
@[simp]
theorem
PredOrder.limitRecOn_pred
{α : Type u_1}
{motive : α → Sort u_2}
[LinearOrder α]
[PredOrder α]
[WellFoundedGT α]
(isMax : (a : α) → IsMax a → motive a)
(pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
(isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → motive b) → motive a)
[NoMinOrder α]
(b : α)
: