Documentation

Mathlib.Order.SuccPred.Limit

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 #

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

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

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

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

theorem Order.not_isSuccPrelimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :

¬IsSuccPrelimit a ↔ ∃ (b : α), b ⋖ a

theorem Order.not_isPredPrelimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :

¬IsPredPrelimit a ↔ ∃ (b : α), a ⋖ b

@[simp]

theorem Order.IsSuccPrelimit.of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) :

IsSuccPrelimit a

@[simp]

theorem Order.IsPredPrelimit.of_dense {α : Type u_1} [LT α] [DenselyOrdered α] (a : α) :

IsPredPrelimit a

@[simp]

theorem Order.isSuccPrelimit_toDual_iff {α : Type u_1} {a : α} [LT α] :

IsSuccPrelimit (OrderDual.toDual a) ↔ IsPredPrelimit a

@[simp]

theorem Order.isPredPrelimit_toDual_iff {α : Type u_1} {a : α} [LT α] :

IsPredPrelimit (OrderDual.toDual a) ↔ IsSuccPrelimit a

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.

theorem Order.IsSuccPrelimit.dual {α : Type u_1} {a : α} [LT α] :

IsSuccPrelimit a → IsPredPrelimit (OrderDual.toDual a)

def Order.IsSuccLimit {α : Type u_1} [Preorder α] (a : α) :

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.

Use IsSuccPrelimit if you want to include the case of a minimal element.

Equations

Order.IsSuccLimit a = (¬IsMin a ∧ Order.IsSuccPrelimit a)

Instances For

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

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.

Use IsPredPrelimit if you want to include the case of a maximal element.

Equations

Order.IsPredLimit a = (¬IsMax a ∧ Order.IsPredPrelimit a)

Instances For

theorem Order.IsSuccLimit.not_isMin {α : Type u_1} {a : α} [Preorder α] (h : IsSuccLimit a) :

theorem Order.IsPredLimit.not_isMax {α : Type u_1} {a : α} [Preorder α] (h : IsPredLimit a) :

theorem Order.IsSuccLimit.isSuccPrelimit {α : Type u_1} {a : α} [Preorder α] (h : IsSuccLimit a) :

IsSuccPrelimit a

theorem Order.IsPredLimit.isPredPrelimit {α : Type u_1} {a : α} [Preorder α] (h : IsPredLimit a) :

IsPredPrelimit a

theorem Order.IsSuccPrelimit.isSuccLimit_of_not_isMin {α : Type u_1} {a : α} [Preorder α] (h : IsSuccPrelimit a) (ha : ¬IsMin a) :

theorem Order.IsPredPrelimit.isPredLimit_of_not_isMax {α : Type u_1} {a : α} [Preorder α] (h : IsPredPrelimit a) (ha : ¬IsMax a) :

theorem Order.IsSuccPrelimit.isSuccLimit {α : Type u_1} {a : α} [Preorder α] [NoMinOrder α] (h : IsSuccPrelimit a) :

theorem Order.IsPredPrelimit.isPredLimit {α : Type u_1} {a : α} [Preorder α] [NoMaxOrder α] (h : IsPredPrelimit a) :

theorem Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin {α : Type u_1} {a : α} [Preorder α] (h : ¬IsMin a) :

IsSuccPrelimit a ↔ IsSuccLimit a

theorem Order.isPredPrelimit_iff_isPredLimit_of_not_isMax {α : Type u_1} {a : α} [Preorder α] (h : ¬IsMax a) :

IsPredPrelimit a ↔ IsPredLimit a

theorem Order.isSuccPrelimit_iff_isSuccLimit {α : Type u_1} {a : α} [Preorder α] [NoMinOrder α] :

IsSuccPrelimit a ↔ IsSuccLimit a

theorem Order.isPredPrelimit_iff_isPredLimit {α : Type u_1} {a : α} [Preorder α] [NoMaxOrder α] :

IsPredPrelimit a ↔ IsPredLimit a

theorem IsMin.not_isSuccLimit {α : Type u_1} {a : α} [Preorder α] (h : IsMin a) :

¬Order.IsSuccLimit a

theorem IsMax.not_isPredLimit {α : Type u_1} {a : α} [Preorder α] (h : IsMax a) :

¬Order.IsPredLimit a

theorem IsMin.isSuccPrelimit {α : Type u_1} {a : α} [Preorder α] :

IsMin a → Order.IsSuccPrelimit a

theorem IsMax.isPredPrelimit {α : Type u_1} {a : α} [Preorder α] :

IsMax a → Order.IsPredPrelimit a

