WithBot
, WithTop
#
Adding a bot
or a top
to an order.
Main declarations #
With<Top/Bot> α
: EquipsOption α
with the order onα
plusnone
as the top/bottom element.
Specialization of Option.getD
to values in WithBot α
that respects API boundaries.
Equations
Instances For
Alias of WithBot.unbotD
.
Specialization of Option.getD
to values in WithBot α
that respects API boundaries.
Equations
Instances For
Alias of WithBot.unbotD_bot
.
Alias of WithBot.unbotD_coe
.
Alias of WithBot.eq_bot_iff_forall_ne
.
Equations
There is a general version le_bot_iff
, but this lemma does not require a PartialOrder
.
A version of bot_lt_iff_ne_bot
for WithBot
that only requires LT α
, not
PartialOrder α
.
Equations
Alias of the reverse direction of WithBot.monotone_map_iff
.
Alias of the reverse direction of WithBot.strictMono_map_iff
.
Alias of WithBot.le_coe_unbotD
.
Alias of WithBot.eq_bot_iff_forall_lt
.
Alias of WithBot.eq_bot_iff_forall_le
.
Equations
Equations
Equations
Equations
Equations
WithTop.toDual
is the equivalence sending ⊤
to ⊥
and any a : α
to toDual a : αᵒᵈ
.
See WithTop.toDualBotEquiv
for the related order-iso.
Equations
Instances For
WithTop.ofDual
is the equivalence sending ⊤
to ⊥
and any a : αᵒᵈ
to ofDual a : α
.
See WithTop.toDualBotEquiv
for the related order-iso.
Equations
Instances For
WithBot.toDual
is the equivalence sending ⊥
to ⊤
and any a : α
to toDual a : αᵒᵈ
.
See WithBot.toDual_top_equiv
for the related order-iso.
Equations
Instances For
WithBot.ofDual
is the equivalence sending ⊥
to ⊤
and any a : αᵒᵈ
to ofDual a : α
.
See WithBot.ofDual_top_equiv
for the related order-iso.
Equations
Instances For
Specialization of Option.getD
to values in WithTop α
that respects API boundaries.
Equations
Instances For
Alias of WithTop.untopD
.
Specialization of Option.getD
to values in WithTop α
that respects API boundaries.
Equations
Instances For
Alias of WithTop.untopD_top
.
Alias of WithTop.untopD_coe
.
Alias of WithTop.eq_top_iff_forall_ne
.
Equations
There is a general version top_le_iff
, but this lemma does not require a PartialOrder
.
A version of lt_top_iff_ne_top
for WithTop
that only requires LT α
, not
PartialOrder α
.
Equations
Alias of the reverse direction of WithTop.monotone_map_iff
.
Alias of the reverse direction of WithTop.strictMono_map_iff
.
Alias of WithTop.coe_untopD_le
.
Alias of WithTop.eq_top_iff_forall_gt
.
Alias of WithTop.eq_top_iff_forall_ge
.