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.
Equations
- WithBot.instRepr = { reprPrec := fun (o : WithBot α) (x : ℕ) => match o with | none => Std.Format.text "⊥" | some a => Std.Format.text "↑" ++ repr a }
Specialization of Option.getD
to values in WithBot α
that respects API boundaries.
Equations
- WithBot.unbot' d x = WithBot.recBotCoe d id x
Instances For
Lift a map f : α → β
to WithBot α → WithBot β
. Implemented using Option.map
.
Equations
- WithBot.map f = Option.map f
Instances For
Equations
- WithBot.orderBot = OrderBot.mk ⋯
Equations
- WithBot.orderTop = OrderTop.mk ⋯
Equations
- WithBot.instBoundedOrder = let __src := WithBot.orderBot; let __src_1 := WithBot.orderTop; BoundedOrder.mk
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
- WithBot.preorder = Preorder.mk ⋯ ⋯ ⋯
Equations
- WithBot.partialOrder = let __src := WithBot.preorder; PartialOrder.mk ⋯
Alias of the reverse direction of WithBot.monotone_map_iff
.
Alias of the reverse direction of WithBot.strictMono_map_iff
.
Equations
- WithBot.semilatticeSup = SemilatticeSup.mk ⋯ ⋯ ⋯
Equations
- WithBot.semilatticeInf = let __src := WithBot.partialOrder; let __src_1 := WithBot.orderBot; SemilatticeInf.mk ⋯ ⋯ ⋯
Equations
- WithBot.lattice = let __src := WithBot.semilatticeSup; let __src_1 := WithBot.semilatticeInf; Lattice.mk ⋯ ⋯ ⋯
Equations
- WithBot.distribLattice = let __src := WithBot.lattice; DistribLattice.mk ⋯
Equations
- WithBot.decidableEq = inferInstanceAs (DecidableEq (Option α))
Equations
- WithBot.linearOrder = Lattice.toLinearOrder (WithBot α)
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- WithTop.instRepr = { reprPrec := fun (o : WithTop α) (x : ℕ) => match o with | none => Std.Format.text "⊤" | some a => Std.Format.text "↑" ++ repr a }
WithTop.toDual
is the equivalence sending ⊤
to ⊥
and any a : α
to toDual a : αᵒᵈ
.
See WithTop.toDualBotEquiv
for the related order-iso.
Equations
- WithTop.toDual = Equiv.refl (WithTop α)
Instances For
WithTop.ofDual
is the equivalence sending ⊤
to ⊥
and any a : αᵒᵈ
to ofDual a : α
.
See WithTop.toDualBotEquiv
for the related order-iso.
Equations
- WithTop.ofDual = Equiv.refl (WithTop αᵒᵈ)
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
- WithBot.toDual = Equiv.refl (WithBot α)
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
- WithBot.ofDual = Equiv.refl (WithBot αᵒᵈ)
Instances For
Specialization of Option.getD
to values in WithTop α
that respects API boundaries.
Equations
- WithTop.untop' d x = WithTop.recTopCoe d id x
Instances For
Lift a map f : α → β
to WithTop α → WithTop β
. Implemented using Option.map
.
Equations
- WithTop.map f = Option.map f
Instances For
Equations
- WithTop.orderTop = OrderTop.mk ⋯
Equations
- WithTop.orderBot = OrderBot.mk ⋯
Equations
- WithTop.boundedOrder = let __src := WithTop.orderTop; let __src_1 := WithTop.orderBot; BoundedOrder.mk
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
- WithTop.preorder = Preorder.mk ⋯ ⋯ ⋯
Equations
- WithTop.partialOrder = PartialOrder.mk ⋯
Alias of the reverse direction of WithTop.monotone_map_iff
.
Alias of the reverse direction of WithTop.strictMono_map_iff
.
Equations
- WithTop.semilatticeInf = let __src := WithTop.partialOrder; SemilatticeInf.mk ⋯ ⋯ ⋯
Equations
- WithTop.semilatticeSup = let __src := WithTop.partialOrder; SemilatticeSup.mk ⋯ ⋯ ⋯
Equations
- WithTop.lattice = let __src := WithTop.semilatticeSup; let __src_1 := WithTop.semilatticeInf; Lattice.mk ⋯ ⋯ ⋯
Equations
- WithTop.distribLattice = let __src := WithTop.lattice; DistribLattice.mk ⋯
Equations
- WithTop.decidableEq = inferInstanceAs (DecidableEq (Option α))
Equations
- x✝.decidableLE x = decidable_of_decidable_of_iff ⋯
Equations
- x✝.decidableLT x = decidable_of_decidable_of_iff ⋯
Equations
- WithTop.linearOrder = Lattice.toLinearOrder (WithTop α)
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