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

TODO #

The plan is to eventually replace Ordinal.IsLimit and Cardinal.IsLimit with the common predicate Order.IsSuccLimit.

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

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

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

@[deprecated Order.not_isSuccPrelimit_iff_exists_covBy]

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

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

Alias of Order.not_isSuccPrelimit_iff_exists_covBy.

@[simp]

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

Order.IsSuccPrelimit a

@[deprecated Order.IsSuccPrelimit.of_dense]

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

Order.IsSuccPrelimit a

Alias of Order.IsSuccPrelimit.of_dense.

@[deprecated Order.IsSuccPrelimit.of_dense]

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

Order.IsSuccPrelimit a

Alias of Order.IsSuccPrelimit.of_dense.

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.

This previously allowed the element to be minimal. This usage is now covered by IsSuccPrelimit.

Equations

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

Instances For

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

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

Order.IsSuccPrelimit a

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

Order.IsSuccLimit a

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

Order.IsSuccLimit a

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

Order.IsSuccPrelimit a ↔ Order.IsSuccLimit a

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

Order.IsSuccPrelimit a ↔ Order.IsSuccLimit a

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

¬Order.IsSuccLimit a

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

IsMin a → Order.IsSuccPrelimit a

@[deprecated IsMin.isSuccPrelimit]

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

IsMin a → Order.IsSuccPrelimit a

Alias of IsMin.isSuccPrelimit.

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

Order.IsSuccPrelimit ⊥

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

¬Order.IsSuccLimit ⊥

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

@[deprecated Order.isSuccPrelimit_bot]

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

Order.IsSuccPrelimit ⊥

Alias of Order.isSuccPrelimit_bot.

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

¬Order.IsSuccLimit a ↔ IsMin a ∨ ¬Order.IsSuccPrelimit a

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

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

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

¬Order.IsSuccPrelimit (Order.succ a)

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

¬Order.IsSuccLimit (Order.succ a)

noncomputable def Order.IsSuccPrelimit.mid {α : Type u_1} [Preorder α] {i j : α} (hi : Order.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 : Order.IsSuccPrelimit a) (b : α) :

Order.succ b ≠ a

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

Order.succ b ≠ a

@[simp]

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

¬Order.IsSuccPrelimit (Order.succ a)

@[simp]

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

¬Order.IsSuccLimit (Order.succ a)

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

@[deprecated Order.IsSuccPrelimit.isMin_of_noMax]

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

Alias of Order.IsSuccPrelimit.isMin_of_noMax.

@[simp]

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

Order.IsSuccPrelimit a ↔ IsMin a

@[deprecated Order.isSuccPrelimit_iff_of_noMax]

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

Order.IsSuccPrelimit a ↔ IsMin a

Alias of Order.isSuccPrelimit_iff_of_noMax.

@[simp]

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

¬Order.IsSuccLimit a

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

¬Order.IsSuccPrelimit a

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

Order.IsSuccLimit a ↔ a ≠ ⊥ ∧ Order.IsSuccPrelimit a

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

Order.IsSuccPrelimit a

@[deprecated Order.isSuccPrelimit_of_succ_ne]

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

Order.IsSuccPrelimit a

Alias of Order.isSuccPrelimit_of_succ_ne.

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

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

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

a ∈ Set.range Order.succ

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

@[deprecated Order.mem_range_succ_of_not_isSuccPrelimit]

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

a ∈ Set.range Order.succ

Alias of Order.mem_range_succ_of_not_isSuccPrelimit.

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

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

a ∈ Set.range Order.succ ∨ Order.IsSuccPrelimit a

@[deprecated Order.mem_range_succ_or_isSuccPrelimit]

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

a ∈ Set.range Order.succ ∨ Order.IsSuccPrelimit a

Alias of Order.mem_range_succ_or_isSuccPrelimit.

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

Order.IsSuccPrelimit b

@[deprecated Order.isSuccPrelimit_of_succ_lt]

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

Order.IsSuccPrelimit b

Alias of Order.isSuccPrelimit_of_succ_lt.

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

Order.succ a < b

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

Order.succ a < b

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

Order.succ a < b ↔ a < b

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

Order.succ a < b ↔ a < b

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

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

