complete lattice of setoids

Stream: new members

[Amelia Livingston]

Hi! I've written a small file of results about setoids that were generalisations of things I've written about congruence relations.
It's at https://github.com/leanprover-community/mathlib/blob/setoid_complete_lattice/src/data/setoid.lean and it's got stuff like the complete lattice of setoids on a type, results about the inductively defined equivalence closure of a binary relation, eqv_gen, and the analogues of some isomorphism theorems for quotients of arbitrary types.
I'd like to try and make it PR-able if it's deemed useful.

I'm assuming there's a reason there's no coercion from setoid α to α → α → Prop; is

def r' (r : setoid α) := @setoid.r _ r

a sensible alternative if I want to easily talk about different setoids on the same type?

I'd like to add to the file if there's more that should be there, and I realise it might be better off without the lemmas about kernels, split into sections and put in existing appropriate files.

[Bryan Gin-ge Chen]

the complete lattice of setoids on a type,

Johannes suggested adding that here, and I would happily close that PR in favor of something built off what you're putting together.

[Floris van Doorn]

For the latest Proving for Fun problem set we also had different setoids on a single type. I think it's very welcome to have better support for that. I would maybe call it setoid.rel instead of setoid.r'.

[Johan Commelin]

+1 from me. Projection notation to the win! @Amelia Livingston With the suggestion of Floris, we would be able to type foo.rel to access the relation, for foo : setoid X.

[Amelia Livingston]

@Bryan Gin-ge Chen brilliant, thanks so much for the link! I'll incorporate what's in the partitions file into mine.
& rel would definitely be better!

[Amelia Livingston]

I've incorporated the partitions file into mine following the advice on the partitions PR and the tutorial thread; as such there's not much infrastructure for working with partitions instead of setoids and I haven't made them a separate structure. I also haven't assumed a partition doesn't contain the empty set until it's needed in theorems (so the docstrings aren't strictly precise).

I was working on showing the Bell numbers are the number of possible partitions of a finite set until I found @Neil Strickland's done this here in a neat and computationally efficient way. If it's okay with him I could try and write an adaptation of that compatible with my file at some point, but it's long and I'm trying to get round to PR'ing some other stuff before term starts. I left in a couple of lemmas about my Bell number function, not sure they should be there.