# 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.

### Successor limits #

source
def Order.IsSuccPrelimit {α : Type u_1} [LT α] (a : α) :
Prop

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

Instances For

source
theorem Order.not_isSuccPrelimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
¬IsSuccPrelimit a ↔ ∃ (b : α), b ⋖ a
source
@[simp]
theorem Order.IsSuccPrelimit.of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) :
IsSuccPrelimit a
source
def Order.IsSuccLimit {α : Type u_1} [Preorder α] (a : α) :
Prop

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

source
theorem Order.IsSuccLimit.not_isMin {α : Type u_1} {a : α} [Preorder α] (h : IsSuccLimit a) :
¬IsMin a
source
theorem Order.IsSuccLimit.isSuccPrelimit {α : Type u_1} {a : α} [Preorder α] (h : IsSuccLimit a) :
IsSuccPrelimit a
source
theorem Order.IsSuccPrelimit.isSuccLimit_of_not_isMin {α : Type u_1} {a : α} [Preorder α] (h : IsSuccPrelimit a) (ha : ¬IsMin a) :
IsSuccLimit a
source
theorem Order.IsSuccPrelimit.isSuccLimit {α : Type u_1} {a : α} [Preorder α] [NoMinOrder α] (h : IsSuccPrelimit a) :
IsSuccLimit a
source
theorem Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin {α : Type u_1} {a : α} [Preorder α] (h : ¬IsMin a) :
IsSuccPrelimit a ↔ IsSuccLimit a
source
theorem Order.isSuccPrelimit_iff_isSuccLimit {α : Type u_1} {a : α} [Preorder α] [NoMinOrder α] :
IsSuccPrelimit a ↔ IsSuccLimit a
source
theorem IsMin.not_isSuccLimit {α : Type u_1} {a : α} [Preorder α] (h : IsMin a) :
¬Order.IsSuccLimit a
source
theorem IsMin.isSuccPrelimit {α : Type u_1} {a : α} [Preorder α] :
IsMin a → Order.IsSuccPrelimit a
source
theorem Order.IsSuccLimit.nonempty_Iio {α : Type u_1} {a : α} [Preorder α] (h : IsSuccLimit a) :
(Set.Iio a).Nonempty
source
theorem Order.isSuccPrelimit_bot {α : Type u_1} [Preorder α] [OrderBot α] :
IsSuccPrelimit ⊥
source
theorem Order.not_isSuccLimit_bot {α : Type u_1} [Preorder α] [OrderBot α] :
¬IsSuccLimit ⊥
source
theorem Order.IsSuccLimit.ne_bot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] (h : IsSuccLimit a) :
a ≠ ⊥
source
theorem Order.not_isSuccLimit_iff {α : Type u_1} {a : α} [Preorder α] :
¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
source
theorem Order.IsSuccPrelimit.isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : IsSuccPrelimit (succ a)) :
IsMax a
source
theorem Order.IsSuccLimit.isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : IsSuccLimit (succ a)) :
IsMax a
source
theorem Order.not_isSuccPrelimit_succ_of_not_isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (ha : ¬IsMax a) :
¬IsSuccPrelimit (succ a)
source
theorem Order.not_isSuccLimit_succ_of_not_isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (ha : ¬IsMax a) :
¬IsSuccLimit (succ a)
source
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)) ⋯

Instances For

