IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory func1 imports func Fol1 ZF1
begin

This theory covers basic properties of function spaces. A set of functions with domain \(X\) and values in the set \(Y\) is denoted in Isabelle as \(X\rightarrow Y\). It just happens that the colon ":" is a synonym of the set membership symbol \(\in\) in Isabelle/ZF so we can write \(f:X\rightarrow Y\) instead of \(f \in X\rightarrow Y\). This is the only case that we use the colon instead of the regular set membership symbol.

Properties of functions, function spaces and (inverse) images.

Functions in ZF are sets of pairs. This means that if \(f: X\rightarrow Y \) then \(f\subseteq X\times Y\). This section is mostly about consequences of this understanding of the notion of function.

We define the notion of function that preserves a collection here. Given two collection of sets a function preserves the collections if the inverse image of sets in one collection belongs to the second one. This notion does not have a name in romantic math. It is used to define continuous functions in Topology_ZF_2 theory. We define it here so that we can use it for other purposes, like defining measurable functions. Recall that \( f^{-1}(A) \) means the inverse image of the set \(A\).

Definition

\( \text{PresColl}(f,S,T) \equiv \forall A\in T.\ f^{-1}(A)\in S \)

A definition that allows to get the first factor of the domain of a binary function \(f: X\times Y \rightarrow Z\).

Definition

\( \text{fstdom}(f) \equiv domain(domain(f)) \)

If a function maps \(A\) into another set, then \(A\) is the domain of the function.

lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \) using assms , domain_of_fun

Standard Isabelle defines a \( function(f) \) predicate. the next lemma shows that our function satisfy that predicate. It is a special version of Isabelle's fun_is_function.

lemma fun_is_fun:

assumes \( f:X\rightarrow Y \)

shows \( function(f) \) using assms , fun_is_function

A lemma explains what fstdom is for.

lemma fstdomdef:

assumes A1: \( f: X\times Y \rightarrow Z \) and A2: \( Y\neq 0 \)

shows \( \text{fstdom}(f) = X \)proof
from A1 have \( domain(f) = X\times Y \) using func1_1_L1
with A2 show \( \text{fstdom}(f) = X \) unfolding fstdom_def
qed

A first-order version of Pi_type.

lemma func1_1_L1A:

assumes A1: \( f:X\rightarrow Y \) and A2: \( \forall x\in X.\ f(x) \in Z \)

shows \( f:X\rightarrow Z \)proof
{
fix \( x \)
assume \( x\in X \)
with A2 have \( f(x) \in Z \)
}
with A1 show \( f:X\rightarrow Z \) by (rule Pi_type )
qed

A variant of func1_1_L1A.

lemma func1_1_L1B:

assumes A1: \( f:X\rightarrow Y \) and A2: \( Y\subseteq Z \)

shows \( f:X\rightarrow Z \)proof
from A1, A2 have \( \forall x\in X.\ f(x) \in Z \) using apply_funtype
with A1 show \( f:X\rightarrow Z \) using func1_1_L1A
qed

There is a value for each argument.

lemma func1_1_L2:

assumes A1: \( f:X\rightarrow Y \), \( x\in X \)

shows \( \exists y\in Y.\ \langle x,y\rangle \in f \)proof
from A1 have \( f(x) \in Y \) using apply_type
moreover
from A1 have \( \langle x,f(x)\rangle \in f \) using apply_Pair
ultimately show \( thesis \)
qed

The inverse image is the image of converse. True for relations as well.

lemma vimage_converse:

shows \( r^{-1}(A) = converse(r)(A) \) using vimage_iff , image_iff , converse_iff

The image is the inverse image of converse.

lemma image_converse:

shows \( converse(r)^{-1}(A) = r(A) \) using vimage_iff , image_iff , converse_iff

The inverse image by a composition is the composition of inverse images.

lemma vimage_comp:

shows \( (r\circ s)^{-1}(A) = s^{-1}(r^{-1}(A)) \) using vimage_converse , converse_comp , image_comp , image_converse

A version of vimage_comp for three functions.

lemma vimage_comp3:

shows \( (r\circ s\circ t)^{-1}(A) = t^{-1}(s^{-1}(r^{-1}(A))) \) using vimage_comp

Inverse image of any set is contained in the domain.

lemma func1_1_L3:

assumes A1: \( f:X\rightarrow Y \)

shows \( f^{-1}(D) \subseteq X \)proof
have \( \forall x.\ x\in f^{-1}(D) \longrightarrow x \in domain(f) \) using vimage_iff , domain_iff
with A1 have \( \forall x.\ (x \in f^{-1}(D)) \longrightarrow (x\in X) \) using func1_1_L1
then show \( thesis \)
qed

The inverse image of the range is the domain.

lemma func1_1_L4:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(Y) = X \) using assms , func1_1_L3 , func1_1_L2 , vimage_iff

The arguments belongs to the domain and values to the range.

lemma func1_1_L5:

assumes A1: \( \langle x,y\rangle \in f \) and A2: \( f:X\rightarrow Y \)

shows \( x\in X \wedge y\in Y \)proof
from A1, A2 show \( x\in X \) using apply_iff
with A2 have \( f(x)\in Y \) using apply_type
with A1, A2 show \( y\in Y \) using apply_iff
qed

Function is a subset of cartesian product.

lemma fun_subset_prod:

assumes A1: \( f:X\rightarrow Y \)

shows \( f \subseteq X\times Y \)proof
fix \( p \)
assume \( p \in f \)
with A1 have \( \exists x\in X.\ p = \langle x, f(x)\rangle \) using Pi_memberD
then obtain \( x \) where I: \( p = \langle x, f(x)\rangle \)
with A1, \( p \in f \) have \( x\in X \wedge f(x) \in Y \) using func1_1_L5
with I show \( p \in X\times Y \)
qed

The (argument, value) pair belongs to the graph of the function.

lemma func1_1_L5A:

assumes A1: \( f:X\rightarrow Y \), \( x\in X \), \( y = f(x) \)

shows \( \langle x,y\rangle \in f \), \( y \in \text{range}(f) \)proof
from A1 show \( \langle x,y\rangle \in f \) using apply_Pair
then show \( y \in \text{range}(f) \) using rangeI
qed

The next theorem illustrates the meaning of the concept of function in ZF.

theorem fun_is_set_of_pairs:

assumes A1: \( f:X\rightarrow Y \)

shows \( f = \{\langle x, f(x)\rangle .\ x \in X\} \)proof
from A1 show \( \{\langle x, f(x)\rangle .\ x \in X\} \subseteq f \) using func1_1_L5A
next
{
fix \( p \)
assume \( p \in f \)
with A1 have \( p \in X\times Y \) using fun_subset_prod
with A1, \( p \in f \) have \( p \in \{\langle x, f(x)\rangle .\ x \in X\} \) using apply_equality
}
thus \( f \subseteq \{\langle x, f(x)\rangle .\ x \in X\} \)
qed

The range of function thet maps \(X\) into \(Y\) is contained in \(Y\).

lemma func1_1_L5B:

assumes A1: \( f:X\rightarrow Y \)

shows \( \text{range}(f) \subseteq Y \)proof
fix \( y \)
assume \( y \in \text{range}(f) \)
then obtain \( x \) where \( \langle x,y\rangle \in f \) using range_def , converse_def , domain_def
with A1 show \( y\in Y \) using func1_1_L5
qed

The image of any set is contained in the range.

lemma func1_1_L6:

assumes A1: \( f:X\rightarrow Y \)

shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)proof
show \( f(B) \subseteq \text{range}(f) \) using image_iff , rangeI
with A1 show \( f(B) \subseteq Y \) using func1_1_L5B
qed

The inverse image of any set is contained in the domain.

lemma func1_1_L6A:

assumes A1: \( f:X\rightarrow Y \)

shows \( f^{-1}(A)\subseteq X \)proof
fix \( x \)
assume A2: \( x\in f^{-1}(A) \)
then obtain \( y \) where \( \langle x,y\rangle \in f \) using vimage_iff
with A1 show \( x\in X \) using func1_1_L5
qed

Image of a greater set is greater.

lemma func1_1_L8:

assumes A1: \( A\subseteq B \)

shows \( f(A)\subseteq f(B) \) using assms , image_Un

A set is contained in the the inverse image of its image. There is similar theorem in equalities.thy (function_image_vimage) which shows that the image of inverse image of a set is contained in the set.

lemma func1_1_L9:

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

shows \( A \subseteq f^{-1}(f(A)) \)proof
from A1, A2 have \( \forall x\in A.\ \langle x,f(x)\rangle \in f \) using apply_Pair
then show \( thesis \) using image_iff
qed

The inverse image of the image of the domain is the domain.

lemma inv_im_dom:

assumes A1: \( f:X\rightarrow Y \)

shows \( f^{-1}(f(X)) = X \)proof
from A1 show \( f^{-1}(f(X)) \subseteq X \) using func1_1_L3
from A1 show \( X \subseteq f^{-1}(f(X)) \) using func1_1_L9
qed

A technical lemma needed to make the func1_1_L11 proof more clear.

lemma func1_1_L10:

assumes A1: \( f \subseteq X\times Y \) and A2: \( \exists !y.\ (y\in Y \wedge \langle x,y\rangle \in f) \)

shows \( \exists !y.\ \langle x,y\rangle \in f \)proof
from A2 show \( \exists y.\ \langle x, y\rangle \in f \)
fix \( y \) \( n \)
assume \( \langle x,y\rangle \in f \) and \( \langle x,n\rangle \in f \)
with A1, A2 show \( y=n \)
qed

If \(f\subseteq X\times Y\) and for every \(x\in X\) there is exactly one \(y\in Y\) such that \((x,y)\in f\) then \(f\) maps \(X\) to \(Y\).

lemma func1_1_L11:

assumes \( f \subseteq X\times Y \) and \( \forall x\in X.\ \exists !y.\ y\in Y \wedge \langle x,y\rangle \in f \)

shows \( f: X\rightarrow Y \) using assms , func1_1_L10 , Pi_iff_old

