Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-parts Structured version   Visualization version   GIF version

Definition df-parts 38747
Description: Define the class of all partitions, cf. the comment of df-disjs 38686. Partitions are disjoints on domain quotients (or: domain quotients restricted to disjoints).

This is a more general meaning of partition than we we are familiar with: the conventional meaning of partition (e.g. partition 𝐴 of 𝑋, [Halmos] p. 28: "A partition of 𝑋 is a disjoint collection 𝐴 of non-empty subsets of 𝑋 whose union is 𝑋", or Definition 35, [Suppes] p. 83., cf. https://oeis.org/A000110 38686) is what we call membership partition here, cf. dfmembpart2 38752.

The binary partitions relation and the partition predicate are the same, that is, (𝑅 Parts 𝐴𝑅 Part 𝐴) if 𝐴 and 𝑅 are sets, cf. brpartspart 38755. (Contributed by Peter Mazsa, 26-Jun-2021.)

Assertion
Ref Expression
df-parts Parts = ( DomainQss ↾ Disjs )

Detailed syntax breakdown of Definition df-parts
StepHypRef Expression
1 cparts 38200 . 2 class Parts
2 cdmqss 38185 . . 3 class DomainQss
3 cdisjs 38195 . . 3 class Disjs
42, 3cres 5691 . 2 class ( DomainQss ↾ Disjs )
51, 4wceq 1537 1 wff Parts = ( DomainQss ↾ Disjs )
Colors of variables: wff setvar class
This definition is referenced by:  brparts  38753
  Copyright terms: Public domain W3C validator