IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Partitions_ZF imports Finite_ZF InductiveSeq_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_def

Kind 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_def

Bisection 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_def

The set of bisections of the empty set is empty.

lemma bisec_empty:

shows \( \text{Bisections}(0) = 0 \) using Bisections_def

The 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

have \( (A - \{x\}) \cup (B - \{x\}) = (A \cup B) - \{x\} \)

also

from assms have \( (A \cup B) - \{x\} = X \) using Bisections_def

finally show \( thesis \)

qed

moreover

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 {

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

} moreover {

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

} ultimately show \( thesis \)

qed

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 {

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 \)

} ultimately show \( A = X \)

with A2 show \( X \neq 0 \) using Bisections_def

qed

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 {

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 \)

} ultimately show \( A = X \)

with A2 show \( X \neq 0 \) using Bisections_def

qed

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 nonempty and 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 {

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 \)

} ultimately have \( p(x) \neq 0 \wedge (\forall t \in X.\ x\neq t \longrightarrow 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

Collections of pairwise disjoint sets

The notion of collection of pairwise disjoint sets is similar to a partition except that we don't require the members to be nonempty.

A set valued function \(X\) is pairwise disjoint if for any two different indices the corresponding sets have empty intersection.

definition

\( X \text{ is pairwise disjoint } \equiv \forall i\in domain(X).\ \forall j\in domain(X).\ i\neq j \longrightarrow X(i)\cap X(j)=\emptyset \)

Suppose that \(X:I\rightarrow Y\) is pairwise disjoint collection of sets and we know that \(x\) is a member of a set in the collection. Then the index of that set can be expressed as \(\bigcup\{ j in I: x\in X(j)\}\).

lemma get_the_one:

assumes \( X:I\rightarrow Y \), \( X \text{ is pairwise disjoint } \), \( i\in I \), \( x\in X(i) \)

shows \( i = \bigcup \{j\in I.\ x\in X(j)\} \)proof

from assms have U: \( \exists !i.\ i\in I \wedge x\in X(i) \) using func1_1_L1 unfolding IsPairwiseDisjoint_def

with assms(3,4) show \( thesis \) using ZF1_1_L9(2,3)

qed

A kind of inverse of get_the_one: if \(X:I\rightarrow Y\) is pairwise disjoint collection of sets and \(x\in\bigcup_{i\in I} X(i)\) then \(i:=\bigcup\{ j\in I: x\in X(j)\}\) is an index and \(x\in X(i)\).

lemma one_is_the_one:

assumes \( X:I\rightarrow Y \), \( X \text{ is pairwise disjoint } \), \( x\in (\bigcup j\in I.\ X(j)) \)

defines \( i \equiv \bigcup \{j\in I.\ x\in X(j)\} \)

shows \( i\in I \), \( x\in X(i) \) using assms, get_the_one

A special case of pairwise disjoint collection is the sequence of set differences of consecutive elements of sequence of sets that is monotonic in the inclusion order. The next lemma shows that if a sequence \(\{\mathcal{U}_i\}_{i\in\mathbb{N}}\) of subsets of \(X\) is decreasing in the inclusion order on the powerset of \(X\) then the sequence \(\{\mathcal{U}_i\setminus \mathcal{U}_{i+1}\}_{i\in\mathbb{N}}\) is pairwise disjoint. In addition, the union \(\bigcup_{n\in\mathbb{N}}\mathcal{U}_{n}\setminus \mathcal{U}_{n+1}\) is the same as \(\mathcal{U}_0\setminus \bigcap_{n\in\mathbb{N}} \mathcal{U}_n\).

lemma decr_pair_disj:

assumes \( \text{IsDecreasingSeq}(Pow(X), \text{InclusionOn}(Pow(X)),\mathcal{U} ) \)

shows \( \{\langle n,\mathcal{U} (n)\setminus \mathcal{U} (n + 1)\rangle .\ n\in nat\} \text{ is pairwise disjoint } \), \( (\bigcup n\in nat.\ \mathcal{U} (n)\setminus \mathcal{U} (n + 1)) = \mathcal{U} (0)\setminus (\bigcap n\in nat.\ \mathcal{U} (n)) \)proof

let \( r = \text{InclusionOn}(Pow(X)) \)

let \( F = \{\langle n,\mathcal{U} (n)\setminus \mathcal{U} (n + 1)\rangle .\ n\in nat\} \)

have \( domain(F) = nat \) and \( \text{IsPreorder}(Pow(X),r) \) using incl_is_partorder(2)

{

fix \( i \) \( j \)

assume \( i\in nat \), \( j\in nat \), \( i\neq j \)

then have \( i \lt j \vee j \lt i \) using nat_mem_total

moreover {

assume \( i \lt j \)

with assms, \( j\in nat \) have \( \langle \mathcal{U} (j), \mathcal{U} (i + 1)\rangle \in r \) using nat_less_succ_leq, incl_is_partorder(2), decreasing_seq_mono1

then have \( (\mathcal{U} (i)\setminus \mathcal{U} (i + 1)) \cap (\mathcal{U} (j)\setminus \mathcal{U} (j + 1)) = \emptyset \) unfolding InclusionOn_def

} moreover {

assume \( j \lt i \)

with assms, \( i\in nat \) have \( \langle \mathcal{U} (i), \mathcal{U} (j + 1)\rangle \in r \) using nat_less_succ_leq, incl_is_partorder(2), decreasing_seq_mono1

then have \( (\mathcal{U} (i)\setminus \mathcal{U} (i + 1)) \cap (\mathcal{U} (j)\setminus \mathcal{U} (j + 1)) = \emptyset \) unfolding InclusionOn_def

} ultimately have \( (\mathcal{U} (i)\setminus \mathcal{U} (i + 1)) \cap (\mathcal{U} (j)\setminus \mathcal{U} (j + 1)) = \emptyset \)

with \( i\in nat \), \( j\in nat \) have \( F(i) \cap F(j) = \emptyset \) using ZF_fun_from_tot_val2

}

hence \( \forall i\in nat.\ \forall j\in nat.\ i\neq j \longrightarrow F(i) \cap F(j) = \emptyset \)

with \( domain(F) = nat \) show \( \{\langle n,\mathcal{U} (n)\setminus \mathcal{U} (n + 1)\rangle .\ n\in nat\} \text{ is pairwise disjoint } \) unfolding IsPairwiseDisjoint_def

show \( (\bigcup n\in nat.\ \mathcal{U} (n)\setminus \mathcal{U} (n + 1)) = \mathcal{U} (0)\setminus (\bigcap n\in nat.\ \mathcal{U} (n)) \)proof

let \( L = \bigcup n\in nat.\ \mathcal{U} (n)\setminus \mathcal{U} (n + 1) \)

let \( R = \mathcal{U} (0)\setminus (\bigcap n\in nat.\ \mathcal{U} (n)) \)

{

fix \( x \)

assume \( x\in L \)

then obtain \( n \) where \( n\in nat \) and \( x\in \mathcal{U} (n)\setminus \mathcal{U} (n + 1) \)

then have \( x\in \mathcal{U} (n) \) and \( 0\leq n \)

with assms, \( \text{IsPreorder}(Pow(X),r) \), \( n\in nat \) have \( \langle \mathcal{U} (n),\mathcal{U} (0)\rangle \in r \) using decreasing_seq_mono1

with \( x\in \mathcal{U} (n) \) have \( x\in \mathcal{U} (0) \) unfolding InclusionOn_def

with \( n\in nat \), \( x\in \mathcal{U} (n)\setminus \mathcal{U} (n + 1) \) have \( x\in R \)

}

thus \( L\subseteq R \)

{

fix \( x \)

assume \( x\in R \)

then have \( x\in \mathcal{U} (0) \) and \( x\notin (\bigcap n\in nat.\ \mathcal{U} (n)) \)

let \( B = \{k\in nat.\ x\notin \mathcal{U} (k)\} \)

let \( m = \text{Minimum}(Le,B) \)

from \( x\notin (\bigcap n\in nat.\ \mathcal{U} (n)) \) have \( B\subseteq nat \) and \( B\neq \emptyset \)

then have \( m\in nat \), \( m\in B \) and \( \forall n\in B.\ m \leq n \) using subset_nat_has_min(2,3)

from \( x\in \mathcal{U} (0) \), \( m\in B \) have \( m\neq 0 \)

with \( m\in nat \) obtain \( n \) where \( n\in nat \) and \( m = n + 1 \) using nat_not0_succ

with \( \forall n\in B.\ m\leq n \), \( m\in B \) have \( \exists n\in nat.\ x \in \mathcal{U} (n)\setminus \mathcal{U} (n + 1) \) using nat_less_add_one

}

thus \( R\subseteq L \)

qed

If a sequence \(\{\mathcal{U}_i\}_{i\in\mathbb{N}}\) of subsets of \(X\) is increasing in the inclusion order on the powerset of \(X\) then the sequence \(\{\mathcal{U}_{i+1}\setminus \mathcal{U}_{i}\}_{i\in\mathbb{N}}\) is pairwise disjoint.

lemma incr_pair_disj:

assumes \( \text{IsIncreasingSeq}(Pow(X), \text{InclusionOn}(Pow(X)),\mathcal{U} ) \)

shows \( \{\langle n,\mathcal{U} (n + 1)\setminus \mathcal{U} (n)\rangle .\ n\in nat\} \text{ is pairwise disjoint } \)proof

let \( r = \text{InclusionOn}(Pow(X)) \)

let \( F = \{\langle n,\mathcal{U} (n + 1)\setminus \mathcal{U} (n)\rangle .\ n\in nat\} \)

have \( domain(F) = nat \) and \( \text{IsPreorder}(Pow(X),r) \) using incl_is_partorder(2)

{

fix \( i \) \( j \)

assume \( i\in nat \), \( j\in nat \), \( i\neq j \)

then have \( i \lt j \vee j \lt i \) using nat_mem_total

moreover {

assume \( i \lt j \)

with assms, \( j\in nat \) have \( \langle \mathcal{U} (i + 1), \mathcal{U} (j)\rangle \in r \) using incl_is_partorder(2), increasing_seq_mono1, nat_less_succ_leq

then have \( (\mathcal{U} (i + 1)\setminus \mathcal{U} (i)) \cap (\mathcal{U} (j + 1)\setminus \mathcal{U} (j)) = \emptyset \) unfolding InclusionOn_def

} moreover {

assume \( j \lt i \)

with assms, \( i\in nat \) have \( \langle \mathcal{U} (j + 1), \mathcal{U} (i)\rangle \in r \) using incl_is_partorder(2), increasing_seq_mono1, nat_less_succ_leq

then have \( (\mathcal{U} (i + 1)\setminus \mathcal{U} (i)) \cap (\mathcal{U} (j + 1)\setminus \mathcal{U} (j)) = \emptyset \) unfolding InclusionOn_def

} ultimately have \( (\mathcal{U} (i + 1)\setminus \mathcal{U} (i)) \cap (\mathcal{U} (j + 1)\setminus \mathcal{U} (j)) = \emptyset \)

with \( i\in nat \), \( j\in nat \) have \( F(i) \cap F(j) = \emptyset \) using ZF_fun_from_tot_val2

}

hence \( \forall i\in nat.\ \forall j\in nat.\ i\neq j \longrightarrow F(i) \cap F(j) = \emptyset \)

with \( domain(F) = nat \) show \( thesis \) unfolding IsPairwiseDisjoint_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\setminus \{x\} = \emptyset \)

shows \( A = \emptyset \vee A = \{x\} \)

lemma singl_diff_eq:

assumes \( A\setminus \{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) \)

Definition of IsPairwiseDisjoint: \( X \text{ is pairwise disjoint } \equiv \forall i\in domain(X).\ \forall j\in domain(X).\ i\neq j \longrightarrow X(i)\cap X(j)=\emptyset \)

lemma ZF1_1_L9:

assumes \( \exists ! x.\ x\in A \wedge \phi (x) \)

shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \), \( \exists x\in A.\ \phi (x) \)

lemma get_the_one:

assumes \( X:I\rightarrow Y \), \( X \text{ is pairwise disjoint } \), \( i\in I \), \( x\in X(i) \)

shows \( i = \bigcup \{j\in I.\ x\in X(j)\} \)

lemma incl_is_partorder: shows \( \text{IsPartOrder}(X, \text{InclusionOn}(X)) \) and \( \text{IsPreorder}(X, \text{InclusionOn}(X)) \)

lemma nat_mem_total:

assumes \( i \in nat \), \( j \in nat \), \( i\neq j \)

shows \( i \lt j \vee j \lt i \)

lemma nat_less_succ_leq:

assumes \( n\in nat \) and \( k \lt n \)

shows \( k + 1 \leq n \)

lemma decreasing_seq_mono1:

assumes \( \text{IsPreorder}(X,r) \), \( \text{IsDecreasingSeq}(X,r,s) \), \( m\in nat \), \( n\leq m \)