theorem Order.IsSuccLimit.nonempty_Iio {α : Type u_1} {a : α} [Preorder α] (h : IsSuccLimit a) :

(Set.Iio a).Nonempty

theorem Order.isSuccPrelimit_bot {α : Type u_1} [Preorder α] [OrderBot α] :

IsSuccPrelimit ⊥

theorem Order.isPredPrelimit_top {α : Type u_1} [Preorder α] [OrderTop α] :

IsPredPrelimit ⊤

theorem Order.not_isSuccLimit_bot {α : Type u_1} [Preorder α] [OrderBot α] :

¬IsSuccLimit ⊥

theorem Order.not_isPredLimit_top {α : Type u_1} [Preorder α] [OrderTop α] :

¬IsPredLimit ⊤

theorem Order.IsSuccLimit.ne_bot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] (h : IsSuccLimit a) :

theorem Order.IsPredLimit.ne_top {α : Type u_1} {a : α} [Preorder α] [OrderTop α] (h : IsPredLimit a) :

theorem Order.not_isSuccLimit_iff {α : Type u_1} {a : α} [Preorder α] :

¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a

theorem Order.not_isPredLimit_iff {α : Type u_1} {a : α} [Preorder α] :

¬IsPredLimit a ↔ IsMax a ∨ ¬IsPredPrelimit a

theorem Order.IsSuccPrelimit.isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : IsSuccPrelimit (succ a)) :

theorem Order.IsPredPrelimit.isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (h : IsPredPrelimit (pred a)) :

theorem Order.IsSuccLimit.isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (h : IsSuccLimit (succ a)) :

theorem Order.IsPredLimit.isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (h : IsPredLimit (pred a)) :

theorem Order.not_isSuccPrelimit_succ_of_not_isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (ha : ¬IsMax a) :

¬IsSuccPrelimit (succ a)

theorem Order.not_isPredPrelimit_pred_of_not_isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (ha : ¬IsMin a) :

¬IsPredPrelimit (pred a)

theorem Order.not_isSuccLimit_succ_of_not_isMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] (ha : ¬IsMax a) :

¬IsSuccLimit (succ a)

theorem Order.not_isPredLimit_pred_of_not_isMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] (ha : ¬IsMin a) :

¬IsPredLimit (pred 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)) ⋯

Instances For

theorem Order.IsSuccPrelimit.succ_ne {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : IsSuccPrelimit a) (b : α) :

theorem Order.IsPredPrelimit.pred_ne {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [NoMinOrder α] (h : IsPredPrelimit a) (b : α) :

theorem Order.IsSuccLimit.succ_ne {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [NoMaxOrder α] (h : IsSuccLimit a) (b : α) :

theorem Order.IsPredLimit.pred_ne {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [NoMinOrder α] (h : IsPredLimit a) (b : α) :

@[simp]

theorem Order.not_isSuccPrelimit_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :

¬IsSuccPrelimit (succ a)

@[simp]

theorem Order.not_isPredPrelimit_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :

¬IsPredPrelimit (pred a)

@[simp]

theorem Order.not_isSuccLimit_succ {α : Type u_1} [Preorder α] [SuccOrder α] [NoMaxOrder α] (a : α) :

¬IsSuccLimit (succ a)

@[simp]

theorem Order.not_isPredLimit_pred {α : Type u_1} [Preorder α] [PredOrder α] [NoMinOrder α] (a : α) :

¬IsPredLimit (pred a)

theorem Order.IsSuccPrelimit.isMin_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] (h : IsSuccPrelimit a) :

@[simp]

theorem Order.isSuccPrelimit_iff_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] :

IsSuccPrelimit a ↔ IsMin a

@[simp]

theorem Order.not_isSuccLimit_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] :

¬IsSuccLimit a

theorem Order.not_isSuccPrelimit_of_noMax {α : Type u_1} {a : α} [Preorder α] [SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α] [NoMinOrder α] :

¬IsSuccPrelimit a

theorem Order.isSuccLimit_iff {α : Type u_1} {a : α} [PartialOrder α] [OrderBot α] :

IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

theorem Order.isPredLimit_iff {α : Type u_1} {a : α} [PartialOrder α] [OrderTop α] :

IsPredLimit a ↔ a ≠ ⊤ ∧ IsPredPrelimit a

theorem Order.IsSuccLimit.bot_lt {α : Type u_1} {a : α} [PartialOrder α] [OrderBot α] (h : IsSuccLimit a) :

theorem Order.IsPredLimit.lt_top {α : Type u_1} {a : α} [PartialOrder α] [OrderTop α] (h : IsPredLimit a) :

theorem Order.isSuccPrelimit_of_succ_ne {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] (h : ∀ (b : α), succ b ≠ a) :

