refinement of partitions

Stream: general

[Kenny Lau]

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]

What do you mean by partition?

[Kenny Lau]

preimage of list.join

[Mario Carneiro]

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

[Kenny Lau]

well there's a minimal refinement

[Mario Carneiro]

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