Zulip Chat Archive

Stream: general

Topic: refinement of partitions


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:11):

What do you mean by partition?

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:12):

preimage of list.join

view this post on Zulip Mario Carneiro (Apr 18 2018 at 00:17):

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

view this post on Zulip Kenny Lau (Apr 18 2018 at 00:18):

well there's a minimal refinement

view this post on Zulip 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