A set defined by a lambda-type expression is a fuction. There is a similar lemma in func.thy, but I had problems with lambda expressions syntax so I could not apply it. This lemma is a workaround for this. Besides, lambda expressions are not readable.

lemma func1_1_L11A:

assumes A1: \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y \)proof
let \( f = \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} \)
have \( f \subseteq X\times Y \)
moreover
have \( \forall x\in X.\ \exists !y.\ y\in Y \wedge \langle x,y\rangle \in f \)proof
fix \( x \)
assume A2: \( x\in X \)
show \( \exists !y.\ y\in Y \wedge \langle x, y\rangle \in \{\langle x,y\rangle \in X\times Y .\ b(x) = y\} \)proof
from A2, A1 show \( \exists y.\ y\in Y \wedge \langle x, y\rangle \in \{\langle x,y\rangle \in X\times Y .\ b(x) = y\} \)
next
fix \( y \) \( y1 \)
assume \( y\in Y \wedge \langle x, y\rangle \in \{\langle x,y\rangle \in X\times Y .\ b(x) = y\} \) and \( y1\in Y \wedge \langle x, y1\rangle \in \{\langle x,y\rangle \in X\times Y .\ b(x) = y\} \)
then show \( y = y1 \)
qed
qed
ultimately show \( \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y \) using func1_1_L11
qed

The next lemma will replace func1_1_L11A one day.

lemma ZF_fun_from_total:

assumes A1: \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)proof
let \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
{
fix \( x \)
assume A2: \( x\in X \)
have \( \exists !y.\ y\in Y \wedge \langle x, y\rangle \in f \)proof
from A1, A2 show \( \exists y.\ y\in Y \wedge \langle x, y\rangle \in f \)
next
fix \( y \) \( y1 \)
assume \( y\in Y \wedge \langle x, y\rangle \in f \) and \( y1\in Y \wedge \langle x, y1\rangle \in f \)
then show \( y = y1 \)
qed
}
then have \( \forall x\in X.\ \exists !y.\ y\in Y \wedge \langle x,y\rangle \in f \)
moreover
from A1 have \( f \subseteq X\times Y \)
ultimately show \( thesis \) using func1_1_L11
qed

The value of a function defined by a meta-function is this meta-function.

lemma func1_1_L11B:

assumes A1: \( f:X\rightarrow Y \), \( x\in X \) and A2: \( f = \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} \)

shows \( f(x) = b(x) \)proof
from A1 have \( \langle x,f(x)\rangle \in f \) using apply_iff
with A2 show \( thesis \)
qed

The next lemma will replace func1_1_L11B one day.

lemma ZF_fun_from_tot_val:

assumes A1: \( f:X\rightarrow Y \), \( x\in X \) and A2: \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \)proof
from A1 have \( \langle x,f(x)\rangle \in f \) using apply_iff
with A2 show \( thesis \)
qed

Identical meaning as ZF_fun_from_tot_val, but phrased a bit differently.

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) \) using assms , ZF_fun_from_tot_val

Another way of expressing that lambda expression is a function.

lemma lam_is_fun_range:

assumes \( f=\{\langle x,g(x)\rangle .\ x\in X\} \)

shows \( f:X\rightarrow \text{range}(f) \)proof
have \( \forall x\in X.\ g(x) \in \text{range}(\{\langle x,g(x)\rangle .\ x\in X\}) \) unfolding range_def
then have \( \{\langle x,g(x)\rangle .\ x\in X\} : X\rightarrow \text{range}(\{\langle x,g(x)\rangle .\ x\in X\}) \) by (rule ZF_fun_from_total )
with assms show \( thesis \)
qed

Yet another way of expressing value of a function.

lemma ZF_fun_from_tot_val1:

assumes \( x\in X \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \)proof
let \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
have \( f:X\rightarrow \text{range}(f) \) using lam_is_fun_range
with assms show \( thesis \) using ZF_fun_from_tot_val0
qed

We can extend a function by specifying its values on a set disjoint with the domain.

lemma func1_1_L11C:

assumes A1: \( f:X\rightarrow Y \) and A2: \( \forall x\in A.\ b(x)\in B \) and A3: \( X\cap A = 0 \) and Dg: \( g = f \cup \{\langle x,b(x)\rangle .\ x\in A\} \)

shows \( g : X\cup A \rightarrow Y\cup B \), \( \forall x\in X.\ g(x) = f(x) \), \( \forall x\in A.\ g(x) = b(x) \)proof
let \( h = \{\langle x,b(x)\rangle .\ x\in A\} \)
from A1, A2, A3 have I: \( f:X\rightarrow Y \), \( h : A\rightarrow B \), \( X\cap A = 0 \) using ZF_fun_from_total
then have \( f\cup h : X\cup A \rightarrow Y\cup B \) by (rule fun_disjoint_Un )
with Dg show \( g : X\cup A \rightarrow Y\cup B \)
{
fix \( x \)
assume A4: \( x\in A \)
with A1, A3 have \( (f\cup h)(x) = h(x) \) using func1_1_L1 , fun_disjoint_apply2
moreover
from I, A4 have \( h(x) = b(x) \) using ZF_fun_from_tot_val
ultimately have \( (f\cup h)(x) = b(x) \)
}
with Dg show \( \forall x\in A.\ g(x) = b(x) \)
{
fix \( x \)
assume A5: \( x\in X \)
with A3, I have \( x \notin domain(h) \) using func1_1_L1
then have \( (f\cup h)(x) = f(x) \) using fun_disjoint_apply1
}
with Dg show \( \forall x\in X.\ g(x) = f(x) \)
qed

We can extend a function by specifying its value at a point that does not belong to the domain.

lemma func1_1_L11D:

assumes A1: \( f:X\rightarrow Y \) and A2: \( a\notin X \) and Dg: \( g = f \cup \{\langle a,b\rangle \} \)

shows \( g : X\cup \{a\} \rightarrow Y\cup \{b\} \), \( \forall x\in X.\ g(x) = f(x) \), \( g(a) = b \)proof
let \( h = \{\langle a,b\rangle \} \)
from A1, A2, Dg have I: \( f:X\rightarrow Y \), \( \forall x\in \{a\}.\ b\in \{b\} \), \( X\cap \{a\} = 0 \), \( g = f \cup \{\langle x,b\rangle .\ x\in \{a\}\} \)
then show \( g : X\cup \{a\} \rightarrow Y\cup \{b\} \) by (rule func1_1_L11C )
from I show \( \forall x\in X.\ g(x) = f(x) \) by (rule func1_1_L11C )
from I have \( \forall x\in \{a\}.\ g(x) = b \) by (rule func1_1_L11C )
then show \( g(a) = b \)
qed

A technical lemma about extending a function both by defining on a set disjoint with the domain and on a point that does not belong to any of those sets.

lemma func1_1_L11E:

assumes A1: \( f:X\rightarrow Y \) and A2: \( \forall x\in A.\ b(x)\in B \) and A3: \( X\cap A = 0 \) and A4: \( a\notin X\cup A \) and Dg: \( g = f \cup \{\langle x,b(x)\rangle .\ x\in A\} \cup \{\langle a,c\rangle \} \)

shows \( g : X\cup A\cup \{a\} \rightarrow Y\cup B\cup \{c\} \), \( \forall x\in X.\ g(x) = f(x) \), \( \forall x\in A.\ g(x) = b(x) \), \( g(a) = c \)proof
let \( h = f \cup \{\langle x,b(x)\rangle .\ x\in A\} \)
from assms show \( g : X\cup A\cup \{a\} \rightarrow Y\cup B\cup \{c\} \) using func1_1_L11C , func1_1_L11D
from A1, A2, A3 have I: \( f:X\rightarrow Y \), \( \forall x\in A.\ b(x)\in B \), \( X\cap A = 0 \), \( h = f \cup \{\langle x,b(x)\rangle .\ x\in A\} \)
from assms have II: \( h : X\cup A \rightarrow Y\cup B \), \( a\notin X\cup A \), \( g = h \cup \{\langle a,c\rangle \} \) using func1_1_L11C
then have III: \( \forall x\in X\cup A.\ g(x) = h(x) \) by (rule func1_1_L11D )
moreover
from I have \( \forall x\in X.\ h(x) = f(x) \) by (rule func1_1_L11C )
ultimately show \( \forall x\in X.\ g(x) = f(x) \)
from I have \( \forall x\in A.\ h(x) = b(x) \) by (rule func1_1_L11C )
with III show \( \forall x\in A.\ g(x) = b(x) \)
from II show \( g(a) = c \) by (rule func1_1_L11D )
qed

A way of defining a function on a union of two possibly overlapping sets. We decompose the union into two differences and the intersection and define a function separately on each part.

lemma fun_union_overlap:

assumes \( \forall x\in A\cap B.\ h(x) \in Y \), \( \forall x\in A-B.\ f(x) \in Y \), \( \forall x\in B-A.\ g(x) \in Y \)

shows \( \{\langle x,if x\in A-B then f(x) else if x\in B-A then g(x) else h(x)\rangle .\ x \in A\cup B\}: A\cup B \rightarrow Y \)proof
let \( F = \{\langle x,if x\in A-B then f(x) else if x\in B-A then g(x) else h(x)\rangle .\ x \in A\cap B\} \)
from assms have \( \forall x\in A\cup B.\ (if x\in A-B then f(x) else if x\in B-A then g(x) else h(x)) \in Y \)
then show \( thesis \) by (rule ZF_fun_from_total )
qed

Inverse image of intersection is the intersection of inverse images.

lemma invim_inter_inter_invim:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A\cap B) = f^{-1}(A) \cap f^{-1}(B) \) using assms , fun_is_fun , function_vimage_Int

The inverse image of an intersection of a nonempty collection of sets is the intersection of the inverse images. This generalizes invim_inter_inter_invim which is proven for the case of two sets.

lemma func1_1_L12:

assumes A1: \( B \subseteq Pow(Y) \) and A2: \( B\neq 0 \) and A3: \( f:X\rightarrow Y \)