source
theorem Order.IsSuccPrelimit.succ_ne {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : IsSuccPrelimit a) (b : α) :
succ b ≠ a
source
theorem Order.IsSuccLimit.succ_ne {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : IsSuccLimit a) (b : α) :
succ b ≠ a
source
@[simp]
theorem Order.not_isSuccPrelimit_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
¬IsSuccPrelimit (succ a)
source
@[simp]
theorem Order.not_isSuccLimit_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :
¬IsSuccLimit (succ a)
source
theorem Order.IsSuccPrelimit.isMin_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] (h : IsSuccPrelimit a) :
IsMin a
source
@[simp]
theorem Order.isSuccPrelimit_iff_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] :
IsSuccPrelimit a ↔ IsMin a
source
@[simp]
theorem Order.not_isSuccLimit_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] :
¬IsSuccLimit a
source
theorem Order.not_isSuccPrelimit_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] [NoMinOrder α] :
¬IsSuccPrelimit a
source
theorem Order.isSuccLimit_iff {α : Type u_1} {a : α} [PartialOrder α] [OrderBot α] :
IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a
source
theorem Order.IsSuccLimit.bot_lt {α : Type u_1} {a : α} [PartialOrder α] [OrderBot α] (h : IsSuccLimit a) :
⊥ < a
source
theorem Order.isSuccPrelimit_of_succ_ne {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ∀ (b : α), succ b ≠ a) :
IsSuccPrelimit a
source
theorem Order.not_isSuccPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] :
¬IsSuccPrelimit a ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a
source
theorem Order.mem_range_succ_of_not_isSuccPrelimit {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ¬IsSuccPrelimit a) :
a ∈ Set.range succ

See `not_isSuccPrelimit_iff` for a version that states that `a` is a successor of a value other than itself.

source
theorem Order.mem_range_succ_or_isSuccPrelimit {α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) :
a ∈ Set.range succ ∨ IsSuccPrelimit a
source
theorem Order.isMin_or_mem_range_succ_or_isSuccLimit {α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) :
IsMin a ∨ a ∈ Set.range succ ∨ IsSuccLimit a
source
theorem Order.isSuccPrelimit_of_succ_lt {α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] (H : ∀ a < b, succ a < b) :
IsSuccPrelimit b
source
theorem Order.IsSuccPrelimit.succ_lt {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccPrelimit b) (ha : a < b) :
succ a < b
source
theorem Order.IsSuccLimit.succ_lt {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccLimit b) (ha : a < b) :
succ a < b
source
theorem Order.IsSuccPrelimit.succ_lt_iff {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccPrelimit b) :
succ a < b ↔ a < b
source
theorem Order.IsSuccLimit.succ_lt_iff {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccLimit b) :
succ a < b ↔ a < b
source
theorem Order.isSuccPrelimit_iff_succ_lt {α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] :
IsSuccPrelimit b ↔ ∀ a < b, succ a < b
source
theorem Order.isSuccPrelimit_iff_succ_ne {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] :
IsSuccPrelimit a ↔ ∀ (b : α), succ b ≠ a
source
theorem Order.not_isSuccPrelimit_iff' {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] :
¬IsSuccPrelimit a ↔ a ∈ Set.range succ
source
theorem Order.IsSuccPrelimit.isMin {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (h : IsSuccPrelimit a) :
IsMin a
source
@[simp]
theorem Order.isSuccPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] :
IsSuccPrelimit a ↔ IsMin a
source
@[simp]
theorem Order.not_isSuccLimit {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] :
¬IsSuccLimit a
source
theorem Order.not_isSuccPrelimit {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] [NoMinOrder α] :
¬IsSuccPrelimit a
source
theorem Order.IsSuccPrelimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccPrelimit a) :
a ≤ b ↔ ∀ c < a, c ≤ b
source
theorem Order.IsSuccLimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccLimit a) :
a ≤ b ↔ ∀ c < a, c ≤ b
source
theorem Order.IsSuccPrelimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccPrelimit b) :
a < b ↔ ∃ c < b, a < c
source
theorem Order.IsSuccLimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccLimit b) :
a < b ↔ ∃ c < b, a < c
source
theorem IsLUB.isSuccPrelimit_of_notMem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :
Order.IsSuccPrelimit a
source
@[deprecated IsLUB.isSuccPrelimit_of_notMem (since := "2025-05-23")]
theorem IsLUB.isSuccPrelimit_of_not_mem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :
Order.IsSuccPrelimit a

