This theory extends Isabelle standard *Finite* theory.
It is obsolete and should not be used for new development.
Use the *Finite_ZF* instead.

In this section we consider various properties of *Fin*
datatype (even though there are no datatypes in ZF set theory).

In *Topology_ZF* theory we consider
induced topology that is
obtained by taking a subset of a topological space. To show that a topology
restricted to a subset is also a topology
on that subset we may need a fact that
if \(T\) is a collection of sets and \(A\) is a set then every finite collection
\(\{ V_i \}\) is of the form \(V_i=U_i \cap A\), where \(\{U_i\}\) is a finite
subcollection of \(T\). This is one of those trivial
facts that require suprisingly
long formal proof.
Actually, the need for this fact is avoided by requiring intersection
two open sets to be open (rather than intersection of
a finite number of open sets).
Still, the fact is left here as an example of a proof by induction.
We will use *Fin_induct* lemma from Finite.thy.
First we define a property of
finite sets that we want to show.

** Definition **

\( \text{Prfin}(T,A,M) \equiv ( (M = 0) | (\exists N\in Fin(T).\ \forall V\in M.\ \exists U\in N.\ (V = U\cap A))) \)

Now we show the main induction step in a separate lemma. This will make
the proof of the theorem FinRestr below look short and nice.
The premises of the *ind_step* lemma are those needed by
the main induction step in
lemma *Fin_induct* (see standard Isabelle's Finite.thy).

** lemma ** ind_step:

** assumes **A: \( \forall V\in TA.\ \exists U\in T.\ V=U\cap A \)** and **A1: \( W\in TA \)** and **A2: \( M\in Fin(TA) \)** and **A3: \( W\notin M \)** and **A4: \( \text{Prfin}(T,A,M) \)

{
** assume **A7: \( M=0 \)
** have ** \( \text{Prfin}(T, A, cons(W, M)) \)proof
** from **A1, A ** obtain **\( U \)** where **A5: \( U\in T \)** and **A6: \( W=U\cap A \)
** let **\( N = \{U\} \)
** from **A5 ** have ** T1: \( N \in Fin(T) \)
** from **A7, A6 ** have ** T2: \( \forall V\in cons(W,M).\ \exists U\in N.\ V=U\cap A \)
** from **A7, T1, T2 ** show ** \( \text{Prfin}(T, A, cons(W, M)) \)** using ** Prfin_def
** qed **
** } **
** moreover ** {
** assume **A8: \( M\neq 0 \)
** have ** \( \text{Prfin}(T, A, cons(W, M)) \)proof
** from **A1, A ** obtain **\( U \)** where **A5: \( U\in T \)** and **A6: \( W=U\cap A \)
** from **A8, A4 ** obtain **\( N0 \)** where **A9: \( N0\in Fin(T) \)** and **A10: \( \forall V\in M.\ \exists U0\in N0.\ (V = U0\cap A) \)** using ** Prfin_def
** let **\( N = cons(U,N0) \)
** from **A5, A9 ** have ** \( N \in Fin(T) \)
** moreover ** ** from **A10, A6 ** have ** \( \forall V\in cons(W,M).\ \exists U\in N.\ V=U\cap A \)
** ultimately **** have ** \( \exists N\in Fin(T).\ \forall V\in cons(W,M).\ \exists U\in N.\ V=U\cap A \)
** with **A8 ** show ** \( \text{Prfin}(T, A, cons(W, M)) \)** using ** Prfin_def
** qed **
** } **
** ultimately **** show ** \( thesis \)
** qed **

Now we are ready to prove the statement we need.

** theorem ** FinRestr0:

** assumes **A: \( \forall V \in TA.\ \exists U\in T.\ V=U\cap A \)

{
** fix **\( M \)
** assume **\( M \in Fin(TA) \)
** moreover ** ** have ** \( \text{Prfin}(T,A,0) \)** using ** Prfin_def
** moreover ** {
** fix **\( W \) \( M \)
** assume **\( W\in TA \), \( M\in Fin(TA) \), \( W\notin M \), \( \text{Prfin}(T,A,M) \)
** with **A ** have ** \( \text{Prfin}(T,A,cons(W,M)) \)** by (rule **ind_step** ) **
** } **
** ultimately **** have ** \( \text{Prfin}(T,A,M) \)** by (rule **Fin_induct** ) **
** } **
** thus ** \( thesis \)
** qed **

This is a different form of the above theorem:

** theorem ** ZF1FinRestr:

** assumes **A1: \( M\in Fin(TA) \)** and **A2: \( M\neq 0 \)** and **A3: \( \forall V\in TA.\ \exists U\in T.\ V=U\cap A \)

Purely technical lemma used in *Topology_ZF_1* to show
that if a topology is \(T_2\), then it is \(T_1\).

** lemma ** Finite1_L2:

** assumes **A: \( \exists U V.\ (U\in T \wedge V\in T \wedge x\in U \wedge y\in V \wedge U\cap V=0) \)

A collection closed with respect to taking a union of two sets is closed under taking finite unions. Proof by induction with the induction step formulated in a separate lemma.

** lemma ** Finite1_L3_IndStep:

** assumes **A1: \( \forall A B.\ ((A\in C \wedge B\in C) \longrightarrow A\cup B\in C) \)** and **A2: \( A\in C \)** and **A3: \( N\in Fin(C) \)** and **A4: \( A\notin N \)** and **A5: \( \bigcup N \in C \)

The lemma: a collection closed with respect to taking a union of two sets is closed under taking finite unions.

** lemma ** Finite1_L3:

** assumes **A1: \( 0 \in C \)** and **A2: \( \forall A B.\ ((A\in C \wedge B\in C) \longrightarrow A\cup B\in C) \)** and **A3: \( N\in Fin(C) \)

A collection closed with respect to taking a intersection of two sets
is closed under taking finite intersections.
Proof by induction with
the induction step formulated in a separate lemma. This is sligltly more
involved than the union case in *Finite1_L3*, because the intersection
of empty collection is undefined (or should be treated as such).
To simplify notation we define the property to be proven for finite sets
as a separate notion.

** Definition **

\( \text{IntPr}(T,N) \equiv (N = 0 | \bigcap N \in T) \)

The induction step.

** lemma ** Finite1_L4_IndStep:

** assumes **A1: \( \forall A B.\ ((A\in T \wedge B\in T) \longrightarrow A\cap B\in T) \)** and **A2: \( A\in T \)** and **A3: \( N\in Fin(T) \)** and **A4: \( A\notin N \)** and **A5: \( \text{IntPr}(T,N) \)

{
** assume **A6: \( N=0 \)
** with **A2 ** have ** \( \text{IntPr}(T,cons(A,N)) \)** using ** IntPr_def
** } **
** moreover ** {
** assume **A7: \( N\neq 0 \)
** have ** \( \text{IntPr}(T, cons(A, N)) \)proof
** from **A7, A5, A2, A1 ** have ** \( \bigcap N \cap A \in T \)** using ** IntPr_def
** moreover ** ** from **A7 ** have ** \( \bigcap cons(A, N) = \bigcap N \cap A \)
** ultimately **** show ** \( \text{IntPr}(T, cons(A, N)) \)** using ** IntPr_def
** qed **
** } **
** ultimately **** show ** \( thesis \)
** qed **

The lemma.

** lemma ** Finite1_L4:

** assumes **A1: \( \forall A B.\ A\in T \wedge B\in T \longrightarrow A\cap B \in T \)** and **A2: \( N\in Fin(T) \)

Next is a restatement of the above lemma that does not depend on the IntPr meta-function.

** lemma ** Finite1_L5:

** assumes **A1: \( \forall A B.\ ((A\in T \wedge B\in T) \longrightarrow A\cap B\in T) \)** and **A2: \( N\neq 0 \)** and **A3: \( N\in Fin(T) \)

The images of finite subsets by a meta-function are finite. For example in topology if we have a finite collection of sets, then closing each of them results in a finite collection of closed sets. This is a very useful lemma with many unexpected applications. The proof is by induction. The next lemma is the induction step.

** lemma ** fin_image_fin_IndStep:

** assumes **\( \forall V\in B.\ K(V)\in C \)** and **\( U\in B \)** and **\( N\in Fin(B) \)** and **\( U\notin N \)** and **\( \{K(V).\ V\in N\}\in Fin(C) \)

The lemma:

** lemma ** fin_image_fin:

** assumes **A1: \( \forall V\in B.\ K(V)\in C \)** and **A2: \( N\in Fin(B) \)

The image of a finite set is finite.

** lemma ** Finite1_L6A:

** assumes **A1: \( f:X\rightarrow Y \)** and **A2: \( N \in Fin(X) \)

If the set defined by a meta-function is finite, then every set defined by a composition of this meta function with another one is finite.

** lemma ** Finite1_L6B:

** assumes **A1: \( \forall x\in X.\ a(x) \in Y \)** and **A2: \( \{b(y).\ y\in Y\} \in Fin(Z) \)

** lemma ** Finite1_L6C:

** assumes **A1: \( \forall y\in Y.\ b(y) \in Z \)** and **A2: \( \{a(x).\ x\in X\} \in Fin(Y) \)

If an intersection of a collection is not empty, then the collection is not empty. We are (ab)using the fact the the intesection of empty collection is defined to be empty and prove by contradiction. Should be in ZF1.thy

** lemma ** Finite1_L9:

** assumes **A1: \( \bigcap A \neq 0 \)

{
** assume **A2: \( \neg A \neq 0 \)
** with **A1 ** have ** \( False \)
** } **
** thus ** \( thesis \)
** qed **

Cartesian product of finite sets is finite.

** lemma ** Finite1_L12:

** assumes **A1: \( A \in Fin(A) \)** and **A2: \( B \in Fin(B) \)

We define the characterisic meta-function that is the identity on a set and assigns a default value everywhere else.

** Definition **

\( \text{Characteristic}(A,default,x) \equiv (if x\in A then x else default) \)

A finite subset is a finite subset of itself.

** lemma ** Finite1_L13:

** assumes **A1: \( A \in Fin(X) \)

{
** assume **\( A=0 \)
** hence ** \( A \in Fin(A) \)
** } **
** moreover ** {
** assume **A2: \( A\neq 0 \)
** then **** obtain **\( c \)** where **D1: \( c\in A \)
** then **** have ** \( \forall x\in X.\ \text{Characteristic}(A,c,x) \in A \)** using ** Characteristic_def
** moreover ** ** note **A1
** ultimately **** have ** \( \{ \text{Characteristic}(A,c,x).\ x\in A\} \in Fin(A) \)** by (rule **fin_image_fin** ) **
** moreover ** ** from **D1 ** have ** \( \{ \text{Characteristic}(A,c,x).\ x\in A\} = A \)** using ** Characteristic_def
** ultimately **** have ** \( A \in Fin(A) \)
** } **
** ultimately **** show ** \( thesis \)
** qed **

Cartesian product of finite subsets is a finite subset of cartesian product.

** lemma ** Finite1_L14:

** assumes **A1: \( A \in Fin(X) \), \( B \in Fin(Y) \)

The next lemma is needed in the *Group_ZF_3* theory in a
couple of places.

** lemma ** Finite1_L15:

** assumes **A1: \( \{b(x).\ x\in A\} \in Fin(B) \), \( \{c(x).\ x\in A\} \in Fin(C) \)** and **A2: \( f : B\times C\rightarrow E \)

Singletons are in the finite powerset.

** lemma ** Finite1_L16:

** assumes **\( x\in X \)

A special case of *Finite1_L15* where the second
set is a singleton. *Group_ZF_3* theory this corresponds
to the situation where we multiply by a constant.

** lemma ** Finite1_L16AA:

** assumes **\( \{b(x).\ x\in A\} \in Fin(B) \)** and **\( c\in C \)** and **\( f : B\times C\rightarrow E \)

First order version of the induction for the finite powerset.

** lemma ** Finite1_L16B:

** assumes **A1: \( P(0) \)** and **A2: \( B\in Fin(X) \)** and **A3: \( \forall A\in Fin(X).\ \forall x\in X.\ x\notin A \wedge P(A)\longrightarrow P(A\cup \{x\}) \)

In this section we define functions
\(f : X\rightarrow Y\), with the property that \(f(X)\) is
a finite subset of \(Y\). Such functions play a important
role in the construction of real numbers in the *Real_ZF* series.

Definition of finite range functions.

** Definition **

\( \text{FinRangeFunctions}(X,Y) \equiv \{f:X\rightarrow Y.\ f(X) \in Fin(Y)\} \)

Constant functions have finite range.

** lemma ** Finite1_L17:

** assumes **\( c\in Y \)** and **\( X\neq 0 \)

Finite range functions have finite range.

** lemma ** Finite1_L18:

** assumes **\( f \in \text{FinRangeFunctions}(X,Y) \)

An alternative form of the definition of finite range functions.

** lemma ** Finite1_L19:

** assumes **\( f:X\rightarrow Y \)** and **\( \{f(x).\ x\in X\} \in Fin(Y) \)

A composition of a finite range function with another function is a finite range function.

** lemma ** Finite1_L20:

** assumes **A1: \( f \in \text{FinRangeFunctions}(X,Y) \)** and **A2: \( g : Y\rightarrow Z \)

Image of any subset of the domain of a finite range function is finite.

** lemma ** Finite1_L21:

** assumes **\( f \in \text{FinRangeFunctions}(X,Y) \)** and **\( A\subseteq X \)

Definition of Prfin:
\( \text{Prfin}(T,A,M) \equiv ( (M = 0) | (\exists N\in Fin(T).\ \forall V\in M.\ \exists U\in N.\ (V = U\cap A))) \)

** assumes **\( \forall V\in TA.\ \exists U\in T.\ V=U\cap A \)** and **\( W\in TA \)** and **\( M\in Fin(TA) \)** and **\( W\notin M \)** and **\( \text{Prfin}(T,A,M) \)

** assumes **\( \forall V \in TA.\ \exists U\in T.\ V=U\cap A \)

** assumes **\( \forall A B.\ ((A\in C \wedge B\in C) \longrightarrow A\cup B\in C) \)** and **\( A\in C \)** and **\( N\in Fin(C) \)** and **\( A\notin N \)** and **\( \bigcup N \in C \)

Definition of IntPr:
\( \text{IntPr}(T,N) \equiv (N = 0 | \bigcap N \in T) \)

** assumes **\( \forall A B.\ ((A\in T \wedge B\in T) \longrightarrow A\cap B\in T) \)** and **\( A\in T \)** and **\( N\in Fin(T) \)** and **\( A\notin N \)** and **\( \text{IntPr}(T,N) \)

** assumes **\( \forall A B.\ A\in T \wedge B\in T \longrightarrow A\cap B \in T \)** and **\( N\in Fin(T) \)

** assumes **\( \forall V\in B.\ K(V)\in C \)** and **\( U\in B \)** and **\( N\in Fin(B) \)** and **\( U\notin N \)** and **\( \{K(V).\ V\in N\}\in Fin(C) \)

** assumes **\( \forall V\in B.\ K(V)\in C \)** and **\( N \in \text{FinPow}(B) \)

** assumes **\( f:X\rightarrow Y \)** and **\( A\subseteq X \)

Definition of Characteristic:
\( \text{Characteristic}(A,default,x) \equiv (if x\in A then x else default) \)

** assumes **\( A \in Fin(A) \)** and **\( B \in Fin(B) \)

** assumes **\( A \in Fin(X) \), \( B \in Fin(Y) \)

** assumes **\( f:X\rightarrow Y \)** and **\( N \in Fin(X) \)

** assumes **\( f \in X\rightarrow Y \)** and **\( \forall x\in A.\ b(x) \in X \)

** assumes **\( \forall y\in Y.\ b(y) \in Z \)** and **\( \{a(x).\ x\in X\} \in Fin(Y) \)

Definition of FinRangeFunctions:
\( \text{FinRangeFunctions}(X,Y) \equiv \{f:X\rightarrow Y.\ f(X) \in Fin(Y)\} \)

** assumes **\( f \in \text{FinRangeFunctions}(X,Y) \)

** assumes **\( f:X\rightarrow Y \)** and **\( \{f(x).\ x\in X\} \in Fin(Y) \)