Order continuity #
We say that a function is left order continuous if it sends all least upper bounds to least upper bounds. The order dual notion is called right order continuity.
For monotone functions ℝ → ℝ
these notions correspond to the usual left and right continuity.
We prove some basic lemmas (map_sup
, map_sSup
etc) and prove that a RelIso
is both left
and right order continuous.
Definitions #
A function f
between preorders is left order continuous if it preserves all suprema. We
define it using IsLUB
instead of sSup
so that the proof works both for complete lattices and
conditionally complete lattices.
Instances For
A function f
between preorders is right order continuous if it preserves all infima. We
define it using IsGLB
instead of sInf
so that the proof works both for complete lattices and
conditionally complete lattices.
Instances For
Convert an injective left order continuous function to an order embedding.
Equations
- LeftOrdContinuous.toOrderEmbedding f hf h = { toFun := f, inj' := h, map_rel_iff' := ⋯ }
Instances For
Convert an injective left order continuous function to an OrderEmbedding
.
Equations
- RightOrdContinuous.toOrderEmbedding f hf h = { toFun := f, inj' := h, map_rel_iff' := ⋯ }