IsarMathLib

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

theory Finite1 imports ZF.EquivClass ZF.Finite func1 ZF1
begin

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

Finite powerset

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

shows \( \text{Prfin}(T,A,cons(W,M)) \)proof
{
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 \)

shows \( \forall M\in Fin(TA).\ \text{Prfin}(T,A,M) \)proof
{
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 \)

shows \( \exists N\in Fin(T).\ (\forall V\in M.\ \exists U\in N.\ (V = U\cap A)) \wedge N\neq 0 \)proof
from A3, A1 have \( \text{Prfin}(T,A,M) \) using FinRestr0
then have \( \exists N\in Fin(T).\ \forall V\in M.\ \exists U\in N.\ (V = U\cap A) \) using A2, Prfin_def
then obtain \( N \) where D1: \( N\in Fin(T) \wedge (\forall V\in M.\ \exists U\in N.\ (V = U\cap A)) \)
with A2 have \( N\neq 0 \)
with D1 show \( thesis \)
qed

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

shows \( \exists U\in T.\ (x\in U \wedge y\notin U) \)proof
from A obtain \( U \) \( V \) where D1: \( U\in T \wedge V\in T \wedge x\in U \wedge y\in V \wedge U\cap V=0 \)
with D1 show \( thesis \)
qed

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

shows \( \bigcup cons(A,N) \in C \)proof
have \( \bigcup cons(A,N) = A\cup \bigcup N \)
with A1, A2, A5 show \( thesis \)
qed

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

shows \( \bigcup N\in C \)proof
note A3
moreover
from A1 have \( \bigcup 0 \in C \)
moreover {
fix \( A \) \( N \)
assume \( A\in C \), \( N\in Fin(C) \), \( A\notin N \), \( \bigcup N \in C \)
with A2 have \( \bigcup cons(A,N) \in C \) by (rule Finite1_L3_IndStep )
} ultimately show \( \bigcup N\in C \) by (rule Fin_induct )
qed

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

shows \( \text{IntPr}(T,cons(A,N)) \)proof
{
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) \)

shows \( \text{IntPr}(T,N) \)proof
note A2
moreover
have \( \text{IntPr}(T,0) \) using IntPr_def
moreover {
fix \( A \) \( N \)
assume \( A\in T \), \( N\in Fin(T) \), \( A\notin N \), \( \text{IntPr}(T,N) \)
with A1 have \( \text{IntPr}(T,cons(A,N)) \) by (rule Finite1_L4_IndStep )
} ultimately show \( \text{IntPr}(T,N) \) by (rule Fin_induct )
qed

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

shows \( \bigcap N \in T \)proof
from A1, A3 have \( \text{IntPr}(T,N) \) using Finite1_L4
with A2 show \( thesis \) using IntPr_def
qed

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

shows \( \{K(V).\ V\in cons(U,N)\} \in Fin(C) \) using assms

The lemma:

lemma fin_image_fin:

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

shows \( \{K(V).\ V\in N\} \in Fin(C) \)proof
note A2
moreover
have \( \{K(V).\ V\in 0\} \in Fin(C) \)
moreover {
fix \( U \) \( N \)
assume \( U\in B \), \( N\in Fin(B) \), \( U\notin N \), \( \{K(V).\ V\in N\}\in Fin(C) \)
with A1 have \( \{K(V).\ V\in cons(U,N)\} \in Fin(C) \) by (rule fin_image_fin_IndStep )
} ultimately show \( thesis \) by (rule Fin_induct )
qed

The image of a finite set is finite.

lemma Finite1_L6A:

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

shows \( f(N) \in Fin(Y) \)proof
from A1 have \( \forall x\in X.\ f(x) \in Y \) using apply_type
moreover
note A2
ultimately have \( \{f(x).\ x\in N\} \in Fin(Y) \) by (rule fin_image_fin )
with A1, A2 show \( thesis \) using FinD, func_imagedef
qed

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

shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \)proof
from A1 have \( \{b(a(x)).\ x\in X\} \subseteq \{b(y).\ y\in Y\} \)
with A2 show \( thesis \) using Fin_subset_lemma
qed

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_L6C:

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

shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \)proof
let \( N = \{a(x).\ x\in X\} \)
from A1, A2 have \( \{b(y).\ y \in N\} \in Fin(Z) \) by (rule fin_image_fin )
moreover
have \( \{b(a(x)).\ x\in X\} = \{b(y).\ y\in N\} \)
ultimately show \( thesis \)
qed

Cartesian product of finite sets is finite.

lemma Finite1_L12:

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

shows \( A\times B \in Fin(A\times B) \)proof
have T1: \( \forall a\in A.\ \forall b\in B.\ \{\langle a,b\rangle \} \in Fin(A\times B) \)
have \( \forall a\in A.\ \{\{\langle a,b\rangle \}.\ b \in B\} \in Fin(Fin(A\times B)) \)proof
fix \( a \)
assume A3: \( a \in A \)
with T1 have \( \forall b\in B.\ \{\langle a,b\rangle \} \in Fin(A\times B) \)
moreover
note A2
ultimately show \( \{\{\langle a,b\rangle \}.\ b \in B\} \in Fin(Fin(A\times B)) \) by (rule fin_image_fin )
qed
then have \( \forall a\in A.\ \bigcup \{\{\langle a,b\rangle \}.\ b \in B\} \in Fin(A\times B) \) using Fin_UnionI
moreover
have \( \forall a\in A.\ \bigcup \{\{\langle a,b\rangle \}.\ b \in B\} = \{a\}\times B \)
ultimately have \( \forall a\in A.\ \{a\}\times B \in Fin(A\times B) \)
moreover
note A1
ultimately have \( \{\{a\}\times B.\ a\in A\} \in Fin(Fin(A\times B)) \) by (rule fin_image_fin )
then have \( \bigcup \{\{a\}\times B.\ a\in A\} \in Fin(A\times B) \) using Fin_UnionI
moreover
have \( \bigcup \{\{a\}\times B.\ a\in A\} = A\times B \)
ultimately show \( thesis \)
qed

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

definition

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

A finite subset is a finite subset of itself.

lemma Finite1_L13:

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

shows \( A \in Fin(A) \)proof
{
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) \)

shows \( A\times B \in Fin(X\times Y) \)proof
from A1 have \( A\times B \subseteq X\times Y \) using FinD
then have \( Fin(A\times B) \subseteq Fin(X\times Y) \) using Fin_mono
moreover
from A1 have \( A\times B \in Fin(A\times B) \) using Finite1_L13, Finite1_L12
ultimately show \( thesis \)
qed

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

shows \( \{f\langle b(x),c(x)\rangle .\ x\in A\} \in Fin(E) \)proof
from A1 have \( \{b(x).\ x\in A\}\times \{c(x).\ x\in A\} \in Fin(B\times C) \) using Finite1_L14
moreover
have \( \{\langle b(x),c(x)\rangle .\ x\in A\} \subseteq \{b(x).\ x\in A\}\times \{c(x).\ x\in A\} \)
ultimately have T0: \( \{\langle b(x),c(x)\rangle .\ x\in A\} \in Fin(B\times C) \) by (rule Fin_subset_lemma )
with A2 have T1: \( f\{\langle b(x),c(x)\rangle .\ x\in A\} \in Fin(E) \) using Finite1_L6A
from T0 have \( \forall x\in A.\ \langle b(x),c(x)\rangle \in B\times C \) using FinD
with A2 have \( f\{\langle b(x),c(x)\rangle .\ x\in A\} = \{f\langle b(x),c(x)\rangle .\ x\in A\} \) using func1_1_L17
with T1 show \( thesis \)
qed

Singletons are in the finite powerset.

lemma Finite1_L16:

assumes \( x\in X \)

shows \( \{x\} \in Fin(X) \) using assms, emptyI, consI

A special case of Finite1_L15 where the second set is a singleton. In 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 \)

shows \( \{f\langle b(x),c\rangle .\ x\in A\} \in Fin(E) \)proof
from assms have \( \forall y\in B.\ f\langle y,c\rangle \in E \), \( \{b(x).\ x\in A\} \in Fin(B) \) using apply_funtype
then show \( thesis \) by (rule Finite1_L6C )
qed

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

