mathlib3 documentation

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 : α) :

decidable_eq (finpartition 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

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.

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

finpartition.of_erase parts sup_indep sup_parts = {parts := parts.erase ⊥, sup_indep := _, sup_parts := _, not_bot_mem := _}

@[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

P.of_subset subset sup_parts = {parts := parts, sup_indep := _, sup_parts := sup_parts, not_bot_mem := _}

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

P.copy h = {parts := P.parts, sup_indep := _, sup_parts := _, not_bot_mem := _}

@[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 α] :

(finpartition.empty α).parts = ∅

@[protected]

def finpartition.empty (α : Type u_1) [lattice α] [order_bot α] :

finpartition ⊥

The empty finpartition.

Equations

finpartition.empty α = {parts := ∅, sup_indep := _, sup_parts := _, not_bot_mem := _}

@[protected, instance]

def finpartition.inhabited (α : Type u_1) [lattice α] [order_bot α] :

inhabited (finpartition ⊥)

Equations

finpartition.inhabited α = {default := finpartition.empty α _inst_2}

@[simp]

theorem finpartition.default_eq_empty (α : Type u_1) [lattice α] [order_bot α] :

inhabited.default = finpartition.empty α

@[simp]

theorem finpartition.indiscrete_parts {α : Type u_1} [lattice α] [order_bot α] {a : α} (ha : a ≠ ⊥) :

(finpartition.indiscrete ha).parts = {a}

def finpartition.indiscrete {α : Type u_1} [lattice α] [order_bot α] {a : α} (ha : a ≠ ⊥) :

The finpartition in one part, aka indiscrete finpartition.

Equations

finpartition.indiscrete ha = {parts := {a}, sup_indep := _, sup_parts := _, not_bot_mem := _}

@[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) :

↑(P.parts).pairwise_disjoint id

theorem finpartition.parts_eq_empty_iff {α : Type u_1} [lattice α] [order_bot α] {a : α} {P : finpartition a} :

P.parts = ∅ ↔ a = ⊥

theorem finpartition.parts_nonempty_iff {α : Type u_1} [lattice α] [order_bot α] {a : α} {P : finpartition a} :

P.parts.nonempty ↔ a ≠ ⊥

theorem finpartition.parts_nonempty {α : Type u_1} [lattice α] [order_bot α] {a : α} (P : finpartition a) (ha : a ≠ ⊥) :

P.parts.nonempty

@[protected, instance]

def finpartition.unique {α : Type u_1} [lattice α] [order_bot α] :

unique (finpartition ⊥)

Equations

finpartition.unique = {to_inhabited := {default := inhabited.default (finpartition.inhabited α)}, uniq := _}

@[reducible]

def is_atom.unique_finpartition {α : Type u_1} [lattice α] [order_bot α] {a : α} (ha : is_atom a) :

unique (finpartition a)

There's a unique partition of an atom.

Equations

ha.unique_finpartition = {to_inhabited := {default := finpartition.indiscrete _}, uniq := _}

@[protected, instance]

def finpartition.fintype {α : Type u_1} [lattice α] [order_bot α] [fintype α] [decidable_eq α] (a : α) :

fintype (finpartition a)

Equations

finpartition.fintype a = fintype.of_surjective (λ (i : {p // p.sup_indep id ∧ p.sup id = a ∧ ⊥ ∉ p}), {parts := i.val, sup_indep := _, sup_parts := _, not_bot_mem := _}) _

Refinement order #

@[protected, instance]

def finpartition.has_le {α : Type u_1} [lattice α] [order_bot α] {a : α} :

has_le (finpartition a)

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

Equations

finpartition.has_le = {le := λ (P Q : finpartition a), ∀ ⦃b : α⦄, b ∈ P.parts → (∃ (c : α) (H : c ∈ Q.parts), b ≤ c)}

@[protected, instance]

def finpartition.partial_order {α : Type u_1} [lattice α] [order_bot α] {a : α} :

partial_order (finpartition a)

Equations

finpartition.partial_order = {le := has_le.le finpartition.has_le, lt := preorder.lt._default has_le.le, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def finpartition.order_top {α : Type u_1} [lattice α] [order_bot α] {a : α} [decidable (a = ⊥)] :

order_top (finpartition a)

Equations

finpartition.order_top = {top := dite (a = ⊥) (λ (ha : a = ⊥), (finpartition.empty α).copy _) (λ (ha : ¬a = ⊥), finpartition.indiscrete ha), le_top := _}

theorem finpartition.parts_top_subset {α : Type u_1} [lattice α] [order_bot α] (a : α) [decidable (a = ⊥)] :

⊤.parts ⊆ {a}

theorem finpartition.parts_top_subsingleton {α : Type u_1} [lattice α] [order_bot α] (a : α) [decidable (a = ⊥)] :

↑(⊤.parts).subsingleton

@[protected, instance]

def finpartition.has_inf {α : Type u_1} [distrib_lattice α] [order_bot α] [decidable_eq α] {a : α} :

has_inf (finpartition a)

Equations

finpartition.has_inf = {inf := λ (P Q : finpartition a), finpartition.of_erase (finset.image (λ (bc : α × α), bc.fst ⊓ bc.snd) (P.parts ×ˢ Q.parts)) _ _}

@[simp]

theorem finpartition.parts_inf {α : Type u_1} [distrib_lattice α] [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} [distrib_lattice α] [order_bot α] [decidable_eq α] {a : α} :

semilattice_inf (finpartition a)

Equations

finpartition.semilattice_inf = {inf := has_inf.inf finpartition.has_inf, le := partial_order.le finpartition.partial_order, lt := partial_order.lt finpartition.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

theorem finpartition.exists_le_of_le {α : Type u_1} [distrib_lattice α] [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} [distrib_lattice α] [order_bot α] {a : α} {P Q : finpartition a} (h : P ≤ Q) :

Q.parts.card ≤ P.parts.card

@[simp]

theorem finpartition.bind_parts {α : Type u_1} [distrib_lattice α] [order_bot α] [decidable_eq α] {a : α} (P : finpartition a) (Q : Π (i : α), i ∈ P.parts → finpartition i) :

(P.bind Q).parts = P.parts.attach.bUnion (λ (i : {x // x ∈ P.parts}), (Q i.val _).parts)

def finpartition.bind {α : Type u_1} [distrib_lattice α] [order_bot α] [decidable_eq α] {a : α} (P : finpartition a) (Q : Π (i : α), i ∈ P.parts → finpartition i) :

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.bUnion (λ (i : {x // x ∈ P.parts}), (Q i.val _).parts), sup_indep := _, sup_parts := _, not_bot_mem := _}

theorem finpartition.mem_bind {α : Type u_1} [distrib_lattice α] [order_bot α] [decidable_eq α] {a b : α} {P : finpartition a} {Q : Π (i : α), i ∈ P.parts → finpartition i} :

b ∈ (P.bind Q).parts ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts

theorem finpartition.card_bind {α : Type u_1} [distrib_lattice α] [order_bot α] [decidable_eq α] {a : α} {P : finpartition a} (Q : Π (i : α), i ∈ P.parts → finpartition i) :

(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} [distrib_lattice α] [order_bot α] [decidable_eq α] {a b c : α} (P : finpartition a) (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 := has_insert.insert b P.parts, sup_indep := _, sup_parts := _, not_bot_mem := _}

@[simp]

theorem finpartition.extend_parts {α : Type u_1} [distrib_lattice α] [order_bot α] [decidable_eq α] {a b c : α} (P : finpartition a) (hb : b ≠ ⊥) (hab : disjoint a b) (hc : a ⊔ b = c) :

(P.extend hb hab hc).parts = has_insert.insert b P.parts

theorem finpartition.card_extend {α : Type u_1} [distrib_lattice α] [order_bot α] [decidable_eq α] {a : α} (P : finpartition a) (b c : α) {hb : b ≠ ⊥} {hab : disjoint a b} {hc : a ⊔ b = c} :

(P.extend hb hab hc).parts.card = P.parts.card + 1

def finpartition.avoid {α : Type u_1} [generalized_boolean_algebra α] [decidable_eq α] {a : α} (P : finpartition a) (b : α) :

finpartition (a \ b)

Restricts a finpartition to avoid a given element.

Equations

P.avoid b = finpartition.of_erase (finset.image (λ (_x : α), _x \ b) P.parts) _ _

@[simp]

theorem finpartition.avoid_parts_val {α : Type u_1} [generalized_boolean_algebra α] [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} [generalized_boolean_algebra α] [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) :

P.parts.bUnion id = 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 α) :

has_bot (finpartition s)

⊥ is the partition in singletons, aka discrete partition.

Equations

finpartition.has_bot s = {bot := {parts := finset.map {to_fun := has_singleton.singleton finset.has_singleton, inj' := _} s, sup_indep := _, sup_parts := _, not_bot_mem := _}}

@[simp]

theorem finpartition.parts_bot {α : Type u_1} [decidable_eq α] (s : finset α) :

⊥.parts = finset.map {to_fun := has_singleton.singleton finset.has_singleton, inj' := _} s

theorem finpartition.card_bot {α : Type u_1} [decidable_eq α] (s : finset α) :

⊥.parts.card = s.card

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 α) :

order_bot (finpartition s)

Equations

finpartition.order_bot s = {bot := ⊥, bot_le := _}

theorem finpartition.card_parts_le_card {α : Type u_1} [decidable_eq α] {s : finset α} (P : finpartition s) :

P.parts.card ≤ s.card

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

finpartition.atomise s F = finpartition.of_erase (finset.image (λ (Q : finset (finset α)), finset.filter (λ (i : α), ∀ (t : finset α), t ∈ F → (t ∈ Q ↔ i ∈ t)) s) F.powerset) _ _

theorem finpartition.mem_atomise {α : Type u_1} [decidable_eq α] {s t : finset α} {F : finset (finset α)} :

t ∈ (finpartition.atomise s 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) :

(finpartition.atomise s ∅).parts = {s}

theorem finpartition.card_atomise_le {α : Type u_1} [decidable_eq α] {s : finset α} {F : finset (finset α)} :

(finpartition.atomise s 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) (finpartition.atomise s 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) (finpartition.atomise s F).parts).card ≤ 2 ^ (F.card - 1)