Documentation

Mathlib.Order.IsWellOrderLimitElement

Limit elements in well-ordered types #

This file introduces two main definitions:

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 (x x_1 : α) => x < x_1] (a : α) :
α

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

Equations
Instances For
    theorem self_le_wellOrderSucc {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (a : α) :
    theorem wellOrderSucc_le {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] {a : α} {b : α} (ha : a < b) :
    theorem self_lt_wellOrderSucc {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] {a : α} {b : α} (h : a < b) :
    theorem le_of_lt_wellOrderSucc {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] {a : α} {b : α} (h : a < wellOrderSucc b) :
    a b
    class IsWellOrderLimitElement {α : Type u_1} [LinearOrder α] (a : α) :

    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
    Instances
      theorem IsWellOrderLimitElement.not_bot {α : Type u_1} [LinearOrder α] {a : α} [self : IsWellOrderLimitElement a] :
      ∃ (b : α), b < a
      theorem IsWellOrderLimitElement.not_succ {α : Type u_1} [LinearOrder α] {a : α} [self : IsWellOrderLimitElement a] (b : α) (hb : b < a) :
      ∃ (c : α), b < c c < a
      theorem IsWellOrderLimitElement.wellOrderSucc_lt {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] {a : α} [ha : IsWellOrderLimitElement a] {b : α} (hb : b < a) :
      theorem eq_bot_or_eq_succ_or_isWellOrderLimitElement {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] [OrderBot α] (a : α) :
      a = (∃ (b : α), a = wellOrderSucc b b < a) IsWellOrderLimitElement a
      theorem IsWellOrderLimitElement.neq_succ {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (a : α) (ha : a < wellOrderSucc a) [IsWellOrderLimitElement (wellOrderSucc a)] :
      @[simp]
      theorem Nat.wellOrderSucc_eq (a : ) :
      wellOrderSucc a = a.succ