shows \( f^{-1}(\bigcap B) = (\bigcap U\in B.\ f^{-1}(U)) \)proof
from A2 show \( f^{-1}(\bigcap B) \subseteq (\bigcap U\in B.\ f^{-1}(U)) \)
show \( (\bigcap U\in B.\ f^{-1}(U)) \subseteq f^{-1}(\bigcap B) \)proof
fix \( x \)
assume A4: \( x \in (\bigcap U\in B.\ f^{-1}(U)) \)
from A3 have \( \forall U\in B.\ f^{-1}(U) \subseteq X \) using func1_1_L6A
with A4 have \( \forall U\in B.\ x\in X \)
with A2 have \( x\in X \)
with A3 have \( \exists !y.\ \langle x,y\rangle \in f \) using Pi_iff_old
with A2, A4 show \( x \in f^{-1}(\bigcap B) \) using vimage_iff
qed
qed

The inverse image of a set does not change when we intersect the set with the image of the domain.

lemma inv_im_inter_im:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A \cap f(X)) = f^{-1}(A) \) using assms , invim_inter_inter_invim , inv_im_dom , func1_1_L6A

If the inverse image of a set is not empty, then the set is not empty. Proof by contradiction.

lemma func1_1_L13:

assumes A1: \( f^{-1}(A) \neq 0 \)

shows \( A\neq 0 \) using assms

If the image of a set is not empty, then the set is not empty. Proof by contradiction.

lemma func1_1_L13A:

assumes A1: \( f(A)\neq 0 \)

shows \( A\neq 0 \) using assms

What is the inverse image of a singleton?

lemma func1_1_L14:

assumes \( f\in X\rightarrow Y \)

shows \( f^{-1}(\{y\}) = \{x\in X.\ f(x) = y\} \) using assms , func1_1_L6A , vimage_singleton_iff , apply_iff

A lemma that can be used instead fun_extension_iff to show that two functions are equal

lemma func_eq:

assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)

shows \( f = g \) using assms , fun_extension_iff

Function defined on a singleton is a single pair.

lemma func_singleton_pair:

assumes A1: \( f : \{a\}\rightarrow X \)

shows \( f = \{\langle a, f(a)\rangle \} \)proof
let \( g = \{\langle a, f(a)\rangle \} \)
note A1
moreover
have \( g : \{a\} \rightarrow \{f(a)\} \) using singleton_fun
moreover
have \( \forall x \in \{a\}.\ f(x) = g(x) \) using singleton_apply
ultimately show \( f = g \) by (rule func_eq )
qed

A single pair is a function on a singleton. This is similar to singleton_fun from standard Isabelle/ZF.

lemma pair_func_singleton:

assumes A1: \( y \in Y \)

shows \( \{\langle x,y\rangle \} : \{x\} \rightarrow Y \)proof
have \( \{\langle x,y\rangle \} : \{x\} \rightarrow \{y\} \) using singleton_fun
moreover
from A1 have \( \{y\} \subseteq Y \)
ultimately show \( \{\langle x,y\rangle \} : \{x\} \rightarrow Y \) by (rule func1_1_L1B )
qed

The value of a pair on the first element is the second one.

lemma pair_val:

shows \( \{\langle x,y\rangle \}(x) = y \) using singleton_fun , apply_equality

A more familiar definition of inverse image.

lemma func1_1_L15:

assumes A1: \( f:X\rightarrow Y \)

shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \)proof
have \( f^{-1}(A) = (\bigcup y\in A .\ f^{-1}\{y\}) \) by (rule vimage_eq_UN )
with A1 show \( thesis \) using func1_1_L14
qed

A more familiar definition of image.

lemma func_imagedef:

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

shows \( f(A) = \{f(x).\ x \in A\} \)proof
from A1 show \( f(A) \subseteq \{f(x).\ x \in A\} \) using image_iff , apply_iff
show \( \{f(x).\ x \in A\} \subseteq f(A) \)proof
fix \( y \)
assume \( y \in \{f(x).\ x \in A\} \)
then obtain \( x \) where \( x\in A \wedge y = f(x) \)
with A1, A2 show \( y \in f(A) \) using apply_iff , image_iff
qed
qed

The image of a set contained in domain under identity is the same set.

lemma image_id_same:

assumes \( A\subseteq X \)

shows \( id(X)(A) = A \) using assms , id_type , id_conv

The inverse image of a set contained in domain under identity is the same set.

lemma vimage_id_same:

assumes \( A\subseteq X \)

shows \( id(X)^{-1}(A) = A \) using assms , id_type , id_conv

What is the image of a singleton?

lemma singleton_image:

assumes \( f\in X\rightarrow Y \) and \( x\in X \)

shows \( f\{x\} = \{f(x)\} \) using assms , func_imagedef

If an element of the domain of a function belongs to a set, then its value belongs to the imgage of that set.

lemma func1_1_L15D:

assumes \( f:X\rightarrow Y \), \( x\in A \), \( A\subseteq X \)

shows \( f(x) \in f(A) \) using assms , func_imagedef

Range is the image of the domain. Isabelle/ZF defines \( \text{range}(f) \) as \( domain(converse(f)) \), and that's why we have something to prove here.

lemma range_image_domain:

assumes A1: \( f:X\rightarrow Y \)

shows \( f(X) = \text{range}(f) \)proof
show \( f(X) \subseteq \text{range}(f) \) using image_def
{
fix \( y \)
assume \( y \in \text{range}(f) \)
then obtain \( x \) where \( \langle y,x\rangle \in converse(f) \)
with A1 have \( x\in X \) using func1_1_L5
with A1 have \( f(x) \in f(X) \) using func_imagedef
with A1, \( \langle y,x\rangle \in converse(f) \) have \( y \in f(X) \) using apply_equality
}
then show \( \text{range}(f) \subseteq f(X) \)
qed

The difference of images is contained in the image of difference.

lemma diff_image_diff:

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

shows \( f(X) - f(A) \subseteq f(X-A) \)proof
fix \( y \)
assume \( y \in f(X) - f(A) \)
hence \( y \in f(X) \) and I: \( y \notin f(A) \)
with A1 obtain \( x \) where \( x\in X \) and II: \( y = f(x) \) using func_imagedef
with A1, A2, I have \( x\notin A \) using func1_1_L15D
with \( x\in X \) have \( x \in X-A \), \( X-A \subseteq X \)
with A1, II show \( y \in f(X-A) \) using func1_1_L15D
qed

The image of an intersection is contained in the intersection of the images.

lemma image_of_Inter:

assumes A1: \( f:X\rightarrow Y \) and A2: \( I\neq 0 \) and A3: \( \forall i\in I.\ P(i) \subseteq X \)

shows \( f(\bigcap i\in I.\ P(i)) \subseteq ( \bigcap i\in I.\ f(P(i)) ) \)proof
fix \( y \)
assume A4: \( y \in f(\bigcap i\in I.\ P(i)) \)
from A1, A2, A3 have \( f(\bigcap i\in I.\ P(i)) = \{f(x).\ x \in ( \bigcap i\in I.\ P(i) )\} \) using ZF1_1_L7 , func_imagedef
with A4 obtain \( x \) where \( x \in ( \bigcap i\in I.\ P(i) ) \) and \( y = f(x) \)
with A1, A2, A3 show \( y \in ( \bigcap i\in I.\ f(P(i)) ) \) using func_imagedef
qed

The image of union is the union of images.

lemma image_of_Union:

assumes A1: \( f:X\rightarrow Y \) and A2: \( \forall A\in M.\ A\subseteq X \)

shows \( f(\bigcup M) = \bigcup \{f(A).\ A\in M\} \)proof
from A2 have \( \bigcup M \subseteq X \)
{
fix \( y \)
assume \( y \in f(\bigcup M) \)
with A1, \( \bigcup M \subseteq X \) obtain \( x \) where \( x\in \bigcup M \) and I: \( y = f(x) \) using func_imagedef
then obtain \( A \) where \( A\in M \) and \( x\in A \)
with assms, I have \( y \in \bigcup \{f(A).\ A\in M\} \) using func_imagedef
}
thus \( f(\bigcup M) \subseteq \bigcup \{f(A).\ A\in M\} \)
{
fix \( y \)
assume \( y \in \bigcup \{f(A).\ A\in M\} \)
then obtain \( A \) where \( A\in M \) and \( y \in f(A) \)
with assms, \( \bigcup M \subseteq X \) have \( y \in f(\bigcup M) \) using func_imagedef
}
thus \( \bigcup \{f(A).\ A\in M\} \subseteq f(\bigcup M) \)
qed

The image of a nonempty subset of domain is nonempty.

lemma func1_1_L15A:

assumes A1: \( f: X\rightarrow Y \) and A2: \( A\subseteq X \) and A3: \( A\neq 0 \)

shows \( f(A) \neq 0 \)proof
from A3 obtain \( x \) where \( x\in A \)
with A1, A2 have \( f(x) \in f(A) \) using func_imagedef
then show \( f(A) \neq 0 \)
qed

The next lemma allows to prove statements about the values in the domain of a function given a statement about values in the range.

lemma func1_1_L15B:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall y\in f(A).\ P(y) \)

shows \( \forall x\in A.\ P(f(x)) \) using assms , func_imagedef

An image of an image is the image of a composition.

lemma func1_1_L15C:

assumes A1: \( f:X\rightarrow Y \) and A2: \( g:Y\rightarrow Z \) and A3: \( A\subseteq X \)

shows \( g(f(A)) = \{g(f(x)).\ x\in A\} \), \( g(f(A)) = (g\circ f)(A) \)proof
from A1, A3 have \( \{f(x).\ x\in A\} \subseteq Y \) using apply_funtype
with A2 have \( g\{f(x).\ x\in A\} = \{g(f(x)).\ x\in A\} \) using func_imagedef
with A1, A3 show I: \( g(f(A)) = \{g(f(x)).\ x\in A\} \) using func_imagedef
from A1, A3 have \( \forall x\in A.\ (g\circ f)(x) = g(f(x)) \) using comp_fun_apply
with I have \( g(f(A)) = \{(g\circ f)(x).\ x\in A\} \)
moreover
from A1, A2, A3 have \( (g\circ f)(A) = \{(g\circ f)(x).\ x\in A\} \) using comp_fun , func_imagedef
ultimately show \( g(f(A)) = (g\circ f)(A) \)
qed

