⊤ 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
- topOrderOrNoTopOrder α = if H : ∀ (a : α), ∃ (b : α), ¬b ≤ a then PSum.inr ⋯ else PSum.inl (OrderTop.mk ⋯)
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
.
An order is an OrderBot
if it has a least element.
We state this using a data mixin, holding the value of ⊥
and the least element constraint.
- bot : α
⊥
is the least element
Instances
- Additive.orderBot
- BotHom.instOrderBot
- Finset.instOrderBot
- GeneralizedBooleanAlgebra.toOrderBot
- InfHom.instOrderBot
- Multiplicative.orderBot
- Multiset.instOrderBot
- Nat.Subtype.orderBot
- Nat.instOrderBot
- OrderDual.instOrderBot
- Part.instOrderBot
- Pi.instOrderBot
- Prod.instOrderBot
- SupBotHom.instOrderBot
- SupHom.instOrderBot
- ULift.instOrderBot
- WithBot.orderBot
- WithTop.orderBot
- WithZero.orderBot
An order is (noncomputably) either an OrderBot
or a NoBotOrder
. Use as
casesI botOrderOrNoBotOrder α
.
Equations
- botOrderOrNoBotOrder α = if H : ∀ (a : α), ∃ (b : α), ¬a ≤ b then PSum.inr ⋯ else PSum.inl (OrderBot.mk ⋯)
Equations
- OrderDual.instTop α = { top := ⊥ }
Equations
- OrderDual.instBot α = { bot := ⊤ }
Equations
Equations
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
.
Bounded order #
A bounded order describes an order (≤)
with a top and bottom element,
denoted ⊤
and ⊥
respectively.
Instances
- Additive.boundedOrder
- Bool.instBoundedOrder
- BooleanAlgebra.toBoundedOrder
- CoheytingAlgebra.toBoundedOrder
- Complementeds.instBoundedOrder
- CompleteLattice.toBoundedOrder
- Fin.instBoundedOrder
- Finset.boundedOrder
- HeytingAlgebra.toBoundedOrder
- InfHom.instBoundedOrder
- Multiplicative.boundedOrder
- OrderDual.instBoundedOrder
- Pi.instBoundedOrder
- Prod.instBoundedOrder
- Prop.instBoundedOrder
- SupHom.instBoundedOrder
- ULift.instBoundedOrder
- WithBot.instBoundedOrder
- WithTop.boundedOrder
Equations
- OrderDual.instBoundedOrder α = BoundedOrder.mk
Function lattices #
Equations
- Pi.instOrderTop = OrderTop.mk ⋯
Equations
- Pi.instOrderBot = OrderBot.mk ⋯
Equations
- Pi.instBoundedOrder = BoundedOrder.mk
Pullback a BoundedOrder
.
Equations
- BoundedOrder.lift f map_le map_top map_bot = BoundedOrder.mk
Subtype, order dual, product lattices #
A subtype remains a ⊥
-order if the property holds at ⊥
.
Equations
- Subtype.orderBot hbot = OrderBot.mk ⋯
A subtype remains a ⊤
-order if the property holds at ⊤
.
Equations
- Subtype.orderTop htop = OrderTop.mk ⋯
A subtype remains a bounded order if the property holds at ⊥
and ⊤
.
Equations
- Subtype.boundedOrder hbot htop = BoundedOrder.mk
Equations
- Prod.instOrderTop α β = OrderTop.mk ⋯
Equations
- Prod.instOrderBot α β = OrderBot.mk ⋯
Equations
- Prod.instBoundedOrder α β = BoundedOrder.mk
Equations
- ULift.instOrderBot = OrderBot.lift ULift.down ⋯ ⋯
Equations
- ULift.instOrderTop = OrderTop.lift ULift.down ⋯ ⋯
Equations
- ULift.instBoundedOrder = BoundedOrder.mk
Equations
- Bool.instBoundedOrder = BoundedOrder.mk