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):
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