FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Added seq partition theory

Open hacklex opened this issue 2 years ago • 0 comments

This module contains utilities for sequence-based set partitions.

We call a sequence with no duplicates a set here;

We call a set of subsets of a given set s a partition, if and only if its set union contains all elements from the given set s (no matter their order), the parts have no intersections with each other, and the parts contain no duplicates as well (that is included in them being called subsets, but I'd rather make myself as clear as possible here).

We prove the natural (and intuitively obvious) fact that the sum of partition lengths must equal the length of the base set s.

hacklex avatar Jan 20 '23 20:01 hacklex