Partitions of a set

Stream: Is there code for X?

[Peter Nelson]

I can't see a good way to work with non-indexed partitions of a set s, where s may be infinite and there may be infinitely many parts. Working with Setoid s quickly leads to DTT hell if one wants to work with the cells of the partition as sets themselves.

Finpartition has a good API when the partition has finitely many parts; is there a reason Set.Partition doesn't exist?

[Ruben Van de Velde]

Probably because nobody has created it :)

[Peter Nelson]

Ok. Presumably CompleteLattice is the right setting. Something like the following :

structure Partition [CompleteLattice α] (s : α) :=
  parts : Set α
  pairwiseDisjoint : parts.PairwiseDisjoint id
  bot_not_mem : ⊥ ∉ parts
  Sup_eq : ⨆ x ∈ parts, x = s

Would Partition by itself be ok as a name here? Or maybe PartitionOf

[Kyle Miller]

You could look at https://github.com/leanprover-community/mathlib4/blob/b383ae3471c02c9c6249948d26394b577203edf5//Mathlib/Combinatorics/SimpleGraph/Partition.lean#L59-L66

It looks like we used docs#Setoid.IsPartition on a plain Set (Set α)

[Kyle Miller]

I don't see why there couldn't be def Set.partitions (s : Set α) := {p : Set (Set α) | Setoid.IsPartition p}

[Peter Nelson]

Presumably you don't need the (s : Set α) there.

[Peter Nelson]

or I guess ⋃₀ p = s in the set builder.

[Peter Nelson]

That wouldn't cover lattice partitions though - would there be value in that extra generality?

[Yaël Dillies]

Peter Nelson said:

Finpartition has a good API when the partition has finitely many parts; is there a reason Set.Partition doesn't exist?

The reason is basically two-fold:

• I didn't need it
• I am not yet happy enough with the Finpartition API to copy the design over

[Peter Nelson]

Given that I do need it and am starting to crib from it as we speak, what are some of those design concerns?