blob: b9fe8dc31a60218309415e5cae81492c4de945ae (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
\import{set.tex}
\subsection{Partitions}
\begin{definition}\label{partition}
$P$ is a partition iff
$\emptyset\notin P$ and
for all $B, C\in P$ such that $B\neq C$ we have $B$ is disjoint from $C$.
\end{definition}
\begin{abbreviation}\label{partition_of}
$P$ is a partition of $A$ iff
$P$ is a partition and
$\unions{P} = A$.
\end{abbreviation}
\begin{proposition}\label{partition_emptyset}
$\emptyset$ is a partition of $\emptyset$.
\end{proposition}
\begin{proof}
Follows by \cref{emptyset,partition,setext,unions_iff}.
\end{proof}
\begin{definition}\label{partition_refinement}
$P'$ is a refinement of $P$ iff
for every $A'\in P'$ there exists
$A\in P$ such that $A'\subseteq A$.
\end{definition}
\begin{abbreviation}\label{partition_refines}
$P'\refines P$ iff
$P'$ is a refinement of $P$.
\end{abbreviation}
\begin{proposition}\label{partition_refinement_transitive}
Suppose $P''\refines P'\refines P$.
Then $P''\refines P$.
\end{proposition}
\begin{proof}
Follows by \cref{partition_refinement,subset_transitive}.
\end{proof}
%\begin{definition}\label{set_of_representatives}
% $X$ is a set of representatives for $P$ iff
% for all $A\in P$ there exists $a\in A$ such that
% $X\inter A = \{a\}$.
%\end{definition}
|
