:: We present a proof of Cantor-Bernstein-Schr\"oder based on Knaster's argument in~\cite{Knaster1928}.
:: The proof is given at a level of detail sufficient to prepare the reader to consider corresponding formal
:: proofs in interactive theorem provers.
environ
vocabularies CBS,SEQM_3,RELAT_1, XBOOLE_0, PARTFUN1, FUNCT_1, TARSKI, SUBSET_1, ZFMISC_1,
RELAT_2, MCART_1, SETFAM_1, FUNCT_2, GROUP_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1,
MCART_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2;
constructors RELAT_2, PARTFUN1, MCART_1, SETFAM_1, RELSET_1,
XTUPLE_0, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1,
GRFUNC_1, ZFMISC_1, FUNCT_2, FUNCOP_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1, FUNCT_2;
equalities PARTFUN1, SUBSET_1;
expansions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1, FUNCT_2;
theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, PARTFUN1, GRFUNC_1, RELSET_1,
SUBSET_1, XBOOLE_0, XBOOLE_1, RELAT_2, MCART_1, SETFAM_1, XTUPLE_0, FUNCT_2;
schemes FUNCT_1, PARTFUN1, XBOOLE_0, RELSET_1, SUBSET_1, FUNCT_2;
begin
:
reserve A,B,C for set;
reserve F for Function of bool A, bool B;
reserve G for Function of bool B, bool C;
reserve H for Function of bool A, bool C;
reserve U,V for Subset of A;
:: Let $\Phi:\wp(A)\to\wp(B)$. We say $\Phi$ is {\em{monotone}} if
:: $\Phi(U)\subseteq \Phi(V)$ forall $U,V\in\wp(A)$ such that $U\subseteq V$.
:: We say $\Phi$ is {\em{antimonotone}} if
:: $\Phi(V)\subseteq \Phi(U)$ forall $U,V\in\wp(A)$ such that $U\subseteq V$.
definition
let A,B; let F;
attr F is monotone means :DefMon:
for U,V st U c= V holds F . U c= F . V;
attr F is anti-monotone means :DefAntiMon:
for U,V st U c= V holds F . V c= F . U;
end;
:: For sets $A$ and $B$ we
:: write $A\setminus B$ for $\{u\in A | u\notin B\}$.
:: JU: this is A \ B in Mizar:
theorem A \ B = A \ B;
:: Let $A$ be a set and $\Phi:\wp(A)\to\wp(A)$ be
:: given by $\Phi(X)= A\setminus X$.
:: Then $\Phi$ is antimonotone.
theorem TSetMinusAntimon:
for F being Function of bool A, bool A st
(for U holds F . U = A \ U) holds
F is anti-monotone;
:: Let $f:A\to B$ be a function from a set $A$ to a set $B$.
:: For $X\in \wp(A)$ we write $f(X)$ for $\{f(x) | x\in X\}$.
:: JU: this is F " X or F .:X - lets test:
theorem F .: U = F .: U;
reserve f for Function of A, B;
:: Let $f:A\to B$ be a function from a set $A$ to a set $B$.
:: Let $\Phi:\wp(A)\to\wp(B)$ be given by $\Phi(X) = f(X)$.
:: Then $\Phi$ is monotone.
theorem TImMon:
for F st ( for U holds F . U = f .: U)
holds F is monotone
proof
let F;
assume A0: for U holds F . U = f .: U;
let U,V such that A1: U c= V;
A2: f .: U c= f .: V by RELAT_1:123,A1;
F . V = f .: V & F . U = f .: U by A0;
hence F . U c= F . V by A2;
end;
theorem TAMonMon:
F is anti-monotone & G is monotone
& (for U holds H . U = G . (F . U)) implies
H is anti-monotone
proof
assume Z0: F is anti-monotone;
assume Z1: G is monotone;
assume Z2: for U holds H . U = G . (F . U);
let U,V such that Z3: U c= V;
Z4: F . V c= F . U by Z3,Z0;
then G . (F . V) c= G . (F . U) by Z1;
then H . V c= G . (F . U) by Z2;
hence H . V c= H . U by Z2;
end;
theorem TAMonAMon:
F is anti-monotone & G is anti-monotone
& (for U holds H . U = G . (F . U)) implies
H is monotone;
theorem TMonMon:
F is monotone & G is monotone
& (for U holds H . U = G . (F . U)) implies
H is monotone;
theorem TMonMon1:
F is monotone & G is monotone implies G * F is monotone
proof
assume Z4: F is monotone;
assume Z5: G is monotone;
let U,V such that Z6: U c= V;
Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;
(G * F) . V = G . (F . V) by FUNCT_2:15;
hence (G * F) . U c= (G * F) . V by Z7,Z5,Z6,Z4;
end;
registration
let A,B;
cluster monotone anti-monotone for Function of bool A, bool B;
existence
proof
consider F being constant Function of bool A, bool B such that not contradiction;
take F;
thus F is monotone
proof
let U,V such that A1: U c= V;
U in bool A & V in bool A;
then U in dom F & V in dom F by FUNCT_2:def 1; :: [ATP details]
then F . U = F . V by FUNCT_1:def 10;
hence F . U c= F . V;
end;
let U,V such that A1: U c= V;
U in bool A & V in bool A;
then U in dom F & V in dom F by FUNCT_2:def 1; :: [ATP details]
then F . U = F . V by FUNCT_1:def 10;
hence F . V c= F . U;
end;
end;
registration
let A,B,C;
let F be monotone Function of bool A, bool B;
let G be monotone Function of bool B, bool C;
cluster G * F -> monotone for Function of bool A, bool C;
correctness by TMonMon1;
end;
theorem TAMonAMon1:
F is anti-monotone & G is anti-monotone implies G * F is monotone
proof
assume Z4: F is anti-monotone;
assume Z5: G is anti-monotone;
let U,V such that Z6: U c= V;
Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;
(G * F) . V = G . (F . V) by FUNCT_2:15;
hence (G * F) . U c= (G * F) . V by Z7,Z5,Z6,Z4;
end;
registration
let A,B,C;
let F be anti-monotone Function of bool A, bool B;
let G be anti-monotone Function of bool B, bool C;
cluster G * F -> monotone for Function of bool A, bool C;
correctness by TAMonAMon1;
end;
theorem TAMonMon1:
F is anti-monotone & G is monotone implies G * F is anti-monotone
proof
assume Z4: F is anti-monotone;
assume Z5: G is monotone;
let U,V such that Z6: U c= V;
Z7: (G * F) . U = G . (F . U) by FUNCT_2:15;
(G * F) . V = G . (F . V) by FUNCT_2:15;
hence (G * F) . V c= (G * F) . U by Z7,Z5,Z6,Z4;
end;
registration
let A,B,C;
let F be anti-monotone Function of bool A, bool B;
let G be monotone Function of bool B, bool C;
cluster G * F -> anti-monotone for Function of bool A, bool C;
correctness by TAMonMon1;
end;
reserve x,y for Element of A;
::$N Knaster-Tarski theorem
:: Let $\Phi:\wp(A)\to\wp(A)$.
:: Assume $\Phi$ is monotone.
:: Then there is some $Y\in\wp(A)$ such that $\Phi(Y)=Y$.
theorem TKnasterTarski:
for A for F being Function of bool A, bool A st F is monotone holds
ex U st F . U = U
proof
let A;
let F be Function of bool A, bool A;
assume A0: F is monotone;
:: Let $Y$ be $\{u\in A | \forall X\in\wp(A). \Phi(X)\subseteq X \to u\in X\}$.
set Y0 = {U : F . U c= U };
B0: Y0 is non empty
proof
F . [#] A c= A;
then [#] A in Y0;
hence thesis;
end;
Y0 c= bool A
proof
let u be object such that Z1: u in Y0;
consider U such that Z2: U = u & F . U c= U by Z1;
U in bool A;
hence thesis by B0,Z2;
end;
then reconsider Y1 = Y0 as Subset-Family of A by B0;
set Y = meet Y1;
Y is Subset of A;
take Y;
A1: for U st (F . U c= U) holds Y c= U
proof
let U; assume Z1: F . U c= U; then U in Y0;
hence Y c= U by SETFAM_1:3; :: [ATP details]
end;
thus A2: F . Y c= Y
proof
let z be object such that B1: z in F.Y;
:: for U st (F . U c= U) holds z in U;
for u being set st u in Y0 holds z in u
proof
let u be set such that Z2: u in Y0;
consider U such that Z3: u = U and Z4: F . U c= U by Z2;
Y c= U by A1,Z4;
then F . Y c= F . U by A0,DefMon;
hence z in u by B1,Z3,Z4,TARSKI:def 3;
end;
then z in meet Y0 by B0,SETFAM_1:def 1;
hence z in Y;
end;
thus Y c= F . Y
proof
F . (F . Y) c= F . Y by A2,A0,DefMon;
hence Y c= F . Y by A1;
end;
end;
reserve A,B for non empty set;
reserve f for Function of A, B;
reserve x,y,z,u for object;
:: Let $f:A\to B$ be a function.
:: We say $f$ is {\em{injective}} if $\forall xy\in A. f(x) = f(y) \to x = y$.
:: JU: this is one-to-one in Mizar:
:: for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2;
theorem ThInj:
f is one-to-one iff for x,y being object st x in A & y in A & f . x = f . y holds x = y by FUNCT_2:19; :: [ATP details]
:: We say sets $A$ and $B$ are {\em{equipotent}} if there exists a relation $R$ such that
:: \item $\forall x\in A.\exists y\in B. (x,y)\in R$
:: \item $\forall y\in B.\exists x\in A. (x,y)\in R$
:: \item $\forall x\in A.\forall y\in B.\forall z\in A.\forall w\in B.(x,y)\in R \land (z,w)\in R \to (x=z \iff y=w)$
theorem A,B are_equipotent iff A,B are_equipotent;
:: JU: this is exactly in Mizar:
:: pred X,Y are_equipotent means
:: :: TARSKI:def 6
:: ex Z st
:: (for x st x in X ex y st y in Y & [x,y] in Z) &
:: (for y st y in Y ex x st x in X & [x,y] in Z) &
:: for x,y,z,u st [x,y] in Z & [z,u] in Z holds x = z iff y = u;
reserve g for Function of B, A;
reserve U,V for Subset of A;
reserve W for Subset of B;
:: this is by KNASTER:12; too bad, let's ignore KNASTER
:: If $f:A\to B$ and $g:B\to A$ are injective,
:: then $A$ and $B$ are equipotent.
theorem TCBS:
f is one-to-one & g is one-to-one implies A,B are_equipotent
proof
assume A0: f is one-to-one & g is one-to-one;
:: Let $\Phi:\wp(A)\to\wp(A)$ be defined by $\Phi(X) = g(B\setminus f(A\setminus X))$.
deffunc F0(Subset of A) = g .: ( B \ ( f .: ( A \ $1)));
:: here we need Satallax in the ATP service - done only for version 1275 :-(
consider F being Function of bool A, bool A such that
A1: F . U = F0(U) from FUNCT_2:sch 4;
:: It is easy to see that $\Phi$ is monotone by Lemmas~\ref{setminusantimon} and~\ref{immon}.
A2: F is monotone
proof
:: JU: the pain of working with lambda functions in Mizar
deffunc F1(Subset of A) = A \ $1;
deffunc F2(Subset of A) = f .: $1;
deffunc F3(Subset of B) = B \ $1;
deffunc F4(Subset of B) = g .: $1;
consider G1 being Function of bool A, bool A such that B1: G1 . U = F1(U) from FUNCT_2:sch 4;
consider G2 being Function of bool A, bool B such that B2: G2 . U = F2(U) from FUNCT_2:sch 4;
consider G3 being Function of bool B, bool B such that B3: G3 . W = F3(W) from FUNCT_2:sch 4;
consider G4 being Function of bool B, bool A such that B4: G4 . W = F4(W) from FUNCT_2:sch 4;
B5: F0(U) = F4(F3(F2(F1(U))));
B6: for u being object st u in bool A holds F . u = G4 . ( G3 . ( G2 . ( G1 . u )))
& F . u = ( G4 * ( G3 * ( G2 * G1 ) ) ) . u
proof
let u be object such that D1: u in bool A;
reconsider U=u as Element of bool A by D1;
D2: F . U = F0(U) by A1 .= F4(F3(F2(F1(U)))) .= F4(F3(F2( G1 . U ))) by B1
.= F4(F3(G2 . ( G1 . U ))) by B2
.= F4(G3 . (G2 . ( G1 . U ))) by B3
.= G4 . (G3 . (G2 . ( G1 . U ))) by B4;
G2 . ( G1 . U ) = ( G2 * G1 ) . U by FUNCT_2:15;
then G3 . (G2 . ( G1 . U )) = (G3 * ( G2 * G1 )) . U by FUNCT_2:15;
then G4. (G3 . (G2 . ( G1 . U ))) = (G4 * (G3 * ( G2 * G1 ))) . U by FUNCT_2:15;
hence thesis by D2,FUNCT_2:15;
end;
then B7: F = G4 * ( G3 * ( G2 * G1 ) ) by FUNCT_2:15,FUNCT_2:12;
C1: G1 is anti-monotone by TSetMinusAntimon,B1; :: [ATP details]
C2: G2 is monotone by TImMon,B2;
C3: G3 is anti-monotone by TSetMinusAntimon,B3; :: [ATP details]
C4: G4 is monotone by TImMon,B4;
hence F is monotone by B7,C1,C2,C3,C4;
end;
consider C being Subset of A such that A3: F . C = C by TKnasterTarski,A2; :: [ATP details]
A4: C c= A;
A5: for x being object holds x in C iff x in g .: ( B \ ( f .: ( A \ C))) by A1,A3; :: [ATP details]
:: Let $R = \{(x,y)\in A\times B| x\notin C \land y = f(x) \lor x\in C \land x = g(y)\}$.
set R = {[x,y] where x is Element of A, y is Element of B : (not x in C & y = f . x) or (x in C & x = g . y )};
take R;
thus for x st x in A ex y st y in B & [x,y] in R
proof
let x such that B0: x in A;
reconsider x1 = x as Element of A by B0;
per cases;
suppose B1: not x1 in C;
take y = f . x1;
thus y in B;
thus [x,y] in R by B1;
end;
suppose B2: x1 in C;
then x1 in g .: ( B \ ( f .: ( A \ C))) by A5;
then consider y being object such that B3: y in B & y in B \ ( f .: ( A \ C)) & x1 = g . y by FUNCT_2:64,A5,B2; :: [ATP details]
take y;
thus y in B by B3;
thus [x,y] in R by B2,B3;
end;
end;
thus for y st y in B ex x st x in A & [x,y] in R;
:: \forall x\in A.\forall y \in B. x\in C \land x = g(y) \to y\notin f(A\setminus C)
A6: for x,y st x in A & y in B & x in C & x = g . y holds not y in f .: (A \ C);
thus for x,y,z,u st [x,y] in R & [z,u] in R holds x = z iff y = u;
end;
:: If $f:A\to B$ is injective and $B\subseteq A$,
:: then $A$ and $B$ are equipotent.
theorem TCor1:
f is one-to-one & B c= A implies A,B are_equipotent;