shows \( P(B) \)proof
note \( B\in Fin(X) \), and, \( P(0) \)
moreover {
fix \( A \) \( x \)
assume \( x \in X \), \( A \in Fin(X) \), \( x \notin A \), \( P(A) \)
moreover
have \( cons(x,A) = A\cup \{x\} \)
moreover
note A3
ultimately have \( P(cons(x,A)) \)
} ultimately show \( P(B) \) by (rule Fin_induct )
qed

Finite range functions

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

shows \( \text{ConstantFunction}(X,c) \in \text{FinRangeFunctions}(X,Y) \) using assms, func1_3_L1, func_imagedef, func1_3_L2, Finite1_L16, FinRangeFunctions_def

Finite range functions have finite range.

lemma Finite1_L18:

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

shows \( \{f(x).\ x\in X\} \in Fin(Y) \) using assms, FinRangeFunctions_def, func_imagedef

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

shows \( f \in \text{FinRangeFunctions}(X,Y) \) using assms, func_imagedef, FinRangeFunctions_def

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

shows \( g\circ f \in \text{FinRangeFunctions}(X,Z) \)proof
from A1, A2 have \( g\{f(x).\ x\in X\} \in Fin(Z) \) using Finite1_L18, Finite1_L6A
with A1, A2 have \( \{(g\circ f)(x).\ x\in X\} \in Fin(Z) \) using FinRangeFunctions_def, apply_funtype, func1_1_L17, comp_fun_apply
with A1, A2 show \( thesis \) using FinRangeFunctions_def, comp_fun, Finite1_L19
qed

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

shows \( f(A) \in Fin(Y) \)proof
from assms have \( f(X) \in Fin(Y) \), \( f(A) \subseteq f(X) \) using FinRangeFunctions_def, func1_1_L8
then show \( f(A) \in Fin(Y) \) using Fin_subset_lemma
qed
end
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))) \)
lemma ind_step:

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

shows \( \text{Prfin}(T,A,cons(W,M)) \)
theorem FinRestr0:

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

shows \( \forall M\in Fin(TA).\ \text{Prfin}(T,A,M) \)
lemma Finite1_L3_IndStep:

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

shows \( \bigcup cons(A,N) \in C \)
Definition of IntPr: \( \text{IntPr}(T,N) \equiv (N = 0 | \bigcap N \in T) \)
lemma Finite1_L4_IndStep:

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

shows \( \text{IntPr}(T,cons(A,N)) \)
lemma Finite1_L4:

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

shows \( \text{IntPr}(T,N) \)
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) \)

shows \( \{K(V).\ V\in cons(U,N)\} \in Fin(C) \)
lemma fin_image_fin:

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

shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \)
lemma func_imagedef:

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

shows \( f(A) = \{f(x).\ x \in A\} \)
Definition of Characteristic: \( \text{Characteristic}(A,\text{default},x) \equiv (\text{if }x\in A\text{ then }x\text{ else }\text{default}) \)
lemma Finite1_L13:

assumes \( A \in Fin(X) \)

shows \( A \in Fin(A) \)
lemma Finite1_L12:

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

shows \( A\times B \in Fin(A\times B) \)
lemma Finite1_L14:

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

shows \( A\times B \in Fin(X\times Y) \)
lemma Finite1_L6A:

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

shows \( f(N) \in Fin(Y) \)
lemma func1_1_L17:

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

shows \( f(\{b(x).\ x\in A\}) = \{f(b(x)).\ x\in A\} \)
lemma Finite1_L6C:

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

shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \)
lemma func1_3_L1:

assumes \( c\in Y \)

shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \)
lemma func1_3_L2:

assumes \( x\in X \)

shows \( \text{ConstantFunction}(X,c)(x) = c \)
lemma Finite1_L16:

assumes \( x\in X \)

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

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

shows \( \{f(x).\ x\in X\} \in Fin(Y) \)
lemma Finite1_L19:

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

shows \( f \in \text{FinRangeFunctions}(X,Y) \)
lemma func1_1_L8:

assumes \( A\subseteq B \)

shows \( f(A)\subseteq f(B) \)