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.toSubtype: Turns a finpartition of a type to one of a subtype.
• Finpartition.bind: Puts together the finpartitions of the parts of a finpartition into a new finpartition.
• Finpartition.extend: Extends a finpartition of a to a finpartition of a ⊔ b by adding b as a new part.
• Finpartition.extendOfLE: Extends a finpartition of a to a finpartition of b when a ≤ b, by adding b \ a as a new part (if nonempty).
• Finpartition.restrict: Restricts a finpartition of a to b where b ≤ a by intersecting each part with b.
• Finpartition.ofPairwiseDisjoint: Builds a finpartition from a finset parts of pairwise disjoint elements.
• Finpartition.combine: Combines a family of partitions of pairwise disjoint elements into a partition of their sup.
• Finpartition.ofExistsUnique: Builds a finpartition from a collection of parts such that each element is in exactly one part.
• 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?

The specialisation to Finset α could be generalised to atomistic orders.

structure Finpartition {α : Type u_1} [Lattice α] [OrderBot α] (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 : Finset α

  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

• bot_notMem : ⊥ ∉ self.parts

  No element of the partition is bottom

theorem Finpartition.ext_iff {α : Type u_1} {inst✝ : Lattice α} {inst✝¹ : OrderBot α} {a : α} {x y : Finpartition a} : x = y ↔ x.parts = y.parts

theorem Finpartition.ext {α : Type u_1} {inst✝ : Lattice α} {inst✝¹ : OrderBot α} {a : α} {x y : Finpartition a} (parts : x.parts = y.parts) : x = y

def instDecidableEqFinpartition.decEq {α✝ : Type u_2} {inst✝ : Lattice α✝} {inst✝¹ : OrderBot α✝} {a✝ : α✝} [DecidableEq α✝] (x✝ x✝¹ : Finpartition a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instDecidableEqFinpartition {α✝ : Type u_2} {inst✝ : Lattice α✝} {inst✝¹ : OrderBot α✝} {a✝ : α✝} [DecidableEq α✝] : DecidableEq (Finpartition a✝)

Equations

• instDecidableEqFinpartition = instDecidableEqFinpartition.decEq

def Finpartition.ofErase {α : Type u_1} [Lattice α] [OrderBot α] [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a) : Finpartition 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 := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.ofErase_parts {α : Type u_1} [Lattice α] [OrderBot α] [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a) : (ofErase parts sup_indep sup_parts).parts = parts.erase ⊥

def Finpartition.ofSubset {α : Type u_1} [Lattice α] [OrderBot α] {a b : α} (P : Finpartition a) {parts : Finset α} (subset : parts ⊆ P.parts) (sup_parts : parts.sup id = b) : Finpartition b

A Finpartition constructor from a bigger existing finpartition.

Equations

• P.ofSubset subset sup_parts = { parts := parts, supIndep := ⋯, sup_parts := sup_parts, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.ofSubset_parts {α : Type u_1} [Lattice α] [OrderBot α] {a b : α} (P : Finpartition a) {parts : Finset α} (subset : parts ⊆ P.parts) (sup_parts : parts.sup id = b) : (P.ofSubset subset sup_parts).parts = parts

theorem Finpartition.sum_ofSubset_eq_sum {α : Type u_1} [Lattice α] [OrderBot α] {a b : α} (P : Finpartition a) {parts : Finset α} (subset : parts ⊆ P.parts) (sup_parts : parts.sup id = b) {X : Type u_2} [AddCommMonoid X] (f : α → X) (hf : ∀ p ∈ P.parts, p ∉ parts → f p = 0) : ∑ p ∈ (P.ofSubset subset sup_parts).parts, f p = ∑ p ∈ P.parts, f p

def Finpartition.copy {α : Type u_1} [Lattice α] [OrderBot α] {a b : α} (P : Finpartition a) (h : a = b) : Finpartition b

Changes the type of a finpartition to an equal one.

Equations

• P.copy h = { parts := P.parts, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.copy_parts {α : Type u_1} [Lattice α] [OrderBot α] {a b : α} (P : Finpartition a) (h : a = b) : (P.copy h).parts = P.parts

def Finpartition.map {α : Type u_1} [Lattice α] [OrderBot α] {β : Type u_2} [Lattice β] [OrderBot β] {a : α} (e : α ≃o β) (P : Finpartition a) : Finpartition (e a)

Transfer a finpartition over an order isomorphism.

Equations

• Finpartition.map e P = { parts := Finset.map (↑e).toEmbedding P.parts, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.parts_map {α : Type u_1} [Lattice α] [OrderBot α] {β : Type u_2} [Lattice β] [OrderBot β] {a : α} {e : α ≃o β} {P : Finpartition a} : (map e P).parts = Finset.map (↑e).toEmbedding P.parts

def Finpartition.empty (α : Type u_1) [Lattice α] [OrderBot α] : Finpartition ⊥

The empty finpartition.

Equations

• Finpartition.empty α = { parts := ∅, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.empty_parts (α : Type u_1) [Lattice α] [OrderBot α] : (Finpartition.empty α).parts = ∅

@[instance_reducible]

instance Finpartition.instInhabitedBot (α : Type u_1) [Lattice α] [OrderBot α] : Inhabited (Finpartition ⊥)

Equations

• Finpartition.instInhabitedBot α = { default := Finpartition.empty α }

@[simp]

theorem Finpartition.default_eq_empty (α : Type u_1) [Lattice α] [OrderBot α] : default = Finpartition.empty α

def Finpartition.indiscrete {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (ha : a ≠ ⊥) : Finpartition a

The finpartition in one part, aka indiscrete finpartition.

Equations

• Finpartition.indiscrete ha = { parts := {a}, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.indiscrete_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (ha : a ≠ ⊥) : (indiscrete ha).parts = {a}

theorem Finpartition.le {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {b : α} (hb : b ∈ P.parts) : b ≤ a

theorem Finpartition.ne_bot {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {b : α} (hb : b ∈ P.parts) : b ≠ ⊥

theorem Finpartition.disjoint {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) : (↑P.parts).PairwiseDisjoint id

theorem Finpartition.sup_parts_apply {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {β : Type u_2} {f : α → β} [SemilatticeSup β] [OrderBot β] (hf : ∀ (x y : α), f (x ⊔ y) = f x ⊔ f y) (hbot : f ⊥ = ⊥) : P.parts.sup f = f a

The sup of a sup-bot-preserving map f over the parts of a Finpartition equals f a.

theorem Finpartition.pairwiseDisjoint_apply {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {β : Type u_2} {f : α → β} [SemilatticeInf β] [OrderBot β] (hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) (hbot : f ⊥ = ⊥) : (↑P.parts).PairwiseDisjoint f

Parts of a Finpartition are pairwise disjoint under an inf-bot-preserving map.

@[simp]

theorem Finpartition.parts_eq_empty_iff {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} : P.parts = ∅ ↔ a = ⊥

@[simp]

theorem Finpartition.parts_nonempty_iff {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} : P.parts.Nonempty ↔ a ≠ ⊥

theorem Finpartition.parts_nonempty {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) (ha : a ≠ ⊥) : P.parts.Nonempty

@[instance_reducible]

instance Finpartition.instUniqueBot {α : Type u_1} [Lattice α] [OrderBot α] : Unique (Finpartition ⊥)

Equations

• Finpartition.instUniqueBot = { toInhabited := inferInstance, uniq := ⋯ }

instance Finpartition.instNonempty {α : Type u_1} [Lattice α] [OrderBot α] {a : α} : Nonempty (Finpartition a)

@[reducible, inline]

abbrev IsAtom.uniqueFinpartition {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} (ha : IsAtom a) : Unique (Finpartition a)

There's a unique partition of an atom.

Equations

• ha.uniqueFinpartition = { default := Finpartition.indiscrete ⋯, uniq := ⋯ }

@[instance_reducible]

instance Finpartition.instFintypeOfDecidableEq {α : Type u_1} [Lattice α] [OrderBot α] [Fintype α] [DecidableEq α] (a : α) : Fintype (Finpartition a)

Equations

• One or more equations did not get rendered due to their size.

Refinement order

@[instance_reducible]

instance Finpartition.instLE {α : Type u_1} [Lattice α] [OrderBot α] {a : α} : 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.instLE = { le := fun (P Q : Finpartition a) => ∀ ⦃b : α⦄, b ∈ P.parts → ∃ c ∈ Q.parts, b ≤ c }

@[instance_reducible]

instance Finpartition.instPartialOrder {α : Type u_1} [Lattice α] [OrderBot α] {a : α} : PartialOrder (Finpartition a)

Equations

• Finpartition.instPartialOrder = { toLE := inferInstance, lt := fun (a_1 b : Finpartition a) => a_1 ≤ b ∧ ¬b ≤ a_1, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[instance_reducible]

instance Finpartition.instOrderTopOfDecidableEqBot {α : Type u_1} [Lattice α] [OrderBot α] {a : α} [Decidable (a = ⊥)] : OrderTop (Finpartition a)

Equations

• Finpartition.instOrderTopOfDecidableEqBot = { top := if ha : a = ⊥ then (Finpartition.empty α).copy ⋯ else Finpartition.indiscrete ha, le_top := ⋯ }

theorem Finpartition.parts_top_subset {α : Type u_1} [Lattice α] [OrderBot α] (a : α) [Decidable (a = ⊥)] : ⊤.parts ⊆ {a}

theorem Finpartition.parts_top_subsingleton {α : Type u_1} [Lattice α] [OrderBot α] (a : α) [Decidable (a = ⊥)] : (↑⊤.parts).Subsingleton

@[instance_reducible]

instance Finpartition.instFintypeFinset {α : Type u_1} [DecidableEq α] {s : Finset α} : Fintype (Finpartition s)

Equations

• One or more equations did not get rendered due to their size.

theorem Finpartition.exists_le_of_le {α : Type u_1} [Lattice α] [OrderBot α] {a b : α} {P Q : Finpartition a} (h : P ≤ Q) (hb : b ∈ Q.parts) : ∃ c ∈ P.parts, c ≤ b

theorem Finpartition.card_mono {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P Q : Finpartition a} (h : P ≤ Q) : Q.parts.card ≤ P.parts.card

noncomputable def Finpartition.toSubtype {α : Type u_1} [Lattice α] [OrderBot α] {s : α} (P : Finpartition s) {Pr : α → Prop} (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)) (Prbot : Pr ⊥) (hs : Pr s) (hP : ∀ p ∈ P.parts, Pr p) : Finpartition ⟨s, hs⟩

A Finpartition constructor in Subtype Pr for Pr : Set X → Prop such that Pr is closed under intersection and union and Pr ⊥ holds from a P : Finpartition s with explicit assumptions that Pr s and Pr p for each part p.

Equations

• P.toSubtype Prsup Prinf Prbot hs hP = { parts := P.parts.preimage Subtype.val ⋯, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.mem_toSubtype_iff {α : Type u_1} [Lattice α] [OrderBot α] {s : α} (P : Finpartition s) {Pr : α → Prop} (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)) (Prbot : Pr ⊥) (hs : Pr s) (hP : ∀ p ∈ P.parts, Pr p) (p : Subtype Pr) : p ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts ↔ ↑p ∈ P.parts

theorem Finpartition.sum_eq_sum_finpartition_subtype {α : Type u_1} [Lattice α] [OrderBot α] {s : α} (P : Finpartition s) {Pr : α → Prop} (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)) (Prbot : Pr ⊥) (hs : Pr s) (hP : ∀ p ∈ P.parts, Pr p) {X : Type u_2} [AddCommMonoid X] (f : α → X) : ∑ p ∈ P.parts, f p = ∑ p ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts, f ↑p

@[instance_reducible]

instance Finpartition.instMin {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} : Min (Finpartition a)

Equations

• Finpartition.instMin = { min := fun (P Q : Finpartition a) => Finpartition.ofErase (Finset.image (fun (bc : α × α) => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) ⋯ ⋯ }

@[simp]

theorem Finpartition.parts_inf {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P Q : Finpartition a) : (P ⊓ Q).parts = (Finset.image (fun (bc : α × α) => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).erase ⊥

@[instance_reducible]

instance Finpartition.instSemilatticeInf {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} : SemilatticeInf (Finpartition a)

Equations

• Finpartition.instSemilatticeInf = { toPartialOrder := Finpartition.instPartialOrder, inf := min, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

def Finpartition.restrict {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a b : α} (P : Finpartition a) (hb : b ≤ a) : Finpartition b

Restrict a partition of a to b where b ≤ a by intersecting each part with b.

Equations

• P.restrict hb = { parts := (Finset.image (fun (x : α) => x ⊓ b) P.parts).erase ⊥, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

theorem Finpartition.sum_restrict {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a b : α} (P : Finpartition a) (hb : b ≤ a) {M : Type u_2} [AddCommMonoid M] (f : α → M) (hf : f ⊥ = 0) : ∑ p ∈ (P.restrict hb).parts, f p = ∑ q ∈ P.parts, f (q ⊓ b)

The sum of a set-valued function over restricted partition parts equals the sum over original parts with f (· ⊓ b), provided f ⊥ = 0 (so bottom terms don't contribute).

def Finpartition.ofPairwiseDisjoint {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] (parts : Finset α) (hdisjoint : (↑parts).PairwiseDisjoint id) : Finpartition (parts.sup id)

A Finpartition constructor of parts.sup id from a finset parts of pairwise disjoint elements. Any ⊥ elements in parts are erased.

Equations

• Finpartition.ofPairwiseDisjoint parts hdisjoint = { parts := parts.erase ⊥, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.ofPairwiseDisjoint_parts {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] (parts : Finset α) (hdisjoint : (↑parts).PairwiseDisjoint id) : (ofPairwiseDisjoint parts hdisjoint).parts = parts.erase ⊥

theorem Finpartition.sum_ofPairwiseDisjoint_eq_sum {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {parts : Finset α} (hdisjoint : (↑parts).PairwiseDisjoint id) {X : Type u_2} [AddCommMonoid X] {f : α → X} (hf : f ⊥ = 0) : ∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p = ∑ p ∈ parts, f p

def Finpartition.combine {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {ι : Type u_2} {I : Finset ι} {a : ι → α} (P : (i : ι) → Finpartition (a i)) (ha : I.SupIndep a) : Finpartition (I.sup a)

Combine a family of partitions of pairwise disjoint elements into a partition of their sup.

Equations

• Finpartition.combine P ha = { parts := I.biUnion fun (i : ι) => (P i).parts, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.combine_parts {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {ι : Type u_2} {I : Finset ι} {a : ι → α} (P : (i : ι) → Finpartition (a i)) (ha : I.SupIndep a) : (combine P ha).parts = I.biUnion fun (i : ι) => (P i).parts

theorem Finpartition.sum_combine {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {ι : Type u_2} {I : Finset ι} {s : ι → α} (P : (i : ι) → Finpartition (s i)) (ha : I.SupIndep s) {M : Type u_3} [AddCommMonoid M] (f : α → M) : ∑ p ∈ (combine P ha).parts, f p = ∑ i ∈ I, ∑ p ∈ (P i).parts, f p

The sum of a set-valued function over a combined partition equals the sum of sums over component partitions.

def Finpartition.bind {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : (i : α) → i ∈ P.parts → Finpartition i) : Finpartition a

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 = (Finpartition.combine (fun (i : ↥P.parts) => Q ↑i ⋯) ⋯).copy ⋯

@[simp]

theorem Finpartition.bind_parts {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : (i : α) → i ∈ P.parts → Finpartition i) : (P.bind Q).parts = P.parts.attach.biUnion fun (i : ↥P.parts) => (Q ↑i ⋯).parts

theorem Finpartition.mem_bind {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {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} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {a : α} {P : Finpartition a} (Q : (i : α) → i ∈ P.parts → Finpartition i) : (P.bind Q).parts.card = ∑ A ∈ P.parts.attach, (Q ↑A ⋯).parts.card

def Finpartition.extend {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {a b c : α} (P : Finpartition a) (hb : b ≠ ⊥) (hab : Disjoint a b) (hc : a ⊔ b = c) : Finpartition 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 := ⋯, bot_notMem := ⋯ }

@[simp]

theorem Finpartition.extend_parts {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {a b c : α} (P : Finpartition a) (hb : b ≠ ⊥) (hab : Disjoint a b) (hc : a ⊔ b = c) : (P.extend hb hab hc).parts = insert b P.parts

theorem Finpartition.card_extend {α : Type u_1} [Lattice α] [OrderBot α] [IsModularLattice α] [DecidableEq α] {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} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) : Finpartition (a \ b)

Restricts a finpartition to avoid a given element.

Equations

• P.avoid b = Finpartition.ofErase (Finset.image (fun (x : α) => x \ b) P.parts) ⋯ ⋯

@[simp]

theorem Finpartition.avoid_parts_val {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) : (P.avoid b).parts.val = (Multiset.map (fun (x : α) => x \ b) P.parts.val).dedup.erase ⊥

@[simp]

theorem Finpartition.mem_avoid {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a b c : α} (P : Finpartition a) : c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

def Finpartition.extendOfLE {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a b : α} (P : Finpartition a) (hab : a ≤ b) : Finpartition b

Extend a partition of a to a partition of b when a ≤ b, by adding b \ a as a part.

Equations

• P.extendOfLE hab = if hr : b \ a = ⊥ then ⋯ ▸ P else P.extend hr ⋯ ⋯

theorem Finpartition.parts_extendOfLE_of_eq {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a b : α} (P : Finpartition a) (hab : a = b) : (P.extendOfLE ⋯).parts = P.parts

theorem Finpartition.parts_extendOfLE_of_lt {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a b : α} (P : Finpartition a) (hab : a < b) : (P.extendOfLE ⋯).parts = insert (b \ a) P.parts

theorem Finpartition.parts_subset_extendOfLE {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a b : α} (P : Finpartition a) (hab : a ≤ b) : P.parts ⊆ (P.extendOfLE hab).parts

theorem Finpartition.mem_parts_or_eq_sdiff_of_mem_extendOfLE {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a b : α} (P : Finpartition a) (hab : a ≤ b) {p : α} (hp : p ∈ (P.extendOfLE hab).parts) : p ∈ P.parts ∨ p = b \ a

Finite partitions of finsets

theorem Finpartition.subset {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : Finset α} (ha : a ∈ P.parts) : a ⊆ s

theorem Finpartition.nonempty_of_mem_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : Finset α} (ha : a ∈ P.parts) : a.Nonempty

@[simp]

theorem Finpartition.empty_notMem_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ∅ ∉ P.parts

theorem Finpartition.ne_empty {α : Type u_1} [DecidableEq α] {s t : Finset α} (P : Finpartition s) (h : t ∈ P.parts) : t ≠ ∅

theorem Finpartition.eq_of_mem_parts {α : Type u_1} [DecidableEq α] {s t u : Finset α} (P : Finpartition s) {a : α} (ht : t ∈ P.parts) (hu : u ∈ P.parts) (hat : a ∈ t) (hau : a ∈ u) : t = u

theorem Finpartition.exists_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a ∈ s) : ∃ t ∈ P.parts, a ∈ t

theorem Finpartition.biUnion_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : P.parts.biUnion id = s

theorem Finpartition.existsUnique_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a ∈ s) : ∃! t : Finset α, t ∈ P.parts ∧ a ∈ t

def Finpartition.ofExistsUnique {α : Type u_1} [DecidableEq α] {s : Finset α} (parts : Finset (Finset α)) (h : ∀ p ∈ parts, p ⊆ s) (h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t) (h'' : ∅ ∉ parts) : Finpartition s

Construct a Finpartition s from a finset of finsets parts such that each element of s is in exactly one member of parts. This provides a converse to Finpartition.subset, Finpartition.not_empty_mem_parts and Finpartition.existsUnique_mem.

Equations

• Finpartition.ofExistsUnique parts h h' h'' = { parts := parts, supIndep := ⋯, sup_parts := ⋯, bot_notMem := h'' }

@[simp]

theorem Finpartition.ofExistsUnique_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (parts : Finset (Finset α)) (h : ∀ p ∈ parts, p ⊆ s) (h' : ∀ a ∈ s, ∃! t : Finset α, t ∈ parts ∧ a ∈ t) (h'' : ∅ ∉ parts) : (ofExistsUnique parts h h' h'').parts = parts

def Finpartition.part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) (a : α) : Finset α

The part of the finpartition that a lies in.

Equations

• P.part a = if ha : a ∈ s then Finset.choose (fun (a_1 : Finset α) => a ∈ a_1) P.parts ⋯ else ∅

@[simp]

theorem Finpartition.part_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} : P.part a ∈ P.parts ↔ a ∈ s

@[simp]

theorem Finpartition.part_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} : P.part a = ∅ ↔ a ∉ s

@[simp]

theorem Finpartition.part_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} : (P.part a).Nonempty ↔ a ∈ s

@[simp]

theorem Finpartition.part_subset {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) (a : α) : P.part a ⊆ s

@[simp]

theorem Finpartition.mem_part_self {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} : a ∈ P.part a ↔ a ∈ s

theorem Finpartition.mem_part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} : a ∈ s → a ∈ P.part a

Alias of the reverse direction of Finpartition.mem_part_self.

theorem Finpartition.part_eq_iff_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} (P : Finpartition s) {a : α} (ht : t ∈ P.parts) : P.part a = t ↔ a ∈ t

theorem Finpartition.part_eq_of_mem {α : Type u_1} [DecidableEq α] {s t : Finset α} (P : Finpartition s) {a : α} (ht : t ∈ P.parts) (hat : a ∈ t) : P.part a = t

theorem Finpartition.mem_part_iff_part_eq_part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {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} [DecidableEq α] {s : Finset α} (P : Finpartition s) : Set.SurjOn P.part ↑s ↑P.parts

theorem Finpartition.exists_subset_part_bijOn {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

theorem Finpartition.mem_part_iff_exists {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a b : α} : a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p

def Finpartition.equivSigmaParts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ↥s ≃ (t : ↥P.parts) × ↥↑t

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

Equations

• P.equivSigmaParts = { toFun := fun (x : ↥s) => ⟨⟨P.part ↑x, ⋯⟩, ⟨↑x, ⋯⟩⟩, invFun := fun (x : (t : ↥P.parts) × ↥↑t) => ⟨↑x.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Finpartition.exists_enumeration {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ∃ (f : ↥s ≃ (t : ↥P.parts) × Fin (↑t).card), ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst

theorem Finpartition.sum_card_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ∑ i ∈ P.parts, i.card = s.card

@[instance_reducible]

instance Finpartition.instBotFinset {α : Type u_1} [DecidableEq α] (s : Finset α) : Bot (Finpartition s)

⊥ is the partition in singletons, aka discrete partition.

Equations

• Finpartition.instBotFinset s = { bot := { parts := Finset.map { toFun := singleton, inj' := ⋯ } s, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ } }

@[simp]

theorem Finpartition.parts_bot {α : Type u_1} [DecidableEq α] (s : Finset α) : ⊥.parts = Finset.map { toFun := singleton, inj' := ⋯ } s

theorem Finpartition.card_bot {α : Type u_1} [DecidableEq α] (s : Finset α) : ⊥.parts.card = s.card

theorem Finpartition.mem_bot_iff {α : Type u_1} [DecidableEq α] {s t : Finset α} : t ∈ ⊥.parts ↔ ∃ a ∈ s, {a} = t

@[instance_reducible]

instance Finpartition.instOrderBotFinset {α : Type u_1} [DecidableEq α] (s : Finset α) : OrderBot (Finpartition s)

Equations

• Finpartition.instOrderBotFinset s = { toBot := inferInstance, bot_le := ⋯ }

theorem Finpartition.card_parts_le_card {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : P.parts.card ≤ s.card

theorem Finpartition.card_mod_card_parts_le {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : s.card % P.parts.card ≤ P.parts.card

def Finpartition.ofSetSetoid {α : Type u_1} [DecidableEq α] (s : Setoid α) (x : Finset α) [DecidableRel ⇑s] : Finpartition x

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

Equations

• Finpartition.ofSetSetoid s x = { parts := Finset.image (fun (a : α) => {b ∈ x | s a b}) x, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }

theorem Finpartition.ofSetSetoid_parts {α : Type u_1} [DecidableEq α] (s : Setoid α) (x : Finset α) [DecidableRel ⇑s] : (ofSetSetoid s x).parts = Finset.image (fun (a : α) => {b ∈ x | s a b}) x

theorem Finpartition.mem_part_ofSetSetoid_iff_rel {α : Type u_1} [DecidableEq α] {a : α} {s : Setoid α} (x : Finset α) [DecidableRel ⇑s] {b : α} : b ∈ (ofSetSetoid s x).part a ↔ a ∈ x ∧ b ∈ x ∧ s a b

def Finpartition.ofSetoid {α : Type u_1} [DecidableEq α] [Fintype α] (s : Setoid α) [DecidableRel ⇑s] : 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

• Finpartition.ofSetoid s = Finpartition.ofSetSetoid s Finset.univ

theorem Finpartition.ofSetoid_parts_val {α : Type u_1} [DecidableEq α] [Fintype α] (s : Setoid α) [DecidableRel ⇑s] : (ofSetoid s).parts.val = (Multiset.map (fun (a : α) => {b : α | s a b}) Finset.univ.val).dedup

theorem Finpartition.mem_part_ofSetoid_iff_rel {α : Type u_1} [DecidableEq α] {a : α} [Fintype α] {s : Setoid α} [DecidableRel ⇑s] {b : α} : b ∈ (ofSetoid s).part a ↔ s a b

def Finpartition.atomise {α : Type u_1} [DecidableEq α] (s : Finset α) (F : Finset (Finset α)) : Finpartition s

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.ofErase (Finset.image (fun (Q : Finset (Finset α)) => {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) ⋯ ⋯

theorem Finpartition.mem_atomise {α : Type u_1} [DecidableEq α] {s t : Finset α} {F : Finset (Finset α)} : t ∈ (atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = t

theorem Finpartition.atomise_empty {α : Type u_1} [DecidableEq α] {s : Finset α} (hs : s.Nonempty) : (atomise s ∅).parts = {s}

theorem Finpartition.card_atomise_le {α : Type u_1} [DecidableEq α] {s : Finset α} {F : Finset (Finset α)} : (atomise s F).parts.card ≤ 2 ^ F.card

theorem Finpartition.biUnion_filter_atomise {α : Type u_1} [DecidableEq α] {s t : Finset α} {F : Finset (Finset α)} (ht : t ∈ F) (hts : t ⊆ s) : {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}.biUnion id = t

theorem Finpartition.card_filter_atomise_le_two_pow {α : Type u_1} [DecidableEq α] {s t : Finset α} {F : Finset (Finset α)} (ht : t ∈ F) : {u ∈ (atomise s F).parts | u ⊆ t ∧ u.Nonempty}.card ≤ 2 ^ (F.card - 1)