| Description: Define the class of all
partitions, cf. the comment of df-disjs 38705.
     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 38705) is what we call
     membership partition here, cf. dfmembpart2 38771.
 
     The binary partitions relation and the partition predicate are the same,
     that is, (𝑅 Parts 𝐴 ↔ 𝑅 Part 𝐴) if 𝐴 and 𝑅 are
sets, cf.
     brpartspart 38774.  (Contributed by Peter Mazsa,
26-Jun-2021.) |