# 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.

## Instances For

Convert an injective left order continuous function to an `OrderEmbedding`

.