@[deprecated Order.isSuccPrelimit_iff_succ_lt]

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

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

Alias of Order.isSuccPrelimit_iff_succ_lt.

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

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

@[deprecated Order.isSuccPrelimit_iff_succ_ne]

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

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

Alias of Order.isSuccPrelimit_iff_succ_ne.

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

¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ

@[deprecated Order.not_isSuccPrelimit_iff']

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

¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ

Alias of Order.not_isSuccPrelimit_iff'.

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

@[simp]

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

Order.IsSuccPrelimit a ↔ IsMin a

@[simp]

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

¬Order.IsSuccLimit a

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

¬Order.IsSuccPrelimit a

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

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

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

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

Predecessor limits #

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_isPredPrelimit_iff_exists_covBy {α : Type u_1} [LT α] (a : α) :

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

@[deprecated Order.not_isPredPrelimit_iff_exists_covBy]

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

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

Alias of Order.not_isPredPrelimit_iff_exists_covBy.

@[simp]

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

Order.IsPredPrelimit a

@[deprecated Order.IsPredPrelimit.of_dense]

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

Order.IsPredPrelimit a

Alias of Order.IsPredPrelimit.of_dense.

@[deprecated Order.IsPredPrelimit.of_dense]

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

Order.IsPredPrelimit a

Alias of Order.IsPredPrelimit.of_dense.

@[simp]

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

Order.IsSuccPrelimit (OrderDual.toDual a) ↔ Order.IsPredPrelimit a

@[simp]

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

Order.IsPredPrelimit (OrderDual.toDual a) ↔ Order.IsSuccPrelimit a

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

Order.IsPredPrelimit a → Order.IsSuccPrelimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.

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

Order.IsSuccPrelimit a → Order.IsPredPrelimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.

@[deprecated Order.IsPredPrelimit.dual]

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

Order.IsPredPrelimit a → Order.IsSuccPrelimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.

Alias of the reverse direction of Order.isSuccPrelimit_toDual_iff.

@[deprecated Order.IsSuccPrelimit.dual]

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

Order.IsSuccPrelimit a → Order.IsPredPrelimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.

Alias of the reverse direction of Order.isPredPrelimit_toDual_iff.

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.

This previously allowed the element to be maximal. This usage is now covered by IsPredPreLimit.

Equations

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

Instances For

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

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

Order.IsPredPrelimit a

@[simp]

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

Order.IsSuccLimit (OrderDual.toDual a) ↔ Order.IsPredLimit a

@[simp]

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

Order.IsPredLimit (OrderDual.toDual a) ↔ Order.IsSuccLimit a

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

Order.IsPredLimit a → Order.IsSuccLimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isSuccLimit_toDual_iff.

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

Order.IsSuccLimit a → Order.IsPredLimit (OrderDual.toDual a)

Alias of the reverse direction of Order.isPredLimit_toDual_iff.

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

Order.IsPredLimit a

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

Order.IsPredLimit a

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

Order.IsPredPrelimit a ↔ Order.IsPredLimit a

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

Order.IsPredPrelimit a ↔ Order.IsPredLimit a

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

¬Order.IsPredLimit a

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

IsMax a → Order.IsPredPrelimit a

@[deprecated IsMax.isPredPrelimit]

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

IsMax a → Order.IsPredPrelimit a

Alias of IsMax.isPredPrelimit.

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

Order.IsPredPrelimit ⊤

@[deprecated Order.isPredPrelimit_top]

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

Order.IsPredPrelimit ⊤

Alias of Order.isPredPrelimit_top.

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

¬Order.IsPredLimit ⊤

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

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

¬Order.IsPredLimit a ↔ IsMax a ∨ ¬Order.IsPredPrelimit a

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

¬Order.IsPredLimit a

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

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

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

¬Order.IsPredPrelimit (Order.pred a)

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

¬Order.IsPredLimit (Order.pred a)

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

Order.pred b ≠ a

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

Order.pred b ≠ a

@[simp]

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

¬Order.IsPredPrelimit (Order.pred a)

@[simp]

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

¬Order.IsPredLimit (Order.pred a)

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

@[deprecated Order.IsPredPrelimit.isMax_of_noMin]

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

Alias of Order.IsPredPrelimit.isMax_of_noMin.

@[simp]

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

Order.IsPredPrelimit a ↔ IsMax a

@[deprecated Order.isPredPrelimit_iff_of_noMin]

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

Order.IsPredPrelimit a ↔ IsMax a

Alias of Order.isPredPrelimit_iff_of_noMin.

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

¬Order.IsPredPrelimit a

@[simp]

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

¬Order.IsPredLimit a

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

Order.IsPredLimit a ↔ a ≠ ⊤ ∧ Order.IsPredPrelimit a

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

Order.IsPredPrelimit a

@[deprecated Order.isPredPrelimit_of_pred_ne]

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

Order.IsPredPrelimit a

Alias of Order.isPredPrelimit_of_pred_ne.

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

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

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

a ∈ Set.range Order.pred

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

@[deprecated Order.mem_range_pred_of_not_isPredPrelimit]

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

a ∈ Set.range Order.pred

Alias of Order.mem_range_pred_of_not_isPredPrelimit.

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

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

a ∈ Set.range Order.pred ∨ Order.IsPredPrelimit a

@[deprecated Order.mem_range_pred_or_isPredPrelimit]

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

a ∈ Set.range Order.pred ∨ Order.IsPredPrelimit a

Alias of Order.mem_range_pred_or_isPredPrelimit.

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

Order.IsPredPrelimit a

@[deprecated Order.isPredPrelimit_of_pred_lt]

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

Order.IsPredPrelimit a

Alias of Order.isPredPrelimit_of_pred_lt.

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

a < Order.pred b

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

a < Order.pred b

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

a < Order.pred b ↔ a < b

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

a < Order.pred b ↔ a < b

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

Order.IsPredPrelimit a ↔ ∀ b > a, a < Order.pred b

@[deprecated Order.isPredPrelimit_iff_lt_pred]

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

Order.IsPredPrelimit a ↔ ∀ b > a, a < Order.pred b

Alias of Order.isPredPrelimit_iff_lt_pred.

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

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

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

¬Order.IsPredPrelimit a ↔ a ∈ Set.range Order.pred

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

@[deprecated Order.IsPredPrelimit.isMax]

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

Alias of Order.IsPredPrelimit.isMax.

@[simp]

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

Order.IsPredPrelimit a ↔ IsMax a

@[simp]

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

¬Order.IsPredLimit a

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

¬Order.IsPredPrelimit a

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

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

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

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

Induction principles #

noncomputable def Order.isSuccPrelimitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) :