IsSuccPrelimit a

theorem Order.isPredPrelimit_of_pred_ne {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (h : ∀ (b : α), pred b ≠ a) :

IsPredPrelimit a

theorem Order.not_isSuccPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] :

¬IsSuccPrelimit a ↔ ∃ (b : α), ¬IsMax b ∧ succ b = a

theorem Order.not_isPredPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] :

¬IsPredPrelimit a ↔ ∃ (b : α), ¬IsMin b ∧ pred b = a

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.

theorem Order.mem_range_pred_of_not_isPredPrelimit {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] (h : ¬IsPredPrelimit a) :

a ∈ Set.range pred

theorem Order.mem_range_succ_or_isSuccPrelimit {α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) :

a ∈ Set.range succ ∨ IsSuccPrelimit a

theorem Order.mem_range_pred_or_isPredPrelimit {α : Type u_1} [PartialOrder α] [PredOrder α] (a : α) :

a ∈ Set.range pred ∨ IsPredPrelimit a

theorem Order.isMin_or_mem_range_succ_or_isSuccLimit {α : Type u_1} [PartialOrder α] [SuccOrder α] (a : α) :

IsMin a ∨ a ∈ Set.range succ ∨ IsSuccLimit a

theorem Order.isMax_or_mem_range_pred_or_isPredLimit {α : Type u_1} [PartialOrder α] [PredOrder α] (a : α) :

IsMax a ∨ a ∈ Set.range pred ∨ IsPredLimit a

theorem Order.isSuccPrelimit_of_succ_lt {α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] (H : ∀ a < b, succ a < b) :

IsSuccPrelimit b

theorem Order.isPredPrelimit_of_lt_pred {α : Type u_1} {b : α} [PartialOrder α] [PredOrder α] (H : ∀ (a : α), b < a → b < pred a) :

IsPredPrelimit b

@[deprecated Order.isPredPrelimit_of_lt_pred (since := "2025-12-20")]

theorem Order.isPredPrelimit_of_pred_lt {α : Type u_1} {b : α} [PartialOrder α] [PredOrder α] (H : ∀ (a : α), b < a → b < pred a) :

IsPredPrelimit b

Alias of Order.isPredPrelimit_of_lt_pred.

theorem Order.IsSuccPrelimit.succ_lt {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccPrelimit b) (ha : a < b) :

succ a < b

theorem Order.IsPredPrelimit.lt_pred {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (hb : IsPredPrelimit b) (ha : b < a) :

b < pred a

theorem Order.IsSuccLimit.succ_lt {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccLimit b) (ha : a < b) :

succ a < b

theorem Order.IsPredLimit.lt_pred {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (hb : IsPredLimit b) (ha : b < a) :

b < pred a

theorem Order.IsSuccPrelimit.succ_lt_iff {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccPrelimit b) :

succ a < b ↔ a < b

theorem Order.IsPredPrelimit.lt_pred_iff {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (hb : IsPredPrelimit b) :

b < pred a ↔ b < a

theorem Order.IsSuccLimit.succ_lt_iff {α : Type u_1} {a b : α} [PartialOrder α] [SuccOrder α] (hb : IsSuccLimit b) :

succ a < b ↔ a < b

theorem Order.IsPredLimit.lt_pred_iff {α : Type u_1} {a b : α} [PartialOrder α] [PredOrder α] (hb : IsPredLimit b) :

b < pred a ↔ b < a

theorem Order.isSuccPrelimit_iff_succ_lt {α : Type u_1} {b : α} [PartialOrder α] [SuccOrder α] :

IsSuccPrelimit b ↔ ∀ a < b, succ a < b

theorem Order.isPredPrelimit_iff_lt_pred {α : Type u_1} {b : α} [PartialOrder α] [PredOrder α] :

IsPredPrelimit b ↔ ∀ (a : α), b < a → b < pred a

theorem Order.isSuccPrelimit_iff_succ_ne {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] :

IsSuccPrelimit a ↔ ∀ (b : α), succ b ≠ a

theorem Order.isPredPrelimit_iff_pred_ne {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [NoMinOrder α] :

IsPredPrelimit a ↔ ∀ (b : α), pred b ≠ a

theorem Order.not_isSuccPrelimit_iff' {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [NoMaxOrder α] :

¬IsSuccPrelimit a ↔ a ∈ Set.range succ

theorem Order.not_isPredPrelimit_iff' {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [NoMinOrder α] :

¬IsPredPrelimit a ↔ a ∈ Set.range pred

theorem Order.IsSuccPrelimit.isMin {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] (h : IsSuccPrelimit a) :

@[simp]

theorem Order.isSuccPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] :

IsSuccPrelimit a ↔ IsMin a

@[simp]

theorem Order.not_isSuccLimit {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] :

¬IsSuccLimit a

theorem Order.not_isSuccPrelimit {α : Type u_1} {a : α} [PartialOrder α] [SuccOrder α] [IsSuccArchimedean α] [NoMinOrder α] :

¬IsSuccPrelimit a

theorem Order.IsSuccPrelimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccPrelimit a) :

a ≤ b ↔ ∀ c < a, c ≤ b

theorem Order.IsSuccLimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccLimit a) :

a ≤ b ↔ ∀ c < a, c ≤ b

theorem Order.IsSuccPrelimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccPrelimit b) :