What is the image of a set defined by a meta-fuction?

lemma func1_1_L17:

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

shows \( f(\{b(x).\ x\in A\}) = \{f(b(x)).\ x\in A\} \)proof
from A2 have \( \{b(x).\ x\in A\} \subseteq X \)
with A1 show \( thesis \) using func_imagedef
qed

What are the values of composition of three functions?

lemma func1_1_L18:

assumes A1: \( f:A\rightarrow B \), \( g:B\rightarrow C \), \( h:C\rightarrow D \) and A2: \( x\in A \)

shows \( (h\circ g\circ f)(x) \in D \), \( (h\circ g\circ f)(x) = h(g(f(x))) \)proof
from A1 have \( (h\circ g\circ f) : A\rightarrow D \) using comp_fun
with A2 show \( (h\circ g\circ f)(x) \in D \) using apply_funtype
from A1, A2 have \( (h\circ g\circ f)(x) = h( (g\circ f)(x)) \) using comp_fun , comp_fun_apply
with A1, A2 show \( (h\circ g\circ f)(x) = h(g(f(x))) \) using comp_fun_apply
qed

A composition of functions is a function. This is a slight generalization of standard Isabelle's comp_fun

lemma comp_fun_subset:

assumes A1: \( g:A\rightarrow B \) and A2: \( f:C\rightarrow D \) and A3: \( B \subseteq C \)

shows \( f\circ g : A \rightarrow D \)proof
from A1, A3 have \( g:A\rightarrow C \) by (rule func1_1_L1B )
with A2 show \( f\circ g : A \rightarrow D \) using comp_fun
qed

This lemma supersedes the lemma comp_eq_id_iff in Isabelle/ZF. Contributed by Victor Porton.

lemma comp_eq_id_iff1:

assumes A1: \( g: B\rightarrow A \) and A2: \( f: A\rightarrow C \)

shows \( (\forall y\in B.\ f(g(y)) = y) \longleftrightarrow f\circ g = id(B) \)proof
from assms have \( f\circ g: B\rightarrow C \) and \( id(B): B\rightarrow B \) using comp_fun , id_type
then have \( (\forall y\in B.\ (f\circ g)y = id(B)(y)) \longleftrightarrow f\circ g = id(B) \) by (rule fun_extension_iff )
moreover
from A1 have \( \forall y\in B.\ (f\circ g)y = f(gy) \) and \( \forall y\in B.\ id(B)(y) = y \)
ultimately show \( (\forall y\in B.\ f(gy) = y) \longleftrightarrow f\circ g = id(B) \)
qed

A lemma about a value of a function that is a union of some collection of functions.

lemma fun_Union_apply:

assumes A1: \( \bigcup F : X\rightarrow Y \) and A2: \( f\in F \) and A3: \( f:A\rightarrow B \) and A4: \( x\in A \)

shows \( (\bigcup F)(x) = f(x) \)proof
from A3, A4 have \( \langle x, f(x)\rangle \in f \) using apply_Pair
with A2 have \( \langle x, f(x)\rangle \in \bigcup F \)
with A1 show \( (\bigcup F)(x) = f(x) \) using apply_equality
qed

Functions restricted to a set

Standard Isabelle/ZF defines the notion \( \text{restrict}(f,A) \) of to mean a function (or relation) \(f\) restricted to a set. This means that if \(f\) is a function defined on \(X\) and \(A\) is a subset of \(X\) then \( \text{restrict}(f,A) \) is a function whith the same values as \(f\), but whose domain is \(A\).

What is the inverse image of a set under a restricted fuction?

lemma func1_2_L1:

assumes A1: \( f:X\rightarrow Y \) and A2: \( B\subseteq X \)

shows \( \text{restrict}(f,B)^{-1}(A) = f^{-1}(A) \cap B \)proof
let \( g = \text{restrict}(f,B) \)
from A1, A2 have \( g:B\rightarrow Y \) using restrict_type2
with A2, A1 show \( g^{-1}(A) = f^{-1}(A) \cap B \) using func1_1_L15 , restrict_if
qed

A criterion for when one function is a restriction of another. The lemma below provides a result useful in the actual proof of the criterion and applications.

lemma func1_2_L2:

assumes A1: \( f:X\rightarrow Y \) and A2: \( g \in A\rightarrow Z \) and A3: \( A\subseteq X \) and A4: \( f \cap A\times Z = g \)

shows \( \forall x\in A.\ g(x) = f(x) \)proof
fix \( x \)
assume \( x\in A \)
with A2 have \( \langle x,g(x)\rangle \in g \) using apply_Pair
with A4, A1 show \( g(x) = f(x) \) using apply_iff
qed

Here is the actual criterion.

lemma func1_2_L3:

assumes A1: \( f:X\rightarrow Y \) and A2: \( g:A\rightarrow Z \) and A3: \( A\subseteq X \) and A4: \( f \cap A\times Z = g \)

shows \( g = \text{restrict}(f,A) \)proof
from A4 show \( g \subseteq \text{restrict}(f, A) \) using restrict_iff
show \( \text{restrict}(f, A) \subseteq g \)proof
fix \( z \)
assume A5: \( z \in \text{restrict}(f,A) \)
then obtain \( x \) \( y \) where D1: \( z\in f \wedge x\in A \wedge z = \langle x,y\rangle \) using restrict_iff
with A1 have \( y = f(x) \) using apply_iff
with A1, A2, A3, A4, D1 have \( y = g(x) \) using func1_2_L2
with A2, D1 show \( z\in g \) using apply_Pair
qed
qed

Which function space a restricted function belongs to?

lemma func1_2_L4:

assumes A1: \( f:X\rightarrow Y \) and A2: \( A\subseteq X \) and A3: \( \forall x\in A.\ f(x) \in Z \)

shows \( \text{restrict}(f,A) : A\rightarrow Z \)proof
let \( g = \text{restrict}(f,A) \)
from A1, A2 have \( g : A\rightarrow Y \) using restrict_type2
moreover {
fix \( x \)
assume \( x\in A \)
with A1, A3 have \( g(x) \in Z \) using restrict
} ultimately show \( thesis \) by (rule Pi_type )
qed

A simpler case of func1_2_L4, where the range of the original and restricted function are the same.

corollary restrict_fun:

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

shows \( \text{restrict}(f,A) : A \rightarrow Y \)proof
from assms have \( \forall x\in A.\ f(x) \in Y \) using apply_funtype
with assms show \( thesis \) using func1_2_L4
qed

A composition of two functions is the same as composition with a restriction.

lemma comp_restrict:

assumes A1: \( f : A\rightarrow B \) and A2: \( g : X \rightarrow C \) and A3: \( B\subseteq X \)

shows \( g\circ f = \text{restrict}(g,B)\circ f \)proof
from assms have \( g\circ f : A \rightarrow C \) using comp_fun_subset
moreover
from assms have \( \text{restrict}(g,B)\circ f : A \rightarrow C \) using restrict_fun , comp_fun
moreover
from A1 have \( \forall x\in A.\ (g\circ f)(x) = (\text{restrict}(g,B)\circ f)(x) \) using comp_fun_apply , apply_funtype , restrict
ultimately show \( g\circ f = \text{restrict}(g,B)\circ f \) by (rule func_eq )
qed

A way to look at restriction. Contributed by Victor Porton.

lemma right_comp_id_any:

shows \( r\circ id(C) = \text{restrict}(r,C) \) unfolding restrict_def

Constant functions

Constant functions are trivial, but still we need to prove some properties to shorten proofs.

We define constant(\(=c\)) functions on a set \(X\) in a natural way as ConstantFunction\((X,c)\).

Definition

\( \text{ConstantFunction}(X,c) \equiv X\times \{c\} \)

Constant function belongs to the function space.

lemma func1_3_L1:

assumes A1: \( c\in Y \)

shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \)proof
from A1 have \( X\times \{c\} = \{\langle x,y\rangle \in X\times Y.\ c = y\} \)
with A1 show \( thesis \) using func1_1_L11A , ConstantFunction_def
qed

Constant function is equal to the constant on its domain.

lemma func1_3_L2:

assumes A1: \( x\in X \)

shows \( \text{ConstantFunction}(X,c)(x) = c \)proof
have \( \text{ConstantFunction}(X,c) \in X\rightarrow \{c\} \) using func1_3_L1
moreover
from A1 have \( \langle x,c\rangle \in \text{ConstantFunction}(X,c) \) using ConstantFunction_def
ultimately show \( thesis \) using apply_iff
qed

Injections, surjections, bijections etc.

In this section we prove the properties of the spaces of injections, surjections and bijections that we can't find in the standard Isabelle's Perm.thy.

For injections the image a difference of two sets is the difference of images

lemma inj_image_dif:

assumes A1: \( f \in \text{inj}(A,B) \) and A2: \( C \subseteq A \)

shows \( f(A-C) = f(A) - f(C) \)proof
show \( f(A - C) \subseteq f(A) - f(C) \)proof
fix \( y \)
assume A3: \( y \in f(A - C) \)
from A1 have \( f:A\rightarrow B \) using inj_def
moreover
have \( A-C \subseteq A \)
ultimately have \( f(A-C) = \{f(x).\ x \in A-C\} \) using func_imagedef
with A3 obtain \( x \) where I: \( f(x) = y \) and \( x \in A-C \)
hence \( x\in A \)
with \( f:A\rightarrow B \), I have \( y \in f(A) \) using func_imagedef
moreover
have \( y \notin f(C) \)proof
{
assume \( y \in f(C) \)
with A2, \( f:A\rightarrow B \) obtain \( x_0 \) where II: \( f(x_0) = y \) and \( x_0 \in C \) using func_imagedef
with A1, A2, I, \( x\in A \) have \( f \in \text{inj}(A,B) \), \( f(x) = f(x_0) \), \( x\in A \), \( x_0 \in A \)
then have \( x = x_0 \) by (rule inj_apply_equality )
with \( x \in A-C \), \( x_0 \in C \) have \( False \)
}
thus \( thesis \)
qed
ultimately show \( y \in f(A) - f(C) \)
qed
from A1, A2 show \( f(A) - f(C) \subseteq f(A-C) \) using inj_def , diff_image_diff
qed

