# mathlib3documentation

order.partition.finpartition

# 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 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.of_erase: Builds a finpartition by erasing ⊥ for you.
• 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 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.of_erase.

## TODO #

Link finpartition and setoid.is_partition.

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?

@[protected, instance]
def finpartition.decidable_eq {α : Type u_1} [a : decidable_eq α] [lattice α] [order_bot α] (a_1 : α) :
theorem finpartition.ext_iff {α : Type u_1} {_inst_1 : lattice α} {_inst_2 : order_bot α} {a : α} (x y : finpartition a) :
x = y x.parts = y.parts
theorem finpartition.ext {α : Type u_1} {_inst_1 : lattice α} {_inst_2 : order_bot α} {a : α} (x y : finpartition a) (h : x.parts = y.parts) :
x = y
@[ext]
structure finpartition {α : Type u_1} [lattice α] [order_bot α] (a : α) :
Type u_1

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

Instances for finpartition
def finpartition.of_erase {α : Type u_1} [lattice α] [order_bot α] [decidable_eq α] {a : α} (parts : finset α) (sup_indep : parts.sup_indep id) (sup_parts : parts.sup id = a) :

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

Equations
@[simp]
theorem finpartition.of_erase_parts {α : Type u_1} [lattice α] [order_bot α] [decidable_eq α] {a : α} (parts : finset α) (sup_indep : parts.sup_indep id) (sup_parts : parts.sup id = a) :
(finpartition.of_erase parts sup_indep sup_parts).parts = parts.erase
@[simp]
theorem finpartition.of_subset_parts {α : Type u_1} [lattice α] [order_bot α] {a b : α} (P : finpartition a) {parts : finset α} (subset : parts P.parts) (sup_parts : parts.sup id = b) :
(P.of_subset subset sup_parts).parts = parts
def finpartition.of_subset {α : Type u_1} [lattice α] [order_bot α] {a b : α} (P : finpartition a) {parts : finset α} (subset : parts P.parts) (sup_parts : parts.sup id = b) :

A finpartition constructor from a bigger existing finpartition.

Equations
def finpartition.copy {α : Type u_1} [lattice α] [order_bot α] {a b : α} (P : finpartition a) (h : a = b) :

Changes the type of a finpartition to an equal one.

Equations
@[simp]
theorem finpartition.copy_parts {α : Type u_1} [lattice α] [order_bot α] {a b : α} (P : finpartition a) (h : a = b) :
(P.copy h).parts = P.parts
@[simp]
theorem finpartition.empty_parts (α : Type u_1) [lattice α] [order_bot α] :
@[protected]
def finpartition.empty (α : Type u_1) [lattice α] [order_bot α] :

The empty finpartition.

Equations
@[protected, instance]
def finpartition.inhabited (α : Type u_1) [lattice α] [order_bot α] :
Equations
@[simp]
theorem finpartition.default_eq_empty (α : Type u_1) [lattice α] [order_bot α] :
@[simp]
theorem finpartition.indiscrete_parts {α : Type u_1} [lattice α] [order_bot α] {a : α} (ha : a ) :
= {a}
def finpartition.indiscrete {α : Type u_1} [lattice α] [order_bot α] {a : α} (ha : a ) :

The finpartition in one part, aka indiscrete finpartition.

Equations
@[protected]
theorem finpartition.le {α : Type u_1} [lattice α] [order_bot α] {a : α} (P : finpartition a) {b : α} (hb : b P.parts) :
b a
theorem finpartition.ne_bot {α : Type u_1} [lattice α] [order_bot α] {a : α} (P : finpartition a) {b : α} (hb : b P.parts) :
@[protected]
theorem finpartition.disjoint {α : Type u_1} [lattice α] [order_bot α] {a : α} (P : finpartition a) :
theorem finpartition.parts_eq_empty_iff {α : Type u_1} [lattice α] [order_bot α] {a : α} {P : finpartition a} :
theorem finpartition.parts_nonempty_iff {α : Type u_1} [lattice α] [order_bot α] {a : α} {P : finpartition a} :
theorem finpartition.parts_nonempty {α : Type u_1} [lattice α] [order_bot α] {a : α} (P : finpartition a) (ha : a ) :
@[protected, instance]
def finpartition.unique {α : Type u_1} [lattice α] [order_bot α] :
Equations
@[reducible]
def is_atom.unique_finpartition {α : Type u_1} [lattice α] [order_bot α] {a : α} (ha : is_atom a) :

There's a unique partition of an atom.

Equations
@[protected, instance]
def finpartition.fintype {α : Type u_1} [lattice α] [order_bot α] [fintype α] [decidable_eq α] (a : α) :
Equations

### Refinement order #

@[protected, instance]
def finpartition.has_le {α : Type u_1} [lattice α] [order_bot α] {a : α} :

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

