theory Partitions_ZF imports Finite_ZF FiniteSeq_ZF
begin
It is a common trick in proofs that we divide a set into non-overlapping subsets. The first case is when we split the set into two nonempty disjoint sets. Here this is modeled as an ordered pair of sets and the set of such divisions of set \(X\) is called \( \text{Bisections}(X) \). The second variation on this theme is a set-valued function (aren't they all in ZF?) whose values are nonempty and mutually disjoint.
Bisections
This section is about dividing sets into two non-overlapping subsets.
The set of bisections of a given set \(A\) is a set of pairs of nonempty subsets of \(A\) that do not overlap and their union is equal to \(A\).
definition
\( \text{Bisections}(X) = \{p \in Pow(X)\times Pow(X).\ \) \( \text{fst}(p)\neq 0 \wedge \text{snd}(p)\neq 0 \wedge \text{fst}(p)\cap \text{snd}(p) = 0 \wedge \text{fst}(p)\cup \text{snd}(p) = X\} \)
Properties of bisections.
lemma bisec_props:
assumes \( \langle A,B\rangle \in \text{Bisections}(X) \)
shows \( A\neq 0 \), \( B\neq 0 \), \( A \subseteq X \), \( B \subseteq X \), \( A \cap B = 0 \), \( A \cup B = X \), \( X \neq 0 \) using assms, Bisections_defKind of inverse of bisec_props: a pair of nonempty disjoint sets form a bisection of their union.
lemma is_bisec:
assumes \( A\neq 0 \), \( B\neq 0 \), \( A \cap B = 0 \)
shows \( \langle A,B\rangle \in \text{Bisections}(A\cup B) \) using assms, Bisections_defBisection of \(X\) is a pair of subsets of \(X\).
lemma bisec_is_pair:
assumes \( Q \in \text{Bisections}(X) \)
shows \( Q = \langle \text{fst}(Q), \text{snd}(Q)\rangle \) using assms, Bisections_defThe set of bisections of the empty set is empty.
lemma bisec_empty:
shows \( \text{Bisections}(0) = 0 \) using Bisections_defThe next lemma shows what can we say about bisections of a set with another element added.
lemma bisec_add_point:
assumes A1: \( x \notin X \) and A2: \( \langle A,B\rangle \in \text{Bisections}(X \cup \{x\}) \)
shows \( (A = \{x\} \vee B = \{x\}) \vee (\langle A - \{x\}, B - \{x\}\rangle \in \text{Bisections}(X)) \)proof{
}
assume \( A \neq \{x\} \) and \( B \neq \{x\} \)
with A2 have \( A - \{x\} \neq 0 \) and \( B - \{x\} \neq 0 \) using singl_diff_empty, Bisections_def
moreover
have \( (A - \{x\}) \cup (B - \{x\}) = X \)proof
moreover have \( (A - \{x\}) \cup (B - \{x\}) = (A \cup B) - \{x\} \)
also
qed
from assms have \( (A \cup B) - \{x\} = X \) using Bisections_def
finally show \( thesis \)
from A2 have \( (A - \{x\}) \cap (B - \{x\}) = 0 \) using Bisections_def
ultimately have \( \langle A - \{x\}, B - \{x\}\rangle \in \text{Bisections}(X) \) using Bisections_def
thus \( thesis \)
qed
A continuation of the lemma bisec_add_point that refines the case when the pair with removed point bisects the original set.
lemma bisec_add_point_case3:
assumes A1: \( \langle A,B\rangle \in \text{Bisections}(X \cup \{x\}) \) and A2: \( \langle A - \{x\}, B - \{x\}\rangle \in \text{Bisections}(X) \)
shows \( (\langle A, B - \{x\}\rangle \in \text{Bisections}(X) \wedge x \in B) \vee \) \( (\langle A - \{x\}, B\rangle \in \text{Bisections}(X) \wedge x \in A) \)proof from A1 have \( x \in A \cup B \) using Bisections_def
hence \( x\in A \vee x\in B \)
from A1 have \( A - \{x\} = A \vee B - \{x\} = B \) using Bisections_def
moreover {
}
moreover {
}
ultimately show \( thesis \)
qed
assume \( A - \{x\} = A \)
with A2, \( x \in A \cup B \) have \( \langle A, B - \{x\}\rangle \in \text{Bisections}(X) \wedge x \in B \) using singl_diff_eq
assume \( B - \{x\} = B \)
with A2, \( x \in A \cup B \) have \( \langle A - \{x\}, B\rangle \in \text{Bisections}(X) \wedge x \in A \) using singl_diff_eq
Another lemma about bisecting a set with an added point.
lemma point_set_bisec:
assumes A1: \( x \notin X \) and A2: \( \langle \{x\}, A\rangle \in \text{Bisections}(X \cup \{x\}) \)
shows \( A = X \) and \( X \neq 0 \)proof from A2 have \( A \subseteq X \) using Bisections_def
moreover {
}
ultimately show \( A = X \)
qed
fix \( a \)
assume \( a\in X \)
with A2 have \( a \in \{x\} \cup A \) using Bisections_def
with A1, \( a\in X \) have \( a \in A \)
with A2 show \( X \neq 0 \) using Bisections_def
Yet another lemma about bisecting a set with an added point, very similar to point_set_bisec with almost the same proof.
lemma set_point_bisec:
assumes A1: \( x \notin X \) and A2: \( \langle A, \{x\}\rangle \in \text{Bisections}(X \cup \{x\}) \)
shows \( A = X \) and \( X \neq 0 \)proof from A2 have \( A \subseteq X \) using Bisections_def
moreover {
}
ultimately show \( A = X \)
qed
fix \( a \)
assume \( a\in X \)
with A2 have \( a \in A \cup \{x\} \) using Bisections_def
with A1, \( a\in X \) have \( a \in A \)
with A2 show \( X \neq 0 \) using Bisections_def
If a pair of sets bisects a finite set, then both elements of the pair are finite.
lemma bisect_fin:
assumes A1: \( A \in \text{FinPow}(X) \) and A2: \( Q \in \text{Bisections}(A) \)
shows \( \text{fst}(Q) \in \text{FinPow}(X) \) and \( \text{snd}(Q) \in \text{FinPow}(X) \)proof from A2 have \( \langle \text{fst}(Q), \text{snd}(Q)\rangle \in \text{Bisections}(A) \) using bisec_is_pair
then have \( \text{fst}(Q) \subseteq A \) and \( \text{snd}(Q) \subseteq A \) using bisec_props
with A1 show \( \text{fst}(Q) \in \text{FinPow}(X) \) and \( \text{snd}(Q) \in \text{FinPow}(X) \) using FinPow_def, subset_Finite
qed
Partitions
This sections covers the situation when we have an arbitrary number of sets we want to partition into.
We define a notion of a partition as a set valued function such that the values for different arguments are disjoint. The name is derived from the fact that such function "partitions" the union of its arguments. Please let me know if you have a better idea for a name for such notion. We would prefer to say ''is a partition'', but that reserves the letter ''a'' as a keyword(?) which causes problems.
definition
\( P \text{ is partition } \equiv \forall x \in domain(P).\ \) \( P(x) \neq 0 \wedge (\forall y \in domain(P).\ x\neq y \longrightarrow P(x) \cap P(y) = 0) \)
A fact about lists of mutually disjoint sets.
lemma list_partition:
assumes A1: \( n \in nat \) and A2: \( a : succ(n) \rightarrow X \), \( a \text{ is partition } \)
shows \( (\bigcup i\in n.\ a(i)) \cap a(n) = 0 \)proof{
}
assume \( (\bigcup i\in n.\ a(i)) \cap a(n) \neq 0 \)
then have \( \exists x.\ x \in (\bigcup i\in n.\ a(i)) \cap a(n) \) by (rule nonempty_has_element )
then obtain \( x \) where \( x \in (\bigcup i\in n.\ a(i)) \) and I: \( x \in a(n) \)
then obtain \( i \) where \( i \in n \) and \( x \in a(i) \)
with A2, I have \( False \) using mem_imp_not_eq, func1_1_L1, Partition_def
thus \( thesis \)
qed
We can turn every injection into a partition.
lemma inj_partition:
assumes A1: \( b \in \text{inj}(X,Y) \)
shows \( \forall x \in X.\ \{\langle x, \{b(x)\}\rangle .\ x \in X\}(x) = \{b(x)\} \) and \( \{\langle x, \{b(x)\}\rangle .\ x \in X\} \text{ is partition } \)proof let \( p = \{\langle x, \{b(x)\}\rangle .\ x \in X\} \)
{
fix \( x \)
assume \( x \in X \)
from A1 have \( b : X \rightarrow Y \) using inj_def
with \( x \in X \) have \( \{b(x)\} \in Pow(Y) \) using apply_funtype
hence \( \forall x \in X.\ \{b(x)\} \in Pow(Y) \)
then have \( p : X \rightarrow Pow(Y) \) using ZF_fun_from_total
then have \( domain(p) = X \) using func1_1_L1
from \( p : X \rightarrow Pow(Y) \) show I: \( \forall x \in X.\ p(x) = \{b(x)\} \) using ZF_fun_from_tot_val0
{
fix \( x \)
assume \( x \in X \)
with I have \( p(x) = \{b(x)\} \)
hence \( p(x) \neq 0 \)
moreover {
}
ultimately have \( p(x) \neq 0 \wedge (\forall t \in X.\ x\neq t \longrightarrow p(x) \cap p(t) = 0) \)
fix \( t \)
assume \( t \in X \) and \( x \neq t \)
with A1, \( x \in X \) have \( b(x) \neq b(t) \) using inj_def
with I, \( x\in X \), \( t \in X \) have \( p(x) \cap p(t) = 0 \)
with \( domain(p) = X \) show \( \{\langle x, \{b(x)\}\rangle .\ x \in X\} \text{ is partition } \) using Partition_def
qed
end
Definition of Bisections:
\( \text{Bisections}(X) = \{p \in Pow(X)\times Pow(X).\ \)
\( \text{fst}(p)\neq 0 \wedge \text{snd}(p)\neq 0 \wedge \text{fst}(p)\cap \text{snd}(p) = 0 \wedge \text{fst}(p)\cup \text{snd}(p) = X\} \)
lemma singl_diff_empty:
assumes \( A - \{x\} = \emptyset \)
shows \( A = \emptyset \vee A = \{x\} \) lemma singl_diff_eq:
assumes \( A - \{x\} = A \)
shows \( x \notin A \) lemma bisec_is_pair:
assumes \( Q \in \text{Bisections}(X) \)
shows \( Q = \langle \text{fst}(Q), \text{snd}(Q)\rangle \) lemma bisec_props:
assumes \( \langle A,B\rangle \in \text{Bisections}(X) \)
shows \( A\neq 0 \), \( B\neq 0 \), \( A \subseteq X \), \( B \subseteq X \), \( A \cap B = 0 \), \( A \cup B = X \), \( X \neq 0 \)Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma nonempty_has_element:
assumes \( X\neq \emptyset \)
shows \( \exists x.\ x\in X \) lemma func1_1_L1:
assumes \( f:A\rightarrow C \)
shows \( domain(f) = A \)Definition of Partition:
\( P \text{ is partition } \equiv \forall x \in domain(P).\ \)
\( P(x) \neq 0 \wedge (\forall y \in domain(P).\ x\neq y \longrightarrow P(x) \cap P(y) = 0) \)
lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) lemma ZF_fun_from_tot_val0:
assumes \( f:X\rightarrow Y \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( \forall x\in X.\ f(x) = b(x) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8