For injections the image of intersection is the intersection of images.

lemma inj_image_inter:

assumes A1: \( f \in \text{inj}(X,Y) \) and A2: \( A\subseteq X \), \( B\subseteq X \)

shows \( f(A\cap B) = f(A) \cap f(B) \)proof
show \( f(A\cap B) \subseteq f(A) \cap f(B) \) using image_Int_subset
{
from A1 have \( f:X\rightarrow Y \) using inj_def
fix \( y \)
assume \( y \in f(A) \cap f(B) \)
then have \( y \in f(A) \) and \( y \in f(B) \)
with A2, \( f:X\rightarrow Y \) obtain \( x_A \) \( x_B \) where \( x_A \in A \), \( x_B \in B \) and I: \( y = f(x_A) \), \( y = f(x_B) \) using func_imagedef
with A2 have \( x_A \in X \), \( x_B \in X \) and \( f(x_A) = f(x_B) \)
with A1 have \( x_A = x_B \) using inj_def
with \( x_A \in A \), \( x_B \in B \) have \( f(x_A) \in \{f(x).\ x \in A\cap B\} \)
moreover
from A2, \( f:X\rightarrow Y \) have \( f(A\cap B) = \{f(x).\ x \in A\cap B\} \) using func_imagedef
ultimately have \( f(x_A) \in f(A\cap B) \)
with I have \( y \in f(A\cap B) \)
}
thus \( f(A) \cap f(B) \subseteq f(A \cap B) \)
qed

For surjection from \(A\) to \(B\) the image of the domain is \(B\).

lemma surj_range_image_domain:

assumes A1: \( f \in \text{surj}(A,B) \)

shows \( f(A) = B \)proof
from A1 have \( f(A) = \text{range}(f) \) using surj_def , range_image_domain
with A1 show \( f(A) = B \) using surj_range
qed

For injections the inverse image of an image is the same set.

lemma inj_vimage_image:

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

shows \( f^{-1}(f(A)) = A \)proof
have \( f^{-1}(f(A)) = (converse(f)\circ f)(A) \) using vimage_converse , image_comp
with assms show \( thesis \) using left_comp_inverse , image_id_same
qed

For surjections the image of an inverse image is the same set.

lemma surj_image_vimage:

assumes A1: \( f \in \text{surj}(X,Y) \) and A2: \( A\subseteq Y \)

shows \( f(f^{-1}(A)) = A \)proof
have \( f(f^{-1}(A)) = (f\circ converse(f))(A) \) using vimage_converse , image_comp
with assms show \( thesis \) using right_comp_inverse , image_id_same
qed

A lemma about how a surjection maps collections of subsets in domain and rangge.

lemma surj_subsets:

assumes A1: \( f \in \text{surj}(X,Y) \) and A2: \( B \subseteq Pow(Y) \)

shows \( \{ f(U).\ U \in \{f^{-1}(V).\ V\in B\} \} = B \)proof
{
fix \( W \)
assume \( W \in \{ f(U).\ U \in \{f^{-1}(V).\ V\in B\} \} \)
then obtain \( U \) where I: \( U \in \{f^{-1}(V).\ V\in B\} \) and II: \( W = f(U) \)
then obtain \( V \) where \( V\in B \) and \( U = f^{-1}(V) \)
with II have \( W = f(f^{-1}(V)) \)
moreover
from assms, \( V\in B \) have \( f \in \text{surj}(X,Y) \) and \( V\subseteq Y \)
ultimately have \( W=V \) using surj_image_vimage
with \( V\in B \) have \( W \in B \)
}
thus \( \{ f(U).\ U \in \{f^{-1}(V).\ V\in B\} \} \subseteq B \)
{
fix \( W \)
assume \( W\in B \)
let \( U = f^{-1}(W) \)
from \( W\in B \) have \( U \in \{f^{-1}(V).\ V\in B\} \)
moreover
from A1, A2, \( W\in B \) have \( W = f(U) \) using surj_image_vimage
ultimately have \( W \in \{ f(U).\ U \in \{f^{-1}(V).\ V\in B\} \} \)
}
thus \( B \subseteq \{ f(U).\ U \in \{f^{-1}(V).\ V\in B\} \} \)
qed

Restriction of an bijection to a set without a point is a a bijection.

lemma bij_restrict_rem:

assumes A1: \( f \in \text{bij}(A,B) \) and A2: \( a\in A \)

shows \( \text{restrict}(f, A-\{a\}) \in \text{bij}(A-\{a\}, B-\{f(a)\}) \)proof
let \( C = A-\{a\} \)
from A1 have \( f \in \text{inj}(A,B) \), \( C \subseteq A \) using bij_def
then have \( \text{restrict}(f,C) \in \text{bij}(C, f(C)) \) using restrict_bij
moreover
have \( f(C) = B-\{f(a)\} \)proof
from A2, \( f \in \text{inj}(A,B) \) have \( f(C) = f(A) - f\{a\} \) using inj_image_dif
moreover
from A1 have \( f(A) = B \) using bij_def , surj_range_image_domain
moreover
from A1, A2 have \( f\{a\} = \{f(a)\} \) using bij_is_fun , singleton_image
ultimately show \( f(C) = B-\{f(a)\} \)
qed
ultimately show \( thesis \)
qed

The domain of a bijection between \(X\) and \(Y\) is \(X\).

lemma domain_of_bij:

assumes A1: \( f \in \text{bij}(X,Y) \)

shows \( domain(f) = X \)proof
from A1 have \( f:X\rightarrow Y \) using bij_is_fun
then show \( domain(f) = X \) using func1_1_L1
qed

The value of the inverse of an injection on a point of the image of a set belongs to that set.

lemma inj_inv_back_in_set:

assumes A1: \( f \in \text{inj}(A,B) \) and A2: \( C\subseteq A \) and A3: \( y \in f(C) \)

shows \( converse(f)(y) \in C \), \( f(converse(f)(y)) = y \)proof
from A1 have I: \( f:A\rightarrow B \) using inj_is_fun
with A2, A3 obtain \( x \) where II: \( x\in C \), \( y = f(x) \) using func_imagedef
with A1, A2 show \( converse(f)(y) \in C \) using left_inverse
from A1, A2, I, II show \( f(converse(f)(y)) = y \) using func1_1_L5A , right_inverse
qed

For injections if a value at a point belongs to the image of a set, then the point belongs to the set.

lemma inj_point_of_image:

assumes A1: \( f \in \text{inj}(A,B) \) and A2: \( C\subseteq A \) and A3: \( x\in A \) and A4: \( f(x) \in f(C) \)

shows \( x \in C \)proof
from A1, A2, A4 have \( converse(f)(f(x)) \in C \) using inj_inv_back_in_set
moreover
from A1, A3 have \( converse(f)(f(x)) = x \) using left_inverse_eq
ultimately show \( x \in C \)
qed

For injections the image of intersection is the intersection of images.

lemma inj_image_of_Inter:

assumes A1: \( f \in \text{inj}(A,B) \) and A2: \( I\neq 0 \) and A3: \( \forall i\in I.\ P(i) \subseteq A \)

shows \( f(\bigcap i\in I.\ P(i)) = ( \bigcap i\in I.\ f(P(i)) ) \)proof
from A1, A2, A3 show \( f(\bigcap i\in I.\ P(i)) \subseteq ( \bigcap i\in I.\ f(P(i)) ) \) using inj_is_fun , image_of_Inter
from A1, A2, A3 have \( f:A\rightarrow B \) and \( ( \bigcap i\in I.\ P(i) ) \subseteq A \) using inj_is_fun , ZF1_1_L7
then have I: \( f(\bigcap i\in I.\ P(i)) = \{ f(x).\ x \in ( \bigcap i\in I.\ P(i) ) \} \) using func_imagedef
{
fix \( y \)
assume A4: \( y \in ( \bigcap i\in I.\ f(P(i)) ) \)
let \( x = converse(f)(y) \)
from A2 obtain \( i_0 \) where \( i_0 \in I \)
with A1, A4 have II: \( y \in \text{range}(f) \) using inj_is_fun , func1_1_L6
with A1 have III: \( f(x) = y \) using right_inverse
from A1, II have IV: \( x \in A \) using inj_converse_fun , apply_funtype
{
fix \( i \)
assume \( i\in I \)
with A3, A4, III have \( P(i) \subseteq A \) and \( f(x) \in f(P(i)) \)
with A1, IV have \( x \in P(i) \) using inj_point_of_image
}
then have \( \forall i\in I.\ x \in P(i) \)
with A2, I have \( f(x) \in f( \bigcap i\in I.\ P(i) ) \)
with III have \( y \in f( \bigcap i\in I.\ P(i) ) \)
}
then show \( ( \bigcap i\in I.\ f(P(i)) ) \subseteq f( \bigcap i\in I.\ P(i) ) \)
qed

An injection is injective onto its range. Suggested by Victor Porton.

lemma inj_inj_range:

assumes \( f \in \text{inj}(A,B) \)

shows \( f \in \text{inj}(A,\text{range}(f)) \) using assms , inj_def , range_of_fun

An injection is a bijection on its range. Suggested by Victor Porton.

lemma inj_bij_range:

assumes \( f \in \text{inj}(A,B) \)

shows \( f \in \text{bij}(A,\text{range}(f)) \)proof
from assms have \( f \in \text{surj}(A,\text{range}(f)) \) using inj_def , fun_is_surj
with assms show \( thesis \) using inj_inj_range , bij_def
qed

A lemma about extending a surjection by one point.

lemma surj_extend_point:

assumes A1: \( f \in \text{surj}(X,Y) \) and A2: \( a\notin X \) and A3: \( g = f \cup \{\langle a,b\rangle \} \)

