# Documentation

Mathlib.Order.Partition.Finpartition

# Finite partitions #

In this file, we define finite partitions. A finpartition of a : α is a finite set of pairwise disjoint parts parts : Finset α which does not contain ⊥ and whose supremum is a.

Finpartitions of a finset are at the heart of Szemerédi's regularity lemma. They are also studied purely order theoretically in Sperner theory.

## Constructions #

We provide many ways to build finpartitions:

• Finpartition.ofErase: Builds a finpartition by erasing ⊥ for you.
• Finpartition.ofSubset: 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 s along all finsets in F : Finset (Finset α). Two elements of s belong to the same part iff they belong to the same elements of F.

Finpartition.indiscrete and Finpartition.bind together form the monadic structure of Finpartition.

## Implementation notes #

Forbidding ⊥ as a part follows mathematical tradition and is a pragmatic choice concerning operations on 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 Finpartition.ofErase.

## TODO #

Link Finpartition and Setoid.isPartition.

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?

theorem Finpartition.ext {α : Type u_1} :
∀ {inst : } {inst_1 : } {a : α} (x y : ), x.parts = y.partsx = y
theorem Finpartition.ext_iff {α : Type u_1} :
∀ {inst : } {inst_1 : } {a : α} (x y : ), x = y x.parts = y.parts
structure Finpartition {α : Type u_1} [] [] (a : α) :
Type u_1
• parts :

The elements of the finite partition of a

• supIndep : Finset.SupIndep s.parts id

The partition is supremum-independent

• supParts : Finset.sup s.parts id = a

The supremum of the partition is a

• not_bot_mem : ¬ s.parts

No element of the partition is bottom

A finite partition of a : α is a pairwise disjoint finite set of elements whose supremum is a. We forbid ⊥ as a part.

Instances For
instance instDecidableEqFinpartition :
{α : Type u_2} → {inst : } → {inst_1 : } → {a : α} → [inst_2 : ] →
@[simp]
theorem Finpartition.ofErase_parts {α : Type u_1} [] [] [] {a : α} (parts : ) (sup_indep : Finset.SupIndep parts id) (sup_parts : Finset.sup parts id = a) :
(Finpartition.ofErase parts sup_indep sup_parts).parts = Finset.erase parts
def Finpartition.ofErase {α : Type u_1} [] [] [] {a : α} (parts : ) (sup_indep : Finset.SupIndep parts id) (sup_parts : Finset.sup parts id = a) :

A Finpartition constructor which does not insist on ⊥ not being a part.

Instances For
@[simp]
theorem Finpartition.ofSubset_parts {α : Type u_1} [] [] {a : α} {b : α} (P : ) {parts : } (subset : parts P.parts) (sup_parts : Finset.sup parts id = b) :
(Finpartition.ofSubset P subset sup_parts).parts = parts
def Finpartition.ofSubset {α : Type u_1} [] [] {a : α} {b : α} (P : ) {parts : } (subset : parts P.parts) (sup_parts : Finset.sup parts id = b) :

A Finpartition constructor from a bigger existing finpartition.

Instances For
@[simp]
theorem Finpartition.copy_parts {α : Type u_1} [] [] {a : α} {b : α} (P : ) (h : a = b) :
().parts = P.parts
def Finpartition.copy {α : Type u_1} [] [] {a : α} {b : α} (P : ) (h : a = b) :

Changes the type of a finpartition to an equal one.

Instances For
@[simp]
theorem Finpartition.empty_parts (α : Type u_1) [] [] :
().parts =
def Finpartition.empty (α : Type u_1) [] [] :

The empty finpartition.

Instances For
@[simp]
theorem Finpartition.default_eq_empty (α : Type u_1) [] [] :
default =
@[simp]
theorem Finpartition.indiscrete_parts {α : Type u_1} [] [] {a : α} (ha : a ) :
().parts = {a}
def Finpartition.indiscrete {α : Type u_1} [] [] {a : α} (ha : a ) :

The finpartition in one part, aka indiscrete finpartition.

Instances For
theorem Finpartition.le {α : Type u_1} [] [] {a : α} (P : ) {b : α} (hb : b P.parts) :
b a
theorem Finpartition.ne_bot {α : Type u_1} [] [] {a : α} (P : ) {b : α} (hb : b P.parts) :
theorem Finpartition.disjoint {α : Type u_1} [] [] {a : α} (P : ) :
Set.PairwiseDisjoint (P.parts) id
theorem Finpartition.parts_eq_empty_iff {α : Type u_1} [] [] {a : α} {P : } :
P.parts = a =
theorem Finpartition.parts_nonempty_iff {α : Type u_1} [] [] {a : α} {P : } :
theorem Finpartition.parts_nonempty {α : Type u_1} [] [] {a : α} (P : ) (ha : a ) :
@[reducible]
def IsAtom.uniqueFinpartition {α : Type u_1} [] [] {a : α} {P : } (ha : ) :

There's a unique partition of an atom.

Instances For
instance Finpartition.instFintypeFinpartition {α : Type u_1} [] [] [] [] (a : α) :

### Refinement order #

instance Finpartition.instLEFinpartition {α : Type u_1} [] [] {a : α} :
LE ()

We say that P ≤ Q if P refines Q: each part of P is less than some part of Q.