C b

A value can be built by building it on successors and successor pre-limits.

Equations

Order.isSuccPrelimitRecOn b hs hl = if hb : Order.IsSuccPrelimit b then hl b hb else cast ⋯ (hs (Classical.choose ⋯) ⋯)

Instances For

theorem Order.isSuccPrelimitRecOn_of_isSuccPrelimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) (hb : Order.IsSuccPrelimit b) :

Order.isSuccPrelimitRecOn b hs hl = hl b hb

@[deprecated Order.isSuccPrelimitRecOn_of_isSuccPrelimit]

theorem Order.isSuccLimitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) (hb : Order.IsSuccPrelimit b) :

Order.isSuccPrelimitRecOn b hs hl = hl b hb

Alias of Order.isSuccPrelimitRecOn_of_isSuccPrelimit.

@[deprecated Order.isSuccPrelimitRecOn_of_isSuccPrelimit]

theorem Order.isSuccPrelimitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) (hb : Order.IsSuccPrelimit b) :

Order.isSuccPrelimitRecOn b hs hl = hl b hb

Alias of Order.isSuccPrelimitRecOn_of_isSuccPrelimit.

theorem Order.isSuccPrelimitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) (hb : ¬IsMax b) :

Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b hb

@[deprecated Order.isSuccPrelimitRecOn_succ_of_not_isMax]

theorem Order.isSuccLimitRecOn_succ' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) (hb : ¬IsMax b) :

Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b hb

Alias of Order.isSuccPrelimitRecOn_succ_of_not_isMax.

@[deprecated Order.isSuccPrelimitRecOn_succ_of_not_isMax]

