Documentation

Mathlib.Order.SuccPred.WithBot

Successor function on WithBot #

This file defines the successor of a : WithBot α as an element of α, and dually for WithTop.

source
def WithBot.succ {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : WithBot α) :
α

The successor of a : WithBot α as an element of α.

Equations
Instances For
    source
    @[simp]
    theorem WithBot.succ_bot {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] :
    ⊥.succ = ⊥

    Not to be confused with WithBot.orderSucc_bot, which is about Order.succ.

    source
    @[simp]
    theorem WithBot.succ_coe {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : α) :
    (↑a).succ = Order.succ a

    Not to be confused with WithBot.orderSucc_coe, which is about Order.succ.

    source
    theorem WithBot.succ_eq_succ {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] (a : WithBot α) :
    ↑a.succ = Order.succ a
    source
    theorem WithBot.lt_succ {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (x : WithBot α) :
    x < ↑x.succ
    source
    theorem WithBot.succ_mono {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] :
    Monotone succ
    source
    theorem WithBot.succ_strictMono {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] :
    StrictMono succ
    source
    theorem WithBot.succ_le_succ {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] {x y : WithBot α} (hxy : x ≤ y) :
    x.succ ≤ y.succ
    source
    theorem WithBot.succ_lt_succ {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] {x y : WithBot α} [NoMaxOrder α] (hxy : x < y) :
    x.succ < y.succ
    source
    @[simp]
    theorem WithBot.succ_eq_bot {α : Type u_2} [Nontrivial α] [LinearOrder α] [OrderBot α] [SuccOrder α] (a : WithBot α) :
    a.succ = ⊥ ↔ a = ⊥
    source
    def WithTop.pred {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : WithTop α) :
    α

    The predecessor of a : WithTop α as an element of α.

    Equations
    Instances For
      source
      @[simp]
      theorem WithTop.pred_top {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] :
      ⊤.pred = ⊤

      Not to be confused with WithTop.orderPred_top, which is about Order.pred.

      source
      @[simp]
      theorem WithTop.pred_coe {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : α) :
      (↑a).pred = Order.pred a

      Not to be confused with WithTop.orderPred_coe, which is about Order.pred.

      source
      theorem WithTop.pred_eq_pred {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : WithTop α) :
      ↑a.pred = Order.pred a
      source
      theorem WithTop.pred_mono {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] :
      Monotone pred
      source
      theorem WithTop.pred_strictMono {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] [NoMinOrder α] :
      StrictMono pred
      source
      theorem WithTop.pred_le_pred {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] {x y : WithTop α} (hxy : x ≤ y) :
      x.pred ≤ y.pred
      source
      theorem WithTop.pred_lt_pred {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] {x y : WithTop α} [NoMinOrder α] (hxy : x < y) :
      x.pred < y.pred
      source
      @[simp]
      theorem WithTop.pred_eq_top {α : Type u_2} [Nontrivial α] [LinearOrder α] [OrderTop α] [PredOrder α] (a : WithTop α) :
      a.pred = ⊤ ↔ a = ⊤