shows \( g \in \text{surj}(X\cup \{a\},Y\cup \{b\}) \)proof
from A1, A2, A3 have \( g : X\cup \{a\} \rightarrow Y\cup \{b\} \) using surj_def , func1_1_L11D
moreover
have \( \forall y \in Y\cup \{b\}.\ \exists x \in X\cup \{a\}.\ y = g(x) \)proof
fix \( y \)
assume \( y \in Y \cup \{b\} \)
then have \( y \in Y \vee y = b \)
moreover {
assume \( y \in Y \)
with A1 obtain \( x \) where \( x\in X \) and \( y = f(x) \) using surj_def
with A1, A2, A3 have \( x \in X\cup \{a\} \) and \( y = g(x) \) using surj_def , func1_1_L11D
then have \( \exists x \in X\cup \{a\}.\ y = g(x) \)
} moreover {
assume \( y = b \)
with A1, A2, A3 have \( y = g(a) \) using surj_def , func1_1_L11D
then have \( \exists x \in X\cup \{a\}.\ y = g(x) \)
} ultimately show \( \exists x \in X\cup \{a\}.\ y = g(x) \)
qed
ultimately show \( g \in \text{surj}(X\cup \{a\},Y\cup \{b\}) \) using surj_def
qed

A lemma about extending an injection by one point. Essentially the same as standard Isabelle's inj_extend.

lemma inj_extend_point:

assumes \( f \in \text{inj}(X,Y) \), \( a\notin X \), \( b\notin Y \)

shows \( (f \cup \{\langle a,b\rangle \}) \in \text{inj}(X\cup \{a\},Y\cup \{b\}) \)proof
from assms have \( cons(\langle a,b\rangle ,f) \in \text{inj}(cons(a, X), cons(b, Y)) \) using assms , inj_extend
moreover
have \( cons(\langle a,b\rangle ,f) = f \cup \{\langle a,b\rangle \} \) and \( cons(a, X) = X\cup \{a\} \) and \( cons(b, Y) = Y\cup \{b\} \)
ultimately show \( thesis \)
qed

A lemma about extending a bijection by one point.

lemma bij_extend_point:

assumes \( f \in \text{bij}(X,Y) \), \( a\notin X \), \( b\notin Y \)

shows \( (f \cup \{\langle a,b\rangle \}) \in \text{bij}(X\cup \{a\},Y\cup \{b\}) \) using assms , surj_extend_point , inj_extend_point , bij_def

A quite general form of the \(a^{-1}b = 1\) implies \(a=b\) law.

lemma comp_inv_id_eq:

assumes A1: \( converse(b)\circ a = id(A) \) and A2: \( a \subseteq A\times B \), \( b \in \text{surj}(A,B) \)

shows \( a = b \)proof
from A1 have \( (b\circ converse(b))\circ a = b\circ id(A) \) using comp_assoc
with A2 have \( id(B)\circ a = b\circ id(A) \) using right_comp_inverse
moreover
from A2 have \( a \subseteq A\times B \) and \( b \subseteq A\times B \) using surj_def , fun_subset_prod
then have \( id(B)\circ a = a \) and \( b\circ id(A) = b \) using left_comp_id , right_comp_id
ultimately show \( a = b \)
qed

A special case of comp_inv_id_eq - the \(a^{-1}b = 1\) implies \(a=b\) law for bijections.

lemma comp_inv_id_eq_bij:

assumes A1: \( a \in \text{bij}(A,B) \), \( b \in \text{bij}(A,B) \) and A2: \( converse(b)\circ a = id(A) \)

shows \( a = b \)proof
from A1 have \( a \subseteq A\times B \) and \( b \in \text{surj}(A,B) \) using bij_def , surj_def , fun_subset_prod
with A2 show \( a = b \) by (rule comp_inv_id_eq )
qed

Converse of a converse of a bijection the same bijection. This is a special case of converse_converse from standard Isabelle's equalities theory where it is proved for relations.

lemma bij_converse_converse:

assumes \( a \in \text{bij}(A,B) \)

shows \( converse(converse(a)) = a \)proof
from assms have \( a \subseteq A\times B \) using bij_def , surj_def , fun_subset_prod
then show \( thesis \) using converse_converse
qed

If a composition of bijections is identity, then one is the inverse of the other.

lemma comp_id_conv:

assumes A1: \( a \in \text{bij}(A,B) \), \( b \in \text{bij}(B,A) \) and A2: \( b\circ a = id(A) \)

shows \( a = converse(b) \) and \( b = converse(a) \)proof
from A1 have \( a \in \text{bij}(A,B) \) and \( converse(b) \in \text{bij}(A,B) \) using bij_converse_bij
moreover
from assms have \( converse(converse(b))\circ a = id(A) \) using bij_converse_converse
ultimately show \( a = converse(b) \) by (rule comp_inv_id_eq_bij )
with assms show \( b = converse(a) \) using bij_converse_converse
qed

A version of comp_id_conv with weaker assumptions.

lemma comp_conv_id:

assumes A1: \( a \in \text{bij}(A,B) \) and A2: \( b:B\rightarrow A \) and A3: \( \forall x\in A.\ b(a(x)) = x \)

shows \( b \in \text{bij}(B,A) \) and \( a = converse(b) \) and \( b = converse(a) \)proof
have \( b \in \text{surj}(B,A) \)proof
have \( \forall x\in A.\ \exists y\in B.\ b(y) = x \)proof
{
fix \( x \)
assume \( x\in A \)
let \( y = a(x) \)
from A1, A3, \( x\in A \) have \( y\in B \) and \( b(y) = x \) using bij_def , inj_def , apply_funtype
hence \( \exists y\in B.\ b(y) = x \)
}
thus \( thesis \)
qed
with A2 show \( b \in \text{surj}(B,A) \) using surj_def
qed
moreover
have \( b \in \text{inj}(B,A) \)proof
have \( \forall w\in B.\ \forall y\in B.\ b(w) = b(y) \longrightarrow w=y \)proof
{
fix \( w \) \( y \)
assume \( w\in B \), \( y\in B \) and I: \( b(w) = b(y) \)
from A1 have \( a \in \text{surj}(A,B) \) unfolding bij_def
with \( w\in B \) obtain \( x_w \) where \( x_w \in A \) and II: \( a(x_w) = w \) using surj_def
with I have \( b(a(x_w)) = b(y) \)
moreover
from \( a \in \text{surj}(A,B) \), \( y\in B \) obtain \( x_y \) where \( x_y \in A \) and III: \( a(x_y) = y \) using surj_def
moreover
from A3, \( x_w \in A \), \( x_y \in A \) have \( b(a(x_w)) = x_w \) and \( b(a(x_y)) = x_y \)
ultimately have \( x_w = x_y \)
with II, III have \( w=y \)
}
thus \( thesis \)
qed
with A2 show \( b \in \text{inj}(B,A) \) using inj_def
qed
ultimately show \( b \in \text{bij}(B,A) \) using bij_def
from assms have \( b\circ a = id(A) \) using bij_def , inj_def , comp_eq_id_iff1
with A1, \( b \in \text{bij}(B,A) \) show \( a = converse(b) \) and \( b = converse(a) \) using comp_id_conv
qed

For a surjection the union if images of singletons is the whole range.

lemma surj_singleton_image:

assumes A1: \( f \in \text{surj}(X,Y) \)

shows \( (\bigcup x\in X.\ \{f(x)\}) = Y \)proof
from A1 show \( (\bigcup x\in X.\ \{f(x)\}) \subseteq Y \) using surj_def , apply_funtype
next
{
fix \( y \)
assume \( y \in Y \)
with A1 have \( y \in (\bigcup x\in X.\ \{f(x)\}) \) using surj_def
}
then show \( Y \subseteq (\bigcup x\in X.\ \{f(x)\}) \)
qed

Functions of two variables

In this section we consider functions whose domain is a cartesian product of two sets. Such functions are called functions of two variables (although really in ZF all functions admit only one argument). For every function of two variables we can define families of functions of one variable by fixing the other variable. This section establishes basic definitions and results for this concept.

We can create functions of two variables by combining functions of one variable.

lemma cart_prod_fun:

assumes \( f_1:X_1\rightarrow Y_1 \), \( f_2:X_2\rightarrow Y_2 \) and \( g = \{\langle p,\langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in X_1\times X_2\} \)

shows \( g: X_1\times X_2 \rightarrow Y_1\times Y_2 \) using assms , apply_funtype , ZF_fun_from_total

A reformulation of cart_prod_fun above in a sligtly different notation.

lemma prod_fun:

assumes \( f:X_1\rightarrow X_2 \), \( g:X_3\rightarrow X_4 \)

shows \( \{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times X_3\}:X_1\times X_3\rightarrow X_2\times X_4 \)proof
have \( \{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times X_3\} = \{\langle p,\langle f(\text{fst}(p)),g(\text{snd}(p))\rangle \rangle .\ p \in X_1\times X_3\} \)
with assms show \( thesis \) using cart_prod_fun
qed

Product of two surjections is a surjection.

theorem prod_functions_surj:

assumes \( f\in \text{surj}(A,B) \), \( g\in \text{surj}(C,D) \)

shows \( \{\langle \langle a1,a2\rangle ,\langle fa1,ga2\rangle \rangle .\ \langle a1,a2\rangle \in A\times C\} \in \text{surj}(A\times C,B\times D) \)proof
let \( h = \{\langle \langle x, y\rangle , f(x), g(y)\rangle .\ \langle x,y\rangle \in A \times C\} \)
from assms have fun: \( f:A\rightarrow B \), \( g:C\rightarrow D \) unfolding surj_def
then have pfun: \( h : A \times C \rightarrow B \times D \) using prod_fun
{
fix \( b \)
assume \( b\in B\times D \)
then obtain \( b1 \) \( b2 \) where \( b=\langle b1,b2\rangle \), \( b1\in B \), \( b2\in D \)
with assms obtain \( a1 \) \( a2 \) where \( f(a1)=b1 \), \( g(a2)=b2 \), \( a1\in A \), \( a2\in C \) unfolding surj_def
hence \( \langle \langle a1,a2\rangle ,\langle b1,b2\rangle \rangle \in h \)
with pfun have \( h\langle a1,a2\rangle =\langle b1,b2\rangle \) using apply_equality
with \( b=\langle b1,b2\rangle \), \( a1\in A \), \( a2\in C \) have \( \exists a\in A\times C.\ h(a)=b \)
}
hence \( \forall b\in B\times D.\ \exists a\in A\times C.\ h(a) = b \)
with pfun show \( thesis \) unfolding surj_def
qed