theorem Order.isSuccPrelimitRecOn_succ' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) (hb : ¬IsMax b) :

Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b hb

Alias of Order.isSuccPrelimitRecOn_succ_of_not_isMax.

@[simp]

theorem Order.isSuccPrelimitRecOn_succ {α : Type u_1} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → C a) [NoMaxOrder α] (b : α) :

Order.isSuccPrelimitRecOn (Order.succ b) hs hl = hs b ⋯

noncomputable def Order.isPredPrelimitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) :

C b

A value can be built by building it on predecessors and predecessor pre-limits.

Equations

Order.isPredPrelimitRecOn b hs hl = Order.isSuccPrelimitRecOn b hs fun (a : αᵒᵈ) (ha : Order.IsSuccPrelimit a) => hl a ⋯

Instances For

theorem Order.isPredPrelimitRecOn_of_isPredPrelimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) (hb : Order.IsPredPrelimit b) :

Order.isPredPrelimitRecOn b hs hl = hl b hb

@[deprecated Order.isPredPrelimitRecOn_of_isPredPrelimit]

theorem Order.isPredLimitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) (hb : Order.IsPredPrelimit b) :

Order.isPredPrelimitRecOn b hs hl = hl b hb

Alias of Order.isPredPrelimitRecOn_of_isPredPrelimit.

@[deprecated Order.isPredPrelimitRecOn_of_isPredPrelimit]

theorem Order.isPredPrelimitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) (hb : Order.IsPredPrelimit b) :

Order.isPredPrelimitRecOn b hs hl = hl b hb

Alias of Order.isPredPrelimitRecOn_of_isPredPrelimit.

theorem Order.isPredPrelimitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) (hb : ¬IsMin b) :

Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b hb

@[deprecated Order.isPredPrelimitRecOn_pred_of_not_isMin]

theorem Order.isPredLimitRecOn_pred' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) (hb : ¬IsMin b) :

Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b hb

Alias of Order.isPredPrelimitRecOn_pred_of_not_isMin.

@[deprecated Order.isPredPrelimitRecOn_pred_of_not_isMin]

theorem Order.isPredPrelimitRecOn_pred' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) (hb : ¬IsMin b) :

Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b hb

Alias of Order.isPredPrelimitRecOn_pred_of_not_isMin.

@[simp]

theorem Order.isPredPrelimitRecOn_pred {α : Type u_1} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → C a) [NoMinOrder α] (b : α) :

Order.isPredPrelimitRecOn (Order.pred b) hs hl = hs b ⋯

noncomputable def Order.isSuccLimitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) :

C b

A value can be built by building it on minimal elements, successors, and successor limits.

Equations

Order.isSuccLimitRecOn b hm hs hl = Order.isSuccPrelimitRecOn b hs fun (a : α) (ha : Order.IsSuccPrelimit a) => if h : IsMin a then hm a h else hl a ⋯

Instances For

@[simp]

theorem Order.isSuccLimitRecOn_of_isSuccLimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) (hb : Order.IsSuccLimit b) :

Order.isSuccLimitRecOn b hm hs hl = hl b hb

theorem Order.isSuccLimitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) (hb : ¬IsMax b) :

Order.isSuccLimitRecOn (Order.succ b) hm hs hl = hs b hb

@[simp]

theorem Order.isSuccLimitRecOn_succ {α : Type u_1} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) [NoMaxOrder α] (b : α) :

Order.isSuccLimitRecOn (Order.succ b) hm hs hl = hs b ⋯

theorem Order.isSuccLimitRecOn_of_isMin {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → C a) (hb : IsMin b) :

Order.isSuccLimitRecOn b hm hs hl = hm b hb

noncomputable def Order.isPredLimitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [PredOrder α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) :

C b

A value can be built by building it on maximal elements, predecessors, and predecessor limits.

Equations

Order.isPredLimitRecOn b hm hs hl = Order.isSuccLimitRecOn b hm hs fun (a : αᵒᵈ) (ha : Order.IsSuccLimit a) => hl a ⋯

Instances For

@[simp]

theorem Order.isPredLimitRecOn_of_isPredLimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) (hb : Order.IsPredLimit b) :

Order.isPredLimitRecOn b hm hs hl = hl b hb

