Continuous order homomorphisms #
This file defines continuous order homomorphisms, that is maps which are both continuous and monotone. They are also called Priestley homomorphisms because they are the morphisms of the category of Priestley spaces.
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 #
ContinuousOrderHom: Continuous monotone functions, aka Priestley homomorphisms.
The type of continuous monotone maps from
β, aka Priestley homomorphisms.
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
- map_continuous : ∀ (f : F), Continuous ↑f
- map_monotone : ∀ (f : F), Monotone ↑f
ContinuousOrderHomClass F α β states that
F is a type of continuous monotone maps.
You should extend this class when you extend