Supremum over an order embedding

Stream: Is there code for X?

[Violeta Hernández]

Do we have sSup (f '' s) ≤ f (sSup s) for f an order embedding? Or any lemmas similar to that

[Violeta Hernández]

There's docs#OrderEmbedding.le_map_sup but that's only for the binary supremum

[Violeta Hernández]

Oh wait this is docs#Monotone.le_map_sSup

[Violeta Hernández]

It seems like we don't have conditionally complete versions of this though

[Yury G. Kudryashov]

For a conditionally complete lattice, you need some BddAbove/Set.Nonempty assumptions.

[Yury G. Kudryashov]

See Monotone.le_csSup_image

[Yury G. Kudryashov]

But it lacks sSup on one side.

[Violeta Hernández]

For specifically order isos over a ConditionallyCompleteLatticeOrderBot you can actually omit these hypotheses

[Violeta Hernández]

I think we're also missing these versions