Alias of `IsLUB.isSuccPrelimit_of_notMem`.

source
theorem IsLUB.mem_of_not_isSuccPrelimit {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (ha : ¬Order.IsSuccPrelimit a) :
a ∈ s
source
theorem IsLUB.isSuccLimit_of_notMem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : a ∉ s) :
Order.IsSuccLimit a
source
@[deprecated IsLUB.isSuccLimit_of_notMem (since := "2025-05-23")]
theorem IsLUB.isSuccLimit_of_not_mem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : a ∉ s) :
Order.IsSuccLimit a

Alias of `IsLUB.isSuccLimit_of_notMem`.

source
theorem IsLUB.mem_of_not_isSuccLimit {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) (ha : ¬Order.IsSuccLimit a) :
a ∈ s
source
theorem Order.IsSuccPrelimit.isLUB_Iio {α : Type u_1} {a : α} [LinearOrder α] (ha : IsSuccPrelimit a) :
IsLUB (Set.Iio a) a
source
theorem Order.IsSuccLimit.isLUB_Iio {α : Type u_1} {a : α} [LinearOrder α] (ha : IsSuccLimit a) :
IsLUB (Set.Iio a) a
source
theorem Order.isLUB_Iio_iff_isSuccPrelimit {α : Type u_1} {a : α} [LinearOrder α] :
IsLUB (Set.Iio a) a ↔ IsSuccPrelimit a
source
theorem Order.IsSuccPrelimit.le_succ_iff {α : Type u_1} {a b : α} [LinearOrder α] [SuccOrder α] (hb : IsSuccPrelimit b) :
b ≤ succ a ↔ b ≤ a
source
theorem Order.IsSuccLimit.le_succ_iff {α : Type u_1} {a b : α} [LinearOrder α] [SuccOrder α] (hb : IsSuccLimit b) :
b ≤ succ a ↔ b ≤ a

### Predecessor limits #

source
def Order.IsPredPrelimit {α : Type u_1} [LT α] (a : α) :
Prop

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

Instances For

source
theorem Order.not_isPredPrelimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :
¬IsPredPrelimit a ↔ ∃ (b : α), a ⋖ b
source
@[simp]
theorem Order.IsPredPrelimit.of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) :
IsPredPrelimit a
source
@[simp]
theorem Order.isSuccPrelimit_toDual_iff {α : Type u_1} {a : α} [LT α] :
IsSuccPrelimit (OrderDual.toDual a) ↔ IsPredPrelimit a
source
@[simp]
theorem Order.isPredPrelimit_toDual_iff {α : Type u_1} {a : α} [LT α] :
IsPredPrelimit (OrderDual.toDual a) ↔ IsSuccPrelimit a
source
theorem Order.IsPredPrelimit.dual {α : Type u_1} {a : α} [LT α] :
IsPredPrelimit a → IsSuccPrelimit (OrderDual.toDual a)

Alias of the reverse direction of `Order.isSuccPrelimit_toDual_iff`.

source
theorem Order.IsSuccPrelimit.dual {α : Type u_1} {a : α} [LT α] :
IsSuccPrelimit a → IsPredPrelimit (OrderDual.toDual a)

Alias of the reverse direction of `Order.isPredPrelimit_toDual_iff`.

source
def Order.IsPredLimit {α : Type u_1} [Preorder α] (a : α) :
Prop

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

source
theorem Order.IsPredLimit.not_isMax {α : Type u_1} {a : α} [Preorder α] (h : IsPredLimit a) :
¬IsMax a
source
theorem Order.IsPredLimit.isPredPrelimit {α : Type u_1} {a : α} [Preorder α] (h : IsPredLimit a) :
IsPredPrelimit a
source
@[simp]
theorem Order.isSuccLimit_toDual_iff {α : Type u_1} {a : α} [Preorder α] :
IsSuccLimit (OrderDual.toDual a) ↔ IsPredLimit a
source
@[simp]
theorem Order.isPredLimit_toDual_iff {α : Type u_1} {a : α} [Preorder α] :
IsPredLimit (OrderDual.toDual a) ↔ IsSuccLimit a
source
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`.

source
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`.

