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 38766
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.)

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

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