Partitions

A Partition of an element a in a complete lattice is an independent family of nontrivial elements whose supremum is a.

An important special case is where s : Set α, where a Partition s corresponds to a partition of the elements of s into a family of nonempty sets. This is equivalent to a transitive and symmetric binary relation r : α → α → Prop where s is the set of all x for which r x x.

Partitions are ordered by refinement: P ≤ Q if every part of P is less than or equal to a part of Q.

Main definitions

• Partition s: For [CompleteLattice α] and s : α, a Partition s is an independent collection of nontrivial elements whose supremum is s.
• Partition.removeBot: A constructor for Partition s that removes ⊥ from a set of parts.

TODO

• Link this to Finpartition.

structure Partition {α : Type u_1} [CompleteLattice α] (s : α) : Type u_1

A Partition of an element s of a CompleteLattice is a collection of independent nontrivial elements whose supremum is s.

• parts : Set α

  The collection of parts

• sSupIndep' : _root_.sSupIndep self.parts

  The parts are sSupIndep.

• bot_notMem' : ⊥ ∉ self.parts

  The bottom element is not a part.

• sSup_eq' : sSup self.parts = s

  The supremum of all parts is s.

@[implicit_reducible]

instance Partition.instSetLike {α : Type u_1} [CompleteLattice α] {s : α} : SetLike (Partition s) α

Equations