source
theorem Order.IsPredPrelimit.isPredLimit_of_not_isMax {α : Type u_1} {a : α} [Preorder α] (h : IsPredPrelimit a) (ha : ¬IsMax a) :
IsPredLimit a
source
theorem Order.IsPredPrelimit.isPredLimit {α : Type u_1} {a : α} [Preorder α] [NoMaxOrder α] (h : IsPredPrelimit a) :
IsPredLimit a
source
theorem Order.isPredPrelimit_iff_isPredLimit_of_not_isMax {α : Type u_1} {a : α} [Preorder α] (h : ¬IsMax a) :
IsPredPrelimit a ↔ IsPredLimit a
source
theorem Order.isPredPrelimit_iff_isPredLimit {α : Type u_1} {a : α} [Preorder α] [NoMaxOrder α] :
IsPredPrelimit a ↔ IsPredLimit a
source
theorem IsMax.not_isPredLimit {α : Type u_1} {a : α} [Preorder α] (h : IsMax a) :
¬Order.IsPredLimit a
source
theorem IsMax.isPredPrelimit {α : Type u_1} {a : α} [Preorder α] :
IsMax a → Order.IsPredPrelimit a
source
theorem Order.IsPredLimit.nonempty_Ioi {α : Type u_1} {a : α} [Preorder α] (h : IsPredLimit a) :
(Set.Ioi a).Nonempty
source
theorem Order.isPredPrelimit_top {α : Type u_1} [Preorder α] [OrderTop α] :
IsPredPrelimit ⊤
source
theorem Order.not_isPredLimit_top {α : Type u_1} [Preorder α] [OrderTop α] :
¬IsPredLimit ⊤
source
theorem Order.IsPredLimit.ne_top {α : Type u_1} {a : α} [Preorder α] [OrderTop α] (h : IsPredLimit a) :
a ≠ ⊤
source
theorem Order.not_isPredLimit_iff {α : Type u_1} {a : α} [Preorder α] :
¬IsPredLimit a ↔ IsMax a ∨ ¬IsPredPrelimit a
source
theorem Order.not_isPredLimit_of_not_isPredPrelimit {α : Type u_1} {a : α} [Preorder α] (h : ¬IsPredPrelimit a) :
¬IsPredLimit a
source
theorem Order.IsPredPrelimit.isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (h : IsPredPrelimit (pred a)) :
IsMin a
source
theorem Order.IsPredLimit.isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (h : IsPredLimit (pred a)) :
IsMin a
source
theorem Order.not_isPredPrelimit_pred_of_not_isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (ha : ¬IsMin a) :
¬IsPredPrelimit (pred a)
source
theorem Order.not_isPredLimit_pred_of_not_isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (ha : ¬IsMin a) :
¬IsPredLimit (pred a)
source
theorem Order.IsPredPrelimit.pred_ne {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [NoMinOrder α] (h : IsPredPrelimit a) (b : α) :
pred b ≠ a
source
theorem Order.IsPredLimit.pred_ne {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [NoMinOrder α] (h : IsPredLimit a) (b : α) :
pred b ≠ a
source
@[simp]
theorem Order.not_isPredPrelimit_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
¬IsPredPrelimit (pred a)
source
@[simp]
theorem Order.not_isPredLimit_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :
¬IsPredLimit (pred a)
source
theorem Order.IsPredPrelimit.isMax_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] (h : IsPredPrelimit a) :
IsMax a
source
@[simp]
theorem Order.isPredPrelimit_iff_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] :
IsPredPrelimit a ↔ IsMax a
source
theorem Order.not_isPredPrelimit_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] [NoMaxOrder α] :
¬IsPredPrelimit a
source
@[simp]
theorem Order.not_isPredLimit_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] :
¬IsPredLimit a
source
theorem Order.isPredLimit_iff {α : Type u_1} {a : α} [PartialOrder α] [OrderTop α] :
IsPredLimit a ↔ a ≠ ⊤ ∧ IsPredPrelimit a
source
theorem Order.IsPredLimit.lt_top {α : Type u_1} {a : α} [PartialOrder α] [OrderTop α] (h : IsPredLimit a) :
a < ⊤
source
theorem Order.isPredPrelimit_of_pred_ne {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (h : ∀ (b : α), pred b ≠ a) :
IsPredPrelimit a
source
theorem Order.not_isPredPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] :
¬IsPredPrelimit a ↔ ∃ (b : α), ¬IsMin b ∧ pred b = a
source
theorem Order.mem_range_pred_of_not_isPredPrelimit {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (h : ¬IsPredPrelimit a) :
a ∈ Set.range pred

See `not_isPredPrelimit_iff` for a version that states that `a` is a successor of a value other than itself.

source
theorem Order.mem_range_pred_or_isPredPrelimit {α : Type u_1} [PartialOrder α] [PredOrder α] (a : α) :
a ∈ Set.range pred ∨ IsPredPrelimit a
source
theorem Order.isPredPrelimit_of_pred_lt {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (H : ∀ b > a, a < pred b) :
IsPredPrelimit a
source
theorem Order.IsPredPrelimit.lt_pred {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (ha : IsPredPrelimit a) (hb : a < b) :
a < pred b
source
theorem Order.IsPredLimit.lt_pred {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (ha : IsPredLimit a) (hb : a < b) :
a < pred b
source
theorem Order.IsPredPrelimit.lt_pred_iff {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (ha : IsPredPrelimit a) :
a < pred b ↔ a < b
source
theorem Order.IsPredLimit.lt_pred_iff {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (ha : IsPredLimit a) :
a < pred b ↔ a < b
source
theorem Order.isPredPrelimit_iff_lt_pred {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] :
IsPredPrelimit a ↔ ∀ b > a, a < pred b
source
theorem Order.isPredPrelimit_iff_pred_ne {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [NoMinOrder α] :
IsPredPrelimit a ↔ ∀ (b : α), pred b ≠ a
source
theorem Order.not_isPredPrelimit_iff' {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [NoMinOrder α] :
¬IsPredPrelimit a ↔ a ∈ Set.range pred
source
theorem Order.IsPredPrelimit.isMax {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (h : IsPredPrelimit a) :
IsMax a
source
@[simp]
theorem Order.isPredPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] :
IsPredPrelimit a ↔ IsMax a
source
@[simp]
theorem Order.not_isPredLimit {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] :
¬IsPredLimit a
source
theorem Order.not_isPredPrelimit {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [NoMaxOrder α] :
¬IsPredPrelimit a
source
theorem Order.IsPredPrelimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredPrelimit a) :
b ≤ a ↔ ∀ ⦃c : α⦄, a < c → b ≤ c
source
theorem Order.IsPredLimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredLimit a) :
b ≤ a ↔ ∀ ⦃c : α⦄, a < c → b ≤ c
source
theorem Order.IsPredPrelimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredPrelimit b) :
b < a ↔ ∃ (c : α), b < c ∧ c < a
source
theorem Order.IsPredLimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredLimit b) :
b < a ↔ ∃ (c : α), b < c ∧ c < a
source
theorem IsGLB.isPredPrelimit_of_notMem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :
Order.IsPredPrelimit a
source
@[deprecated IsGLB.isPredPrelimit_of_notMem (since := "2025-05-23")]
theorem IsGLB.isPredPrelimit_of_not_mem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :
Order.IsPredPrelimit a

Alias of `IsGLB.isPredPrelimit_of_notMem`.

source
theorem IsGLB.mem_of_not_isPredPrelimit {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (ha : ¬Order.IsPredPrelimit a) :
a ∈ s
source
theorem IsGLB.isPredLimit_of_notMem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : a ∉ s) :
Order.IsPredLimit a
source
@[deprecated IsGLB.isPredLimit_of_notMem (since := "2025-05-23")]
theorem IsGLB.isPredLimit_of_not_mem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : a ∉ s) :
Order.IsPredLimit a

Alias of `IsGLB.isPredLimit_of_notMem`.

source
theorem IsGLB.mem_of_not_isPredLimit {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty) (ha : ¬Order.IsPredLimit a) :
a ∈ s
source
theorem Order.IsPredPrelimit.isGLB_Ioi {α : Type u_1} {a : α} [LinearOrder α] (ha : IsPredPrelimit a) :
IsGLB (Set.Ioi a) a
source
theorem Order.IsPredLimit.isGLB_Ioi {α : Type u_1} {a : α} [LinearOrder α] (ha : IsPredLimit a) :
IsGLB (Set.Ioi a) a
source
theorem Order.isGLB_Ioi_iff_isPredPrelimit {α : Type u_1} {a : α} [LinearOrder α] :
IsGLB (Set.Ioi a) a ↔ IsPredPrelimit a
source
theorem Order.IsPredPrelimit.pred_le_iff {α : Type u_1} {a b : α} [LinearOrder α] [PredOrder α] (hb : IsPredPrelimit b) :
pred a ≤ b ↔ a ≤ b
source
theorem Order.IsPredLimit.pred_le_iff {α : Type u_1} {a b : α} [LinearOrder α] [PredOrder α] (hb : IsPredLimit b) :
pred a ≤ b ↔ a ≤ b

### Induction principles #

source
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 ⋯) ⋯)

Instances For

source
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) :
isSuccPrelimitRecOn b succ isSuccPrelimit = isSuccPrelimit b hb
source
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) :
isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb
source
@[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 : α) :
isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b ⋯
source
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 ⋯

