Limit elements in well-ordered types

This file introduces two main definitions:

• wellOrderSucc a: the successor of an element a in a well-ordered type
• the typeclass IsWellOrderLimitElement a which asserts that an element a (in a well-ordered type) is neither a successor nor the smallest element, i.e. a is a limit element

Then, the lemma eq_bot_or_eq_succ_or_isWellOrderLimitElement shows that an element in a well-ordered type is either ⊥, a successor, or a limit element.

noncomputable def wellOrderSucc {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] (a : α) : α

Given an element a : α in a well ordered set, this is the successor of a, i.e. the smallest element strictly greater than a if it exists (or a itself otherwise).

Equations

• wellOrderSucc a = ⋯.succ a

theorem self_le_wellOrderSucc {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] (a : α) : a ≤ wellOrderSucc a

theorem wellOrderSucc_le {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (ha : a < b) : wellOrderSucc a ≤ b

theorem self_lt_wellOrderSucc {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < b) : a < wellOrderSucc a

theorem le_of_lt_wellOrderSucc {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} (h : a < wellOrderSucc b) : a ≤ b

class IsWellOrderLimitElement {α : Type u_1} [LinearOrder α] (a : α) : Prop

This property of an element a : α in a well-ordered type holds iff a is a limit element, i.e. it is not a successor and it is not the smallest element of α.

• not_bot : ∃ (b : α), b < a
• not_succ : ∀ b < a, ∃ (c : α), b < c ∧ c < a

theorem IsWellOrderLimitElement.not_bot {α : Type u_1} : ∀ {inst : LinearOrder α} {a : α} [self : IsWellOrderLimitElement a], ∃ (b : α), b < a

theorem IsWellOrderLimitElement.not_succ {α : Type u_1} : ∀ {inst : LinearOrder α} {a : α} [self : IsWellOrderLimitElement a], ∀ b < a, ∃ (c : α), b < c ∧ c < a

theorem IsWellOrderLimitElement.neq_bot {α : Type u_1} [LinearOrder α] (a : α) [ha : IsWellOrderLimitElement a] [OrderBot α] : a ≠ ⊥

theorem IsWellOrderLimitElement.bot_lt {α : Type u_1} [LinearOrder α] (a : α) [ha : IsWellOrderLimitElement a] [OrderBot α] : ⊥ < a

theorem IsWellOrderLimitElement.wellOrderSucc_lt {α : Type u_1} [LinearOrder α] {a : α} [ha : IsWellOrderLimitElement a] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] {b : α} (hb : b < a) : wellOrderSucc b < a

theorem eq_bot_or_eq_succ_or_isWellOrderLimitElement {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] [OrderBot α] (a : α) : a = ⊥ ∨ (∃ (b : α), a = wellOrderSucc b ∧ b < a) ∨ IsWellOrderLimitElement a

theorem IsWellOrderLimitElement.neq_succ {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] (a : α) (ha : a < wellOrderSucc a) [IsWellOrderLimitElement (wellOrderSucc a)] : False

@[simp]

theorem Nat.wellOrderSucc_eq (a : ℕ) : wellOrderSucc a = a.succ

theorem Nat.not_isWellOrderLimitElement (a : ℕ) [IsWellOrderLimitElement a] : False