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