⊤ and ⊥, bounded lattices and variants #
This file defines top and bottom elements (greatest and least elements) of a type, the bounded
variants of different kinds of lattices, sets up the typeclass hierarchy between them and provides
instances for Prop
and fun
.
Main declarations #
<Top/Bot> α
: Typeclasses to declare the⊤
/⊥
notation.Order<Top/Bot> α
: Order with a top/bottom element.BoundedOrder α
: Order with a top and bottom element.
Top, bottom element #
An order is (noncomputably) either an OrderTop
or a NoTopOrder
. Use as
casesI topOrderOrNoTopOrder α
.
Equations
Instances For
Alias of ne_top_of_lt
.
Alias of lt_top_of_lt
.
Alias of the forward direction of isMax_iff_eq_top
.
Alias of the forward direction of isTop_iff_eq_top
.
Alias of top_notMem_iff
.
An order is (noncomputably) either an OrderBot
or a NoBotOrder
. Use as
casesI botOrderOrNoBotOrder α
.
Equations
Instances For
Alias of ne_bot_of_gt
.
Alias of bot_lt_of_lt
.
Alias of the forward direction of isMin_iff_eq_bot
.
Alias of the forward direction of isBot_iff_eq_bot
.
Alias of bot_notMem_iff
.
Bounded order #
Equations
Function lattices #
Equations
Subtype, order dual, product lattices #
A subtype remains a bounded order if the property holds at ⊥
and ⊤
.