For a function of two variables created from functions of one variable as in cart_prod_fun above, the inverse image of a cartesian product of sets is the cartesian product of inverse images.

lemma cart_prod_fun_vimage:

assumes \( f_1:X_1\rightarrow Y_1 \), \( f_2:X_2\rightarrow Y_2 \) and \( g = \{\langle p,\langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in X_1\times X_2\} \)

shows \( g^{-1}(A_1\times A_2) = f_1^{-1}(A_1) \times f_2^{-1}(A_2) \)proof
from assms have \( g: X_1\times X_2 \rightarrow Y_1\times Y_2 \) using cart_prod_fun
then have \( g^{-1}(A_1\times A_2) = \{p \in X_1\times X_2.\ g(p) \in A_1\times A_2\} \) using func1_1_L15
with assms, \( g: X_1\times X_2 \rightarrow Y_1\times Y_2 \) show \( g^{-1}(A_1\times A_2) = f_1^{-1}(A_1) \times f_2^{-1}(A_2) \) using ZF_fun_from_tot_val , func1_1_L15
qed

For a function of two variables defined on \(X\times Y\), if we fix an \(x\in X\) we obtain a function on \(Y\). Note that if \( domain(f) \) is \(X\times Y\), \( \text{range}(domain(f)) \) extracts \(Y\) from \(X\times Y\).

Definition

\( \text{Fix1stVar}(f,x) \equiv \{\langle y,f\langle x,y\rangle \rangle .\ y \in \text{range}(domain(f))\} \)

For every \(y\in Y\) we can fix the second variable in a binary function \(f: X\times Y \rightarrow Z\) to get a function on \(X\).

Definition

\( \text{Fix2ndVar}(f,y) \equiv \{\langle x,f\langle x,y\rangle \rangle .\ x \in domain(domain(f))\} \)

We defined Fix1stVar and Fix2ndVar so that the domain of the function is not listed in the arguments, but is recovered from the function. The next lemma is a technical fact that makes it easier to use this definition.

lemma fix_var_fun_domain:

assumes A1: \( f : X\times Y \rightarrow Z \)

shows \( x\in X \longrightarrow \text{Fix1stVar}(f,x) = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \), \( y\in Y \longrightarrow \text{Fix2ndVar}(f,y) = \{\langle x,f\langle x,y\rangle \rangle .\ x \in X\} \)proof
from A1 have I: \( domain(f) = X\times Y \) using func1_1_L1
{
assume \( x\in X \)
with I have \( \text{range}(domain(f)) = Y \)
then have \( \text{Fix1stVar}(f,x) = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \) using Fix1stVar_def
}
then show \( x\in X \longrightarrow \text{Fix1stVar}(f,x) = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \)
{
assume \( y\in Y \)
with I have \( domain(domain(f)) = X \)
then have \( \text{Fix2ndVar}(f,y) = \{\langle x,f\langle x,y\rangle \rangle .\ x \in X\} \) using Fix2ndVar_def
}
then show \( y\in Y \longrightarrow \text{Fix2ndVar}(f,y) = \{\langle x,f\langle x,y\rangle \rangle .\ x \in X\} \)
qed

If we fix the first variable, we get a function of the second variable.

lemma fix_1st_var_fun:

assumes A1: \( f : X\times Y \rightarrow Z \) and A2: \( x\in X \)

shows \( \text{Fix1stVar}(f,x) : Y \rightarrow Z \)proof
from A1, A2 have \( \forall y\in Y.\ f\langle x,y\rangle \in Z \) using apply_funtype
then have \( \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} : Y \rightarrow Z \) using ZF_fun_from_total
with A1, A2 show \( \text{Fix1stVar}(f,x) : Y \rightarrow Z \) using fix_var_fun_domain
qed

If we fix the second variable, we get a function of the first variable.

lemma fix_2nd_var_fun:

assumes A1: \( f : X\times Y \rightarrow Z \) and A2: \( y\in Y \)

shows \( \text{Fix2ndVar}(f,y) : X \rightarrow Z \)proof
from A1, A2 have \( \forall x\in X.\ f\langle x,y\rangle \in Z \) using apply_funtype
then have \( \{\langle x,f\langle x,y\rangle \rangle .\ x \in X\} : X \rightarrow Z \) using ZF_fun_from_total
with A1, A2 show \( \text{Fix2ndVar}(f,y) : X \rightarrow Z \) using fix_var_fun_domain
qed

What is the value of \( \text{Fix1stVar}(f,x) \) at \(y\in Y\) and the value of \( \text{Fix2ndVar}(f,y) \) at \(x\in X\)"?

lemma fix_var_val:

assumes A1: \( f : X\times Y \rightarrow Z \) and A2: \( x\in X \), \( y\in Y \)

shows \( \text{Fix1stVar}(f,x)(y) = f\langle x,y\rangle \), \( \text{Fix2ndVar}(f,y)(x) = f\langle x,y\rangle \)proof
let \( f_1 = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \)
let \( f_2 = \{\langle x,f\langle x,y\rangle \rangle .\ x \in X\} \)
from A1, A2 have I: \( \text{Fix1stVar}(f,x) = f_1 \), \( \text{Fix2ndVar}(f,y) = f_2 \) using fix_var_fun_domain
moreover
from A1, A2 have \( \text{Fix1stVar}(f,x) : Y \rightarrow Z \), \( \text{Fix2ndVar}(f,y) : X \rightarrow Z \) using fix_1st_var_fun , fix_2nd_var_fun
ultimately have \( f_1 : Y \rightarrow Z \) and \( f_2 : X \rightarrow Z \)
with A2 have \( f_1(y) = f\langle x,y\rangle \) and \( f_2(x) = f\langle x,y\rangle \) using ZF_fun_from_tot_val
with I show \( \text{Fix1stVar}(f,x)(y) = f\langle x,y\rangle \), \( \text{Fix2ndVar}(f,y)(x) = f\langle x,y\rangle \)
qed

Fixing the second variable commutes with restrictig the domain.

lemma fix_2nd_var_restr_comm:

assumes A1: \( f : X\times Y \rightarrow Z \) and A2: \( y\in Y \) and A3: \( X_1 \subseteq X \)

shows \( \text{Fix2ndVar}(\text{restrict}(f,X_1\times Y),y) = \text{restrict}( \text{Fix2ndVar}(f,y),X_1) \)proof
let \( g = \text{Fix2ndVar}(\text{restrict}(f,X_1\times Y),y) \)
let \( h = \text{restrict}( \text{Fix2ndVar}(f,y),X_1) \)
from A3 have I: \( X_1\times Y \subseteq X\times Y \)
with A1 have II: \( \text{restrict}(f,X_1\times Y) : X_1\times Y \rightarrow Z \) using restrict_type2
with A2 have \( g : X_1 \rightarrow Z \) using fix_2nd_var_fun
moreover
from A1, A2 have III: \( \text{Fix2ndVar}(f,y) : X \rightarrow Z \) using fix_2nd_var_fun
with A3 have \( h : X_1 \rightarrow Z \) using restrict_type2
moreover {
fix \( z \)
assume A4: \( z \in X_1 \)
with A2, I, II have \( g(z) = f\langle z,y\rangle \) using restrict , fix_var_val
also
from A1, A2, A3, A4 have \( f\langle z,y\rangle = h(z) \) using restrict , fix_var_val
finally have \( g(z) = h(z) \)
}
then have \( \forall z \in X_1.\ g(z) = h(z) \)
ultimately show \( g = h \) by (rule func_eq )
qed

The next lemma expresses the inverse image of a set by function with fixed first variable in terms of the original function.

lemma fix_1st_var_vimage:

assumes A1: \( f : X\times Y \rightarrow Z \) and A2: \( x\in X \)

shows \( \text{Fix1stVar}(f,x)^{-1}(A) = \{y\in Y.\ \langle x,y\rangle \in f^{-1}(A)\} \)proof
from assms have \( \text{Fix1stVar}(f,x)^{-1}(A) = \{y\in Y.\ \text{Fix1stVar}(f,x)(y) \in A\} \) using fix_1st_var_fun , func1_1_L15
with assms show \( thesis \) using fix_var_val , func1_1_L15
qed

The next lemma expresses the inverse image of a set by function with fixed second variable in terms of the original function.

lemma fix_2nd_var_vimage:

assumes A1: \( f : X\times Y \rightarrow Z \) and A2: \( y\in Y \)

shows \( \text{Fix2ndVar}(f,y)^{-1}(A) = \{x\in X.\ \langle x,y\rangle \in f^{-1}(A)\} \)proof
from assms have I: \( \text{Fix2ndVar}(f,y)^{-1}(A) = \{x\in X.\ \text{Fix2ndVar}(f,y)(x) \in A\} \) using fix_2nd_var_fun , func1_1_L15
with assms show \( thesis \) using fix_var_val , func1_1_L15
qed
end
lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)
Definition of fstdom: \( \text{fstdom}(f) \equiv domain(domain(f)) \)
lemma func1_1_L1A:

assumes \( f:X\rightarrow Y \) and \( \forall x\in X.\ f(x) \in Z \)

shows \( f:X\rightarrow Z \)
lemma vimage_converse: shows \( r^{-1}(A) = converse(r)(A) \)
lemma image_converse: shows \( converse(r)^{-1}(A) = r(A) \)
lemma vimage_comp: shows \( (r\circ s)^{-1}(A) = s^{-1}(r^{-1}(A)) \)
lemma func1_1_L3:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(D) \subseteq X \)
lemma func1_1_L2:

