Theorems · Definition · order theory

WithTop.pred

{α : Type u_1} → [inst : Preorder α] → [OrderTop α] → [PredOrder α] → WithTop α → α

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

Defined in

Mathlib.Order.SuccPred.WithBot

Cited by

8 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

PreorderOrderTopPredOrder