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.

Main definitions

• For [CompleteLattice α] and s : α, a Set.Partition s is an independent collection of nontrivial elements whose supremum is s.

TODO

• Link this to Finpartition.
• Give API lemmas for the specialization to the Set case.

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' := ⋯ }

@[implicit_reducible]

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

Equations

• Partition.instPartialOrder = PartialOrder.ofSetLike (Partition s) α

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

@[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 : α} [CompleteLattice α] {t : α} (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 : α} [CompleteLattice α] {t : α} (P : Partition s) (hst : s = t) : ↑(P.copy hst) = ↑P

@[simp]

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

def Partition.partscopyEquiv {α : Type u_1} {s : α} [CompleteLattice α] {t : α} (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_apply_coe {α : Type u_1} {s : α} [CompleteLattice α] {t : α} (P : Partition s) (hst : s = t) (a : { a : α // (fun (x : α) => x ∈ ↑(P.copy hst)) a }) : ↑((P.partscopyEquiv hst) a) = ↑a

@[simp]

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

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 \ {⊥}