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_funStandard Isabelle defines a \( function(f) \) predicate. The next lemma shows that our functions 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 \emptyset \)
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 version of the Pi_type lemma from the standard Isabelle/ZF library.
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 \)
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_iffThe image is the inverse image of converse.
lemma image_converse:
shows \( converse(r)^{-1}(A) = r(A) \) using vimage_iff, image_iff, converse_iffThe 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_converseA 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_compInverse 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 \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 that 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_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 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
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 (deprecated, use \( ZF\_fun\_from\_tot\_val(1) \) instead).
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 \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \) and \( b(x)\in Y \)proof from assms(1,2) have \( \langle x,f(x)\rangle \in f \) using apply_iff
with assms(3) show \( f(x) = b(x) \)
from assms(1,2) have \( f(x)\in Y \) by (rule apply_funtype )
with \( f(x) = b(x) \) show \( b(x)\in Y \)
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_valAnother 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
An hypotheses-free form of ZF_fun_from_tot_val1: the value of a function \(X\ni x \mapsto p(x)\) is \(p(x)\) for all \(x\in X\).
lemma ZF_fun_from_tot_val2:
shows \( \forall x\in X.\ \{\langle x,b(x)\rangle .\ x\in X\}(x) = b(x) \) using ZF_fun_from_tot_val1The range of a function defined by set comprehension is the set of its values.
lemma range_fun:
shows \( \text{range}(\{\langle x,b(x)\rangle .\ x\in X\}) = \{b(x).\ x\in X\} \)In Isabelle/ZF and Metamath if \(x\) is not in the domain of a function \(f\) then \(f(x)\) is the empty set. This allows us to conclude that if \(y\in f(x)\), then \(x\) must be en element of the domain of \(f\).
lemma arg_in_domain:
assumes \( f:X\rightarrow Y \), \( y\in f(x) \)
shows \( x\in X \)proof{
}
assume \( x\notin X \)
with assms have \( False \) using func1_1_L1, apply_0
thus \( thesis \)
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 = \emptyset \) 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 = \emptyset \) 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\} = \emptyset \), \( 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 = \emptyset \) 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 = \emptyset \), \( 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\setminus B.\ f(x) \in Y \), \( \forall x\in B\setminus A.\ g(x) \in Y \)
shows \( \{\langle x,\text{if }x\in A\setminus B\text{ then }f(x)\text{ else }\text{if }x\in B\setminus A\text{ then }g(x)\text{ else }h(x)\rangle .\ x \in A\cup B\}: A\cup B \rightarrow Y \)proof let \( F = \{\langle x,\text{if }x\in A\setminus B\text{ then }f(x)\text{ else }\text{if }x\in B\setminus A\text{ then }g(x)\text{ else }h(x)\rangle .\ x \in A\cap B\} \)
from assms have \( \forall x\in A\cup B.\ (\text{if }x\in A\setminus B\text{ then }f(x)\text{ else }\text{if }x\in B\setminus A\text{ then }g(x)\text{ 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_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 \emptyset \) 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 \emptyset \)
shows \( A\neq \emptyset \) 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 \emptyset \)
shows \( A\neq \emptyset \) using assmsWhat is the inverse image of a singleton?
lemma func1_1_L14:
assumes \( f: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_iffAn alternative syntax for defining a function: instead of writing \(\{\langle x,p(x)\rangle. x\in X\}\) we can write \(\lambda x\in X. p(x)\).
lemma lambda_fun_alt:
shows \( \{\langle x,p(x)\rangle .\ x\in X\} = (\lambda x\in X.\ p(x)) \)proof let \( L = \{\langle x,p(x)\rangle .\ x\in X\} \)
let \( R = \lambda x\in X.\ p(x) \)
have \( L:X\rightarrow \text{range}(L) \) and \( R:X\rightarrow \text{range}(L) \) using lam_is_fun_range, range_fun, lam_funtype
moreover
qed
have \( \forall x\in X.\ L(x) = R(x) \) using ZF_fun_from_tot_val1, beta
ultimately show \( L = R \) using func_eq
If a function is equal to an expression \(b(x)\) on \(X\), then it has to be of the form \(\{ \langle x, b(x)\rangle | x\in X\}\).
lemma func_eq_set_of_pairs:
assumes \( f:X\rightarrow Y \), \( \forall x\in X.\ f(x) = b(x) \)
shows \( f = \{\langle x, b(x)\rangle .\ x \in X\} \)proof from assms(1) have \( f = \{\langle x, f(x)\rangle .\ x \in X\} \) using fun_is_set_of_pairs
with assms(2) show \( thesis \)
qed
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
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 \) and \( y = f(x) \)
with A1, A2 have \( \langle x,y\rangle \in f \) using apply_iff
with A1, A2, \( x\in A \) show \( y \in f(A) \) using image_iff
qed
If all elements of a nonempty set map to the same element of the codomain, then the image of this set is a singleton.
lemma image_constant_singleton:
assumes \( f:X\rightarrow Y \), \( A\subseteq X \), \( A\neq \emptyset \), \( \forall x\in A.\ f(x) = c \)
shows \( f(A) = \{c\} \) using assms, func_imagedefA technical lemma about graphs of functions: if we have two disjoint sets \(A\) and \(B\) then the cartesian product of the inverse image of \(A\) and \(B\) is disjoint with (the graph of) \(f\).
lemma vimage_prod_dis_graph:
assumes \( f:X\rightarrow Y \), \( A\cap B = \emptyset \)
shows \( f^{-1}(A)\times B \cap f = \emptyset \)proof{
}
assume \( f^{-1}(A)\times B \cap f \neq \emptyset \)
then obtain \( p \) where \( p \in f^{-1}(A)\times B \) and \( p\in f \)
from assms(1), \( p\in f \) have \( p \in \{\langle x, f(x)\rangle .\ x \in X\} \) using fun_is_set_of_pairs
then obtain \( x \) where \( p = \langle x, f(x)\rangle \)
with assms, \( p \in f^{-1}(A)\times B \) have \( False \) using func1_1_L15
thus \( thesis \)
qed
For two functions with the same domain \(X\) and the codomain \(Y,Z\) resp., we can define a third one that maps \(X\) to the cartesian product of \(Y\) and \(Z\).
lemma prod_fun_val:
assumes \( \{\langle x,p(x)\rangle .\ x\in X\}: X\rightarrow Y \), \( \{\langle x,q(x)\rangle .\ x\in X\}: X\rightarrow Z \)
defines \( h \equiv \{\langle x,\langle p(x),q(x)\rangle \rangle .\ x\in X\} \)
shows \( h:X\rightarrow Y\times Z \) and \( \forall x\in X.\ h(x) = \langle p(x),q(x)\rangle \)proof from assms(1,2) have \( \forall x\in X.\ \langle p(x),q(x)\rangle \in Y\times Z \) using ZF_fun_from_tot_val(2)
with assms(3) show \( h:X\rightarrow Y\times Z \) using ZF_fun_from_total
with assms(3) show \( \forall x\in X.\ h(x) = \langle p(x),q(x)\rangle \) using ZF_fun_from_tot_val0
qed
Suppose we have two functions \(f:X\rightarrow Y\) and \(g:X\rightarrow Z\) and the third one is defined as \(h:X\rightarrow Y\times Z\), \(x\mapsto \langle f(x),g(x)\rangle\). Given two sets \(U\), \(V\) we have \(h^{-1}(U\times V) = (f^{-1}(U)) \cap (g^{-1}(V))\). We also show that the set where the function \(f,g\) are equal is the same as \(h^{-1}(\{ \langle y,y\rangle : y\in X\}\). It is a bit surprising that we get the last identity without the assumption that \(Y=Z\).
lemma vimage_prod:
assumes \( f:X\rightarrow Y \), \( g:X\rightarrow Z \)
defines \( h \equiv \{\langle x,\langle f(x),g(x)\rangle \rangle .\ x\in X\} \)
shows \( h:X\rightarrow Y\times Z \), \( \forall x\in X.\ h(x) = \langle f(x),g(x)\rangle \), \( h^{-1}(U\times V) = f^{-1}(U) \cap g^{-1}(V) \), \( \{x\in X.\ f(x) = g(x)\} = h^{-1}(\{\langle y,y\rangle .\ y\in Y\}) \)proof from assms show \( h:X\rightarrow Y\times Z \) using apply_funtype, ZF_fun_from_total
with assms(3) show I: \( \forall x\in X.\ h(x) = \langle f(x),g(x)\rangle \) using ZF_fun_from_tot_val
with assms(1,2), \( h:X\rightarrow Y\times Z \) show \( h^{-1}(U\times V) = f^{-1}(U) \cap g^{-1}(V) \) using func1_1_L15
from assms(1), I, \( h:X\rightarrow Y\times Z \) show \( \{x\in X.\ f(x) = g(x)\} = h^{-1}(\{\langle y,y\rangle .\ y\in Y\}) \) using apply_funtype, func1_1_L15
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_convThe 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_convWhat 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 image 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 \( \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)\setminus f(A) \subseteq f(X\setminus A) \)proof fix \( y \)
assume \( y \in f(X) \setminus 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\setminus A \), \( X\setminus A \subseteq X \)
with A1, II show \( y \in f(X\setminus 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 \emptyset \) 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
If the domain of a function is nonempty, then the codomain is as well.
lemma codomain_nonempty:
assumes \( f:X\rightarrow Y \), \( X\neq \emptyset \)
shows \( Y\neq \emptyset \) using assms, apply_funtypeThe 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 \emptyset \)
shows \( f(A) \neq \emptyset \)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 \emptyset \)
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
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
qed
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) \)
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
qed
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
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 {
}
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 \( \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 function restricted to its domain is itself.
lemma restrict_domain:
assumes \( f:X\rightarrow Y \)
shows \( \text{restrict}(f,X) = f \)proof have \( \forall x\in X.\ \text{restrict}(f,X)(x) = f(x) \) using restrict
with assms show \( thesis \) using func_eq, restrict_fun
qed
Suppose a function \(f:X\rightarrow Y\) is defined by an expression \(q\), i.e. \(f = \{\langle x,y\rangle : x\in X\}\). Then a function that is defined by the same expression, but on a smaller set is the same as the restriction of \(f\) to that smaller set.
lemma restrict_def_alt:
assumes \( A\subseteq X \)
shows \( \text{restrict}(\{\langle x,q(x)\rangle .\ x\in X\},A) = \{\langle x,q(x)\rangle .\ x\in A\} \)proof let \( Y = \{q(x).\ x\in X\} \)
let \( f = \{\langle x,q(x)\rangle .\ x\in X\} \)
have \( \forall x\in X.\ q(x)\in Y \)
with assms have \( f:X\rightarrow Y \) using ZF_fun_from_total
with assms have \( \text{restrict}(f,A):A\rightarrow Y \) using restrict_fun
moreover
qed
from assms have \( \forall x\in A.\ q(x)\in Y \)
then have \( \{\langle x,q(x)\rangle .\ x\in A\}:A\rightarrow Y \) using ZF_fun_from_total
moreover from assms have \( \forall x\in A.\ \text{restrict}(f,A)(x) = \{\langle x,q(x)\rangle .\ x\in A\}(x) \) using restrict, ZF_fun_from_tot_val1
ultimately show \( thesis \) by (rule func_eq )
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
qed
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 )
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_defConstant 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 is a function (i.e. belongs to a 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
qed
from A1 have \( \langle x,c\rangle \in \text{ConstantFunction}(X,c) \) using ConstantFunction_def
ultimately show \( thesis \) using apply_iff
Another way of looking at the constant function - it's a set of pairs \(\langle x,c\rangle\) as \(x\) ranges over \(X\).
lemma const_fun_def_alt:
shows \( \text{ConstantFunction}(X,c) = \{\langle x,c\rangle .\ x\in X\} \) unfolding ConstantFunction_defIf \(c\in A\) then the inverse image of \(A\) by the constant function \(x\mapsto c\) is the whole domain.
lemma const_vimage_domain:
assumes \( c\in A \)
shows \( \text{ConstantFunction}(X,c)^{-1}(A) = X \)proof let \( C = \text{ConstantFunction}(X,c) \)
have \( C^{-1}(A) = \{x\in X.\ C(x) \in A\} \) using func1_3_L1, func1_1_L15
with assms show \( thesis \) using func1_3_L2
qed
If \(c\) is not an element of \(A\) then the inverse image of \(A\) by the constant function \(x\mapsto c\) is empty.
lemma const_vimage_empty:
assumes \( c\notin A \)
shows \( \text{ConstantFunction}(X,c)^{-1}(A) = \emptyset \)proof let \( C = \text{ConstantFunction}(X,c) \)
have \( C^{-1}(A) = \{x\in X.\ C(x) \in A\} \) using func1_3_L1, func1_1_L15
with assms show \( thesis \) using func1_3_L2
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\setminus C) = f(A)\setminus f(C) \)proof show \( f(A\setminus C) \subseteq f(A)\setminus f(C) \)proof
fix \( y \)
assume A3: \( y \in f(A\setminus C) \)
from A1 have \( f:A\rightarrow B \) using inj_def
moreover
have \( A\setminus C \subseteq A \)
ultimately have \( f(A\setminus C) = \{f(x).\ x \in A\setminus C\} \) using func_imagedef
with A3 obtain \( x \) where I: \( f(x) = y \) and \( x \in A\setminus 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)\setminus 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 \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\setminus C \), \( x_0 \in C \) have \( False \)
thus \( thesis \)
qed
from A1, A2 show \( f(A)\setminus f(C) \subseteq f(A\setminus 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
Surjections are functions that map the domain onto the codomain.
lemma surj_def_alt:
shows \( \text{surj}(X,Y) = \{f\in X\rightarrow Y.\ f(X) = Y\} \)proof show \( \text{surj}(X,Y) \subseteq \{f\in X\rightarrow Y.\ f(X) = Y\} \) using surj_range_image_domain unfolding surj_def
show \( \{f\in X\rightarrow Y.\ f(X) = Y\} \subseteq \text{surj}(X,Y) \) using range_image_domain, fun_is_surj
qed
Bijections are functions that preserve complements.
lemma bij_def_alt:
shows \( \text{bij}(X,Y) = \{f\in X\rightarrow Y.\ \forall A\in Pow(X).\ f(X\setminus A) = Y\setminus f(A)\} \)proof let \( R = \{f\in X\rightarrow Y.\ \forall A\in Pow(X).\ f(X\setminus A) = Y\setminus f(A)\} \)
show \( \text{bij}(X,Y) \subseteq R \) using inj_image_dif, surj_range_image_domain, surj_is_fun unfolding bij_def
{
fix \( f \)
assume \( f\in R \)
hence \( f:X\rightarrow Y \) and I: \( \forall A\in Pow(X).\ f(X\setminus A) = Y\setminus f(A) \)
{
fix \( x_1 \) \( x_2 \)
assume \( x_1\in X \), \( x_2\in X \), \( f(x_1) = f(x_2) \)
with \( f:X\rightarrow Y \) have \( f\{x_1\} = \{f(x_1)\} \), \( f\{x_2\} = \{f(x_2)\} \), \( f\{x_1\} = f\{x_2\} \) using singleton_image
{
assume \( x_1\neq x_2 \)
from \( f:X\rightarrow Y \) have \( f(X\setminus \{x_1\}) = \{f(t).\ t\in X\setminus \{x_1\}\} \) using func_imagedef
with I, \( x_2\in X \), \( x_1\in X \), \( x_1\neq x_2 \), \( f\{x_1\} = f\{x_2\} \) have \( f(x_2) \in Y\setminus f\{x_2\} \)
with \( f\{x_2\} = \{f(x_2)\} \) have \( False \)
hence \( x_1=x_2 \)
with \( f:X\rightarrow Y \) have \( f\in \text{inj}(X,Y) \) unfolding inj_def
moreover
from I have \( f(X\setminus \emptyset ) = Y\setminus f(\emptyset ) \)
with \( f:X\rightarrow Y \) have \( f\in \text{surj}(X,Y) \) using surj_def_alt
ultimately have \( f \in \text{bij}(X,Y) \) unfolding bij_def
thus \( R \subseteq \text{bij}(X,Y) \)
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 range.
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\setminus \{a\}) \in \text{bij}(A\setminus \{a\}, B\setminus \{f(a)\}) \)proof let \( C = A\setminus \{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
qed
have \( f(C) = B\setminus \{f(a)\} \)proof
ultimately show \( thesis \)
from A2, \( f \in \text{inj}(A,B) \) have \( f(C) = f(A)\setminus 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\setminus \{f(a)\} \)
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 a bijection between \(Y\) and \(X\) and a set \(A\subseteq X\) an element \(y\in Y\) is in the image \(f(A)\) if and only if \(f^{-1}(y)\) is an element of \(A\). Note this is false with the weakened assumption that \(f\) is an injection, for example consider \(f:\{ 0,1\}\rightarrow \mathbb{N}, f(n)= n+1\) and \(y=3\). Then \(f^{-1}:\{1, 2\}\rightarrow \{ 0,1\}\) and (since \(3\) is not in the domain of the inverse function) \(f^{-1}(3) = \emptyset = 0 \in \{ 0,1\}\), but \(3\) is not in the image \(f(\{ 0,1\})\).
lemma bij_val_image_vimage:
assumes \( f \in \text{bij}(X,Y) \), \( A\subseteq X \), \( y\in Y \)
shows \( y\in f(A) \longleftrightarrow converse(f)(y) \in A \)proof assume \( y\in f(A) \)
with assms(1,2) show \( converse(f)(y) \in A \) unfolding bij_def using inj_inv_back_in_set
next
assume \( converse(f)(y) \in A \)
with assms(1,3) have \( y\in \{f(x).\ x\in A\} \) using right_inverse_bij
with assms(1,2) show \( y\in f(A) \) using bij_is_fun, func_imagedef
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
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 \text{inj}(A,B) \) and A2: \( I\neq \emptyset \) 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_funAn 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
qed
have \( \forall y \in Y\cup \{b\}.\ \exists x \in X\cup \{a\}.\ y = g(x) \)proof
ultimately show \( g \in \text{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 \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
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 \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_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 \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
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 \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 is 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
qed
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
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
ultimately show \( b \in \text{bij}(B,A) \) using bij_def
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
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_totalA 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
qed
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 \)
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
}
qed
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 )
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) \) and \( b(x)\in Y \) 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 ZF_fun_from_tot_val1:
assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(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 = \emptyset \) 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 range_fun: shows \( \text{range}(\{\langle x,b(x)\rangle .\ x\in X\}) = \{b(x).\ x\in 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 \) theorem fun_is_set_of_pairs:
assumes \( f:X\rightarrow Y \)
shows \( f = \{\langle x, f(x)\rangle .\ x \in X\} \) lemma func1_1_L1B:
assumes \( f:X\rightarrow Y \) and \( Y\subseteq Z \)
shows \( f:X\rightarrow Z \) lemma func1_1_L14:
assumes \( f: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_L15:
assumes \( f:X\rightarrow Y \)
shows \( f^{-1}(A) = \{x\in X.\ f(x) \in A\} \) 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) \) and \( b(x)\in Y \) 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_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 \) corollary restrict_fun:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( \text{restrict}(f,A) : A \rightarrow Y \) 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 \) 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 func1_3_L2:
assumes \( x\in X \)
shows \( \text{ConstantFunction}(X,c)(x) = c \) lemma diff_image_diff:
assumes \( f: X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(X)\setminus f(A) \subseteq f(X\setminus A) \) lemma range_image_domain:
assumes \( f:X\rightarrow Y \)
shows \( f(X) = \text{range}(f) \) lemma surj_range_image_domain:
assumes \( f \in \text{surj}(A,B) \)
shows \( f(A) = B \) lemma inj_image_dif:
assumes \( f \in \text{inj}(A,B) \) and \( C \subseteq A \)
shows \( f(A\setminus C) = f(A)\setminus f(C) \) lemma singleton_image:
assumes \( f\in X\rightarrow Y \) and \( x\in X \)
shows \( f\{x\} = \{f(x)\} \) lemma surj_def_alt: shows \( \text{surj}(X,Y) = \{f\in X\rightarrow Y.\ f(X) = Y\} \)
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_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 \emptyset \) 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 \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8