theory func_ZF imports func1
begin
In this theory we consider properties of functions that are binary operations, that is they map \(X\times X\) into \(X\).
Lifting operations to a function space
It happens quite often that we have a binary operation on some set and we need a similar operation that is defined for functions on that set. For example once we know how to add real numbers we also know how to add real-valued functions: for \(f,g:X \rightarrow \mathbf{R}\) we define \((f+g)(x) = f(x) + g(x)\). Note that formally the \(+\) means something different on the left hand side of this equality than on the right hand side. This section aims at formalizing this process. We will call it "lifting to a function space", if you have a suggestion for a better name, please let me know.
Since we are writing in generic set notation, the definition below is a bit complicated. Here it what it says: Given a set \(X\) and another set \(f\) (that represents a binary function on \(X\)) we are defining \(f\) lifted to function space over \(X\) as the binary function (a set of pairs) on the space \(F = X \rightarrow \textrm{range}(f)\) such that the value of this function on pair \(\langle a,b \rangle\) of functions on \(X\) is another function \(c\) on \(X\) with values defined by \(c(x) = f\langle a(x), b(x)\rangle\).
definition
\( f \text{ lifted to function space over } X \equiv \) \( \{\langle p,\{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\}\rangle .\ \) \( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\} \)
The result of the lift belongs to the function space.
lemma func_ZF_1_L1:
assumes A1: \( f : Y\times Y\rightarrow Y \) and A2: \( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f)) \)
shows \( \{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\} : X\rightarrow \text{range}(f) \)proof have \( \forall x\in X.\ f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \in \text{range}(f) \)proof
fix \( x \)
assume \( x\in X \)
let \( p = \langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \)
from A2, \( x\in X \) have \( \text{fst}(p)(x) \in \text{range}(f) \), \( \text{snd}(p)(x) \in \text{range}(f) \) using apply_type
with A1 have \( p \in Y\times Y \) using func1_1_L5B
with A1 have \( \langle p, f(p)\rangle \in f \) using apply_Pair
with A1 show \( f(p) \in \text{range}(f) \) using rangeI
qed
then show \( thesis \) using ZF_fun_from_total
qed
The values of the lift are defined by the value of the liftee in a natural way.
lemma func_ZF_1_L2:
assumes A1: \( f : Y\times Y\rightarrow Y \) and A2: \( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f)) \) and A3: \( x\in X \) and A4: \( P = \{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\} \)
shows \( P(x) = f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \)proof from A1, A2 have \( \{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\} : X \rightarrow \text{range}(f) \) using func_ZF_1_L1
with A4 have \( P : X \rightarrow \text{range}(f) \)
with A3, A4 show \( P(x) = f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \) using ZF_fun_from_tot_val
qed
Function lifted to a function space results in function space operator.
theorem func_ZF_1_L3:
assumes \( f : Y\times Y\rightarrow Y \) and \( F = f \text{ lifted to function space over } X \)
shows \( F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f)) \) using assms, Lift2FcnSpce_def, func_ZF_1_L1, ZF_fun_from_totalThe values of the lift are defined by the values of the liftee in the natural way.
theorem func_ZF_1_L4:
assumes A1: \( f : Y\times Y\rightarrow Y \) and A2: \( F = f \text{ lifted to function space over } X \) and A3: \( s:X\rightarrow \text{range}(f) \), \( r:X\rightarrow \text{range}(f) \) and A4: \( x\in X \)
shows \( (F\langle s,r\rangle )(x) = f\langle s(x),r(x)\rangle \)proof let \( p = \langle s,r\rangle \)
let \( P = \{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\} \)
from A1, A3, A4 have \( f : Y\times Y\rightarrow Y \), \( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f)) \), \( x\in X \), \( P = \{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\} \)
then have \( P(x) = f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \) by (rule func_ZF_1_L2 )
hence \( P(x) = f\langle s(x),r(x)\rangle \)
moreover
qed
have \( P = F\langle s,r\rangle \)proof
ultimately show \( (F\langle s,r\rangle )(x) = f\langle s(x),r(x)\rangle \)
from A1, A2 have \( F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f)) \) using func_ZF_1_L3
moreover
qed
from A3 have \( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f)) \)
moreover from A2 have \( F = \{\langle p,\{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\}\rangle .\ \)
\( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\} \) using Lift2FcnSpce_def
ultimately show \( thesis \) using ZF_fun_from_tot_val
Associative and commutative operations
In this section we define associative and commutative operations and prove that they remain such when we lift them to a function space.
Typically we say that a binary operation "\(\cdot \)" on a set \(G\) is ''associative'' if \((x\cdot y)\cdot z = x\cdot (y\cdot z)\) for all \(x,y,z \in G\). Our actual definition below does not use the multiplicative notation so that we can apply it equally to the additive notation \(+\) or whatever infix symbol we may want to use. Instead, we use the generic set theory notation and write \(P\langle x,y \rangle\) to denote the value of the operation \(P\) on a pair \(\langle x,y \rangle \in G\times G\).
definition
\( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \) \( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \) \( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
A binary function \(f: X\times X \rightarrow Y\) is commutative if \(f\langle x,y \rangle = f\langle y,x \rangle\). Note that in the definition of associativity above we talk about binary ''operation'' and here we say use the term binary ''function''. This is not set in stone, but usually the word "operation" is used when the range is a factor of the domain, while the word "function" allows the range to be a completely unrelated set.
definition
\( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
The lift of a commutative function is commutative.
lemma func_ZF_2_L1:
assumes A1: \( f : G\times G\rightarrow G \) and A2: \( F = f \text{ lifted to function space over } X \) and A3: \( s : X\rightarrow \text{range}(f) \), \( r : X\rightarrow \text{range}(f) \) and A4: \( f \text{ is commutative on } G \)
shows \( F\langle s,r\rangle = F\langle r,s\rangle \)proof from A1, A2 have \( F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f)) \) using func_ZF_1_L3
with A3 have \( F\langle s,r\rangle : X\rightarrow \text{range}(f) \) and \( F\langle r,s\rangle : X\rightarrow \text{range}(f) \) using apply_type
moreover
qed
have \( \forall x\in X.\ (F\langle s,r\rangle )(x) = (F\langle r,s\rangle )(x) \)proof
ultimately show \( thesis \) using fun_extension_iff
fix \( x \)
assume \( x\in X \)
from A1 have \( \text{range}(f)\subseteq G \) using func1_1_L5B
with A3, \( x\in X \) have \( s(x) \in G \) and \( r(x) \in G \) using apply_type
with A1, A2, A3, A4, \( x\in X \) show \( (F\langle s,r\rangle )(x) = (F\langle r,s\rangle )(x) \) using func_ZF_1_L4, IsCommutative_def
qed
The lift of a commutative function is commutative on the function space.
lemma func_ZF_2_L2:
assumes \( f : G\times G\rightarrow G \) and \( f \text{ is commutative on } G \) and \( F = f \text{ lifted to function space over } X \)
shows \( F \text{ is commutative on } (X\rightarrow \text{range}(f)) \) using assms, IsCommutative_def, func_ZF_2_L1The lift of an associative function is associative.
lemma func_ZF_2_L3:
assumes A2: \( F = f \text{ lifted to function space over } X \) and A3: \( s : X\rightarrow \text{range}(f) \), \( r : X\rightarrow \text{range}(f) \), \( q : X\rightarrow \text{range}(f) \) and A4: \( f \text{ is associative on } G \)
shows \( F\langle F\langle s,r\rangle ,q\rangle = F\langle s,F\langle r,q\rangle \rangle \)proof from A4, A2 have \( F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f)) \) using IsAssociative_def, func_ZF_1_L3
with A3 have I: \( F\langle s,r\rangle : X\rightarrow \text{range}(f) \), \( F\langle r,q\rangle : X\rightarrow \text{range}(f) \), \( F\langle F\langle s,r\rangle ,q\rangle : X\rightarrow \text{range}(f) \), \( F\langle s,F\langle r,q\rangle \rangle : X\rightarrow \text{range}(f) \) using apply_type
moreover
qed
have \( \forall x\in X.\ (F\langle F\langle s,r\rangle ,q\rangle )(x) = (F\langle s,F\langle r,q\rangle \rangle )(x) \)proof
ultimately show \( thesis \) using fun_extension_iff
fix \( x \)
assume \( x\in X \)
from A4 have \( f:G\times G\rightarrow G \) using IsAssociative_def
then have \( \text{range}(f)\subseteq G \) using func1_1_L5B
with A3, \( x\in X \) have \( s(x) \in G \), \( r(x) \in G \), \( q(x) \in G \) using apply_type
with A2, I, A3, A4, \( x\in X \), \( f:G\times G\rightarrow G \) show \( (F\langle F\langle s,r\rangle ,q\rangle )(x) = (F\langle s,F\langle r,q\rangle \rangle )(x) \) using func_ZF_1_L4, IsAssociative_def
qed
The lift of an associative function is associative on the function space.
lemma func_ZF_2_L4:
assumes A1: \( f \text{ is associative on } G \) and A2: \( F = f \text{ lifted to function space over } X \)
shows \( F \text{ is associative on } (X\rightarrow \text{range}(f)) \)proof from A1, A2 have \( F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f)) \) using IsAssociative_def, func_ZF_1_L3
moreover
qed
from A1, A2 have \( \forall s \in X\rightarrow \text{range}(f).\ \forall r \in X\rightarrow \text{range}(f).\ \forall q \in X\rightarrow \text{range}(f).\ \)
\( F\langle F\langle s,r\rangle ,q\rangle = F\langle s,F\langle r,q\rangle \rangle \) using func_ZF_2_L3
ultimately show \( thesis \) using IsAssociative_def
Restricting operations
In this section we consider conditions under which restriction of the operation to a set inherits properties like commutativity and associativity.
The commutativity is inherited when restricting a function to a set.
lemma func_ZF_4_L1:
assumes A1: \( f:X\times X\rightarrow Y \) and A2: \( A\subseteq X \) and A3: \( f \text{ is commutative on } X \)
shows \( \text{restrict}(f,A\times A) \text{ is commutative on } A \)proof{
}
fix \( x \) \( y \)
assume \( x\in A \) and \( y\in A \)
with A2 have \( x\in X \) and \( y\in X \)
with A3, \( x\in A \), \( y\in A \) have \( \text{restrict}(f,A\times A)\langle x,y\rangle = \text{restrict}(f,A\times A)\langle y,x\rangle \) using IsCommutative_def, restrict_if
then show \( thesis \) using IsCommutative_def
qed
Next we define what it means that a set is closed with respect to an operation.
definition
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
Associative operation restricted to a set that is closed with resp. to this operation is associative.
lemma func_ZF_4_L2:
assumes A1: \( f \text{ is associative on } X \) and A2: \( A\subseteq X \) and A3: \( A \text{ is closed under } f \) and A4: \( x\in A \), \( y\in A \), \( z\in A \) and A5: \( g = \text{restrict}(f,A\times A) \)
shows \( g\langle g\langle x,y\rangle ,z\rangle = g\langle x,g\langle y,z\rangle \rangle \)proof from A4, A2 have I: \( x\in X \), \( y\in X \), \( z\in X \)
from A3, A4, A5 have \( g\langle g\langle x,y\rangle ,z\rangle = f\langle f\langle x,y\rangle ,z\rangle \), \( g\langle x,g\langle y,z\rangle \rangle = f\langle x,f\langle y,z\rangle \rangle \) using IsOpClosed_def, restrict_if
moreover
qed
from A1, I have \( f\langle f\langle x,y\rangle ,z\rangle = f\langle x,f\langle y,z\rangle \rangle \) using IsAssociative_def
ultimately show \( thesis \)
An associative operation restricted to a set that is closed with resp. to this operation is associative on the set.
lemma func_ZF_4_L3:
assumes A1: \( f \text{ is associative on } X \) and A2: \( A\subseteq X \) and A3: \( A \text{ is closed under } f \)
shows \( \text{restrict}(f,A\times A) \text{ is associative on } A \)proof let \( g = \text{restrict}(f,A\times A) \)
from A1 have \( f:X\times X\rightarrow X \) using IsAssociative_def
moreover
from A2 have \( A\times A \subseteq X\times X \)
moreover from A3 have \( \forall p \in A\times A.\ g(p) \in A \) using IsOpClosed_def, restrict_if
ultimately have \( g : A\times A\rightarrow A \) using func1_2_L4
moreover
qed
from A1, A2, A3 have \( \forall x \in A.\ \forall y \in A.\ \forall z \in A.\ \)
\( g\langle g\langle x,y\rangle ,z\rangle = g\langle x,g\langle y,z\rangle \rangle \) using func_ZF_4_L2
ultimately show \( thesis \) using IsAssociative_def
The essential condition to show that if a set \(A\) is closed with respect to an operation, then it is closed under this operation restricted to any superset of \(A\).
lemma func_ZF_4_L4:
assumes \( A \text{ is closed under } f \) and \( A\subseteq B \) and \( x\in A \), \( y\in A \) and \( g = \text{restrict}(f,B\times B) \)
shows \( g\langle x,y\rangle \in A \) using assms, IsOpClosed_def, restrictIf a set \(A\) is closed under an operation, then it is closed under this operation restricted to any superset of \(A\).
lemma func_ZF_4_L5:
assumes A1: \( A \text{ is closed under } f \) and A2: \( A\subseteq B \)
shows \( A \text{ is closed under } \text{restrict}(f,B\times B) \)proof let \( g = \text{restrict}(f,B\times B) \)
from A1, A2 have \( \forall x\in A.\ \forall y\in A.\ g\langle x,y\rangle \in A \) using func_ZF_4_L4
then show \( thesis \) using IsOpClosed_def
qed
The essential condition to show that intersection of sets that are closed with respect to an operation is closed with respect to the operation.
lemma func_ZF_4_L6:
assumes \( A \text{ is closed under } f \) and \( B \text{ is closed under } f \) and \( x \in A\cap B \), \( y\in A\cap B \)
shows \( f\langle x,y\rangle \in A\cap B \) using assms, IsOpClosed_defIntersection of sets that are closed with respect to an operation is closed under the operation.
lemma func_ZF_4_L7:
assumes \( A \text{ is closed under } f \), \( B \text{ is closed under } f \)
shows \( A\cap B \text{ is closed under } f \) using assms, IsOpClosed_defCompositions
For any set \(X\) we can consider a binary operation on the set of functions \(f:X\rightarrow X\) defined by \(C(f,g) = f\circ g\). Composition of functions (or relations) is defined in the standard Isabelle distribution as a higher order function and denoted with the letter O. In this section we consider the corresponding two-argument ZF-function (binary operation), that is a subset of \(((X\rightarrow X)\times (X\rightarrow X))\times (X\rightarrow X)\).
We define the notion of composition on the set \(X\) as the binary operation on the function space \(X\rightarrow X\) that takes two functions and creates the their composition.
definition
\( \text{Composition}(X) \equiv \) \( \{\langle p,\text{fst}(p)\circ \text{snd}(p)\rangle .\ p \in (X\rightarrow X)\times (X\rightarrow X)\} \)
Composition operation is a function that maps \((X\rightarrow X)\times (X\rightarrow X)\) into \(X\rightarrow X\).
lemma func_ZF_5_L1:
shows \( \text{Composition}(X) : (X\rightarrow X)\times (X\rightarrow X)\rightarrow (X\rightarrow X) \) using comp_fun, Composition_def, ZF_fun_from_totalThe value of the composition operation is the composition of arguments.
lemma func_ZF_5_L2:
assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \)
shows \( \text{Composition}(X)\langle f,g\rangle = f\circ g \)proof from assms have \( \text{Composition}(X) : (X\rightarrow X)\times (X\rightarrow X)\rightarrow (X\rightarrow X) \), \( \langle f,g\rangle \in (X\rightarrow X)\times (X\rightarrow X) \), \( \text{Composition}(X) = \{\langle p,\text{fst}(p)\circ \text{snd}(p)\rangle .\ p \in (X\rightarrow X)\times (X\rightarrow X)\} \) using func_ZF_5_L1, Composition_def
then show \( \text{Composition}(X)\langle f,g\rangle = f\circ g \) using ZF_fun_from_tot_val
qed
What is the value of a composition on an argument?
lemma func_ZF_5_L3:
assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \) and \( x\in X \)
shows \( ( \text{Composition}(X)\langle f,g\rangle )(x) = f(g(x)) \) using assms, func_ZF_5_L2, comp_fun_applyThe essential condition to show that composition is associative.
lemma func_ZF_5_L4:
assumes A1: \( f:X\rightarrow X \), \( g:X\rightarrow X \), \( h:X\rightarrow X \) and A2: \( C = \text{Composition}(X) \)
shows \( C\langle C\langle f,g\rangle ,h\rangle = C\langle f,C\langle g,h\rangle \rangle \)proof from A2 have \( C : ((X\rightarrow X)\times (X\rightarrow X))\rightarrow (X\rightarrow X) \) using func_ZF_5_L1
with A1 have I: \( C\langle f,g\rangle : X\rightarrow X \), \( C\langle g,h\rangle : X\rightarrow X \), \( C\langle C\langle f,g\rangle ,h\rangle : X\rightarrow X \), \( C\langle f,C\langle g,h\rangle \rangle : X\rightarrow X \) using apply_funtype
moreover
qed
have \( \forall x \in X.\ C\langle C\langle f,g\rangle ,h\rangle (x) = C\langle f,C\langle g,h\rangle \rangle (x) \)proof
ultimately show \( thesis \) using fun_extension_iff
fix \( x \)
assume \( x\in X \)
with A1, A2, I have \( C\langle C\langle f,g\rangle ,h\rangle (x) = f(g(h(x))) \), \( C\langle f,C\langle g,h\rangle \rangle (x) = f(g(h(x))) \) using func_ZF_5_L3, apply_funtype
then show \( C\langle C\langle f,g\rangle ,h\rangle (x) = C\langle f,C\langle g,h\rangle \rangle (x) \)
qed
Composition is an associative operation on \(X\rightarrow X\) (the space of functions that map \(X\) into itself).
lemma func_ZF_5_L5:
shows \( \text{Composition}(X) \text{ is associative on } (X\rightarrow X) \)proof let \( C = \text{Composition}(X) \)
have \( \forall f\in X\rightarrow X.\ \forall g\in X\rightarrow X.\ \forall h\in X\rightarrow X.\ \)
\( C\langle C\langle f,g\rangle ,h\rangle = C\langle f,C\langle g,h\rangle \rangle \) using func_ZF_5_L4
then show \( thesis \) using func_ZF_5_L1, IsAssociative_def
qed
Identity function
In this section we show some additional facts about the identity function defined in the standard Isabelle's Perm theory. Note there is also image_id_same lemma in func1 theory.
A function that maps every point to itself is the identity on its domain.
lemma indentity_fun:
assumes A1: \( f:X\rightarrow Y \) and A2: \( \forall x\in X.\ f(x)=x \)
shows \( f = id(X) \)proof from assms have \( f:X\rightarrow Y \) and \( id(X):X\rightarrow X \) and \( \forall x\in X.\ f(x) = id(X)(x) \) using id_type, id_conv
then show \( thesis \) by (rule func_eq )
qed
Composing a function with identity does not change the function.
lemma func_ZF_6_L1A:
assumes A1: \( f : X\rightarrow X \)
shows \( \text{Composition}(X)\langle f,id(X)\rangle = f \), \( \text{Composition}(X)\langle id(X),f\rangle = f \)proof have \( \text{Composition}(X) : (X\rightarrow X)\times (X\rightarrow X)\rightarrow (X\rightarrow X) \) using func_ZF_5_L1
with A1 have \( \text{Composition}(X)\langle id(X),f\rangle : X\rightarrow X \), \( \text{Composition}(X)\langle f,id(X)\rangle : X\rightarrow X \) using id_type, apply_funtype
moreover
qed
note A1
moreover from A1 have \( \forall x\in X.\ ( \text{Composition}(X)\langle id(X),f\rangle )(x) = f(x) \), \( \forall x\in X.\ ( \text{Composition}(X)\langle f,id(X)\rangle )(x) = f(x) \) using id_type, func_ZF_5_L3, apply_funtype, id_conv
ultimately show \( \text{Composition}(X)\langle id(X),f\rangle = f \), \( \text{Composition}(X)\langle f,id(X)\rangle = f \) using fun_extension_iff
An intuitively clear, but surprisingly nontrivial fact: identity is the only function from a singleton to itself.
lemma singleton_fun_id:
shows \( (\{x\} \rightarrow \{x\}) = \{id(\{x\})\} \)proof show \( \{id(\{x\})\} \subseteq (\{x\} \rightarrow \{x\}) \) using id_def
{
let \( g = id(\{x\}) \)
fix \( f \)
assume \( f : \{x\} \rightarrow \{x\} \)
then have \( f : \{x\} \rightarrow \{x\} \) and \( g : \{x\} \rightarrow \{x\} \) using id_def
moreover
from \( f : \{x\} \rightarrow \{x\} \) have \( \forall x \in \{x\}.\ f(x) = g(x) \) using apply_funtype, id_def
ultimately have \( f = g \) by (rule func_eq )
then show \( (\{x\} \rightarrow \{x\}) \subseteq \{id(\{x\})\} \)
qed
Another trivial fact: identity is the only bijection of a singleton with itself.
lemma single_bij_id:
shows \( \text{bij}(\{x\},\{x\}) = \{id(\{x\})\} \)proof show \( \{id(\{x\})\} \subseteq \text{bij}(\{x\},\{x\}) \) using id_bij
{
fix \( f \)
assume \( f \in \text{bij}(\{x\},\{x\}) \)
then have \( f : \{x\} \rightarrow \{x\} \) using bij_is_fun
then have \( f \in \{id(\{x\})\} \) using singleton_fun_id
then show \( \text{bij}(\{x\},\{x\}) \subseteq \{id(\{x\})\} \)
qed
A kind of induction for the identity: if a function \(f\) is the identity on a set with a fixpoint of \(f\) removed, then it is the indentity on the whole set.
lemma id_fixpoint_rem:
assumes A1: \( f:X\rightarrow X \) and A2: \( p\in X \) and A3: \( f(p) = p \) and A4: \( \text{restrict}(f, X-\{p\}) = id(X-\{p\}) \)
shows \( f = id(X) \)proof from A1 have \( f: X\rightarrow X \) and \( id(X) : X\rightarrow X \) using id_def
moreover {
}
}
qed
fix \( x \)
assume \( x\in X \)
{
assume \( x \in X-\{p\} \)
then have \( f(x) = \text{restrict}(f, X-\{p\})(x) \) using restrict
with A4, \( x \in X-\{p\} \) have \( f(x) = x \) using id_def
with A2, A3, \( x\in X \) have \( f(x) = x \)
then have \( \forall x\in X.\ f(x) = id(X)(x) \) using id_def
ultimately show \( f = id(X) \) by (rule func_eq )
Lifting to subsets
Suppose we have a binary operation \(f : X \times X \rightarrow X\) written additively as \(f\langle x,y\rangle = x + y\). Such operation naturally defines another binary operation on the subsets of \(X\) that satisfies \(A+B = \{ x+y : x \in A, y\in B\}\). This new operation which we will call "\(f\) lifted to subsets" inherits many properties of \(f\), such as associativity, commutativity and existence of the neutral element. This notion is useful for considering interval arithmetics.
The next definition describes the notion of a binary operation lifted to subsets. It is written in a way that might be a bit unexpected, but really it is the same as the intuitive definition, but shorter. In the definition we take a pair \(p \in Pow(X)\times Pow(X)\), say \(p = \langle A, B\rangle \), where \(A,B \subseteq X\). Then we assign this pair of sets the set \(\{f\langle x,y \rangle : x\in A, y\in B \} = \{ f(x'): x' \in A\times B\}\) The set on the right hand side is the same as the image of \(A\times B\) under \(f\). In the definition we don't use \(A\) and \(B\) symbols, but write \( \text{fst}(p) \) and \( \text{snd}(p) \), resp. Recall that in Isabelle/ZF \( \text{fst}(p) \) and \( \text{snd}(p) \) denote the first and second components of an ordered pair \(p\). See the lemma lift_subsets_explained for a more intuitive notation.
definition
\( f \text{ lifted to subsets of } X \equiv \) \( \{\langle p, f(\text{fst}(p)\times \text{snd}(p))\rangle .\ p \in Pow(X)\times Pow(X)\} \)
The lift to subsets defines a binary operation on the subsets.
lemma lift_subsets_binop:
assumes A1: \( f : X \times X \rightarrow Y \)
shows \( (f \text{ lifted to subsets of } X) : Pow(X) \times Pow(X) \rightarrow Pow(Y) \)proof let \( F = \{\langle p, f(\text{fst}(p)\times \text{snd}(p))\rangle .\ p \in Pow(X)\times Pow(X)\} \)
from A1 have \( \forall p \in Pow(X) \times Pow(X).\ f(\text{fst}(p)\times \text{snd}(p)) \in Pow(Y) \) using func1_1_L6
then have \( F : Pow(X) \times Pow(X) \rightarrow Pow(Y) \) by (rule ZF_fun_from_total )
then show \( thesis \) unfolding Lift2Subsets_def
qed
The definition of the lift to subsets rewritten in a more intuitive notation. We would like to write the last assertion as \( F\langle A,B\rangle = \{f\langle x,y\rangle .\ x \in A, y \in B\} \), but Isabelle/ZF does not allow such syntax.
lemma lift_subsets_explained:
assumes A1: \( f : X\times X \rightarrow Y \) and A2: \( A \subseteq X \), \( B \subseteq X \) and A3: \( F = f \text{ lifted to subsets of } X \)
shows \( F\langle A,B\rangle \subseteq Y \) and \( F\langle A,B\rangle = f(A\times B) \), \( F\langle A,B\rangle = \{f(p).\ p \in A\times B\} \), \( F\langle A,B\rangle = \{f\langle x,y\rangle .\ \langle x,y\rangle \in A\times B\} \)proof let \( p = \langle A,B\rangle \)
from assms have I: \( F : Pow(X) \times Pow(X) \rightarrow Pow(Y) \) and \( p \in Pow(X) \times Pow(X) \) using lift_subsets_binop
moreover
from A3 have \( F = \{\langle p, f(\text{fst}(p)\times \text{snd}(p))\rangle .\ p \in Pow(X)\times Pow(X)\} \) unfolding Lift2Subsets_def
ultimately show \( F\langle A,B\rangle = f(A\times B) \) using ZF_fun_from_tot_val
also
from A1, A2 have \( A\times B \subseteq X\times X \)
with A1 have \( f(A\times B) = \{f(p).\ p \in A\times B\} \) by (rule func_imagedef )
finally show \( F\langle A,B\rangle = \{f(p) .\ p \in A\times B\} \)
also
have \( \forall x\in A.\ \forall y \in B.\ f\langle x,y\rangle = f\langle x,y\rangle \)
then have \( \{f(p).\ p \in A\times B\} = \{f\langle x,y\rangle .\ \langle x,y\rangle \in A\times B\} \) by (rule ZF1_1_L4A )
finally show \( F\langle A,B\rangle = \{f\langle x,y\rangle .\ \langle x,y\rangle \in A\times B\} \)
from A2, I show \( F\langle A,B\rangle \subseteq Y \) using apply_funtype
qed
A sufficient condition for a point to belong to a result of lifting to subsets.
lemma lift_subset_suff:
assumes A1: \( f : X \times X \rightarrow Y \) and A2: \( A \subseteq X \), \( B \subseteq X \) and A3: \( x\in A \), \( y\in B \) and A4: \( F = f \text{ lifted to subsets of } X \)
shows \( f\langle x,y\rangle \in F\langle A,B\rangle \)proof from A3 have \( f\langle x,y\rangle \in \{f(p) .\ p \in A\times B\} \)
moreover
qed
from A1, A2, A4 have \( \{f(p).\ p \in A\times B\} = F\langle A,B\rangle \) using lift_subsets_explained
ultimately show \( f\langle x,y\rangle \in F\langle A,B\rangle \)
A kind of converse of lift_subset_apply, providing a necessary condition for a point to be in the result of lifting to subsets.
lemma lift_subset_nec:
assumes A1: \( f : X \times X \rightarrow Y \) and A2: \( A \subseteq X \), \( B \subseteq X \) and A3: \( F = f \text{ lifted to subsets of } X \) and A4: \( z \in F\langle A,B\rangle \)
shows \( \exists x y.\ x\in A \wedge y\in B \wedge z = f\langle x,y\rangle \)proof from A1, A2, A3 have \( F\langle A,B\rangle = \{f(p).\ p \in A\times B\} \) using lift_subsets_explained
with A4 show \( thesis \)
qed
Lifting to subsets inherits commutativity.
lemma lift_subset_comm:
assumes A1: \( f : X \times X \rightarrow Y \) and A2: \( f \text{ is commutative on } X \) and A3: \( F = f \text{ lifted to subsets of } X \)
shows \( F \text{ is commutative on } Pow(X) \)proof have \( \forall A \in Pow(X).\ \forall B \in Pow(X).\ F\langle A,B\rangle = F\langle B,A\rangle \)proof
{
}
fix \( A \)
assume \( A \in Pow(X) \)
fix \( B \)
assume \( B \in Pow(X) \)
have \( F\langle A,B\rangle = F\langle B,A\rangle \)proof
have \( \forall z \in F\langle A,B\rangle .\ z \in F\langle B,A\rangle \)proof
fix \( z \)
assume I: \( z \in F\langle A,B\rangle \)
with A1, A3, \( A \in Pow(X) \), \( B \in Pow(X) \) have \( \exists x y.\ x\in A \wedge y\in B \wedge z = f\langle x,y\rangle \) using lift_subset_nec
then obtain \( x \) \( y \) where \( x\in A \) and \( y\in B \) and \( z = f\langle x,y\rangle \)
with A2, \( A \in Pow(X) \), \( B \in Pow(X) \) have \( z = f\langle y,x\rangle \) using IsCommutative_def
with A1, A3, I, \( A \in Pow(X) \), \( B \in Pow(X) \), \( x\in A \), \( y\in B \) show \( z \in F\langle B,A\rangle \) using lift_subset_suff
qed
moreover
qed
have \( \forall z \in F\langle B,A\rangle .\ z \in F\langle A,B\rangle \)proof
ultimately show \( F\langle A,B\rangle = F\langle B,A\rangle \)
fix \( z \)
assume I: \( z \in F\langle B,A\rangle \)
with A1, A3, \( A \in Pow(X) \), \( B \in Pow(X) \) have \( \exists x y.\ x\in B \wedge y\in A \wedge z = f\langle x,y\rangle \) using lift_subset_nec
then obtain \( x \) \( y \) where \( x\in B \) and \( y\in A \) and \( z = f\langle x,y\rangle \)
with A2, \( A \in Pow(X) \), \( B \in Pow(X) \) have \( z = f\langle y,x\rangle \) using IsCommutative_def
with A1, A3, I, \( A \in Pow(X) \), \( B \in Pow(X) \), \( x\in B \), \( y\in A \) show \( z \in F\langle A,B\rangle \) using lift_subset_suff
qed
thus \( thesis \)
qed
then show \( F \text{ is commutative on } Pow(X) \) unfolding IsCommutative_def
qed
Lifting to subsets inherits associativity. To show that \(F\langle \langle A,B\rangle C\rangle = F\langle A,F\langle B,C\rangle\rangle\) we prove two inclusions and the proof of the second inclusion is very similar to the proof of the first one.
lemma lift_subset_assoc:
assumes A1: \( f \text{ is associative on } X \) and A2: \( F = f \text{ lifted to subsets of } X \)
shows \( F \text{ is associative on } Pow(X) \)proof from A1 have \( f : X\times X \rightarrow X \) unfolding IsAssociative_def
with A2 have \( F : Pow(X)\times Pow(X) \rightarrow Pow(X) \) using lift_subsets_binop
moreover
qed
have \( \forall A \in Pow(X).\ \forall B \in Pow(X).\ \forall C \in Pow(X).\ \)
\( F\langle F\langle A,B\rangle ,C\rangle = F\langle A,F\langle B,C\rangle \rangle \)proof
ultimately show \( thesis \) unfolding IsAssociative_def
{
}
fix \( A \) \( B \) \( C \)
assume \( A \in Pow(X) \), \( B \in Pow(X) \), \( C \in Pow(X) \)
have \( F\langle F\langle A,B\rangle ,C\rangle \subseteq F\langle A,F\langle B,C\rangle \rangle \)proof
fix \( z \)
assume I: \( z \in F\langle F\langle A,B\rangle ,C\rangle \)
from \( f:X\times X \rightarrow X \), A2, \( A \in Pow(X) \), \( B \in Pow(X) \) have \( F\langle A,B\rangle \in Pow(X) \) using lift_subsets_binop, apply_funtype
with \( f:X\times X \rightarrow X \), A2, \( C \in Pow(X) \), I have \( \exists x y.\ x \in F\langle A,B\rangle \wedge y \in C \wedge z = f\langle x,y\rangle \) using lift_subset_nec
then obtain \( x \) \( y \) where II: \( x \in F\langle A,B\rangle \) and \( y \in C \) and III: \( z = f\langle x,y\rangle \)
from \( f:X\times X \rightarrow X \), A2, \( A \in Pow(X) \), \( B \in Pow(X) \), II have \( \exists s t.\ s \in A \wedge t \in B \wedge x = f\langle s,t\rangle \) using lift_subset_nec
then obtain \( s \) \( t \) where \( s\in A \) and \( t\in B \) and \( x = f\langle s,t\rangle \)
with A1, \( A \in Pow(X) \), \( B \in Pow(X) \), \( C \in Pow(X) \), III, \( s\in A \), \( t\in B \), \( y\in C \) have IV: \( z = f\langle s, f\langle t,y\rangle \rangle \) using IsAssociative_def
from \( f:X\times X \rightarrow X \), A2, \( B \in Pow(X) \), \( C \in Pow(X) \), \( t\in B \), \( y\in C \) have \( f\langle t,y\rangle \in F\langle B,C\rangle \) using lift_subset_suff
moreover
qed
from \( f:X\times X \rightarrow X \), A2, \( B \in Pow(X) \), \( C \in Pow(X) \) have \( F\langle B,C\rangle \subseteq X \) using lift_subsets_binop, apply_funtype
moreover note \( f:X\times X \rightarrow X \), A2, \( A \in Pow(X) \), \( s\in A \), IV
ultimately show \( z \in F\langle A,F\langle B,C\rangle \rangle \) using lift_subset_suff
moreover
have \( F\langle A,F\langle B,C\rangle \rangle \subseteq F\langle F\langle A,B\rangle ,C\rangle \)proof
ultimately have \( F\langle F\langle A,B\rangle ,C\rangle = F\langle A,F\langle B,C\rangle \rangle \)
fix \( z \)
assume I: \( z \in F\langle A,F\langle B,C\rangle \rangle \)
from \( f:X\times X \rightarrow X \), A2, \( B \in Pow(X) \), \( C \in Pow(X) \) have \( F\langle B,C\rangle \in Pow(X) \) using lift_subsets_binop, apply_funtype
with \( f:X\times X \rightarrow X \), A2, \( A \in Pow(X) \), I have \( \exists x y.\ x \in A \wedge y \in F\langle B,C\rangle \wedge z = f\langle x,y\rangle \) using lift_subset_nec
then obtain \( x \) \( y \) where \( x \in A \) and II: \( y \in F\langle B,C\rangle \) and III: \( z = f\langle x,y\rangle \)
from \( f:X\times X \rightarrow X \), A2, \( B \in Pow(X) \), \( C \in Pow(X) \), II have \( \exists s t.\ s \in B \wedge t \in C \wedge y = f\langle s,t\rangle \) using lift_subset_nec
then obtain \( s \) \( t \) where \( s\in B \) and \( t\in C \) and \( y = f\langle s,t\rangle \)
with III have \( z = f\langle x,f\langle s,t\rangle \rangle \)
moreover
from A1, \( A \in Pow(X) \), \( B \in Pow(X) \), \( C \in Pow(X) \), \( x\in A \), \( s\in B \), \( t\in C \) have \( f\langle f\langle x,s\rangle ,t\rangle = f\langle x,f\langle s,t\rangle \rangle \) using IsAssociative_def
ultimately have IV: \( z = f\langle f\langle x,s\rangle ,t\rangle \)
from \( f:X\times X \rightarrow X \), A2, \( A \in Pow(X) \), \( B \in Pow(X) \), \( x\in A \), \( s\in B \) have \( f\langle x,s\rangle \in F\langle A,B\rangle \) using lift_subset_suff
moreover
qed
from \( f:X\times X \rightarrow X \), A2, \( A \in Pow(X) \), \( B \in Pow(X) \) have \( F\langle A,B\rangle \subseteq X \) using lift_subsets_binop, apply_funtype
moreover note \( f:X\times X \rightarrow X \), A2, \( C \in Pow(X) \), \( t\in C \), IV
ultimately show \( z \in F\langle F\langle A,B\rangle ,C\rangle \) using lift_subset_suff
thus \( thesis \)
qed
Distributive operations
In this section we deal with pairs of operations such that one is distributive with respect to the other, that is \(a\cdot (b+c) = a\cdot b + a\cdot c\) and \((b+c)\cdot a = b\cdot a + c\cdot a\). We show that this property is preserved under restriction to a set closed with respect to both operations. In EquivClass1 theory we show that this property is preserved by projections to the quotient space if both operations are congruent with respect to the equivalence relation.
We define distributivity as a statement about three sets. The first set is the set on which the operations act. The second set is the additive operation (a ZF function) and the third is the multiplicative operation.
definition
\( \text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\ \) \( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \) \( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle ) \)
The essential condition to show that distributivity is preserved by restrictions to sets that are closed with respect to both operations.
lemma func_ZF_7_L1:
assumes A1: \( \text{IsDistributive}(X,A,M) \) and A2: \( Y\subseteq X \) and A3: \( Y \text{ is closed under } A \), \( Y \text{ is closed under } M \) and A4: \( A_r = \text{restrict}(A,Y\times Y) \), \( M_r = \text{restrict}(M,Y\times Y) \) and A5: \( a\in Y \), \( b\in Y \), \( c\in Y \)
shows \( M_r\langle a,A_r\langle b,c\rangle \rangle = A_r\langle M_r\langle a,b\rangle ,M_r\langle a,c\rangle \rangle \wedge \) \( M_r\langle A_r\langle b,c\rangle ,a \rangle = A_r\langle M_r\langle b,a\rangle , M_r\langle c,a\rangle \rangle \)proof from A3, A5 have \( A\langle b,c\rangle \in Y \), \( M\langle a,b\rangle \in Y \), \( M\langle a,c\rangle \in Y \), \( M\langle b,a\rangle \in Y \), \( M\langle c,a\rangle \in Y \) using IsOpClosed_def
with A5, A4 have \( A_r\langle b,c\rangle \in Y \), \( M_r\langle a,b\rangle \in Y \), \( M_r\langle a,c\rangle \in Y \), \( M_r\langle b,a\rangle \in Y \), \( M_r\langle c,a\rangle \in Y \) using restrict
with A1, A2, A4, A5 show \( thesis \) using restrict, IsDistributive_def
qed
Distributivity is preserved by restrictions to sets that are closed with respect to both operations.
lemma func_ZF_7_L2:
assumes \( \text{IsDistributive}(X,A,M) \) and \( Y\subseteq X \) and \( Y \text{ is closed under } A \), \( Y \text{ is closed under } M \) and \( A_r = \text{restrict}(A,Y\times Y) \), \( M_r = \text{restrict}(M,Y\times Y) \)
shows \( \text{IsDistributive}(Y,A_r,M_r) \)proof from assms have \( \forall a\in Y.\ \forall b\in Y.\ \forall c\in Y.\ \)
\( M_r\langle a,A_r\langle b,c\rangle \rangle = A_r\langle M_r\langle a,b\rangle ,M_r\langle a,c\rangle \rangle \wedge \)
\( M_r\langle A_r\langle b,c\rangle ,a \rangle = A_r\langle M_r\langle b,a\rangle ,M_r\langle c,a\rangle \rangle \) using func_ZF_7_L1
then show \( thesis \) using IsDistributive_def
qed
end
lemma func1_1_L5B:
assumes \( f:X\rightarrow Y \)
shows \( \text{range}(f) \subseteq 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 func_ZF_1_L1:
assumes \( f : Y\times Y\rightarrow Y \) and \( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f)) \)
shows \( \{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\} : X\rightarrow \text{range}(f) \) 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 \)Definition of Lift2FcnSpce:
\( f \text{ lifted to function space over } X \equiv \)
\( \{\langle p,\{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\}\rangle .\ \)
\( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\} \)
lemma func_ZF_1_L2:
assumes \( f : Y\times Y\rightarrow Y \) and \( p \in (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f)) \) and \( x\in X \) and \( P = \{\langle x,f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \rangle .\ x \in X\} \)
shows \( P(x) = f\langle \text{fst}(p)(x),\text{snd}(p)(x)\rangle \) theorem func_ZF_1_L3:
assumes \( f : Y\times Y\rightarrow Y \) and \( F = f \text{ lifted to function space over } X \)
shows \( F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f)) \) theorem func_ZF_1_L4:
assumes \( f : Y\times Y\rightarrow Y \) and \( F = f \text{ lifted to function space over } X \) and \( s:X\rightarrow \text{range}(f) \), \( r:X\rightarrow \text{range}(f) \) and \( x\in X \)
shows \( (F\langle s,r\rangle )(x) = f\langle s(x),r(x)\rangle \)Definition of IsCommutative:
\( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
lemma func_ZF_2_L1:
assumes \( f : G\times G\rightarrow G \) and \( F = f \text{ lifted to function space over } X \) and \( s : X\rightarrow \text{range}(f) \), \( r : X\rightarrow \text{range}(f) \) and \( f \text{ is commutative on } G \)
shows \( F\langle s,r\rangle = F\langle r,s\rangle \)Definition of IsAssociative:
\( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \)
\( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \)
\( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
lemma func_ZF_2_L3:
assumes \( F = f \text{ lifted to function space over } X \) and \( s : X\rightarrow \text{range}(f) \), \( r : X\rightarrow \text{range}(f) \), \( q : X\rightarrow \text{range}(f) \) and \( f \text{ is associative on } G \)
shows \( F\langle F\langle s,r\rangle ,q\rangle = F\langle s,F\langle r,q\rangle \rangle \)Definition of IsOpClosed:
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma func1_2_L4:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \) and \( \forall x\in A.\ f(x) \in Z \)
shows \( \text{restrict}(f,A) : A\rightarrow Z \) lemma func_ZF_4_L2:
assumes \( f \text{ is associative on } X \) and \( A\subseteq X \) and \( A \text{ is closed under } f \) and \( x\in A \), \( y\in A \), \( z\in A \) and \( g = \text{restrict}(f,A\times A) \)
shows \( g\langle g\langle x,y\rangle ,z\rangle = g\langle x,g\langle y,z\rangle \rangle \) lemma func_ZF_4_L4:
assumes \( A \text{ is closed under } f \) and \( A\subseteq B \) and \( x\in A \), \( y\in A \) and \( g = \text{restrict}(f,B\times B) \)
shows \( g\langle x,y\rangle \in A \)Definition of Composition:
\( \text{Composition}(X) \equiv \)
\( \{\langle p,\text{fst}(p)\circ \text{snd}(p)\rangle .\ p \in (X\rightarrow X)\times (X\rightarrow X)\} \)
lemma func_ZF_5_L1: shows \( \text{Composition}(X) : (X\rightarrow X)\times (X\rightarrow X)\rightarrow (X\rightarrow X) \)
lemma func_ZF_5_L2:
assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \)
shows \( \text{Composition}(X)\langle f,g\rangle = f\circ g \) lemma func_ZF_5_L3:
assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \) and \( x\in X \)
shows \( ( \text{Composition}(X)\langle f,g\rangle )(x) = f(g(x)) \) lemma func_ZF_5_L4:
assumes \( f:X\rightarrow X \), \( g:X\rightarrow X \), \( h:X\rightarrow X \) and \( C = \text{Composition}(X) \)
shows \( C\langle C\langle f,g\rangle ,h\rangle = C\langle f,C\langle g,h\rangle \rangle \) 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 singleton_fun_id: shows \( (\{x\} \rightarrow \{x\}) = \{id(\{x\})\} \)
lemma func1_1_L6:
assumes \( f:X\rightarrow Y \)
shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)Definition of Lift2Subsets:
\( f \text{ lifted to subsets of } X \equiv \)
\( \{\langle p, f(\text{fst}(p)\times \text{snd}(p))\rangle .\ p \in Pow(X)\times Pow(X)\} \)
lemma lift_subsets_binop:
assumes \( f : X \times X \rightarrow Y \)
shows \( (f \text{ lifted to subsets of } X) : Pow(X) \times Pow(X) \rightarrow Pow(Y) \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) lemma ZF1_1_L4A:
assumes \( \forall x\in X.\ \forall y\in Y.\ a(\langle x,y\rangle ) = b(x,y) \)
shows \( \{a(p).\ p \in X\times Y\} = \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \) lemma lift_subsets_explained:
assumes \( f : X\times X \rightarrow Y \) and \( A \subseteq X \), \( B \subseteq X \) and \( F = f \text{ lifted to subsets of } X \)
shows \( F\langle A,B\rangle \subseteq Y \) and \( F\langle A,B\rangle = f(A\times B) \), \( F\langle A,B\rangle = \{f(p).\ p \in A\times B\} \), \( F\langle A,B\rangle = \{f\langle x,y\rangle .\ \langle x,y\rangle \in A\times B\} \) lemma lift_subset_nec:
assumes \( f : X \times X \rightarrow Y \) and \( A \subseteq X \), \( B \subseteq X \) and \( F = f \text{ lifted to subsets of } X \) and \( z \in F\langle A,B\rangle \)
shows \( \exists x y.\ x\in A \wedge y\in B \wedge z = f\langle x,y\rangle \) lemma lift_subset_suff:
assumes \( f : X \times X \rightarrow Y \) and \( A \subseteq X \), \( B \subseteq X \) and \( x\in A \), \( y\in B \) and \( F = f \text{ lifted to subsets of } X \)
shows \( f\langle x,y\rangle \in F\langle A,B\rangle \)Definition of IsDistributive:
\( \text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\ \)
\( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \)
\( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle ) \)
lemma func_ZF_7_L1:
assumes \( \text{IsDistributive}(X,A,M) \) and \( Y\subseteq X \) and \( Y \text{ is closed under } A \), \( Y \text{ is closed under } M \) and \( A_r = \text{restrict}(A,Y\times Y) \), \( M_r = \text{restrict}(M,Y\times Y) \) and \( a\in Y \), \( b\in Y \), \( c\in Y \)
shows \( M_r\langle a,A_r\langle b,c\rangle \rangle = A_r\langle M_r\langle a,b\rangle ,M_r\langle a,c\rangle \rangle \wedge \) \( M_r\langle A_r\langle b,c\rangle ,a \rangle = A_r\langle M_r\langle b,a\rangle , M_r\langle c,a\rangle \rangle \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8