Order on `Nat.Partition`?

Stream: Is there code for X?

[Anne Baanen]

Do we have anything about the order on docs#Nat.Partition, where x ≤ y if y can be given by further splitting up some of the parts of x?

I don't know how to give a nice precise definition. For docs#Composition it would be:

def Composition.le (x y : Composition n) :=
  ∃ l : List (List ℕ)), l.length = x.blocks.length ∧ l.join = y.blocks ∧
  ∀ i < l.length, IsComposition (l !! i) (x.blocks !! i)

[Yaël Dillies]

Yes, but not quite how you expect it: docs#Finpartition is equipped with the refinement order, and we've shown it has an inf. We haven't yet managed to show it has a sup.

[Anne Baanen]

We can probably make that work, or translate it to the Nat.Partition case. Thanks!