a < b ↔ ∃ c < b, a < c

theorem Order.IsSuccLimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsSuccLimit b) :

a < b ↔ ∃ c < b, a < c

theorem IsLUB.isSuccPrelimit_of_notMem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :

Order.IsSuccPrelimit a

theorem IsLUB.mem_of_not_isSuccPrelimit {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsLUB s a) (ha : ¬Order.IsSuccPrelimit a) :

a ∈ s

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

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

theorem Order.IsSuccPrelimit.isLUB_Iio {α : Type u_1} {a : α} [LinearOrder α] (ha : IsSuccPrelimit a) :

IsLUB (Set.Iio a) a

theorem Order.IsSuccLimit.isLUB_Iio {α : Type u_1} {a : α} [LinearOrder α] (ha : IsSuccLimit a) :

IsLUB (Set.Iio a) a

theorem Order.isLUB_Iio_iff_isSuccPrelimit {α : Type u_1} {a : α} [LinearOrder α] :

IsLUB (Set.Iio a) a ↔ IsSuccPrelimit a

theorem Order.IsSuccPrelimit.le_succ_iff {α : Type u_1} {a b : α} [LinearOrder α] [SuccOrder α] (hb : IsSuccPrelimit b) :

b ≤ succ a ↔ b ≤ a

theorem Order.IsPredPrelimit.pred_le_iff {α : Type u_1} {a b : α} [LinearOrder α] [PredOrder α] (hb : IsPredPrelimit b) :

pred a ≤ b ↔ a ≤ b

theorem Order.IsSuccLimit.le_succ_iff {α : Type u_1} {a b : α} [LinearOrder α] [SuccOrder α] (hb : IsSuccLimit b) :

b ≤ succ a ↔ b ≤ a

theorem Order.IsPredLimit.pred_le_iff {α : Type u_1} {a b : α} [LinearOrder α] [PredOrder α] (hb : IsPredLimit b) :

pred a ≤ b ↔ a ≤ b

Predecessor limits #

@[simp]

theorem Order.isSuccLimit_toDual_iff {α : Type u_1} {a : α} [Preorder α] :

IsSuccLimit (OrderDual.toDual a) ↔ IsPredLimit a

@[simp]

theorem Order.isPredLimit_toDual_iff {α : Type u_1} {a : α} [Preorder α] :

IsPredLimit (OrderDual.toDual a) ↔ IsSuccLimit a

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.IsPredLimit.nonempty_Ioi {α : Type u_1} {a : α} [Preorder α] (h : IsPredLimit a) :

(Set.Ioi a).Nonempty

theorem Order.not_isPredLimit_of_not_isPredPrelimit {α : Type u_1} {a : α} [Preorder α] (h : ¬IsPredPrelimit a) :

¬IsPredLimit a

theorem Order.IsPredPrelimit.isMax_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] (h : IsPredPrelimit a) :

@[simp]

theorem Order.isPredPrelimit_iff_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] :

IsPredPrelimit a ↔ IsMax a

theorem Order.not_isPredPrelimit_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] [NoMaxOrder α] :

¬IsPredPrelimit a

@[simp]

theorem Order.not_isPredLimit_of_noMin {α : Type u_1} {a : α} [Preorder α] [PredOrder α] [IsPredArchimedean α] [NoMinOrder α] :

¬IsPredLimit a

theorem Order.IsPredPrelimit.isMax {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] (h : IsPredPrelimit a) :

@[simp]

theorem Order.isPredPrelimit_iff {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] :

IsPredPrelimit a ↔ IsMax a

@[simp]

theorem Order.not_isPredLimit {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] :

¬IsPredLimit a

theorem Order.not_isPredPrelimit {α : Type u_1} {a : α} [PartialOrder α] [PredOrder α] [IsPredArchimedean α] [NoMaxOrder α] :

¬IsPredPrelimit a

