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
\( 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
\( 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_funStandard 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_functionA lemma explains what fstdom is for.
lemma fstdomdef:
assumes A1: \( f: X\times Y \rightarrow Z \) and A2: \( Y\neq 0 \)
shows \( fstdom(f) = X \)proof from A1 have \( domain(f) = X\times Y \) using func1_1_L1
with A2 show \( 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
qed
from A1 have \( \langle x,f(x)\rangle \in f \) using apply_Pair
ultimately show \( thesis \)
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_iffThe 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 range(f) \)proof from A1 show \( \langle x,y\rangle \in f \) using apply_Pair
then show \( y \in 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 \( range(f) \subseteq Y \)proof fix \( y \)
assume \( y \in 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 range(f) \) and \( f(B) \subseteq Y \)proof show \( f(B) \subseteq 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_UnA 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_oldA set defined by a lambda-type expression is a fuction. There is a similar lemma in func.thy, but I had problems with lamda expressions syntax so I could not apply it. This lemma is a workaround 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
qed
have \( \forall x\in X.\ \exists !y.\ y\in Y \wedge \langle x,y\rangle \in f \)proof
ultimately show \( \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y \) using func1_1_L11
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
qed
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
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
qed
from A1 have \( f \subseteq X\times Y \)
ultimately show \( thesis \) using func1_1_L11
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_valWe 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
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_IntThe 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
qed
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
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_L6AIf 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 assmsIf 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 assmsWhat 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_iffA 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_iffFunction 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
qed
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 )
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
qed
from A1 have \( \{y\} \subseteq Y \)
ultimately show \( \{\langle x,y\rangle \} : \{x\} \rightarrow Y \) by (rule func1_1_L1B )
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_equalityA 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
qed
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
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_imagedefIf 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_imagedefRange is the image of the domain. Isabelle/ZF defines \( 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) = range(f) \)proof show \( f(X) \subseteq range(f) \) using image_def
{
fix \( y \)
assume \( y \in 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 \( 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 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_imagedefAn 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
qed
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) \)
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
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 \( 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 \( 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 \( restrict(f,B)^{-1}(A) = f^{-1}(A) \cap B \)proof let \( g = 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 = restrict(f,A) \)proof from A4 show \( g \subseteq restrict(f, A) \) using restrict_iff
show \( restrict(f, A) \subseteq g \)proof
qed
fix \( z \)
assume A5: \( z \in 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
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 \( restrict(f,A) : A\rightarrow Z \)proof let \( g = restrict(f,A) \)
from A1, A2 have \( g : A\rightarrow Y \) using restrict_type2
moreover {
}
ultimately show \( thesis \) by (rule Pi_type )
qed
fix \( x \)
assume \( x\in A \)
with A1, A3 have \( g(x) \in Z \) using restrict
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 \( 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 = restrict(g,B)\circ f \)proof from assms have \( g\circ f : A \rightarrow C \) using comp_fun_subset
moreover
qed
from assms have \( 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) = (restrict(g,B)\circ f)(x) \) using comp_fun_apply , apply_funtype , restrict
ultimately show \( g\circ f = restrict(g,B)\circ f \) by (rule func_eq )
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
\( ConstantFunction(X,c) \equiv X\times \{c\} \)
Constant function belongs to the function space.
lemma func1_3_L1:
assumes A1: \( c\in Y \)
shows \( 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 \( ConstantFunction(X,c)(x) = c \)proof have \( ConstantFunction(X,c) \in X\rightarrow \{c\} \) using func1_3_L1
moreover
qed
from A1 have \( \langle x,c\rangle \in ConstantFunction(X,c) \) using ConstantFunction_def
ultimately show \( thesis \) using apply_iff
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 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
qed
have \( y \notin f(C) \)proof
ultimately show \( y \in f(A) - f(C) \)
{
}
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 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
from A1, A2 show \( f(A) - f(C) \subseteq f(A-C) \) using inj_def , diff_image_diff
qed
For surjection from \(A\) to \(B\) the image of the domain is \(B\).
lemma surj_range_image_domain:
assumes A1: \( f \in surj(A,B) \)
shows \( f(A) = B \)proof from A1 have \( f(A) = range(f) \) using surj_def , range_image_domain
with A1 show \( f(A) = B \) using surj_range
qed
Restriction of an bijection to a set without a point is a a bijection.
lemma bij_restrict_rem:
assumes A1: \( f \in bij(A,B) \) and A2: \( a\in A \)
shows \( restrict(f, A-\{a\}) \in bij(A-\{a\}, B-\{f(a)\}) \)proof let \( C = A-\{a\} \)
from A1 have \( f \in inj(A,B) \), \( C \subseteq A \) using bij_def
then have \( restrict(f,C) \in bij(C, f(C)) \) using restrict_bij
moreover
qed
have \( f(C) = B-\{f(a)\} \)proof
ultimately show \( thesis \)
from A2, \( f \in inj(A,B) \) have \( f(C) = f(A) - f\{a\} \) using inj_image_dif
moreover
qed
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)\} \)
The domain of a bijection between \(X\) and \(Y\) is \(X\).
lemma domain_of_bij:
assumes A1: \( f \in 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 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 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
qed
from A1, A3 have \( converse(f)(f(x)) = x \) using left_inverse_eq
ultimately show \( x \in C \)
For injections the image of intersection is the intersection of images.
lemma inj_image_of_Inter:
assumes A1: \( f \in 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 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
A lemma about extending a surjection by one point.
lemma surj_extend_point:
assumes A1: \( f \in surj(X,Y) \) and A2: \( a\notin X \) and A3: \( g = f \cup \{\langle a,b\rangle \} \)
shows \( g \in 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
qed
have \( \forall y \in Y\cup \{b\}.\ \exists x \in X\cup \{a\}.\ y = g(x) \)proof
ultimately show \( g \in surj(X\cup \{a\},Y\cup \{b\}) \) using surj_def
fix \( y \)
assume \( y \in Y \cup \{b\} \)
then have \( y \in Y \vee y = b \)
moreover {
}
moreover {
}
ultimately show \( \exists x \in X\cup \{a\}.\ y = g(x) \)
qed
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) \)
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) \)
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 inj(X,Y) \), \( a\notin X \), \( b\notin Y \)
shows \( (f \cup \{\langle a,b\rangle \}) \in inj(X\cup \{a\},Y\cup \{b\}) \)proof from assms have \( cons(\langle a,b\rangle ,f) \in inj(cons(a, X), cons(b, Y)) \) using assms , inj_extend
moreover
qed
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 \)
A lemma about extending a bijection by one point.
lemma bij_extend_point:
assumes \( f \in bij(X,Y) \), \( a\notin X \), \( b\notin Y \)
shows \( (f \cup \{\langle a,b\rangle \}) \in bij(X\cup \{a\},Y\cup \{b\}) \) using assms , surj_extend_point , inj_extend_point , bij_defA 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 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
qed
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 \)
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 bij(A,B) \), \( b \in 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 surj(A,B) \) using bij_def , surj_def , fun_subset_prod
with A2 show \( a = b \) by (rule comp_inv_id_eq )
qed
For a surjection The union if images of singletons is the whole range.
lemma surj_singleton_image:
assumes A1: \( f \in 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
Fixing variables in functions
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.
If we fix an \(x\in X\) we obtain a function on \(Y\). Note that if \( domain(f) \) is \(X\times Y\), \( range(domain(f)) \) extracts \(Y\) from \(X\times Y\).
Definition
\( Fix1stVar(f,x) \equiv \{\langle y,f\langle x,y\rangle \rangle .\ y \in 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
\( 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 Fix1stVar(f,x) = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \), \( y\in Y \longrightarrow 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 \( range(domain(f)) = Y \)
then have \( Fix1stVar(f,x) = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \) using Fix1stVar_def
then show \( x\in X \longrightarrow 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 \( Fix2ndVar(f,y) = \{\langle x,f\langle x,y\rangle \rangle .\ x \in X\} \) using Fix2ndVar_def
then show \( y\in Y \longrightarrow 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 \( 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 \( 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 \( 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 \( Fix2ndVar(f,y) : X \rightarrow Z \) using fix_var_fun_domain
qed
What is the value of \( Fix1stVar(f,x) \) at \(y\in Y\) and the value of \( 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 \( Fix1stVar(f,x)(y) = f\langle x,y\rangle \), \( 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: \( Fix1stVar(f,x) = f_1 \), \( Fix2ndVar(f,y) = f_2 \) using fix_var_fun_domain
moreover
qed
from A1, A2 have \( Fix1stVar(f,x) : Y \rightarrow Z \), \( 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 \( Fix1stVar(f,x)(y) = f\langle x,y\rangle \), \( Fix2ndVar(f,y)(x) = f\langle x,y\rangle \)
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 \( Fix2ndVar(restrict(f,X_1\times Y),y) = restrict(Fix2ndVar(f,y),X_1) \)proof let \( g = Fix2ndVar(restrict(f,X_1\times Y),y) \)
let \( h = restrict(Fix2ndVar(f,y),X_1) \)
from A3 have I: \( X_1\times Y \subseteq X\times Y \)
with A1 have II: \( 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
}
qed
from A1, A2 have III: \( 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 )
end
lemma func1_1_L1: assumes \( f:A\rightarrow C \) shows \( domain(f) = A \)
Definition of fstdom:
\( 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 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 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 \( 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 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 \( 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 \( 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:
\( ConstantFunction(X,c) \equiv X\times \{c\} \)
lemma func1_3_L1: assumes \( c\in Y \) shows \( 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) = range(f) \)
lemma inj_image_dif: assumes \( f \in inj(A,B) \) and \( C \subseteq A \) shows \( f(A-C) = f(A) - f(C) \)
lemma surj_range_image_domain: assumes \( f \in 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 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 range(f) \) and \( f(B) \subseteq Y \)
lemma inj_point_of_image: assumes \( f \in inj(A,B) \) and \( C\subseteq A \) and \( x\in A \) and \( f(x) \in f(C) \) shows \( x \in C \)
lemma surj_extend_point: assumes \( f \in surj(X,Y) \) and \( a\notin X \) and \( g = f \cup \{\langle a,b\rangle \} \) shows \( g \in surj(X\cup \{a\},Y\cup \{b\}) \)
lemma inj_extend_point: assumes \( f \in inj(X,Y) \), \( a\notin X \), \( b\notin Y \) shows \( (f \cup \{\langle a,b\rangle \}) \in 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 surj(A,B) \) shows \( a = b \)
Definition of Fix1stVar:
\( Fix1stVar(f,x) \equiv \{\langle y,f\langle x,y\rangle \rangle .\ y \in range(domain(f))\} \)
Definition of Fix2ndVar:
\( 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 Fix1stVar(f,x) = \{\langle y,f\langle x,y\rangle \rangle .\ y \in Y\} \), \( y\in Y \longrightarrow 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 \( Fix1stVar(f,x) : Y \rightarrow Z \)
lemma fix_2nd_var_fun: assumes \( f : X\times Y \rightarrow Z \) and \( y\in Y \) shows \( 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 \( Fix1stVar(f,x)(y) = f\langle x,y\rangle \), \( Fix2ndVar(f,y)(x) = f\langle x,y\rangle \)
