Conditional complete lattice cleanup

Stream: general

[Violeta Hernández]

Currently, complete_lattice.lean and conditionally_complete_lattice.lean are two very different files with very different structures, even if they have a lot of analogous theorems. A few times already I've wanted to use some result on conditional complete lattices that has only been proved on complete lattices. I want to embark on a refactor to match these two APIs.

Of course, the best way to assure that these APIs remain matched in the future would be to put them in a single file, perhaps even putting analogous statements together. This would also get rid of a few redundant statements like Sup_singleton and cSup_singleton, but it would yield a 2k line file, so I don't know if that's the best idea.

[Yaël Dillies]

I don't think merging the two files would be a good idea. If the files are separate, you can diff them. Try that out on file#data/set/pointwise and file#data/finset/pointwise. This should be instructive.

[Violeta Hernández]

Well, if GitHub allows for this to be done easily, then there shouldn't be an issue with keeping the files separate

[Wrenna Robson]

I agree with this and I'd be happy to help with such a refactor. I think there are questions about the best way to do it though.

As I have remarked elsewhere, defining conditionally complete lattices in terms of their relationship with the lattice completion means that we could simply have theorems on CCLs as special cases of theorems on CLs, which, to me, makes sense. This has the benefit of making it easy to define other partially-complete structures, some of which naturally occur in applications.

[Wrenna Robson]

Even if we don't do this, however, I agree that a refactor would be useful.

[Wrenna Robson]

I have some other ideas for things that this could/should include but I won't get fully into it - I'm just keen and happy to be involved.