instance Finpartition.instPartialOrderFinpartition {α : Type u_1} [] [] {a : α} :
theorem Finpartition.parts_top_subset {α : Type u_1} [] [] (a : α) [Decidable (a = )] :
.parts {a}
theorem Finpartition.parts_top_subsingleton {α : Type u_1} [] [] (a : α) [Decidable (a = )] :
instance Finpartition.instInfFinpartitionToLattice {α : Type u_1} [] [] [] {a : α} :
Inf ()
@[simp]
theorem Finpartition.parts_inf {α : Type u_1} [] [] [] {a : α} (P : ) (Q : ) :
(P Q).parts = Finset.erase (Finset.image (fun bc => bc.fst bc.snd) (P.parts ×ˢ Q.parts))
theorem Finpartition.exists_le_of_le {α : Type u_1} [] [] {a : α} {b : α} {P : } {Q : } (h : P Q) (hb : b Q.parts) :
c, c P.parts c b
theorem Finpartition.card_mono {α : Type u_1} [] [] {a : α} {P : } {Q : } (h : P Q) :
Finset.card Q.parts Finset.card P.parts
@[simp]
theorem Finpartition.bind_parts {α : Type u_1} [] [] [] {a : α} (P : ) (Q : (i : α) → i P.parts) :
().parts = Finset.biUnion (Finset.attach P.parts) fun i => (Q i (_ : i P.parts)).parts
def Finpartition.bind {α : Type u_1} [] [] [] {a : α} (P : ) (Q : (i : α) → i P.parts) :

Given a finpartition P of a and finpartitions of each part of P, this yields the finpartition of a obtained by juxtaposing all the subpartitions.

Instances For
theorem Finpartition.mem_bind {α : Type u_1} [] [] [] {a : α} {b : α} {P : } {Q : (i : α) → i P.parts} :
b ().parts A hA, b (Q A hA).parts
theorem Finpartition.card_bind {α : Type u_1} [] [] [] {a : α} {P : } (Q : (i : α) → i P.parts) :
Finset.card ().parts = Finset.sum (Finset.attach P.parts) fun A => Finset.card (Q A (_ : A P.parts)).parts
@[simp]
theorem Finpartition.extend_parts {α : Type u_1} [] [] [] {a : α} {b : α} {c : α} (P : ) (hb : b ) (hab : Disjoint a b) (hc : a b = c) :
(Finpartition.extend P hb hab hc).parts = insert b P.parts
def Finpartition.extend {α : Type u_1} [] [] [] {a : α} {b : α} {c : α} (P : ) (hb : b ) (hab : Disjoint a b) (hc : a b = c) :

Adds b to a finpartition of a to make a finpartition of a ⊔ b.

Instances For
theorem Finpartition.card_extend {α : Type u_1} [] [] [] {a : α} (P : ) (b : α) (c : α) {hb : b } {hab : Disjoint a b} {hc : a b = c} :
Finset.card (Finpartition.extend P hb hab hc).parts = Finset.card P.parts + 1
@[simp]
theorem Finpartition.avoid_parts_val {α : Type u_1} [] {a : α} (P : ) (b : α) :
().parts.val = Multiset.erase (Multiset.dedup (Multiset.map (fun x => x \ b) P.parts.val))
def Finpartition.avoid {α : Type u_1} [] {a : α} (P : ) (b : α) :

Restricts a finpartition to avoid a given element.

Instances For
@[simp]
theorem Finpartition.mem_avoid {α : Type u_1} [] {a : α} {b : α} {c : α} (P : ) :
c ().parts d, d P.parts ¬d b d \ b = c

### Finite partitions of finsets #

theorem Finpartition.nonempty_of_mem_parts {α : Type u_1} [] {s : } (P : ) {a : } (ha : a P.parts) :
theorem Finpartition.exists_mem {α : Type u_1} [] {s : } (P : ) {a : α} (ha : a s) :
t, t P.parts a t
theorem Finpartition.biUnion_parts {α : Type u_1} [] {s : } (P : ) :
Finset.biUnion P.parts id = s
theorem Finpartition.sum_card_parts {α : Type u_1} [] {s : } (P : ) :
(Finset.sum P.parts fun i => ) =

⊥ is the partition in singletons, aka discrete partition.

@[simp]
theorem Finpartition.parts_bot {α : Type u_1} [] (s : ) :
.parts = Finset.map { toFun := singleton, inj' := (_ : Function.Injective singleton) } s
theorem Finpartition.card_bot {α : Type u_1} [] (s : ) :
theorem Finpartition.mem_bot_iff {α : Type u_1} [] {s : } {t : } :
t .parts a, a s {a} = t
theorem Finpartition.card_parts_le_card {α : Type u_1} [] {s : } (P : ) :
Finset.card P.parts
def Finpartition.atomise {α : Type u_1} [] (s : ) (F : Finset ()) :

Cuts s along the finsets in F: Two elements of s will be in the same part if they are in the same finsets of F.

Instances For
theorem Finpartition.mem_atomise {α : Type u_1} [] {s : } {t : } {F : Finset ()} :
t ().parts Q x, Finset.filter (fun i => ∀ (u : ), u F → (u Q i u)) s = t
theorem Finpartition.atomise_empty {α : Type u_1} [] {s : } (hs : ) :
().parts = {s}
theorem Finpartition.card_atomise_le {α : Type u_1} [] {s : } {F : Finset ()} :
Finset.card ().parts 2 ^
theorem Finpartition.biUnion_filter_atomise {α : Type u_1} [] {s : } {t : } {F : Finset ()} (ht : t F) (hts : t s) :
Finset.biUnion (Finset.filter (fun u => u t ) ().parts) id = t
theorem Finpartition.card_filter_atomise_le_two_pow {α : Type u_1} [] {s : } {t : } {F : Finset ()} (ht : t F) :
Finset.card (Finset.filter (fun u => u t ) ().parts) 2 ^ ( - 1)