assumes \( f:X\rightarrow Y \), \( x\in X \)

shows \( \exists y\in Y.\ \langle x,y\rangle \in f \)
lemma func1_1_L5:

assumes \( \langle x,y\rangle \in f \) and \( f:X\rightarrow Y \)

shows \( x\in X \wedge y\in Y \)
lemma func1_1_L5A:

assumes \( f:X\rightarrow Y \), \( x\in X \), \( y = f(x) \)

shows \( \langle x,y\rangle \in f \), \( y \in \text{range}(f) \)
lemma fun_subset_prod:

assumes \( f:X\rightarrow Y \)

shows \( f \subseteq X\times Y \)
lemma func1_1_L5B:

assumes \( f:X\rightarrow Y \)

shows \( \text{range}(f) \subseteq Y \)
lemma func1_1_L9:

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

shows \( A \subseteq f^{-1}(f(A)) \)
lemma func1_1_L10:

assumes \( f \subseteq X\times Y \) and \( \exists !y.\ (y\in Y \wedge \langle x,y\rangle \in f) \)

shows \( \exists !y.\ \langle x,y\rangle \in f \)
lemma func1_1_L11:

assumes \( f \subseteq X\times Y \) and \( \forall x\in X.\ \exists !y.\ y\in Y \wedge \langle x,y\rangle \in f \)

shows \( f: X\rightarrow Y \)
lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \)
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 lam_is_fun_range:

assumes \( f=\{\langle x,g(x)\rangle .\ x\in X\} \)

shows \( f:X\rightarrow \text{range}(f) \)
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) \)
lemma func1_1_L11C:

assumes \( f:X\rightarrow Y \) and \( \forall x\in A.\ b(x)\in B \) and \( X\cap A = 0 \) and \( g = f \cup \{\langle x,b(x)\rangle .\ x\in A\} \)

shows \( g : X\cup A \rightarrow Y\cup B \), \( \forall x\in X.\ g(x) = f(x) \), \( \forall x\in A.\ g(x) = b(x) \)
lemma func1_1_L11D:

assumes \( f:X\rightarrow Y \) and \( a\notin X \) and \( g = f \cup \{\langle a,b\rangle \} \)

shows \( g : X\cup \{a\} \rightarrow Y\cup \{b\} \), \( \forall x\in X.\ g(x) = f(x) \), \( g(a) = b \)
lemma fun_is_fun:

assumes \( f:X\rightarrow Y \)

shows \( function(f) \)
lemma func1_1_L6A:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A)\subseteq X \)
lemma invim_inter_inter_invim:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A\cap B) = f^{-1}(A) \cap f^{-1}(B) \)
lemma inv_im_dom:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(f(X)) = X \)
lemma func_eq:

assumes \( f: X\rightarrow Y \), \( g: X\rightarrow Z \) and \( \forall x\in X.\ f(x) = g(x) \)

shows \( f = g \)
lemma func1_1_L1B:

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

shows \( f:X\rightarrow Z \)
lemma func1_1_L14:

assumes \( f\in X\rightarrow Y \)

shows \( f^{-1}(\{y\}) = \{x\in X.\ f(x) = y\} \)
lemma func_imagedef:

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

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

assumes \( f:X\rightarrow Y \), \( x\in A \), \( A\subseteq X \)

shows \( f(x) \in f(A) \)
lemma ZF1_1_L7:

assumes \( I\neq 0 \) and \( \forall i\in I.\ P(i) \subseteq X \)

shows \( ( \bigcap i\in I.\ P(i) ) \subseteq X \)
lemma func1_1_L15:

assumes \( f:X\rightarrow Y \)

shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \)
lemma func1_2_L2:

assumes \( f:X\rightarrow Y \) and \( g \in A\rightarrow Z \) and \( A\subseteq X \) and \( f \cap A\times Z = g \)

shows \( \forall x\in A.\ g(x) = f(x) \)
lemma func1_2_L4:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ f(x) \in Z \)

shows \( \text{restrict}(f,A) : A\rightarrow Z \)
lemma comp_fun_subset:

assumes \( g:A\rightarrow B \) and \( f:C\rightarrow D \) and \( B \subseteq C \)

shows \( f\circ g : A \rightarrow D \)
corollary restrict_fun:

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

shows \( \text{restrict}(f,A) : A \rightarrow Y \)
lemma func1_1_L11A:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y \)
Definition of ConstantFunction: \( \text{ConstantFunction}(X,c) \equiv X\times \{c\} \)
lemma func1_3_L1:

assumes \( c\in Y \)

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

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

shows \( f(X) - f(A) \subseteq f(X-A) \)
lemma range_image_domain:

assumes \( f:X\rightarrow Y \)

shows \( f(X) = \text{range}(f) \)
lemma image_id_same:

assumes \( A\subseteq X \)

shows \( id(X)(A) = A \)
lemma surj_image_vimage:

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

shows \( f(f^{-1}(A)) = A \)
lemma inj_image_dif:

assumes \( f \in \text{inj}(A,B) \) and \( C \subseteq A \)

shows \( f(A-C) = f(A) - f(C) \)
lemma surj_range_image_domain:

assumes \( f \in \text{surj}(A,B) \)

shows \( f(A) = B \)
lemma singleton_image:

assumes \( f\in X\rightarrow Y \) and \( x\in X \)

shows \( f\{x\} = \{f(x)\} \)
lemma inj_inv_back_in_set:

assumes \( f \in \text{inj}(A,B) \) and \( C\subseteq A \) and \( y \in f(C) \)

shows \( converse(f)(y) \in C \), \( f(converse(f)(y)) = y \)
lemma image_of_Inter:

assumes \( f:X\rightarrow Y \) and \( I\neq 0 \) and \( \forall i\in I.\ P(i) \subseteq X \)

shows \( f(\bigcap i\in I.\ P(i)) \subseteq ( \bigcap i\in I.\ f(P(i)) ) \)
lemma func1_1_L6:

assumes \( f:X\rightarrow Y \)

shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)
lemma inj_point_of_image:

assumes \( f \in \text{inj}(A,B) \) and \( C\subseteq A \) and \( x\in A \) and \( f(x) \in f(C) \)

shows \( x \in C \)
lemma inj_inj_range:

assumes \( f \in \text{inj}(A,B) \)

shows \( f \in \text{inj}(A,\text{range}(f)) \)
lemma surj_extend_point:

assumes \( f \in \text{surj}(X,Y) \) and \( a\notin X \) and \( g = f \cup \{\langle a,b\rangle \} \)

shows \( g \in \text{surj}(X\cup \{a\},Y\cup \{b\}) \)
lemma inj_extend_point:

assumes \( f \in \text{inj}(X,Y) \), \( a\notin X \), \( b\notin Y \)

shows \( (f \cup \{\langle a,b\rangle \}) \in \text{inj}(X\cup \{a\},Y\cup \{b\}) \)
lemma comp_inv_id_eq:

assumes \( converse(b)\circ a = id(A) \) and \( a \subseteq A\times B \), \( b \in \text{surj}(A,B) \)

shows \( a = b \)
lemma bij_converse_converse:

assumes \( a \in \text{bij}(A,B) \)

shows \( converse(converse(a)) = a \)
lemma comp_inv_id_eq_bij:

assumes \( a \in \text{bij}(A,B) \), \( b \in \text{bij}(A,B) \) and \( converse(b)\circ a = id(A) \)

shows \( a = b \)
lemma comp_eq_id_iff1:

assumes \( g: B\rightarrow A \) and \( f: A\rightarrow C \)

shows \( (\forall y\in B.\ f(g(y)) = y) \longleftrightarrow f\circ g = id(B) \)
lemma comp_id_conv:

assumes \( a \in \text{bij}(A,B) \), \( b \in \text{bij}(B,A) \) and \( b\circ a = id(A) \)

shows \( a = converse(b) \) and \( b = converse(a) \)
lemma cart_prod_fun:

assumes \( f_1:X_1\rightarrow Y_1 \), \( f_2:X_2\rightarrow Y_2 \) and \( g = \{\langle p,\langle f_1(\text{fst}(p)),f_2(\text{snd}(p))\rangle \rangle .\ p \in X_1\times X_2\} \)

shows \( g: X_1\times X_2 \rightarrow Y_1\times Y_2 \)
lemma prod_fun:

assumes \( f:X_1\rightarrow X_2 \), \( g:X_3\rightarrow X_4 \)

shows \( \{\langle \langle x,y\rangle ,\langle fx,gy\rangle \rangle .\ \langle x,y\rangle \in X_1\times X_3\}:X_1\times X_3\rightarrow X_2\times X_4 \)
Definition of Fix1stVar: \( \text{Fix1stVar}(f,x) \equiv \{\langle y,f\langle x,y\rangle \rangle .\ y \in \text{range}(domain(f))\} \)
Definition of Fix2ndVar: \( \text{Fix2ndVar}(f,y) \equiv \{\langle x,f\langle x,y\rangle \rangle .\ x \in domain(domain(f))\} \)
lemma fix_var_fun_domain:

assumes \( f : X\times Y \rightarrow Z \)

shows \( x\in X \longrightarrow \text{Fix1stVar}(f,x) = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \), \( y\in Y \longrightarrow \text{Fix2ndVar}(f,y) = \{\langle x,f\langle x,y\rangle \rangle .\ x \in X\} \)
lemma fix_1st_var_fun:

assumes \( f : X\times Y \rightarrow Z \) and \( x\in X \)

shows \( \text{Fix1stVar}(f,x) : Y \rightarrow Z \)
lemma fix_2nd_var_fun:

assumes \( f : X\times Y \rightarrow Z \) and \( y\in Y \)

shows \( \text{Fix2ndVar}(f,y) : X \rightarrow Z \)
lemma fix_var_val:

assumes \( f : X\times Y \rightarrow Z \) and \( x\in X \), \( y\in Y \)

shows \( \text{Fix1stVar}(f,x)(y) = f\langle x,y\rangle \), \( \text{Fix2ndVar}(f,y)(x) = f\langle x,y\rangle \)
441
149
117
117