semilattices

Stream: general

[Simon Hudon]

I'm looking for a kind of semilattice with a bottom, and I'd like to be able to take the limit of a monotonically increasing series. Does it exist, is it in mathlib and what is it called?

[Johannes Hölzl]

This is often called a chain-complete partial order. I don't think it is in mathlib yet. I have a very old theory about the fixed construction, but it doesn't compile anymore (see https://gist.github.com/johoelzl/900ec0250f46a2ac4070bfc4f4fd0405 )

[Simon Hudon]

Cool! Thanks! Do you mind if I fix it up and PR it?

[Johannes Hölzl]

Of course! Go on.