Finite partitions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we define finite partitions. A finpartition of
a : α is a finite set of pairwise
parts : finset α which does not contain
⊥ and whose supremum is
Finpartitions of a finset are at the heart of Szemerédi's regularity lemma. They are also studied purely order theoretically in Sperner theory.
We provide many ways to build finpartitions:
finpartition.of_erase: Builds a finpartition by erasing
finpartition.of_subset: Builds a finpartition from a subset of the parts of a previous finpartition.
finpartition.empty: The empty finpartition of
finpartition.indiscrete: The indiscrete, aka trivial, aka pure, finpartition made of a single part.
finpartition.discrete: The discrete finpartition of
s : finset αmade of singletons.
finpartition.bind: Puts together the finpartitions of the parts of a finpartition into a new finpartition.
finpartition.atomise: Makes a finpartition of
s : finset αby breaking
salong all finsets in
F : finset (finset α). Two elements of
sbelong to the same part iff they belong to the same elements of
Implementation notes #
⊥ as a part follows mathematical tradition and is a pragmatic choice concerning
finpartition. Not caring about
⊥ being a part or not breaks extensionality (it's
not because the parts of
P and the parts of
Q have the same elements that
P = Q). Enforcing
⊥ to be a part makes
finpartition.bind uglier and doesn't rid us of the need of
The order is the wrong way around to make
finpartition a a graded order. Is it bad to depart from
the literature and turn the order around?
- parts : finset α
- sup_indep : self.parts.sup_indep id
- sup_parts : self.parts.sup id = a
- not_bot_mem : ⊥ ∉ self.parts
A finite partition of
a : α is a pairwise disjoint finite set of elements whose supremum is
a. We forbid
⊥ as a part.
finpartition constructor which does not insist on
⊥ not being a part.
finpartition constructor from a bigger existing finpartition.
Refinement order #
We say that
P ≤ Q if
Q: each part of
P is less than some part of
Given a finpartition
a and finpartitions of each part of
P, this yields the
a obtained by juxtaposing all the subpartitions.
b to a finpartition of
a to make a finpartition of
a ⊔ b.
Finite partitions of finsets #
⊥ is the partition in singletons, aka discrete partition.
s along the finsets in
F: Two elements of
s will be in the same part if they are
in the same finsets of