Equations
@[protected, instance]
def finpartition.partial_order {α : Type u_1} [lattice α] [order_bot α] {a : α} :
Equations
@[protected, instance]
def finpartition.order_top {α : Type u_1} [lattice α] [order_bot α] {a : α} [decidable (a = )] :
Equations
theorem finpartition.parts_top_subset {α : Type u_1} [lattice α] [order_bot α] (a : α) [decidable (a = )] :
theorem finpartition.parts_top_subsingleton {α : Type u_1} [lattice α] [order_bot α] (a : α) [decidable (a = )] :
@[protected, instance]
def finpartition.has_inf {α : Type u_1} [order_bot α] [decidable_eq α] {a : α} :
Equations
@[simp]
theorem finpartition.parts_inf {α : Type u_1} [order_bot α] [decidable_eq α] {a : α} (P Q : finpartition a) :
(P Q).parts = (finset.image (λ (bc : α × α), bc.fst bc.snd) (P.parts ×ˢ Q.parts)).erase
@[protected, instance]
def finpartition.semilattice_inf {α : Type u_1} [order_bot α] [decidable_eq α] {a : α} :
Equations
theorem finpartition.exists_le_of_le {α : Type u_1} [order_bot α] {a b : α} {P Q : finpartition a} (h : P Q) (hb : b Q.parts) :
(c : α) (H : c P.parts), c b
theorem finpartition.card_mono {α : Type u_1} [order_bot α] {a : α} {P Q : finpartition a} (h : P Q) :
@[simp]
theorem finpartition.bind_parts {α : Type u_1} [order_bot α] [decidable_eq α] {a : α} (P : finpartition a) (Q : Π (i : α), i P.parts ) :
(P.bind Q).parts = P.parts.attach.bUnion (λ (i : {x // x P.parts}), (Q i.val _).parts)
def finpartition.bind {α : Type u_1} [order_bot α] [decidable_eq α] {a : α} (P : finpartition a) (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.

Equations
theorem finpartition.mem_bind {α : Type u_1} [order_bot α] [decidable_eq α] {a b : α} {P : finpartition a} {Q : Π (i : α), i P.parts } :
b (P.bind Q).parts (A : α) (hA : A P.parts), b (Q A hA).parts
theorem finpartition.card_bind {α : Type u_1} [order_bot α] [decidable_eq α] {a : α} {P : finpartition a} (Q : Π (i : α), i P.parts ) :
(P.bind Q).parts.card = P.parts.attach.sum (λ (A : {x // x P.parts}), (Q A.val _).parts.card)
def finpartition.extend {α : Type u_1} [order_bot α] [decidable_eq α] {a b c : α} (P : finpartition a) (hb : b ) (hab : b) (hc : a b = c) :

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

Equations
@[simp]
theorem finpartition.extend_parts {α : Type u_1} [order_bot α] [decidable_eq α] {a b c : α} (P : finpartition a) (hb : b ) (hab : b) (hc : a b = c) :
(P.extend hb hab hc).parts =
theorem finpartition.card_extend {α : Type u_1} [order_bot α] [decidable_eq α] {a : α} (P : finpartition a) (b c : α) {hb : b } {hab : b} {hc : a b = c} :
(P.extend hb hab hc).parts.card = P.parts.card + 1
def finpartition.avoid {α : Type u_1} [decidable_eq α] {a : α} (P : finpartition a) (b : α) :

Restricts a finpartition to avoid a given element.

Equations
@[simp]
theorem finpartition.avoid_parts_val {α : Type u_1} [decidable_eq α] {a : α} (P : finpartition a) (b : α) :
(P.avoid b).parts.val = (multiset.map (λ (_x : α), _x \ b) P.parts.val).dedup.erase
@[simp]
theorem finpartition.mem_avoid {α : Type u_1} [decidable_eq α] {a b c : α} (P : finpartition a) :
c (P.avoid b).parts (d : α) (H : d P.parts), ¬d b d \ b = c

### Finite partitions of finsets #

theorem finpartition.nonempty_of_mem_parts {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) {a : finset α} (ha : a P.parts) :
theorem finpartition.exists_mem {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) {a : α} (ha : a s) :
(t : finset α) (H : t P.parts), a t
theorem finpartition.bUnion_parts {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) :
= s
theorem finpartition.sum_card_parts {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) :
P.parts.sum (λ (i : finset α), i.card) = s.card
@[protected, instance]
def finpartition.has_bot {α : Type u_1} [decidable_eq α] (s : finset α) :

⊥ is the partition in singletons, aka discrete partition.

Equations
@[simp]
theorem finpartition.parts_bot {α : Type u_1} [decidable_eq α] (s : finset α) :
theorem finpartition.card_bot {α : Type u_1} [decidable_eq α] (s : finset α) :
theorem finpartition.mem_bot_iff {α : Type u_1} [decidable_eq α] {s t : finset α} :
t .parts (a : α) (H : a s), {a} = t
@[protected, instance]
def finpartition.order_bot {α : Type u_1} [decidable_eq α] (s : finset α) :
Equations
theorem finpartition.card_parts_le_card {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) :
def finpartition.atomise {α : Type u_1} [decidable_eq α] (s : finset α) (F : finset (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.

Equations
theorem finpartition.mem_atomise {α : Type u_1} [decidable_eq α] {s t : finset α} {F : finset (finset α)} :
t F).parts t.nonempty (Q : finset (finset α)) (H : Q F), finset.filter (λ (i : α), (u : finset α), u F (u Q i u)) s = t
theorem finpartition.atomise_empty {α : Type u_1} [decidable_eq α] {s : finset α} (hs : s.nonempty) :
= {s}
theorem finpartition.card_atomise_le {α : Type u_1} [decidable_eq α] {s : finset α} {F : finset (finset α)} :
F).parts.card 2 ^ F.card
theorem finpartition.bUnion_filter_atomise {α : Type u_1} [decidable_eq α] {s t : finset α} {F : finset (finset α)} (ht : t F) (hts : t s) :
(finset.filter (λ (u : finset α), u t u.nonempty) F).parts).bUnion id = t
theorem finpartition.card_filter_atomise_le_two_pow {α : Type u_1} [decidable_eq α] {s t : finset α} {F : finset (finset α)} (ht : t F) :
(finset.filter (λ (u : finset α), u t u.nonempty) F).parts).card 2 ^ (F.card - 1)