theorem Order.isPredLimitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) (hb : ¬IsMin b) :

Order.isPredLimitRecOn (Order.pred b) hm hs hl = hs b hb

@[simp]

theorem Order.isPredLimitRecOn_pred {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) [NoMinOrder α] :

Order.isPredLimitRecOn (Order.pred b) hm hs hl = hs b ⋯

theorem Order.isPredLimitRecOn_of_isMax {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → C a) (hb : IsMax b) :

Order.isPredLimitRecOn b hm hs hl = hm b hb

noncomputable def SuccOrder.prelimitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) :

C b

Recursion principle on a well-founded partial SuccOrder.

Equations

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

Instances For

@[simp]

theorem SuccOrder.prelimitRecOn_of_isSuccPrelimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) (hb : Order.IsSuccPrelimit b) :

SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl

@[deprecated SuccOrder.prelimitRecOn_of_isSuccPrelimit]

theorem SuccOrder.limitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) (hb : Order.IsSuccPrelimit b) :

SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl

Alias of SuccOrder.prelimitRecOn_of_isSuccPrelimit.

@[deprecated SuccOrder.prelimitRecOn_of_isSuccPrelimit]

theorem SuccOrder.prelimitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) (hb : Order.IsSuccPrelimit b) :

SuccOrder.prelimitRecOn b hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.prelimitRecOn x hs hl

Alias of SuccOrder.prelimitRecOn_of_isSuccPrelimit.

theorem SuccOrder.prelimitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) (hb : ¬IsMax b) :

SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b hb (SuccOrder.prelimitRecOn b hs hl)

@[deprecated SuccOrder.prelimitRecOn_succ_of_not_isMax]

theorem SuccOrder.limitRecOn_succ' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) (hb : ¬IsMax b) :

SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b hb (SuccOrder.prelimitRecOn b hs hl)

Alias of SuccOrder.prelimitRecOn_succ_of_not_isMax.

@[deprecated SuccOrder.prelimitRecOn_succ_of_not_isMax]

theorem SuccOrder.prelimitRecOn_succ' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) (hb : ¬IsMax b) :

SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b hb (SuccOrder.prelimitRecOn b hs hl)

Alias of SuccOrder.prelimitRecOn_succ_of_not_isMax.

@[simp]

theorem SuccOrder.prelimitRecOn_succ {α : Type u_1} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → C b) → C a) [NoMaxOrder α] (b : α) :

SuccOrder.prelimitRecOn (Order.succ b) hs hl = hs b ⋯ (SuccOrder.prelimitRecOn b hs hl)

noncomputable def SuccOrder.limitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C b) → C a) :

C b

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

Equations

SuccOrder.limitRecOn b hm hs hl = SuccOrder.prelimitRecOn b hs fun (a : α) (ha : Order.IsSuccPrelimit a) (IH : (b : α) → b < a → C b) => if h : IsMin a then hm a h else hl a ⋯ IH

Instances For

@[simp]

theorem SuccOrder.limitRecOn_isMin {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C b) → C a) (hb : IsMin b) :

SuccOrder.limitRecOn b hm hs hl = hm b hb

@[simp]

theorem SuccOrder.limitRecOn_of_isSuccLimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C b) → C a) (hb : Order.IsSuccLimit b) :

SuccOrder.limitRecOn b hm hs hl = hl b hb fun (x : α) (x_1 : x < b) => SuccOrder.limitRecOn x hm hs hl

theorem SuccOrder.limitRecOn_succ_of_not_isMax {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C b) → C a) (hb : ¬IsMax b) :

SuccOrder.limitRecOn (Order.succ b) hm hs hl = hs b hb (SuccOrder.limitRecOn b hm hs hl)

@[simp]

theorem SuccOrder.limitRecOn_succ {α : Type u_1} {C : α → Sort u_2} [LinearOrder α] [SuccOrder α] [WellFoundedLT α] (hm : (a : α) → IsMin a → C a) (hs : (a : α) → ¬IsMax a → C a → C (Order.succ a)) (hl : (a : α) → Order.IsSuccLimit a → ((b : α) → b < a → C b) → C a) [NoMaxOrder α] (b : α) :

