# 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.ofSetoid: With Fintype α, constructs the finpartition of univ : Finset α induced by the equivalence classes of s : Setoid α.
• 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 #

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

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

• parts :

The elements of the finite partition of a

• supIndep : self.parts.SupIndep id

The partition is supremum-independent

• sup_parts : self.parts.sup id = a

The supremum of the partition is a

• not_bot_mem : self.parts

No element of the partition is bottom

Instances For
theorem Finpartition.supIndep {α : Type u_1} [] [] {a : α} (self : ) :
self.parts.SupIndep id

The partition is supremum-independent

theorem Finpartition.sup_parts {α : Type u_1} [] [] {a : α} (self : ) :
self.parts.sup id = a

The supremum of the partition is a

theorem Finpartition.not_bot_mem {α : Type u_1} [] [] {a : α} (self : ) :
self.parts

No element of the partition is bottom

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

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

Equations
• Finpartition.ofErase parts sup_indep sup_parts = { parts := parts.erase , supIndep := , sup_parts := , not_bot_mem := }
Instances For
@[simp]
theorem Finpartition.ofSubset_parts {α : Type u_1} [] [] {a : α} {b : α} (P : ) {parts : } (subset : parts P.parts) (sup_parts : parts.sup id = b) :
(P.ofSubset subset sup_parts).parts = parts
def Finpartition.ofSubset {α : Type u_1} [] [] {a : α} {b : α} (P : ) {parts : } (subset : parts P.parts) (sup_parts : parts.sup id = b) :

A Finpartition constructor from a bigger existing finpartition.

Equations
• P.ofSubset subset sup_parts = { parts := parts, supIndep := , sup_parts := sup_parts, not_bot_mem := }
Instances For
@[simp]
theorem Finpartition.copy_parts {α : Type u_1} [] [] {a : α} {b : α} (P : ) (h : a = b) :
(P.copy h).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.

Equations
• P.copy h = { parts := P.parts, supIndep := , sup_parts := , not_bot_mem := }
Instances For
def Finpartition.map {α : Type u_1} [] [] {β : Type u_2} [] [] {a : α} (e : α ≃o β) (P : ) :

Transfer a finpartition over an order isomorphism.

Equations
• = { parts := Finset.map (↑e).toEmbedding P.parts, supIndep := , sup_parts := , not_bot_mem := }
Instances For
@[simp]
theorem Finpartition.parts_map {α : Type u_1} [] [] {β : Type u_2} [] [] {a : α} {e : α ≃o β} {P : } :
(Finpartition.map e P).parts = Finset.map (↑e).toEmbedding P.parts
@[simp]
theorem Finpartition.empty_parts (α : Type u_1) [] [] :
.parts =
def Finpartition.empty (α : Type u_1) [] [] :

The empty finpartition.

Equations
• = { parts := , supIndep := , sup_parts := , not_bot_mem := }
Instances For
instance Finpartition.instInhabitedBot (α : Type u_1) [] [] :
Equations
• = { default := }
@[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.

Equations
• = { parts := {a}, supIndep := , sup_parts := , not_bot_mem := }
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 : ) :
(↑P.parts).PairwiseDisjoint 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 : } :
P.parts.Nonempty a
theorem Finpartition.parts_nonempty {α : Type u_1} [] [] {a : α} (P : ) (ha : a ) :
P.parts.Nonempty
instance Finpartition.instUniqueBot {α : Type u_1} [] [] :
Equations
• Finpartition.instUniqueBot = let __src := inferInstance; { toInhabited := __src, uniq := }
@[reducible, inline]
abbrev IsAtom.uniqueFinpartition {α : Type u_1} [] [] {a : α} {P : } (ha : ) :

There's a unique partition of an atom.

Equations
• ha.uniqueFinpartition = { default := , uniq := }
Instances For
instance Finpartition.instFintypeOfDecidableEq {α : Type u_1} [] [] [] [] (a : α) :
Equations
• One or more equations did not get rendered due to their size.

### Refinement order #

instance Finpartition.instLE {α : Type u_1} [] [] {a : α} :

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

