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