:: Homeomorphism between Finite Topological Spaces, Two-Dimensional Lattice
:: Spaces and a Fixed Point Theorem
:: by Masami Tanaka , Hiroshi Imura and Yatsuka Nakamura
::
:: Received July 6, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, XXREAL_0, CARD_1,
FINSEQ_1, ORDERS_2, TOPS_2, FUNCT_2, FIN_TOPO, STRUCT_0, ARYTM_3,
EQREL_1, XCMPLX_0, FINTOPO4, NAT_1, ARYTM_1, TARSKI, COMPLEX1, INT_1,
ZFMISC_1, RELAT_2, FINTOPO5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, RELSET_1, EQREL_1, FUNCT_2,
FINSEQ_1, STRUCT_0, FIN_TOPO, FINTOPO3, ENUMSET1, ORDERS_2, FINTOPO4,
COMPLEX1, INT_1;
constructors ENUMSET1, REAL_1, NAT_1, EQREL_1, FIN_TOPO, FINTOPO3, FINTOPO4,
NAT_D, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, CARD_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities FINSEQ_1, FIN_TOPO, RELAT_1;
expansions TARSKI, FIN_TOPO;
theorems NAT_1, NAT_2, ZFMISC_1, INT_1, FUNCT_1, FUNCT_2, FINSEQ_1, ABSVALUE,
RELSET_1, XBOOLE_0, XBOOLE_1, UNIFORM1, FINTOPO3, ENUMSET1, FINTOPO4,
TARSKI, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, XREAL_0, NAT_D, XTUPLE_0;
schemes NAT_1, FUNCT_2;
begin
theorem Th1:
for X being set, Y being non empty set, f being Function of X,Y,
A being Subset of X st f is one-to-one holds f".:(f.:A)=A
proof
let X be set, Y be non empty set, f be Function of X,Y, A be Subset of X;
A1: dom f = X by FUNCT_2:def 1;
assume f is one-to-one;
hence thesis by A1,FUNCT_1:107;
end;
theorem
for n being Nat holds n>0 iff Seg n<>{};
definition
let FT1,FT2 be RelStr, h be Function of FT1, FT2;
attr h is being_homeomorphism means
h is one-to-one onto & for x
being Element of FT1 holds h.:U_FT x = Im(the InternalRel of FT2,h.x);
end;
theorem Th3:
for FT1,FT2 being non empty RelStr, h being Function of FT1, FT2
st h is being_homeomorphism ex g being Function of FT2, FT1 st g=h" & g is
being_homeomorphism
proof
let FT1,FT2 be non empty RelStr, h be Function of FT1, FT2;
assume
A1: h is being_homeomorphism;
then
A2: h is one-to-one onto;
then
A3: rng h = the carrier of FT2 by FUNCT_2:def 3;
then reconsider g2=h" as Function of FT2, FT1 by A2,FUNCT_2:25;
A4: for y being Element of FT2 holds g2.:U_FT(y)=Im(the InternalRel of FT1,
g2.y)
proof
let y be Element of FT2;
reconsider x = g2.y as Element of FT1;
y=h.x & h.:U_FT x= Im(the InternalRel of FT2,h.x) by A1,A3,
FUNCT_1:35;
hence thesis by A2,Th1;
end;
rng g2=dom h by A2,FUNCT_1:33
.=the carrier of FT1 by FUNCT_2:def 1;
then
A5: g2 is onto by FUNCT_2:def 3;
g2 is one-to-one by A2,FUNCT_1:40;
then g2 is being_homeomorphism by A5,A4;
hence thesis;
end;
theorem Th4:
for FT1,FT2 being non empty RelStr, h being Function of FT1, FT2,
n being Nat, x being Element of FT1, y being Element of FT2 st h is
being_homeomorphism & y=h.x holds for z being Element of FT1 holds z in U_FT(x,
n) iff h.z in U_FT(y,n)
proof
let FT1,FT2 be non empty RelStr, h be Function of FT1, FT2, n be Nat,
x be Element of FT1,y be Element of FT2;
assume that
A1: h is being_homeomorphism and
A2: y=h.x;
A3: h is one-to-one onto by A1;
let z be Element of FT1;
x in the carrier of FT1;
then
A4: x in dom h by FUNCT_2:def 1;
z in the carrier of FT1;
then
A5: z in dom h by FUNCT_2:def 1;
A6: now
defpred P[Nat] means for w being Element of FT2 holds w in U_FT
(y,$1) implies h".w in U_FT(x,$1);
assume
A7: h.z in U_FT(y,n);
consider g being Function of FT2, FT1 such that
A8: g=h" and
A9: g is being_homeomorphism by A1,Th3;
A10: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A11: P[k];
for w being Element of FT2 holds w in U_FT(y,k+1) implies h".w in
U_FT(x,k+1)
proof
let w be Element of FT2;
A12: U_FT(y,k+1)=(U_FT(y,k))^f by FINTOPO3:48;
assume w in U_FT(y,k+1);
then consider x3 being Element of FT2 such that
A13: x3=w and
A14: ex y3 being Element of FT2 st y3 in U_FT(y,k) & x3 in U_FT y3 by A12;
consider y2 being Element of FT2 such that
A15: y2 in U_FT(y,k) and
A16: x3 in U_FT y2 by A14;
reconsider q=g.y2, p=g.x3 as Element of FT1;
A17: for w2 being Element of FT2 holds w2 in U_FT(y2,0) implies h".w2
in U_FT(q,0)
proof
let w2 be Element of FT2;
w2 in the carrier of FT2;
then
A18: w2 in dom g by FUNCT_2:def 1;
A19: h".:U_FT(y2)=Class(the InternalRel of FT1,h".y2) by A8,A9;
hereby
assume w2 in U_FT(y2,0);
then w2 in U_FT y2 by FINTOPO3:47;
then h".w2 in U_FT q by A8,A19,A18,FUNCT_1:def 6;
hence h".w2 in U_FT(q,0) by FINTOPO3:47;
end;
end;
x3 in U_FT(y2,0) by A16,FINTOPO3:47;
then p in U_FT(q,0) by A8,A17;
then
A20: p in U_FT q by FINTOPO3:47;
q in U_FT(x,k) by A8,A11,A15;
then p in (U_FT(x,k))^f by A20;
hence thesis by A8,A13,FINTOPO3:48;
end;
hence thesis;
end;
A21: g.y=x by A2,A4,A3,A8,FUNCT_1:34;
for w being Element of FT2 holds w in U_FT(y,0) implies h".w in U_FT( x,0)
proof
let w be Element of FT2;
w in the carrier of FT2;
then
A22: w in dom g by FUNCT_2:def 1;
A23: g.:U_FT(y)=Class(the InternalRel of FT1,g.y) by A9;
hereby
assume w in U_FT(y,0);
then w in U_FT y by FINTOPO3:47;
then g.w in U_FT x by A21,A23,A22,FUNCT_1:def 6;
hence h".w in U_FT(x,0) by A8,FINTOPO3:47;
end;
end;
then
A24: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A24,A10);
then h".(h.z) in U_FT(x,n) by A7;
hence z in U_FT(x,n) by A3,A5,FUNCT_1:34;
end;
now
defpred P[Nat] means for w being Element of FT1 holds w in U_FT
(x,$1) implies h.w in U_FT(y,$1);
assume
A25: z in U_FT(x,n);
A26: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A27: P[k];
for w being Element of FT1 holds w in U_FT(x,k+1) implies h.w in
U_FT(y,k+1)
proof
let w be Element of FT1;
A28: U_FT(x,k+1)=(U_FT(x,k))^f by FINTOPO3:48;
assume w in U_FT(x,k+1);
then consider x3 being Element of FT1 such that
A29: x3=w and
A30: ex y3 being Element of FT1 st y3 in U_FT(x,k) & x3 in U_FT y3 by A28;
consider y2 being Element of FT1 such that
A31: y2 in U_FT(x,k) and
A32: x3 in U_FT y2 by A30;
reconsider q=h.y2, p=h.x3 as Element of FT2;
A33: for w2 being Element of FT1 holds w2 in U_FT(y2,0) implies h.w2
in U_FT(q,0)
proof
let w2 be Element of FT1;
w2 in the carrier of FT1;
then
A34: w2 in dom h by FUNCT_2:def 1;
A35: h.:U_FT(y2)=Class(the InternalRel of FT2,h.y2) by A1;
hereby
assume w2 in U_FT(y2,0);
then w2 in U_FT y2 by FINTOPO3:47;
then h.w2 in U_FT q by A35,A34,FUNCT_1:def 6;
hence h.w2 in U_FT(q,0) by FINTOPO3:47;
end;
end;
x3 in U_FT(y2,0) by A32,FINTOPO3:47;
then p in U_FT(q,0) by A33;
then
A36: p in U_FT q by FINTOPO3:47;
q in U_FT(y,k) by A27,A31;
then p in (U_FT(y,k))^f by A36;
hence thesis by A29,FINTOPO3:48;
end;
hence thesis;
end;
for w being Element of FT1 holds w in U_FT(x,0) implies h.w in U_FT(y ,0)
proof
let w be Element of FT1;
w in the carrier of FT1;
then
A37: w in dom h by FUNCT_2:def 1;
A38: h.:U_FT(x)=Class(the InternalRel of FT2,h.x) by A1;
hereby
assume w in U_FT(x,0);
then w in U_FT x by FINTOPO3:47;
then h.w in U_FT y by A2,A38,A37,FUNCT_1:def 6;
hence h.w in U_FT(y,0) by FINTOPO3:47;
end;
end;
then
A39: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A39,A26);
hence h.z in U_FT(y,n) by A25;
end;
hence thesis by A6;
end;
theorem
for FT1,FT2 being non empty RelStr, h being Function of FT1, FT2, n
being Nat,x being Element of FT1,y being Element of FT2 st h is
being_homeomorphism & y=h.x holds for v being Element of FT2 holds h".v in U_FT
(x,n) iff v in U_FT(y,n)
proof
let FT1,FT2 be non empty RelStr, h be Function of FT1, FT2, n be Nat,
x be Element of FT1,y be Element of FT2;
assume that
A1: h is being_homeomorphism and
A2: y=h.x;
x in the carrier of FT1;
then
A3: x in dom h by FUNCT_2:def 1;
consider g being Function of FT2, FT1 such that
A4: g=h" and
A5: g is being_homeomorphism by A1,Th3;
h is one-to-one onto by A1;
then x=g.y by A2,A4,A3,FUNCT_1:34;
hence thesis by A4,A5,Th4;
end;
theorem
for n being non zero Nat, f being Function of FTSL1 n,
FTSL1 n st f is_continuous 0 holds ex p being Element of FTSL1 n st f.p in U_FT
(p,0)
proof
let n be non zero Nat, f be Function of FTSL1 n, FTSL1 n;
assume
A1: f is_continuous 0;
assume
A2: for p being Element of FTSL1 n holds not f.p in U_FT(p,0);
defpred P2[Nat] means $1>0 & for j being Nat st $1<=n & j=f.$1 holds $1>j;
A3: n>=0+1 by NAT_1:13;
A4: RelStr(# Seg n,Nbdl1 n #)=FTSL1 n by FINTOPO4:def 4;
A5: FTSL1 n is filled by FINTOPO4:18;
now
A6: n in the carrier of FTSL1 n by A3,A4;
then reconsider p2=n as Element of FTSL1 n;
p2 in U_FT p2 by A5;
then
A7: p2 in U_FT(p2,0) by FINTOPO3:47;
given j being Nat such that
A8: j=f.n and
A9: n<=j;
f.n in the carrier of FTSL1 n by A6,FUNCT_2:5;
then j<=n by A4,A8,FINSEQ_1:1;
then n=j by A9,XXREAL_0:1;
hence contradiction by A2,A8,A7;
end;
then
A10: for j being Nat st n<=n & j=f.n holds n>j;
then
A11: ex k being Nat st P2[k];
ex k being Nat st P2[k] & for m being Nat st P2[m] holds k <= m from
NAT_1:sch 5(A11);
then consider k being Nat such that
A12: P2[k] and
A13: for m being Nat st P2[m] holds k <= m;
A14: 0+1<=k by A12,NAT_1:13;
then
A15: k-1>=0 by XREAL_1:48;
then
A16: k-1=k-'1 by XREAL_0:def 2;
A17: k<=n by A10,A13;
then reconsider pk=k as Element of FTSL1 n by A4,A14,FINSEQ_1:1;
k<k+1 by NAT_1:13;
then
A18: k-1 < k+1-1 by XREAL_1:9;
now
per cases by A13,A16,A18;
case
A19: k-'1<=0;
1 in the carrier of FTSL1 n by A3,A4;
then
A20: f.1 in Seg n by A4,FUNCT_2:5;
then reconsider j0=f.1 as Nat;
k-1=0 by A15,A19,XREAL_0:def 2;
then 1>j0 by A3,A12;
hence contradiction by A20,FINSEQ_1:1;
end;
case
A21: k-'1>0 & ex j being Nat st k-'1<=n & j=f.(k-'1) & k-'1<=j;
A22: k in the carrier of FTSL1 n by A4,A17,A14;
then
A23: f.k in Seg n by A4,FUNCT_2:5;
then reconsider jn=f.k as Nat;
jn<jn+1 by NAT_1:13;
then
A24: jn-1<jn+1-1 by XREAL_1:9;
A25: k-'1>=0+1 by A21,NAT_1:13;
then
A26: k-'1=k or k-'1=max(k-'1,1) or k-'1=min(k+1,n) by XXREAL_0:def 10;
consider j being Nat such that
A27: k-'1<=n and
A28: j=f.(k-'1) and
A29: k-'1<=j by A21;
reconsider pkm=k-'1 as Element of FTSL1 n by A4,A27,A25,FINSEQ_1:1;
k-'1 in Seg n by A27,A25;
then
A30: Im(Nbdl1 n,pkm)={k-'1,max(k-'1-'1,1),min(k-'1+1,n)} by FINTOPO4:def 3;
Im(Nbdl1 n,k)={k,max(k-'1,1),min(k+1,n)} by A4,A22,FINTOPO4:def 3;
then k-'1 in U_FT pk by A4,A26,ENUMSET1:def 1;
then
A31: k-'1 in U_FT(pk,0) by FINTOPO3:47;
reconsider pfk=jn as Element of FTSL1 n by A22,FUNCT_2:5;
A32: f.:( U_FT(pk,0)) c= U_FT(pfk,0) by A1,FINTOPO4:def 2;
A33: jn <k by A12,A17;
then
A34: jn+1<=k by NAT_1:13;
A35: k-'1 in the carrier of FTSL1 n by A4,A27,A25;
now
assume
A36: k-'1=j;
then reconsider pj=j as Element of FTSL1 n by A35;
pj in U_FT pj by A5;
then f.j in U_FT(pj,0) by A28,A36,FINTOPO3:47;
hence contradiction by A2;
end;
then k-'1<j by A29,XXREAL_0:1;
then
A37: k-'1+1<=j by NAT_1:13;
then
A38: jn<j by A16,A33,XXREAL_0:2;
j in the carrier of FTSL1 n by A28,A35,FUNCT_2:5;
then
A39: j<=n by A4,FINSEQ_1:1;
now
assume
A40: k=j;
then min(k-'1+1,n)=k-'1+1 by A16,A39,XXREAL_0:def 9;
then k in U_FT pkm by A4,A16,A30,ENUMSET1:def 1;
then f.(k-'1) in U_FT(pkm,0) by A28,A40,FINTOPO3:47;
hence contradiction by A2;
end;
then
A41: k<j by A16,A37,XXREAL_0:1;
A42: now
per cases;
case
jn+1<=n;
hence j<> min(jn+1,n) by A41,A34,XXREAL_0:def 9;
end;
case
A43: jn+1>n;
then jn>=n by NAT_1:13;
hence j<> min(jn+1,n) by A38,A43,XXREAL_0:def 9;
end;
end;
A44: 1<=jn by A23,FINSEQ_1:1;
then jn-1>=0 by XREAL_1:48;
then
A45: jn-1=jn-'1 by XREAL_0:def 2;
A46: now
per cases;
suppose
jn-'1>=1;
hence j<> max(jn-'1,1) by A38,A45,A24,XXREAL_0:def 10;
end;
suppose
jn-'1<1;
hence j<> max(jn-'1,1) by A44,A38,XXREAL_0:def 10;
end;
end;
k-'1 in dom f by A35,FUNCT_2:def 1;
then f.(k-'1) in f.:(U_FT(pk,0)) by A31,FUNCT_1:def 6;
then
A47: j in U_FT(pfk,0) by A28,A32;
Im(Nbdl1 n,jn)={jn,max(jn-'1,1),min(jn+1,n)} by A23,FINTOPO4:def 3;
then not j in U_FT pfk by A4,A16,A37,A33,A46,A42,ENUMSET1:def 1;
hence contradiction by A47,FINTOPO3:47;
end;
end;
hence thesis;
end;
theorem Th7:
for T being non empty RelStr, p being Element of T, k being
Nat st T is filled holds U_FT(p,k) c= U_FT(p,k+1)
proof
let T be non empty RelStr, p be Element of T, k be Nat;
A1: U_FT(p,k+1) = (U_FT(p,k))^f by FINTOPO3:48;
assume T is filled;
hence thesis by A1,FINTOPO3:1;
end;
theorem Th8:
for T being non empty RelStr, p being Element of T, k being
Nat st T is filled holds U_FT(p,0) c= U_FT(p,k)
proof
let T be non empty RelStr, p be Element of T, k be Nat;
defpred P[Nat] means U_FT(p,0) c= U_FT(p,$1);
assume
A1: T is filled;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
U_FT(p,k) c= U_FT(p,k+1) by A1,Th7;
hence thesis by A3,XBOOLE_1:1;
end;
A4: P[0];
for i being Nat holds P[i] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th9:
for n being non zero Nat, jn,j,k being Nat, p being Element of
FTSL1 n st p=jn holds j in U_FT(p,k) iff j in Seg n & |.jn-j.|<= k+1
proof
let n be non zero Nat, jn,j,k be Nat,p be Element of FTSL1 n;
A1: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
assume
A2: p=jn;
A3: now
defpred P[Nat] means for j2,jn2 being Nat,p2 being Element of FTSL1 n st
jn2=p2 & j2 in Seg n & |.jn2-j2.|<= $1+1 holds j2 in U_FT(p2,$1);
A4: P[0]
proof
let j2,jn2 be Nat,p2 be Element of FTSL1 n;
assume that
A5: jn2=p2 and
A6: j2 in Seg n and
A7: |.jn2-j2.|<= 0+1;
A8: j2<=n by A6,FINSEQ_1:1;
A9: 1<=j2 by A6,FINSEQ_1:1;
now
per cases;
case
jn2-j2>=0;
then
A10: jn2-j2=jn2-'j2 by XREAL_0:def 2;
A11: jn2-'j2>=0+1 or jn2-'j2=0 by NAT_1:13;
jn2-j2<= 1 by A7,ABSVALUE:def 1;
then
A12: jn2-j2=1 or jn2-'j2=0 by A10,A11,XXREAL_0:1;
per cases by A10,A12;
suppose
A13: jn2-1=j2;
then jn2-1=jn2-'1 by XREAL_0:def 2;
hence j2=jn2 or j2=max(jn2-'1,1) or j2=min(jn2+1,n) by A9,A13,
XXREAL_0:def 10;
end;
suppose
jn2=j2;
hence j2=jn2 or j2=max(jn2-'1,1) or j2=min(jn2+1,n);
end;
end;
case
A14: jn2-j2<0;
then jn2-j2+j2<0+j2 by XREAL_1:8;
then
A15: jn2+1<=j2 by NAT_1:13;
-(jn2-j2)<= 1 by A7,A14,ABSVALUE:def 1;
then j2-jn2+jn2<=1+jn2 by XREAL_1:7;
then jn2+1=j2 by A15,XXREAL_0:1;
hence j2=jn2 or j2=max(jn2-'1,1) or j2=min(jn2+1,n) by A8,
XXREAL_0:def 9;
end;
end;
then jn2 in NAT & j2 in {jn2,max(jn2-'1,1),min(jn2+1,n)} by
ENUMSET1:def 1,ORDINAL1:def 12;
then j2 in U_FT p2 by A1,A5,FINTOPO4:def 3;
hence thesis by FINTOPO3:47;
end;
A16: for jj being Nat st P[jj] holds P[jj+1]
proof
let jj be Nat;
assume
A17: P[jj];
let j2,jn2 be Nat,p2 be Element of FTSL1 n;
assume that
A18: jn2=p2 and
A19: j2 in Seg n and
A20: |.jn2-j2.|<= jj+1+1;
A21: j2<=n by A19,FINSEQ_1:1;
reconsider x0=j2 as Element of FTSL1 n by A1,A19;
A22: 1<=j2 by A19,FINSEQ_1:1;
A23: jn2<=n by A1,A18,FINSEQ_1:1;
A24: 1<=jn2 by A1,A18,FINSEQ_1:1;
A25: now
per cases;
suppose
A26: jn2-j2>=0;
per cases by A26;
suppose
A27: jn2-j2=0;
(FTSL1 n) is filled by FINTOPO4:18;
then
A28: x0 in U_FT p2 by A18,A27;
|.jn2-j2.|<=jj+1 by A27,ABSVALUE:def 1;
hence ex y being Element of FTSL1 n st y in U_FT(p2,jj) & x0 in
U_FT y by A17,A18,A19,A27,A28;
end;
suppose
A29: jn2-j2>0;
then jn2-j2=jn2-'j2 by XREAL_0:def 2;
then
A30: jn2-j2>=0+1 by A29,NAT_1:13;
then jn2-j2+j2>=1+j2 by XREAL_1:7;
then
A31: n>=j2+1 by A23,XXREAL_0:2;
j2<j2+1 by NAT_1:13;
then
A32: jn2-(j2+1)<jn2-j2 by XREAL_1:15;
|.jn2-j2.|=jn2-j2 by A29,ABSVALUE:def 1;
then
A33: jn2-(j2+1)<jj+1+1 by A20,A32,XXREAL_0:2;
A34: jn2-j2-1>=1-1 by A30,XREAL_1:9;
then jn2-'(j2+1)=jn2-(j2+1) by XREAL_0:def 2;
then jn2-(j2+1)<=jj+1 by A33,NAT_1:13;
then
A35: |.jn2-(j2+1).|<=jj+1 by A34,ABSVALUE:def 1;
1<=j2+1 by A22,NAT_1:13;
then
A36: j2+1 in Seg n by A31;
then reconsider yj2=j2+1 as Element of FTSL1 n by A1;
|.j2+1-j2.|=1 by ABSVALUE:def 1;
then x0 in U_FT(yj2,0) by A4,A19;
then x0 in U_FT yj2 by FINTOPO3:47;
hence ex y being Element of FTSL1 n st y in U_FT(p2,jj) & x0 in
U_FT y by A17,A18,A36,A35;
end;
end;
suppose
jn2-j2<0;
then
A37: jn2-j2+j2<0+j2 by XREAL_1:6;
then
A38: j2-jn2>0 by XREAL_1:50;
j2-1>=0 by A22,XREAL_1:48;
then
A39: j2-1=j2-'1 by XREAL_0:def 2;
jn2+1<=j2 by A37,NAT_1:13;
then
A40: jn2+1-1<=j2-1 by XREAL_1:9;
then j2-1-jn2>=0 by XREAL_1:48;
then
A41: |.(j2-'1)-jn2.|=(j2-'1)-jn2 by A39,ABSVALUE:def 1;
j2<j2+1 by NAT_1:13;
then j2-1<j2+1-1 by XREAL_1:9;
then
A42: j2-'1<n by A21,A39,XXREAL_0:2;
|.jn2-j2.|=|.j2-jn2.| by UNIFORM1:11
.=1+((j2-'1)-jn2) by A39,A38,ABSVALUE:def 1
.=1+|.jn2-(j2-'1).| by A41,UNIFORM1:11;
then
A43: |.jn2-(j2-'1).|<=jj+1 by A20,XREAL_1:6;
j2-'1>=1 by A24,A40,A39,XXREAL_0:2;
then
A44: j2-'1 in Seg n by A42;
then reconsider pj21=j2-'1 as Element of FTSL1 n by A1;
|.j2-'1-j2.|=|.j2-(j2-'1).| by UNIFORM1:11
.=1 by A39,ABSVALUE:def 1;
then x0 in U_FT(pj21,0) by A4,A19;
then x0 in U_FT pj21 by FINTOPO3:47;
hence ex y being Element of FTSL1 n st y in U_FT(p2,jj) & x0 in U_FT
y by A17,A18,A44,A43;
end;
end;
U_FT(p2,jj+1)=(U_FT(p2,jj))^f by FINTOPO3:48
.= {x where x is Element of FTSL1 n: ex y being Element of FTSL1 n
st y in U_FT(p2,jj) & x in U_FT y};
hence thesis by A25;
end;
A45: for ii being Nat holds P[ii] from NAT_1:sch 2(A4,A16);
assume j in Seg n & |.jn-j.|<= k+1;
hence j in U_FT(p,k) by A2,A45;
end;
now
defpred P[Nat] means for j2,jn2 being Nat,p2 being Element of FTSL1 n st
jn2=p2 & j2 in U_FT(p2,$1) holds |.jn2-j2.|<=$1+1;
A46: P[0]
proof
let j2,jn2 be Nat,p2 being Element of FTSL1 n;
assume that
A47: jn2=p2 and
A48: j2 in U_FT(p2,0);
A49: j2 in U_FT p2 by A48,FINTOPO3:47;
jn2 in NAT by ORDINAL1:def 12;
then
A50: Im(Nbdl1 n,jn2)={jn2,max(jn2-'1,1),min(jn2+1,n)} by A1,A47,FINTOPO4:def 3
;
A51: jn2<=n by A1,A47,FINSEQ_1:1;
per cases by A1,A47,A49,A50,ENUMSET1:def 1;
suppose
j2=jn2;
hence |.jn2-j2.|<=0+1 by ABSVALUE:2;
end;
suppose
A52: j2=max(jn2-'1,1);
per cases;
suppose
A53: jn2-'1>=1;
then j2=jn2-'1 by A52,XXREAL_0:def 10;
then j2=jn2-1 by A53,NAT_D:39;
hence |.jn2-j2.|<=0+1 by ABSVALUE:def 1;
end;
suppose
A54: jn2-'1<1;
then jn2-'1<0+1;
then jn2-'1=0 by NAT_1:13;
then
A55: 1-jn2>=0 by NAT_D:36,XREAL_1:48;
1<=1+jn2 by NAT_1:12;
then
A56: 1-jn2<=1+jn2-jn2 by XREAL_1:9;
j2=1 by A52,A54,XXREAL_0:def 10;
then |.j2-jn2.|=1-jn2 by A55,ABSVALUE:def 1;
hence |.jn2-j2.|<=0+1 by A56,UNIFORM1:11;
end;
end;
suppose
A57: j2=min(jn2+1,n);
per cases;
suppose
jn2+1<=n;
then j2=jn2+1 by A57,XXREAL_0:def 9;
then |.j2-jn2.|=1 by ABSVALUE:def 1;
hence |.jn2-j2.|<=0+1 by UNIFORM1:11;
end;
suppose
A58: jn2+1>n;
then jn2>=n by NAT_1:13;
then
A59: jn2=n by A51,XXREAL_0:1;
j2=n by A57,A58,XXREAL_0:def 9;
hence |.jn2-j2.|<=0+1 by A59,ABSVALUE:2;
end;
end;
end;
A60: for i2 being Nat st P[i2] holds P[i2+1]
proof
let i2 be Nat;
assume
A61: P[i2];
let j3,jn3 be Nat,p2 being Element of FTSL1 n;
assume that
A62: jn3=p2 and
A63: j3 in U_FT(p2,i2+1);
U_FT(p2,i2+1)=(U_FT(p2,i2))^f by FINTOPO3:48
.= {x where x is Element of FTSL1 n: ex y being Element of FTSL1 n
st y in U_FT(p2,i2) & x in U_FT y};
then consider x being Element of FTSL1 n such that
A64: x=j3 and
A65: ex y being Element of FTSL1 n st y in U_FT(p2,i2) & x in U_FT y by A63;
consider y being Element of FTSL1 n such that
A66: y in U_FT(p2,i2) and
A67: x in U_FT y by A65;
y in Seg n by A1;
then reconsider iy=y as Nat;
x in U_FT(y,0) by A67,FINTOPO3:47;
then
A68: |.iy-j3.|<=1 by A46,A64;
|.jn3-iy.|<=i2+1 by A61,A62,A66;
then
A69: |.jn3-iy.|+|.iy-j3.|<=i2+1+1 by A68,XREAL_1:7;
|.jn3-iy+(iy-j3).|<=|.jn3-iy.|+|.iy-j3.| by COMPLEX1:56;
hence |.jn3-j3.|<=i2+1+1 by A69,XXREAL_0:2;
end;
A70: for i3 being Nat holds P[i3] from NAT_1:sch 2(A46,A60);
assume j in U_FT(p,k);
hence j in Seg n & |.jn-j.|<= k+1 by A2,A1,A70;
end;
hence thesis by A3;
end;
:: Fixed Point Theorem
theorem
for kc,km being Nat, n being non zero Nat, f
being Function of FTSL1 n, FTSL1 n st f is_continuous kc & km=[/ (kc/2) \]
holds ex p being Element of FTSL1 n st f.p in U_FT(p,km)
proof
let kc,km be Nat, n be non zero Nat, f be Function of
FTSL1 n, FTSL1 n;
assume that
A1: f is_continuous kc and
A2: km=[/ (kc/2) \];
assume
A3: for p being Element of FTSL1 n holds not f.p in U_FT(p,km);
defpred P2[Nat] means $1>0 & for j being Nat st $1<=n & j=f.$1 holds $1>j;
A4: n>=0+1 by NAT_1:13;
A5: RelStr(# Seg n,Nbdl1 n #)=FTSL1 n by FINTOPO4:def 4;
A6: FTSL1 n is filled by FINTOPO4:18;
now
A7: n in the carrier of FTSL1 n by A4,A5;
then reconsider p2=n as Element of FTSL1 n;
given j being Nat such that
A8: j=f.n and
A9: n<=j;
f.n in the carrier of FTSL1 n by A7,FUNCT_2:5;
then j<=n by A5,A8,FINSEQ_1:1;
then
A10: n=j by A9,XXREAL_0:1;
p2 in U_FT p2 by A6;
then
A11: p2 in U_FT(p2,0) by FINTOPO3:47;
U_FT(p2,0) c= U_FT(p2,km) by Th8,FINTOPO4:18;
hence contradiction by A3,A8,A10,A11;
end;
then
A12: for j being Nat st n<=n & j=f.n holds n>j;
then
A13: ex k being Nat st P2[k];
ex k being Nat st P2[k] & for m being Nat st P2[m] holds k <= m from
NAT_1:sch 5(A13);
then consider k being Nat such that
A14: P2[k] and
A15: for m being Nat st P2[m] holds k <= m;
A16: 0+1<=k by A14,NAT_1:13;
then
A17: k-1>=0 by XREAL_1:48;
then
A18: k-1=k-'1 by XREAL_0:def 2;
k<k+1 by NAT_1:13;
then
A19: k-1 < k+1-1 by XREAL_1:9;
A20: k<=n by A12,A15;
then reconsider pk=k as Element of FTSL1 n by A5,A16,FINSEQ_1:1;
per cases by A15,A18,A19;
suppose
A21: k-'1<=0;
1 in the carrier of FTSL1 n by A4,A5;
then
A22: f.1 in Seg n by A5,FUNCT_2:5;
then reconsider j0=f.1 as Nat;
k-1=0 by A17,A21,XREAL_0:def 2;
then 1>j0 by A4,A14;
hence contradiction by A22,FINSEQ_1:1;
end;
suppose
A23: k-'1>0 & ex j being Nat st k-'1<=n & j=f.(k-'1) & k-'1<=j;
A24: k in the carrier of FTSL1 n by A5,A20,A16;
then f.k in Seg n by A5,FUNCT_2:5;
then reconsider jn=f.k as Nat;
A25: not jn in U_FT(pk,km) by A3;
A26: jn <k by A14,A20;
then
A27: k-jn>0 by XREAL_1:50;
jn in Seg n by A5,A24,FUNCT_2:5;
then not |.k-jn.|<=km+1 by A25,Th9;
then
A28: k-jn>km+1 by A27,ABSVALUE:def 1;
k-jn=k-'jn by A27,XREAL_0:def 2;
then
A29: k-jn>=km+1+1 by A28,NAT_1:13;
reconsider pfk=jn as Element of FTSL1 n by A24,FUNCT_2:5;
A30: kc <kc+2 by XREAL_1:29;
A31: k-'1>=0+1 by A23,NAT_1:13;
then
A32: k-'1=max(k-'1,1) by XXREAL_0:def 10;
Im(Nbdl1 n,k)={k,max(k-'1,1),min(k+1,n)} by A5,A24,FINTOPO4:def 3;
then k-'1 in U_FT pk by A5,A32,ENUMSET1:def 1;
then
A33: k-'1 in U_FT(pk,0) by FINTOPO3:47;
consider j being Nat such that
A34: k-'1<=n and
A35: j=f.(k-'1) and
A36: k-'1<=j by A23;
reconsider pkm=k-'1 as Element of FTSL1 n by A5,A34,A31,FINSEQ_1:1;
A37: not j in U_FT(pkm,km) by A3,A35;
A38: k-'1 in the carrier of FTSL1 n by A5,A34,A31;
then k-'1 in dom f by FUNCT_2:def 1;
then
A39: f.(k-'1) in f.:( U_FT(pk,0)) by A33,FUNCT_1:def 6;
now
assume
A40: k-'1=j;
then reconsider pj=j as Element of FTSL1 n by A38;
pj in U_FT pj by A6;
then
A41: pj in U_FT(pj,0) by FINTOPO3:47;
U_FT(pj,0) c= U_FT(pj,km) by Th8,FINTOPO4:18;
hence contradiction by A3,A35,A40,A41;
end;
then k-'1<j by A36,XXREAL_0:1;
then
A42: k-'1+1<=j by NAT_1:13;
then j-k>=0 by A18,XREAL_1:48;
then
A43: j-k=j-'k by XREAL_0:def 2;
j in the carrier of FTSL1 n by A35,A38,FUNCT_2:5;
then not |.(k-'1)-j.|<=km+1 by A5,A37,Th9;
then |.j-(k-'1).|>km+1 by UNIFORM1:11;
then j-'k+1>km+1 by A18,A43,ABSVALUE:def 1;
then j-k+1>=km+1+1 by A43,NAT_1:13;
then k-jn+(j-k+1)>= km+1+1+(km+1+1) by A29,XREAL_1:7;
then j-jn+1>= km+1+1+(km+1)+1;
then j-jn>= km+1+1+(km+1) by XREAL_1:6;
then j-jn-1>= km+1+1+km+1-1 by XREAL_1:9;
then
A44: (j-jn-1)/2>= ((2*km)+2)/2 by XREAL_1:72;
[/ (kc/2) \] >= kc/2 by INT_1:def 7;
then [/ (kc/2) \]+2/2 >= kc/2 +2/2 by XREAL_1:7;
then (j-jn-1)/2 >= kc/2+2/2 by A2,A44,XXREAL_0:2;
then (j-jn-1)/2*2>=(kc/2+2/2)*2 by XREAL_1:64;
then j-jn-1> kc by A30,XXREAL_0:2;
then
A45: j-jn-1+1>kc+1 by XREAL_1:6;
jn<j by A18,A42,A26,XXREAL_0:2;
then j-jn>=0 by XREAL_1:48;
then
A46: |.j-jn.|=j-jn by ABSVALUE:def 1;
f.:(U_FT(pk,0)) c= U_FT(pfk,kc) & |.jn-j.|=|.j-jn.| by A1,FINTOPO4:def 2
,UNIFORM1:11;
hence contradiction by A35,A39,A46,A45,Th9;
end;
end;
definition
let A,B be set;
let R be Relation of A,B, x be set;
redefine func Im(R,x) -> Subset of B; :: redefines Im (RELAT_1, definition)
coherence
proof
Im(R,x) = R.:{x};
hence thesis;
end;
end;
:: 2-dimensional linear FT_Str
definition
let n,m be Nat;
func Nbdl2(n,m) -> Relation of [:Seg n, Seg m:] means
:Def2:
for x being set
st x in [:Seg n, Seg m:] holds for i,j being Nat st x=[i,j] holds Im
(it,x) = [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):];
existence
proof
defpred P[object,object] means
for i,j being Nat st $1=[i,j] holds $2
= [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):];
A1: for x being object st x in [:Seg n, Seg m:]
ex y being object st y in bool [:Seg n, Seg m:] & P[x,y]
proof
let x be object;
assume x in [:Seg n, Seg m:];
then consider u,y being object such that
A2: u in Seg n & y in Seg m and
A3: x = [u,y] by ZFMISC_1:def 2;
reconsider i=u, j=y as Nat by A2;
set y3= [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):];
A4: y3 c= [:Seg n, Seg m:]
proof
let z be object;
assume z in y3;
then
ex x4,y4 being object st x4 in Im(Nbdl1 n,i) & y4 in Im(Nbdl1 m,j) &
z = [x4,y4] by ZFMISC_1:def 2;
hence thesis by ZFMISC_1:def 2;
end;
for i4,j4 being Nat st x=[i4,j4] holds y3= [:Im(Nbdl1 n,
i4), Im(Nbdl1 m,j4):]
proof
let i4,j4 be Nat;
assume
A5: x=[i4,j4];
then i4=u by A3,XTUPLE_0:1;
hence thesis by A3,A5,XTUPLE_0:1;
end;
hence thesis by A4;
end;
consider f being Function of [:Seg n, Seg m:],bool [:Seg n, Seg m:] such
that
A6: for x being object st x in [:Seg n, Seg m:] holds P[x,f.x] from
FUNCT_2:sch 1(A1);
consider R being Relation of [:Seg n, Seg m:] such that
A7: for i being set st i in [:Seg n, Seg m:] holds Im(R,i) = f.i by FUNCT_2:93;
take R;
let x be set such that
A8: x in [:Seg n, Seg m:];
let i,j be Nat such that
A9: x=[i,j];
thus Im(R,x) = f.x by A7,A8
.= [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):] by A6,A8,A9;
end;
uniqueness
proof
let f1,f2 be Relation of [:Seg n, Seg m:];
assume that
A10: for x being set st x in [:Seg n, Seg m:] holds for i,j being
Nat st x=[i,j] holds Im(f1,x) = [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):]
and
A11: for x being set st x in [:Seg n, Seg m:] holds for i,j being
Nat st x=[i,j] holds Im(f2,x) = [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):];
for x being set st x in [:Seg n, Seg m:] holds Im(f1,x)=Im(f2,x)
proof
let x be set;
assume
A12: x in [:Seg n, Seg m:];
then consider u,y being object such that
A13: u in Seg n & y in Seg m and
A14: x=[u,y] by ZFMISC_1:def 2;
reconsider i=u, j=y as Nat by A13;
Im(f1,x)= [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):] by A10,A12,A14;
hence thesis by A11,A12,A14;
end;
hence f1=f2 by RELSET_1:31;
end;
end;
definition
let n,m be Nat;
func FTSL2(n,m) -> strict RelStr equals
RelStr(# [:Seg n, Seg m:], Nbdl2(n,m
) #);
coherence;
end;
registration
let n,m be non zero Nat;
cluster FTSL2(n,m) -> non empty;
coherence;
end;
theorem
for n,m being non zero Nat holds FTSL2(n,m) is filled
proof
let n,m be non zero Nat;
for x being Element of FTSL2(n,m) holds x in U_FT x
proof
let x be Element of FTSL2(n,m);
consider u,y being object such that
A1: u in Seg n and
A2: y in Seg m and
A3: x=[u,y] by ZFMISC_1:def 2;
reconsider i=u, j=y as Nat by A1,A2;
A4: FTSL1 m = RelStr(# Seg m,Nbdl1 m #) by FINTOPO4:def 4;
then reconsider pj=j as Element of FTSL1 m by A2;
A5: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
then reconsider pi=i as Element of FTSL1 n by A1;
FTSL1 m is filled by FINTOPO4:18;
then
A6: j in U_FT pj;
FTSL1 n is filled by FINTOPO4:18;
then i in U_FT pi;
then x in [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):] by A3,A4,A5,A6,ZFMISC_1:def 2;
hence thesis by A3,Def2;
end;
hence thesis;
end;
theorem
for n,m being non zero Nat holds FTSL2(n,m) is symmetric
proof
let n,m be non zero Nat;
for x, y being Element of FTSL2(n,m) holds y in U_FT x implies x in U_FT y
proof
A1: FTSL1 m is symmetric by FINTOPO4:19;
let x, y be Element of FTSL2(n,m);
consider xu,xv being object such that
A2: xu in Seg n and
A3: xv in Seg m and
A4: x=[xu,xv] by ZFMISC_1:def 2;
reconsider i=xu, j=xv as Nat by A2,A3;
consider yu,yv being object such that
A5: yu in Seg n and
A6: yv in Seg m and
A7: y=[yu,yv] by ZFMISC_1:def 2;
reconsider i2=yu, j2=yv as Nat by A5,A6;
A8: FTSL1 m = RelStr(# Seg m,Nbdl1 m #) by FINTOPO4:def 4;
then reconsider pj=j as Element of FTSL1 m by A3;
reconsider pj2=j2 as Element of FTSL1 m by A8,A6;
assume y in U_FT x;
then y in [:Im(Nbdl1 n,i), Im(Nbdl1 m,j):] by A4,Def2;
then
A9: ex y1,y2 being object
st y1 in Class(Nbdl1 n,i) & y2 in Class(Nbdl1 m,j)
& y=[y1,y2] by ZFMISC_1:def 2;
then j2 in U_FT pj by A8,A7,XTUPLE_0:1;
then
A10: j in U_FT pj2 by A1;
A11: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
then reconsider pi=i as Element of FTSL1 n by A2;
A12: FTSL1 n is symmetric by FINTOPO4:19;
reconsider pi2=i2 as Element of FTSL1 n by A11,A5;
pi2 in U_FT pi by A11,A7,A9,XTUPLE_0:1;
then pi in U_FT pi2 by A12;
then x in [:Im(Nbdl1 n,i2), Im(Nbdl1 m,j2):] by A4,A8,A11,A10,
ZFMISC_1:def 2;
hence thesis by A7,Def2;
end;
hence thesis;
end;
theorem
for n being non zero Nat ex h being Function of FTSL2(n,1),
FTSL1 n st h is being_homeomorphism
proof
defpred P[object,object] means [$2,1]=$1;
let n be non zero Nat;
set FT1=FTSL2(n,1),FT2= FTSL1 n;
A1: for x be object st x in the carrier of FTSL2(n,1)
ex y be object st y in the carrier of FTSL1 n & P[x,y]
proof
let x be object;
A2: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
assume x in the carrier of FTSL2(n,1);
then consider u,v being object such that
A3: u in Seg n and
A4: v in Seg 1 and
A5: x= [u,v] by ZFMISC_1:def 2;
reconsider nu=u,nv=v as Nat by A3,A4;
1<=nv & nv<=1 by A4,FINSEQ_1:1;
then P[x,nu] by A5,XXREAL_0:1;
hence thesis by A3,A2;
end;
ex f being Function of FTSL2(n,1), FTSL1 n st
for x be object st x in the
carrier of FTSL2(n,1) holds P[x,f.x] from FUNCT_2:sch 1(A1);
then consider f being Function of FTSL2(n,1), FTSL1 n such that
A6: for x be object st x in the carrier of FTSL2(n,1) holds P[x,f.x];
A7: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
A8: the carrier of FTSL1 n c= rng f
proof
let x be object;
set z=[x,1];
A9: 1 in Seg 1;
assume x in the carrier of FTSL1 n;
then
A10: z in the carrier of FTSL2(n,1) by A7,A9,ZFMISC_1:def 2;
then [f.z,1]=z by A6;
then
A11: f.z=x by XTUPLE_0:1;
z in dom f by A10,FUNCT_2:def 1;
hence thesis by A11,FUNCT_1:def 3;
end;
A12: for x being Element of FT1 holds f.:U_FT(x)=Im(the InternalRel of FT2,f
.x)
proof
let x be Element of FT1;
consider u,v being object such that
A13: u in Seg n and
A14: v in Seg 1 and
A15: x= [u,v] by ZFMISC_1:def 2;
A16: Im(the InternalRel of FT2,f.x) c= f.:U_FT x
proof
reconsider nv=v as Nat by A14;
let y be object;
assume
A17: y in Im(the InternalRel of FT2,f.x);
1 <= nv & nv <= 1 by A14,FINSEQ_1:1;
then
A18: nv = 1 by XXREAL_0:1;
Im(Nbdl1 n,f.x) c= rng f by A7,A8;
then consider x3 being object such that
A19: x3 in dom f and
A20: y=f.x3 by A7,A17,FUNCT_1:def 3;
set u2=f.x3,v2=1;
Im(Nbdl1 1,v) = {nv, max(nv-'1,1),min(nv+1,1)} by A14,FINTOPO4:def 3
.= {1,max(0,1),min(2,1)} by A18,NAT_2:8
.= {1,1,min(2,1)} by XXREAL_0:def 10
.= {1, min(2,1)} by ENUMSET1:30
.= {1, 1} by XXREAL_0:def 9
.= {1} by ENUMSET1:29;
then
A21: v2 in Im(Nbdl1 1,v) by ZFMISC_1:31;
A22: Im(Nbdl2(n,1),x) = [:Im(Nbdl1 n,u),Im(Nbdl1 1,v):] by A13,A14,A15,Def2;
x=[f.x,1] by A6;
then u2 in Im(Nbdl1 n,u) by A7,A15,A17,A20,XTUPLE_0:1;
then
A23: [u2,v2] in [:Im(Nbdl1 n,u),Im(Nbdl1 1,v):] by A21,ZFMISC_1:def 2;
x3=[f.x3,1] by A6,A19;
hence thesis by A19,A20,A23,A22,FUNCT_1:def 6;
end;
f.:U_FT x c= Im(the InternalRel of FT2,f.x)
proof
x=[f.x,1] by A6;
then
A24: u=f.x by A15,XTUPLE_0:1;
let y be object;
assume y in f.:U_FT x;
then consider x2 being object such that
A25: x2 in dom f and
A26: x2 in Im(Nbdl2(n,1),x) & y=f.x2 by FUNCT_1:def 6;
A27: Im(Nbdl2(n,1),x) =[:Im(Nbdl1 n,u),Im(Nbdl1 1,v):] by A13,A14,A15,Def2;
x2=[f.x2,1] by A6,A25;
hence thesis by A7,A26,A27,A24,ZFMISC_1:87;
end;
hence thesis by A16,XBOOLE_0:def 10;
end;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2 holds x1= x2
proof
let x1,x2 be object;
assume that
A28: x1 in dom f and
A29: x2 in dom f & f.x1=f.x2;
[f.x1,1]=x1 by A6,A28;
hence thesis by A6,A29;
end;
then
A30: f is one-to-one by FUNCT_1:def 4;
rng f= the carrier of FTSL1 n by A8,XBOOLE_0:def 10;
then f is onto by FUNCT_2:def 3;
then f is being_homeomorphism by A30,A12;
hence thesis;
end;
:: 2-dimensional small FT_Str
definition
let n,m be Nat;
func Nbds2(n,m) -> Relation of [:Seg n, Seg m:] means
:Def4:
for x being set
st x in [:Seg n, Seg m:] holds for i,j being Nat st x=[i,j] holds Im
(it,x) = [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,i),{j}:];
existence
proof
defpred P[object,object] means
for i,j being Nat st $1=[i,j] holds $2
= [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,i),{j}:];
A1: for x being object st x in [:Seg n, Seg m:]
ex y being object st y in bool[:Seg n, Seg m:] & P[x,y]
proof
let x be object;
assume x in [:Seg n, Seg m:];
then consider u,y being object such that
A2: u in Seg n and
A3: y in Seg m and
A4: x = [u,y] by ZFMISC_1:def 2;
reconsider i=u, j=y as Nat by A2,A3;
set y3= [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,u),{j}:];
A5: y3 c= [:Seg n, Seg m:]
proof
let z be object;
assume
A6: z in y3;
per cases by A6,XBOOLE_0:def 3;
suppose
z in [:{i}, Im(Nbdl1 m,j):];
then consider x4,y4 being object such that
A7: x4 in {i} and
A8: y4 in Im(Nbdl1 m,j) & z=[x4,y4] by ZFMISC_1:def 2;
x4 = i by A7,TARSKI:def 1;
hence thesis by A2,A8,ZFMISC_1:def 2;
end;
suppose
z in [:Im(Nbdl1 n,u),{j}:];
then consider x4,y4 being object such that
A9: x4 in Im(Nbdl1 n,i) and
A10: y4 in {j} and
A11: z=[x4,y4] by ZFMISC_1:def 2;
y4 in Seg m by A3,A10,TARSKI:def 1;
hence thesis by A9,A11,ZFMISC_1:def 2;
end;
end;
for i4,j4 being Nat st x=[i4,j4] holds y3= [:{i4}, Im(
Nbdl1 m,j4):] \/ [:Im(Nbdl1 n,i4),{j4}:]
proof
let i4,j4 be Nat;
assume x=[i4,j4];
then i4=u & j4=y by A4,XTUPLE_0:1;
hence thesis;
end;
hence thesis by A5;
end;
consider f being Function of [:Seg n, Seg m:],bool [:Seg n, Seg m:] such
that
A12: for x being object st x in [:Seg n, Seg m:] holds P[x,f.x] from
FUNCT_2:sch 1(A1);
consider R being Relation of [:Seg n, Seg m:] such that
A13: for i being set st i in [:Seg n, Seg m:] holds Im(R,i) = f.i by FUNCT_2:93
;
take R;
let x be set such that
A14: x in [:Seg n, Seg m:];
let i,j be Nat such that
A15: x=[i,j];
thus Im(R,x) = f.x by A13,A14
.= [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,i),{j}:] by A12,A14,A15;
end;
uniqueness
proof
let f1,f2 be Relation of [:Seg n, Seg m:];
assume that
A16: for x being set st x in [:Seg n, Seg m:] holds for i,j being
Nat st x=[i,j] holds Im(f1,x) = [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1
n,i),{j }:] and
A17: for x being set st x in [:Seg n, Seg m:] holds for i,j being
Nat st x=[i,j] holds Im(f2,x) = [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1
n,i),{j}:];
for x being set st x in [:Seg n, Seg m:] holds Im(f1,x)=Im(f2,x)
proof
let x be set;
assume
A18: x in [:Seg n, Seg m:];
then consider u,y being object such that
A19: u in Seg n & y in Seg m and
A20: x=[u,y] by ZFMISC_1:def 2;
reconsider i=u, j=y as Nat by A19;
Im(f1,x)= [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,u),{j}:] by A16,A18,A20;
hence thesis by A17,A18,A20;
end;
hence f1=f2 by RELSET_1:31;
end;
end;
definition
let n,m be Nat;
func FTSS2(n,m) -> strict RelStr equals
RelStr(# [:Seg n, Seg m:], Nbds2(n,m
) #);
coherence;
end;
registration
let n,m be non zero Nat;
cluster FTSS2(n,m) -> non empty;
coherence;
end;
theorem
for n,m being non zero Nat holds FTSS2(n,m) is filled
proof
let n,m be non zero Nat;
for x being Element of FTSS2(n,m) holds x in U_FT x
proof
let x be Element of FTSS2(n,m);
consider u,y being object such that
A1: u in Seg n and
A2: y in Seg m and
A3: x=[u,y] by ZFMISC_1:def 2;
reconsider i=u, j=y as Nat by A1,A2;
A4: FTSL1 m = RelStr(# Seg m,Nbdl1 m #) by FINTOPO4:def 4;
then reconsider pj=j as Element of FTSL1 m by A2;
A5: i in {i} by ZFMISC_1:31;
FTSL1 m is filled by FINTOPO4:18;
then j in U_FT pj;
then x in [:{i}, Im(Nbdl1 m,j):] by A3,A4,A5,ZFMISC_1:def 2;
then x in [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,u), {j}:] by
XBOOLE_0:def 3;
hence thesis by A3,Def4;
end;
hence thesis;
end;
theorem
for n,m being non zero Nat holds FTSS2(n,m) is symmetric
proof
let n,m be non zero Nat;
for x, y being Element of FTSS2(n,m) holds y in U_FT x implies x in U_FT y
proof
let x, y be Element of FTSS2(n,m);
consider xu,xv being object such that
A1: xu in Seg n and
A2: xv in Seg m and
A3: x=[xu,xv] by ZFMISC_1:def 2;
reconsider i=xu, j=xv as Nat by A1,A2;
consider yu,yv being object such that
A4: yu in Seg n and
A5: yv in Seg m and
A6: y=[yu,yv] by ZFMISC_1:def 2;
reconsider i2=yu, j2=yv as Nat by A4,A5;
A7: FTSL1 m = RelStr(# Seg m,Nbdl1 m #) by FINTOPO4:def 4;
then reconsider pj=j as Element of FTSL1 m by A2;
A8: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
then reconsider pi=i as Element of FTSL1 n by A1;
reconsider pj2=j2 as Element of FTSL1 m by A7,A5;
reconsider pi2=i2 as Element of FTSL1 n by A8,A4;
assume y in U_FT x;
then
A9: y in [:{i}, Im(Nbdl1 m,j):] \/ [:Im(Nbdl1 n,i),{j}:] by A3,Def4;
now
per cases by A9,XBOOLE_0:def 3;
case
y in [:{i}, Im(Nbdl1 m,j):];
then consider y1,y2 being object such that
A10: y1 in {i} and
A11: y2 in Class(Nbdl1 m,j) and
A12: y=[y1,y2] by ZFMISC_1:def 2;
y1 = i by A10,TARSKI:def 1;
then
A13: i in {i2} by A6,A10,A12,XTUPLE_0:1;
A14: FTSL1 m is symmetric by FINTOPO4:19;
pj2 in U_FT pj by A7,A6,A11,A12,XTUPLE_0:1;
then pj in U_FT pj2 by A14;
hence x in [:{i2}, Im(Nbdl1 m,j2):] by A3,A7,A13,ZFMISC_1:def 2;
end;
case
y in [:Im(Nbdl1 n,i),{j}:];
then consider y1,y2 being object such that
A15: y1 in Class(Nbdl1 n,i) and
A16: y2 in {j} and
A17: y=[y1,y2] by ZFMISC_1:def 2;
y2 = j by A16,TARSKI:def 1;
then
A18: j in {j2} by A6,A16,A17,XTUPLE_0:1;
A19: FTSL1 n is symmetric by FINTOPO4:19;
pi2 in U_FT pi by A8,A6,A15,A17,XTUPLE_0:1;
then pi in U_FT pi2 by A19;
hence x in [:Im(Nbdl1 n,i2), {j2}:] by A3,A8,A18,ZFMISC_1:def 2;
end;
end;
then x in [:{i2}, Im(Nbdl1 m,j2):] \/ [:Im(Nbdl1 n,i2), {j2}:] by
XBOOLE_0:def 3;
hence thesis by A6,Def4;
end;
hence thesis;
end;
theorem
for n being non zero Nat ex h being Function of FTSS2(n,1),
FTSL1 n st h is being_homeomorphism
proof
defpred P[object,object] means [$2,1]=$1;
let n be non zero Nat;
set FT1=FTSS2(n,1),FT2= FTSL1 n;
A1: for x be object st x in the carrier of FTSS2(n,1)
ex y be object st y in the carrier of FTSL1 n & P[x,y]
proof
let x be object;
A2: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
assume x in the carrier of FTSS2(n,1);
then consider u,v being object such that
A3: u in Seg n and
A4: v in Seg 1 and
A5: x= [u,v] by ZFMISC_1:def 2;
reconsider nu=u,nv=v as Nat by A3,A4;
1<=nv & nv<=1 by A4,FINSEQ_1:1;
then P[x,nu] by A5,XXREAL_0:1;
hence thesis by A3,A2;
end;
ex f being Function of FTSS2(n,1), FTSL1 n st
for x be object st x in the
carrier of FTSS2(n,1) holds P[x,f.x] from FUNCT_2:sch 1(A1);
then consider f being Function of FTSS2(n,1), FTSL1 n such that
A6: for x be object st x in the carrier of FTSS2(n,1) holds P[x,f.x];
A7: FTSL1 n = RelStr(# Seg n,Nbdl1 n #) by FINTOPO4:def 4;
A8: the carrier of FTSL1 n c= rng f
proof
let x be object;
set z=[x,1];
A9: 1 in Seg 1;
assume x in the carrier of FTSL1 n;
then
A10: z in the carrier of FTSS2(n,1) by A7,A9,ZFMISC_1:def 2;
then [f.z,1]=z by A6;
then
A11: f.z=x by XTUPLE_0:1;
z in dom f by A10,FUNCT_2:def 1;
hence thesis by A11,FUNCT_1:def 3;
end;
A12: for x being Element of FT1 holds f.:U_FT x=Im(the InternalRel of FT2,f. x)
proof
let x be Element of FT1;
consider u,v being object such that
A13: u in Seg n and
A14: v in Seg 1 and
A15: x= [u,v] by ZFMISC_1:def 2;
A16: f.:U_FT x c= Im(the InternalRel of FT2,f.x)
proof
let y be object;
assume y in f.:U_FT x;
then consider x2 being object such that
A17: x2 in dom f and
A18: x2 in Im(Nbds2(n,1),x) and
A19: y=f.x2 by FUNCT_1:def 6;
consider u2,v2 being object such that
u2 in Seg n and
v2 in Seg 1 and
A20: x2= [u2,v2] by A17,ZFMISC_1:def 2;
x2=[f.x2,1] by A6,A17;
then
A21: u2=f.x2 by A20,XTUPLE_0:1;
A22: Im(Nbds2(n,1),x) = [:{u}, Im(Nbdl1 1,v):] \/ [:Im(Nbdl1 n,u),{v}:]
by A13,A14,A15,Def4;
A23: now
per cases by A18,A22,A20,XBOOLE_0:def 3;
suppose
A24: [u2,v2] in [:{u}, Im(Nbdl1 1,v):];
reconsider pu=u as Element of FTSL1 n by A7,A13;
(FTSL1 n) is filled by FINTOPO4:18;
then
A25: u in U_FT pu;
u2 in {u} by A24,ZFMISC_1:87;
hence u2 in Class(Nbdl1 n,u) by A7,A25,TARSKI:def 1;
end;
suppose
[u2,v2] in [:Im(Nbdl1 n,u),{v}:];
hence u2 in Class(Nbdl1 n,u) by ZFMISC_1:87;
end;
end;
x=[f.x,1] by A6;
hence thesis by A7,A15,A19,A21,A23,XTUPLE_0:1;
end;
Im(the InternalRel of FT2,f.x) c= f.:U_FT x
proof
set X=Im(Nbdl1 n,u), Y=Im(Nbdl1 1,v);
reconsider nv=v as Nat by A14;
let y be object;
assume
A26: y in Im(the InternalRel of FT2,f.x);
Im(Nbdl1 n,f.x) c= rng f by A7,A8;
then consider x3 being object such that
A27: x3 in dom f and
A28: y=f.x3 by A7,A26,FUNCT_1:def 3;
set u2=f.x3,v2=1;
x=[f.x,1] by A6;
then
A29: u2 in Im(Nbdl1 n,u) by A7,A15,A26,A28,XTUPLE_0:1;
A30: Im(Nbds2(n,1),x) = [:{u}, Y:] \/ [:X,{v}:] by A13,A14,A15,Def4;
1 <= nv & nv <= 1 by A14,FINSEQ_1:1;
then
A31: nv = 1 by XXREAL_0:1;
A32: Im(Nbdl1 1,v) = {nv, max(nv-'1,1),min(nv+1,1)} by A14,FINTOPO4:def 3
.= {1,max(0,1),min(2,1)} by A31,NAT_2:8
.= {1,1,min(2,1)} by XXREAL_0:def 10
.= {1, min(2,1)} by ENUMSET1:30
.= {1, 1} by XXREAL_0:def 9
.= {1} by ENUMSET1:29;
then v2 in Im(Nbdl1 1,v) by ZFMISC_1:31;
then [u2,v2] in [:Im(Nbdl1 n,u), Im(Nbdl1 1,v):] by A29,ZFMISC_1:def 2;
then
A33: [u2,v2] in [:X,{v}:] \/ [:{u},Y:] by A31,A32,XBOOLE_0:def 3;
x3=[f.x3,1] by A6,A27;
hence thesis by A27,A28,A33,A30,FUNCT_1:def 6;
end;
hence thesis by A16,XBOOLE_0:def 10;
end;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2
holds x1= x2
proof
let x1,x2 be object;
assume that
A34: x1 in dom f and
A35: x2 in dom f & f.x1=f.x2;
[f.x1,1]=x1 by A6,A34;
hence thesis by A6,A35;
end;
then
A36: f is one-to-one by FUNCT_1:def 4;
rng f= the carrier of FTSL1 n by A8,XBOOLE_0:def 10;
then f is onto by FUNCT_2:def 3;
then f is being_homeomorphism by A36,A12;
hence thesis;
end;