SuccOrder.limitRecOn (Order.succ b) hm hs hl = hs b ⋯ (SuccOrder.limitRecOn b hm hs hl)

noncomputable def PredOrder.prelimitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) :

C b

Recursion principle on a well-founded partial PredOrder.

Equations

PredOrder.prelimitRecOn b hp hl = SuccOrder.prelimitRecOn b hp fun (a : αᵒᵈ) (ha : Order.IsSuccPrelimit a) => hl a ⋯

Instances For

@[simp]

theorem PredOrder.prelimitRecOn_of_isPredPrelimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) (hb : Order.IsPredPrelimit b) :

PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl

@[deprecated PredOrder.prelimitRecOn_of_isPredPrelimit]

theorem PredOrder.limitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) (hb : Order.IsPredPrelimit b) :

PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl

Alias of PredOrder.prelimitRecOn_of_isPredPrelimit.

@[deprecated PredOrder.prelimitRecOn_of_isPredPrelimit]

theorem PredOrder.prelimitRecOn_limit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) (hb : Order.IsPredPrelimit b) :

PredOrder.prelimitRecOn b hp hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.prelimitRecOn x hp hl

Alias of PredOrder.prelimitRecOn_of_isPredPrelimit.

theorem PredOrder.prelimitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) (hb : ¬IsMin b) :

PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b hb (PredOrder.prelimitRecOn b hp hl)

@[deprecated PredOrder.prelimitRecOn_pred_of_not_isMin]

theorem PredOrder.limitRecOn_pred' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) (hb : ¬IsMin b) :

PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b hb (PredOrder.prelimitRecOn b hp hl)

Alias of PredOrder.prelimitRecOn_pred_of_not_isMin.

@[deprecated PredOrder.prelimitRecOn_pred_of_not_isMin]

theorem PredOrder.prelimitRecOn_pred' {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) (hb : ¬IsMin b) :

PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b hb (PredOrder.prelimitRecOn b hp hl)

Alias of PredOrder.prelimitRecOn_pred_of_not_isMin.

@[simp]

theorem PredOrder.prelimitRecOn_pred {α : Type u_1} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hp : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredPrelimit a → ((b : α) → b > a → C b) → C a) [NoMinOrder α] (b : α) :

PredOrder.prelimitRecOn (Order.pred b) hp hl = hp b ⋯ (PredOrder.prelimitRecOn b hp hl)

noncomputable def PredOrder.limitRecOn {α : Type u_1} (b : α) {C : α → Sort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C b) → C a) :

C b

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

Equations

PredOrder.limitRecOn b hm hs hl = SuccOrder.limitRecOn b hm hs fun (a : αᵒᵈ) (ha : Order.IsSuccLimit a) => hl a ⋯

Instances For

@[simp]

theorem PredOrder.limitRecOn_isMax {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C b) → C a) (hb : IsMax b) :

PredOrder.limitRecOn b hm hs hl = hm b hb

@[simp]

theorem PredOrder.limitRecOn_of_isPredLimit {α : Type u_1} {b : α} {C : α → Sort u_2} [PartialOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C b) → C a) (hb : Order.IsPredLimit b) :

PredOrder.limitRecOn b hm hs hl = hl b hb fun (x : α) (x_1 : x > b) => PredOrder.limitRecOn x hm hs hl

theorem PredOrder.limitRecOn_pred_of_not_isMin {α : Type u_1} {b : α} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C b) → C a) (hb : ¬IsMin b) :

PredOrder.limitRecOn (Order.pred b) hm hs hl = hs b hb (PredOrder.limitRecOn b hm hs hl)

@[simp]

theorem PredOrder.limitRecOn_pred {α : Type u_1} {C : α → Sort u_2} [LinearOrder α] [PredOrder α] [WellFoundedGT α] (hm : (a : α) → IsMax a → C a) (hs : (a : α) → ¬IsMin a → C a → C (Order.pred a)) (hl : (a : α) → Order.IsPredLimit a → ((b : α) → b > a → C b) → C a) [NoMinOrder α] (b : α) :

PredOrder.limitRecOn (Order.pred b) hm hs hl = hs b ⋯ (PredOrder.limitRecOn b hm hs hl)