Successor function on WithBot

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

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

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

Equations

• a.succ = WithBot.recBotCoe ⊥ Order.succ a

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

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

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

theorem WithBot.succ_mono {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] : Monotone succ

theorem WithBot.succ_strictMono {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] : StrictMono succ

theorem WithBot.succ_le_succ {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] {x y : WithBot α} (hxy : x ≤ y) : x.succ ≤ y.succ

theorem WithBot.succ_lt_succ {α : Type u_1} [Preorder α] [OrderBot α] [SuccOrder α] {x y : WithBot α} [NoMaxOrder α] (hxy : x < y) : x.succ < y.succ

def WithTop.pred {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] (a : WithTop α) : α

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

Equations

• a.pred = WithTop.recTopCoe ⊤ Order.pred a

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

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

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

theorem WithTop.pred_mono {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] : Monotone pred

theorem WithTop.pred_strictMono {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] [NoMinOrder α] : StrictMono pred

theorem WithTop.pred_le_pred {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] {x y : WithTop α} (hxy : x ≤ y) : x.pred ≤ y.pred

theorem WithTop.pred_lt_pred {α : Type u_1} [Preorder α] [OrderTop α] [PredOrder α] {x y : WithTop α} [NoMinOrder α] (hxy : x < y) : x.pred < y.pred