Bounded order homomorphisms #
This file defines (bounded) order homomorphisms.
We use the FunLike
design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
TopHom
: Maps which preserve⊤
.BotHom
: Maps which preserve⊥
.BoundedOrderHom
: Bounded order homomorphisms. Monotone maps which preserve⊤
and⊥
.
Typeclasses #
- toFun : α → β
The underlying function. The preferred spelling is
FunLike.coe
. - map_top' : TopHom.toFun s ⊤ = ⊤
The function preserves the top element. The preferred spelling is
map_top
.
The type of ⊤
-preserving functions from α
to β
.
Instances For
- toFun : α → β
The underlying function. The preferred spelling is
FunLike.coe
. - map_bot' : BotHom.toFun s ⊥ = ⊥
The function preserves the bottom element. The preferred spelling is
map_bot
.
The type of ⊥
-preserving functions from α
to β
.
Instances For
- toFun : α → β
- monotone' : Monotone s.toFun
- map_top' : OrderHom.toFun s.toOrderHom ⊤ = ⊤
The function preserves the top element. The preferred spelling is
map_top
. - map_bot' : OrderHom.toFun s.toOrderHom ⊥ = ⊥
The function preserves the bottom element. The preferred spelling is
map_bot
.
The type of bounded order homomorphisms from α
to β
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
A
TopHomClass
morphism preserves the top element.
TopHomClass F α β
states that F
is a type of ⊤
-preserving morphisms.
You should extend this class when you extend TopHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
A
BotHomClass
morphism preserves the bottom element.
BotHomClass F α β
states that F
is a type of ⊥
-preserving morphisms.
You should extend this class when you extend BotHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
Morphisms preserve the top element. The preferred spelling is
_root_.map_top
.Morphisms preserve the bottom element. The preferred spelling is
_root_.map_bot
.
BoundedOrderHomClass F α β
states that F
is a type of bounded order morphisms.
You should extend this class when you extend BoundedOrderHom
.
Instances
Turn an element of a type F
satisfying TopHomClass F α β
into an actual
TopHom
. This is declared as the default coercion from F
to TopHom α β
.
Instances For
Turn an element of a type F
satisfying BotHomClass F α β
into an actual
BotHom
. This is declared as the default coercion from F
to BotHom α β
.
Instances For
Turn an element of a type F
satisfying BoundedOrderHomClass F α β
into an actual
BoundedOrderHom
. This is declared as the default coercion from F
to BoundedOrderHom α β
.
Instances For
Top homomorphisms #
Bot homomorphisms #
Bounded order homomorphisms #
Reinterpret a BoundedOrderHom
as a TopHom
.
Instances For
Reinterpret a BoundedOrderHom
as a BotHom
.
Instances For
Copy of a BoundedOrderHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
id
as a BoundedOrderHom
.
Instances For
Composition of BoundedOrderHom
s as a BoundedOrderHom
.
Instances For
Dual homs #
Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual orders.