## Stream: general

### Topic: refinement of partitions

#### Kenny Lau (Apr 18 2018 at 00:04):

what are the existing lemmas related to refinement of partitions, i.e. the idea that if there are two partitions of a list, then there is a partition that refines both?

#### Mario Carneiro (Apr 18 2018 at 00:11):

What do you mean by partition?

#### Kenny Lau (Apr 18 2018 at 00:12):

preimage of list.join

#### Mario Carneiro (Apr 18 2018 at 00:17):

It seems a bit trivial, since there is a maximal partition

#### Kenny Lau (Apr 18 2018 at 00:18):

well there's a minimal refinement

#### Mario Carneiro (Apr 18 2018 at 00:19):

I don't think the subpartition relation exists in mathlib, but you could prove it's a lattice

Last updated: May 16 2021 at 05:21 UTC