Equations
• Finpartition.instLE = { le := fun (P Q : ) => ∀ ⦃b : α⦄, b P.partscQ.parts, b c }
instance Finpartition.instPartialOrder {α : Type u_1} [] [] {a : α} :
Equations
• Finpartition.instPartialOrder = let __src := inferInstance;
instance Finpartition.instOrderTopOfDecidableEqBot {α : Type u_1} [] [] {a : α} [Decidable (a = )] :
Equations
• Finpartition.instOrderTopOfDecidableEqBot =
theorem Finpartition.parts_top_subset {α : Type u_1} [] [] (a : α) [Decidable (a = )] :
.parts {a}
theorem Finpartition.parts_top_subsingleton {α : Type u_1} [] [] (a : α) [Decidable (a = )] :
(↑.parts).Subsingleton
instance Finpartition.instInf {α : Type u_1} [] [] [] {a : α} :
Equations
@[simp]
theorem Finpartition.parts_inf {α : Type u_1} [] [] [] {a : α} (P : ) (Q : ) :
(P Q).parts = (Finset.image (fun (bc : α × α) => bc.1 bc.2) (P.parts ×ˢ Q.parts)).erase
instance Finpartition.instSemilatticeInf {α : Type u_1} [] [] [] {a : α} :
Equations
• Finpartition.instSemilatticeInf = let __src := inferInstance; let __src_1 := inferInstance;
theorem Finpartition.exists_le_of_le {α : Type u_1} [] [] {a : α} {b : α} {P : } {Q : } (h : P Q) (hb : b Q.parts) :
cP.parts, c b
theorem Finpartition.card_mono {α : Type u_1} [] [] {a : α} {P : } {Q : } (h : P Q) :
Q.parts.card P.parts.card
@[simp]
theorem Finpartition.bind_parts {α : Type u_1} [] [] [] {a : α} (P : ) (Q : (i : α) → i P.parts) :
(P.bind Q).parts = P.parts.attach.biUnion fun (i : { x : α // x P.parts }) => (Q i ).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.

Equations
• P.bind Q = { parts := P.parts.attach.biUnion fun (i : { x : α // x P.parts }) => (Q i ).parts, supIndep := , sup_parts := , not_bot_mem := }
Instances For
theorem Finpartition.mem_bind {α : Type u_1} [] [] [] {a : α} {b : α} {P : } {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} [] [] [] {a : α} {P : } (Q : (i : α) → i P.parts) :
(P.bind Q).parts.card = AP.parts.attach, (Q A ).parts.card
@[simp]
theorem Finpartition.extend_parts {α : Type u_1} [] [] [] {a : α} {b : α} {c : α} (P : ) (hb : b ) (hab : Disjoint a b) (hc : a b = c) :
(P.extend 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.

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

Restricts a finpartition to avoid a given element.

Equations
Instances For
@[simp]
theorem Finpartition.mem_avoid {α : Type u_1} [] {a : α} {b : α} {c : α} (P : ) :
c (P.avoid b).parts dP.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) :
a.Nonempty
theorem Finpartition.eq_of_mem_parts {α : Type u_1} [] {s : } {t : } {u : } (P : ) {a : α} (ht : t P.parts) (hu : u P.parts) (hat : a t) (hau : a u) :
t = u
theorem Finpartition.exists_mem {α : Type u_1} [] {s : } (P : ) {a : α} (ha : a s) :
tP.parts, a t
theorem Finpartition.biUnion_parts {α : Type u_1} [] {s : } (P : ) :
P.parts.biUnion id = s
theorem Finpartition.existsUnique_mem {α : Type u_1} [] {s : } (P : ) {a : α} (ha : a s) :
∃! t : , t P.parts a t
def Finpartition.part {α : Type u_1} [] {s : } (P : ) (a : α) :

The part of the finpartition that a lies in.

Equations
Instances For
theorem Finpartition.part_mem {α : Type u_1} [] {s : } (P : ) {a : α} (ha : a s) :
P.part a P.parts
theorem Finpartition.mem_part {α : Type u_1} [] {s : } (P : ) {a : α} (ha : a s) :
a P.part a
theorem Finpartition.part_eq_of_mem {α : Type u_1} [] {s : } {t : } (P : ) {a : α} (ht : t P.parts) (hat : a t) :
P.part a = t
theorem Finpartition.mem_part_iff_part_eq_part {α : Type u_1} [] {s : } (P : ) {a : α} {b : α} (ha : a s) (hb : b s) :
a P.part b P.part a = P.part b
theorem Finpartition.part_surjOn {α : Type u_1} [] {s : } (P : ) :
Set.SurjOn P.part s P.parts
theorem Finpartition.exists_subset_part_bijOn {α : Type u_1} [] {s : } (P : ) :
rs, Set.BijOn P.part r P.parts
def Finpartition.equivSigmaParts {α : Type u_1} [] {s : } (P : ) :
{ x : α // x s } (t : { x : // x P.parts }) × { x : α // x t }

Equivalence between a finpartition's parts as a dependent sum and the partitioned set.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Finpartition.exists_enumeration {α : Type u_1} [] {s : } (P : ) :
∃ (f : { x : α // x s } (t : { x : // x P.parts }) × Fin (↑t).card), ∀ (a b : { x : α // x s }), P.part a = P.part b (f a).fst = (f b).fst
theorem Finpartition.sum_card_parts {α : Type u_1} [] {s : } (P : ) :
iP.parts, i.card = s.card
instance Finpartition.instBotFinset {α : Type u_1} [] (s : ) :

⊥ is the partition in singletons, aka discrete partition.

Equations
• = { bot := { parts := Finset.map { toFun := singleton, inj' := } s, supIndep := , sup_parts := , not_bot_mem := } }
@[simp]
theorem Finpartition.parts_bot {α : Type u_1} [] (s : ) :
.parts = Finset.map { toFun := singleton, inj' := } s
theorem Finpartition.card_bot {α : Type u_1} [] (s : ) :
.parts.card = s.card
theorem Finpartition.mem_bot_iff {α : Type u_1} [] {s : } {t : } :
t .parts as, {a} = t
instance Finpartition.instOrderBotFinset {α : Type u_1} [] (s : ) :
Equations
• = let __src := inferInstance;
theorem Finpartition.card_parts_le_card {α : Type u_1} [] {s : } (P : ) :
P.parts.card s.card
theorem Finpartition.card_mod_card_parts_le {α : Type u_1} [] {s : } (P : ) :
s.card % P.parts.card P.parts.card
def Finpartition.ofSetoid {α : Type u_1} [] [] (s : ) [DecidableRel Setoid.r] :
Finpartition Finset.univ

A setoid over a finite type induces a finpartition of the type's elements, where the parts are the setoid's equivalence classes.

Equations
Instances For
theorem Finpartition.mem_part_ofSetoid_iff_rel {α : Type u_1} [] {a : α} [] {s : } [DecidableRel Setoid.r] {b : α} :
b .part a Setoid.r a b
def Finpartition.atomise {α : Type u_1} [] [] (s : ) (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
Instances For
theorem Finpartition.mem_atomise {α : Type u_1} [] {s : } {t : } [] {F : Finset (Finset α)} :
t .parts t.Nonempty QF, Finset.filter (fun (i : α) => uF, u Q i u) s = t
theorem Finpartition.atomise_empty {α : Type u_1} [] {s : } [] (hs : s.Nonempty) :
.parts = {s}
theorem Finpartition.card_atomise_le {α : Type u_1} [] {s : } [] {F : Finset (Finset α)} :
.parts.card 2 ^ F.card
theorem Finpartition.biUnion_filter_atomise {α : Type u_1} [] {s : } {t : } [] {F : Finset (Finset α)} (ht : t F) (hts : t s) :
(Finset.filter (fun (u : ) => u t u.Nonempty) .parts).biUnion id = t
theorem Finpartition.card_filter_atomise_le_two_pow {α : Type u_1} [] {s : } {t : } [] {F : Finset (Finset α)} (ht : t F) :
(Finset.filter (fun (u : ) => u t u.Nonempty) .parts).card 2 ^ (F.card - 1)