theorem Order.IsPredPrelimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredPrelimit a) :

b ≤ a ↔ ∀ ⦃c : α⦄, a < c → b ≤ c

theorem Order.IsPredLimit.le_iff_forall_le {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredLimit a) :

b ≤ a ↔ ∀ ⦃c : α⦄, a < c → b ≤ c

theorem Order.IsPredPrelimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredPrelimit b) :

b < a ↔ ∃ (c : α), b < c ∧ c < a

theorem Order.IsPredLimit.lt_iff_exists_lt {α : Type u_1} {a b : α} [LinearOrder α] (h : IsPredLimit b) :

b < a ↔ ∃ (c : α), b < c ∧ c < a

theorem IsGLB.isPredPrelimit_of_notMem {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :

Order.IsPredPrelimit a

theorem IsGLB.mem_of_not_isPredPrelimit {α : Type u_1} {a : α} [LinearOrder α] {s : Set α} (hs : IsGLB s a) (ha : ¬Order.IsPredPrelimit a) :

a ∈ s

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

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

theorem Order.IsPredPrelimit.isGLB_Ioi {α : Type u_1} {a : α} [LinearOrder α] (ha : IsPredPrelimit a) :

IsGLB (Set.Ioi a) a

theorem Order.IsPredLimit.isGLB_Ioi {α : Type u_1} {a : α} [LinearOrder α] (ha : IsPredLimit a) :

IsGLB (Set.Ioi a) a

theorem Order.isGLB_Ioi_iff_isPredPrelimit {α : Type u_1} {a : α} [LinearOrder α] :

IsGLB (Set.Ioi a) a ↔ IsPredPrelimit a

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

Instances For

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 succ isSuccPrelimit = if hb : Order.IsPredPrelimit b then isSuccPrelimit b hb else cast ⋯ (succ (Classical.choose ⋯) ⋯)

Instances For

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

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

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

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

@[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 ⋯

@[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 ⋯

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

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 isMin succ isSuccLimit = Order.isPredPrelimitRecOn b succ fun (a : α) (ha : Order.IsPredPrelimit a) => if h : IsMax a then isMin a h else isSuccLimit a ⋯

Instances For

@[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

@[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

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

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

@[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 ⋯

@[simp]

theorem Order.isPredLimitRecOn_pred {α : Type u_1} {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 α] (b : α) :

isPredLimitRecOn (Order.pred b) isMax pred isPredLimit = pred 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) :

isSuccLimitRecOn b isMin succ isSuccLimit = isMin b hb

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

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

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 : α) → a < b → motive b) → motive a) :

motive b

Recursion principle on a well-founded partial PredOrder.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[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

@[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 : α) → a < b → motive b) → motive a) (hb : Order.IsPredPrelimit b) :

prelimitRecOn b pred isPredPrelimit = isPredPrelimit b hb fun (x : α) (x_1 : b < x) => prelimitRecOn x pred isPredPrelimit

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)

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 : α) → a < b → motive b) → motive a) (hb : ¬IsMin b) :

prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb (prelimitRecOn b pred isPredPrelimit)

@[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)

@[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 : α) → a < b → motive b) → motive a) [NoMinOrder α] (b : α) :

prelimitRecOn (Order.pred b) pred isPredPrelimit = pred b ⋯ (prelimitRecOn b pred isPredPrelimit)

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

noncomputable def PredOrder.colimitRecOn {α : 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 : α) → a < b → motive b) → motive a) :

motive b

Recursion principle on a well-founded partial PredOrder, separating out the case of a minimal element.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[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

@[simp]

theorem PredOrder.colimitRecOn_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 : α) → a < b → motive b) → motive a) (hb : IsMax b) :

colimitRecOn b isMax pred isPredLimit = isMax b hb

@[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

@[simp]

theorem PredOrder.colimitRecOn_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 : α) → a < b → motive b) → motive a) (hb : Order.IsPredLimit b) :

colimitRecOn b isMax pred isPredLimit = isPredLimit b hb fun (x : α) (x_1 : b < x) => colimitRecOn x isMax pred isPredLimit

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)

theorem PredOrder.colimitRecOn_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 : α) → a < b → motive b) → motive a) (hb : ¬IsMin b) :

colimitRecOn (Order.pred b) isMax pred isPredLimit = pred b hb (colimitRecOn b isMax pred isPredLimit)

@[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)

@[simp]

theorem PredOrder.colimitRecOn_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 : α) → a < b → motive b) → motive a) [NoMinOrder α] (b : α) :

colimitRecOn (Order.pred b) isMax pred isPredLimit = pred b ⋯ (colimitRecOn b isMax pred isPredLimit)