Instances For

source
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) :
isPredPrelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb
source
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) :
isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb
source
@[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 : α) :
isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b ⋯
source
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 ⋯

Instances For

source
@[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) :
isSuccLimitRecOn b isMin succ isSuccLimit = isSuccLimit b hb
source
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) :
isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb
source
@[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 : α) :
isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b ⋯
source
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) :
isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb
source
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 ⋯

Instances For

source
@[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) :
isPredLimitRecOn b isMax pred isPredLimit = isPredLimit b hb
source
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) :
isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb
source
@[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 α] :
isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred b ⋯
source
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) :
isPredLimitRecOn b isMax pred isPredLimit = isMax b hb
source
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.

Instances For

source
@[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
source
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) :
prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb (prelimitRecOn b succ isSuccPrelimit)
source
@[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 : α) :
prelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b ⋯ (prelimitRecOn b succ isSuccPrelimit)
source
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.

Instances For

source
@[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) :
limitRecOn b isMin succ isSuccLimit = isMin b hb
source
@[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
source
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) :
limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb (limitRecOn b isMin succ isSuccLimit)
source
@[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 : α) :
limitRecOn (Order.succ b) isMin succ isSuccLimit = succ b ⋯ (limitRecOn b isMin succ isSuccLimit)
source
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 ⋯

Instances For

source
@[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
source
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) :
prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb (prelimitRecOn b pred isPredPrelimit)
source
@[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 : α) :
prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b ⋯ (prelimitRecOn b pred isPredPrelimit)
source
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 ⋯

Instances For

source
@[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) :
limitRecOn b isMax pred isPredLimit = isMax b hb
source
@[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
source
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) :
limitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb (limitRecOn b isMax pred isPredLimit)
source
@[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 : α) :
limitRecOn (Order.pred b) isMax pred isPredLimit = pred b ⋯ (limitRecOn b isMax pred isPredLimit)