• Partition.instSetLike = { coe := Partition.parts, coe_injective' := ⋯ }

def Partition.Simps.coe {α : Type u_1} [CompleteLattice α] {s : α} (P : Partition s) : Set α

See Note [custom simps projection].

Equations

• Partition.Simps.coe P = ↑P

@[simp]

theorem Partition.coe_parts {α : Type u_1} {s : α} [CompleteLattice α] {P : Partition s} : P.parts = ↑P

theorem Partition.ext {α : Type u_1} {s : α} [CompleteLattice α] {P Q : Partition s} (hP : ∀ (x : α), x ∈ P ↔ x ∈ Q) : P = Q

theorem Partition.ext_iff {α : Type u_1} {s : α} [CompleteLattice α] {P Q : Partition s} : P = Q ↔ ∀ (x : α), x ∈ P ↔ x ∈ Q

@[simp]

theorem Partition.sSupIndep {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : _root_.sSupIndep ↑P

theorem Partition.disjoint {α : Type u_1} {s x y : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) (hy : y ∈ P) (hxy : x ≠ y) : Disjoint x y

theorem Partition.pairwiseDisjoint {α : Type u_1} {s : α} [CompleteLattice α] {P : Partition s} : (↑P).PairwiseDisjoint id

theorem Partition.eq_or_disjoint {α : Type u_1} {s x y : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) (hy : y ∈ P) : x = y ∨ Disjoint x y

theorem Partition.eq_of_not_disjoint {α : Type u_1} {s x y : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) (hy : y ∈ P) (hxy : ¬Disjoint x y) : x = y

@[simp]

theorem Partition.sSup_eq {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : sSup ↑P = s

@[simp]

theorem Partition.iSup_eq {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : ⨆ x ∈ P, x = s

theorem Partition.le_of_mem {α : Type u_1} {s x : α} [CompleteLattice α] (P : Partition s) (hx : x ∈ P) : x ≤ s

theorem Partition.parts_nonempty {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) (hs : s ≠ ⊥) : (↑P).Nonempty

@[simp]

theorem Partition.bot_notMem {α : Type u_1} {s : α} [CompleteLattice α] (P : Partition s) : ⊥ ∉ P

theorem Partition.ne_bot_of_mem {α : Type u_1} {s x : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) : x ≠ ⊥

theorem Partition.bot_lt_of_mem {α : Type u_1} {s x : α} [CompleteLattice α] {P : Partition s} (hx : x ∈ P) : ⊥ < x

def Partition.copy {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) : Partition t

Convert a Partition s into a Partition t via an equality s = t.

Equations

• P.copy hst = { parts := ↑P, sSupIndep' := ⋯, bot_notMem' := ⋯, sSup_eq' := ⋯ }

@[simp]

theorem Partition.coe_copy {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) : ↑(P.copy hst) = ↑P

@[simp]

theorem Partition.mem_copy_iff {α : Type u_1} {s t x : α} [CompleteLattice α] {P : Partition s} (hst : s = t) : x ∈ P.copy hst ↔ x ∈ P

def Partition.partscopyEquiv {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) : ↥(P.copy hst) ≃ ↥P

The natural equivalence between the subtype of parts and the subtype of parts of a copy.

Equations

• P.partscopyEquiv hst = Equiv.setCongr ⋯

@[simp]

theorem Partition.partscopyEquiv_symm_apply_coe {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) (b : { b : α // (fun (x : α) => x ∈ ↑P) b }) : ↑((P.partscopyEquiv hst).symm b) = ↑b

@[simp]

theorem Partition.partscopyEquiv_apply_coe {α : Type u_1} {s t : α} [CompleteLattice α] (P : Partition s) (hst : s = t) (a : { a : α // (fun (x : α) => x ∈ ↑(P.copy hst)) a }) : ↑((P.partscopyEquiv hst) a) = ↑a

def Partition.removeBot {α : Type u_1} {s : α} [CompleteLattice α] (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : Partition s

A constructor for Partition s that removes ⊥ from the set of parts.

Equations

• Partition.removeBot P indep sSup_eq = { parts := P \ {⊥}, sSupIndep' := ⋯, bot_notMem' := ⋯, sSup_eq' := ⋯ }

@[simp]

theorem Partition.coe_removeBot {α : Type u_1} {s : α} [CompleteLattice α] (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : ↑(removeBot P indep sSup_eq) = P \ {⊥}

@[simp]

theorem Partition.mem_removeBot {α : Type u_1} {s x : α} [CompleteLattice α] (P : Set α) (indep : _root_.sSupIndep P) (sSup_eq : sSup P = s) : x ∈ removeBot P indep sSup_eq ↔ x ∈ P ∧ x ≠ ⊥

@[simp]

theorem Partition.notMem_of_bot {α : Type u_1} [CompleteLattice α] (P : Partition ⊥) (x : α) : x ∉ P

@[implicit_reducible]

instance Partition.instUniqueBot {α : Type u_1} [CompleteLattice α] : Unique (Partition ⊥)

There is a unique partition of ⊥.

Equations

• Partition.instUniqueBot = { default := Partition.removeBot ∅ ⋯ ⋯, uniq := ⋯ }

theorem Partition.ne_bot_of_mem' {α : Type u_1} {s x : α} [CompleteLattice α] {P : Partition s} (hxP : x ∈ P) : s ≠ ⊥

@[implicit_reducible]

instance Partition.instPartialOrder {α : Type u_1} {s : α} [CompleteLattice α] : PartialOrder (Partition s)

Partitions on s are ordered by refinement: P ≤ Q if every part of P is contained in a part of Q.

Equations

• Partition.instPartialOrder = { le := fun (P Q : Partition s) => ∀ ⦃x : α⦄, x ∈ P → ∃ y ∈ Q, x ≤ y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Partition.le_def {α : Type u_1} {s : α} [CompleteLattice α] {P Q : Partition s} : P ≤ Q ↔ ∀ x ∈ P, ∃ y ∈ Q, x ≤ y

theorem Partition.exists_le_of_mem_le {α : Type u_1} {s x : α} [CompleteLattice α] {P Q : Partition s} (h : P ≤ Q) (hx : x ∈ P) : ∃ y ∈ Q, x ≤ y

theorem Partition.existsUnique_of_mem_le {α : Type u_1} {s x : α} [CompleteLattice α] {P Q : Partition s} (h : P ≤ Q) (hx : x ∈ P) : ∃! y : α, y ∈ Q ∧ x ≤ y

@[implicit_reducible]

instance Partition.instOrderTop {α : Type u_1} {s : α} [CompleteLattice α] : OrderTop (Partition s)

The top partition of s is the partition with the single part s.

Equations

• Partition.instOrderTop = { top := Partition.removeBot {s} ⋯ ⋯, le_top := ⋯ }

theorem Partition.top_def {α : Type u_1} {s : α} [CompleteLattice α] : ⊤ = removeBot {s} ⋯ ⋯

@[simp]

theorem Partition.parts_top {α : Type u_1} {s : α} [CompleteLattice α] (hs : s ≠ ⊥) : ↑⊤ = {s}

@[simp]

theorem Partition.mem_top_iff {α : Type u_1} {s : α} [CompleteLattice α] {a : α} : a ∈ ⊤ ↔ a = s ∧ a ≠ ⊥

theorem Partition.parts_top_subset {α : Type u_1} {s : α} [CompleteLattice α] : ↑⊤ ⊆ {s}