:: Continuous Mappings between Finite and One-Dimensional Finite Topological
:: Spaces
:: by Hiroshi Imura , Masami Tanaka and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004-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, ORDERS_2, SUBSET_1, CONNSP_1, FIN_TOPO,
XXREAL_0, FINTOPO3, TARSKI, ARYTM_3, ARYTM_1, CARD_1, RELAT_2, FUNCT_1,
STRUCT_0, RELAT_1, NAT_1, FINSEQ_1, ZFMISC_1, FINTOPO4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1,
STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1;
constructors ENUMSET1, NAT_1, EQREL_1, NAT_D, FIN_TOPO, FINTOPO3, FINSEQ_1,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, RELAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FIN_TOPO;
equalities FIN_TOPO, FINSEQ_1;
expansions TARSKI, FIN_TOPO;
theorems TARSKI, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1,
FIN_TOPO, FINTOPO3, RELAT_1, ENUMSET1, XREAL_1, XXREAL_0, ORDINAL1,
RELSET_1, XREAL_0, NAT_D;
schemes NAT_1, FUNCT_2, RELSET_1;
begin
definition
let FT be non empty RelStr, A,B be Subset of FT;
pred A,B are_separated means
A^b misses B & A misses B^b;
symmetry;
end;
theorem Th1:
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Finf(A,n) c= Finf(A,m)
proof
let FT be filled non empty RelStr, A be Subset of FT, n,m be Element of
NAT;
defpred P[Nat] means Finf(A,n) c= Finf(A,n+$1);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A2: Finf(A,n+k) c= Finf(A,n+k+1) by FINTOPO3:37;
assume P[k];
hence thesis by A2,XBOOLE_1:1;
end;
assume n<=m;
then m-n>=0 by XREAL_1:48;
then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
.=m;
A4: P[0];
for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
hence thesis by A3;
end;
theorem
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Fcl(A,n) c= Fcl(A,m)
proof
let FT be filled non empty RelStr,A be Subset of FT, n,m be Element of NAT;
defpred P[Nat] means Fcl(A,n) c= Fcl(A,n+$1);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A2: Fcl(A,n+k) c= Fcl(A,n+k+1) by FINTOPO3:25;
assume P[k];
hence thesis by A2,XBOOLE_1:1;
end;
assume n<=m;
then m-n>=0 by XREAL_1:48;
then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
.=m;
A4: P[0];
for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
hence thesis by A3;
end;
theorem
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Fdfl(A,m) c= Fdfl(A,n)
proof
let FT be filled non empty RelStr,A be Subset of FT, n,m be Element of NAT;
defpred P[Nat] means Fdfl(A,n+$1) c= Fdfl(A,n);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A2: Fdfl(A,n+k+1) c= Fdfl(A,n+k) by FINTOPO3:44;
assume P[k];
hence thesis by A2,XBOOLE_1:1;
end;
assume n<=m;
then m-n>=0 by XREAL_1:48;
then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
.=m;
A4: P[0];
for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
hence thesis by A3;
end;
theorem
for FT being filled non empty RelStr, A being Subset of FT, n,m
being Element of NAT st n<=m holds Fint(A,m) c= Fint(A,n)
proof
let FT be filled non empty RelStr,A be Subset of FT, n,m be Element of NAT;
defpred P[Nat] means Fint(A,n+$1) c= Fint(A,n);
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A2: Fint(A,n+k+1) c= Fint(A,n+k) by FINTOPO3:26;
assume P[k];
hence thesis by A2,XBOOLE_1:1;
end;
assume n<=m;
then m-n>=0 by XREAL_1:48;
then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
.=m;
A4: P[0];
for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
hence thesis by A3;
end;
theorem
for FT being non empty RelStr,A,B being Subset of FT st A,B
are_separated holds B,A are_separated;
theorem Th6:
for FT being filled non empty RelStr, A,B being Subset of FT st
A,B are_separated holds A misses B
by FIN_TOPO:13,XBOOLE_1:63;
theorem
for FT being non empty RelStr, A,B being Subset of FT st FT is
symmetric holds A,B are_separated iff A^f misses B & A misses (B^f)
by FIN_TOPO:12;
theorem Th8:
for FT being filled non empty RelStr, A,B being Subset of FT st
FT is symmetric & A^b misses B holds A misses (B^b)
proof
let FT be filled non empty RelStr, A,B be Subset of FT;
assume that
A1: FT is symmetric and
A2: A^b misses B;
now
assume A meets (B^b);
then consider x being object such that
A3: x in A and
A4: x in B^b by XBOOLE_0:3;
consider x2 being Element of FT such that
A5: x2=x and
A6: U_FT x2 meets B by A4;
set y = the Element of U_FT x2 /\ B;
A7: U_FT x2 /\ B <>{} by A6,XBOOLE_0:def 7;
then
A8: y in U_FT x2 by XBOOLE_0:def 4;
then reconsider y2=y as Element of FT;
x2 in U_FT y2 by A1,A8;
then x2 in U_FT y2 /\ A by A3,A5,XBOOLE_0:def 4;
then U_FT y2 meets A by XBOOLE_0:def 7;
then
A9: y2 in A^b;
y in B by A7,XBOOLE_0:def 4;
hence contradiction by A2,A9,XBOOLE_0:3;
end;
hence thesis;
end;
theorem
for FT being filled non empty RelStr, A,B being Subset of FT st FT
is symmetric & A misses (B^b) holds A^b misses B by Th8;
theorem
for FT being filled non empty RelStr, A,B being Subset of FT st FT
is symmetric holds A,B are_separated iff A^b misses B
by Th8;
theorem
for FT being filled non empty RelStr, A,B being Subset of FT st FT
is symmetric holds A,B are_separated iff A misses (B^b)
by Th8;
theorem Th12:
for FT being filled non empty RelStr, IT being Subset of FT st
FT is symmetric holds IT is connected iff (for A, B being Subset of FT st IT =
A \/ B & A,B are_separated holds A = IT or B = IT)
proof
let FT be filled non empty RelStr,IT be Subset of FT;
assume
A1: FT is symmetric;
A2: now
assume
A3: for A, B being Subset of FT st IT = A \/ B & A,B are_separated
holds A = IT or B = IT;
for A,B being Subset of FT st IT = A \/ B & A <> {} & B <> {} & A
misses B holds A^b meets B
proof
let A,B be Subset of FT;
assume that
A4: IT = A \/ B and
A5: A <> {} & B <> {} and
A misses B;
now
assume
A6: A^b misses B;
now
assume A meets (B^b);
then consider x being object such that
A7: x in A and
A8: x in B^b by XBOOLE_0:3;
consider x2 being Element of FT such that
A9: x2=x and
A10: U_FT x2 meets B by A8;
set y = the Element of U_FT x2 /\ B;
A11: U_FT x2 /\ B <>{} by A10,XBOOLE_0:def 7;
then
A12: y in U_FT x2 by XBOOLE_0:def 4;
then reconsider y2=y as Element of FT;
x2 in U_FT y2 by A1,A12;
then x2 in U_FT y2 /\ A by A7,A9,XBOOLE_0:def 4;
then U_FT y2 meets A by XBOOLE_0:def 7;
then
A13: y2 in A^b;
y in B by A11,XBOOLE_0:def 4;
hence contradiction by A6,A13,XBOOLE_0:3;
end;
then A,B are_separated by A6;
then
A14: A=IT or B=IT by A3,A4;
A15: A c= A^b by FIN_TOPO:13;
A^b /\ B={} by A6,XBOOLE_0:def 7;
then A /\ B ={} by A15,XBOOLE_1:3,26;
hence contradiction by A4,A5,A14,XBOOLE_1:21;
end;
hence thesis;
end;
hence IT is connected;
end;
now
assume
A16: IT is connected;
thus for A, B being Subset of FT st IT = A \/ B & A,B are_separated holds
A = IT or B = IT
proof
let A, B be Subset of FT;
assume that
A17: IT = A \/ B and
A18: A,B are_separated;
A19: A misses B by A18,Th6;
now
assume A<>{};
then B={} by A18,A16,A17,A19;
hence thesis by A17;
end;
hence thesis by A17;
end;
end;
hence thesis by A2;
end;
theorem
for FT being filled non empty RelStr, B being Subset of FT st FT is
symmetric holds B is connected iff not (ex C being Subset of FT st C<>{} & B\C
<>{} & C c= B & (C^b) misses (B\C))
proof
let FT be filled non empty RelStr, B be Subset of FT;
assume
A1: FT is symmetric;
thus B is connected implies not (ex C being Subset of FT st C<>{} & B\C <>{}
& C c= B & (C^b) misses (B\C))
proof
assume
A2: B is connected;
for C being Subset of FT st C c= B & (C^b) misses (B\C) holds C={} or
B\C={}
proof
let C be Subset of FT;
assume that
A3: C c= B and
A4: (C^b) misses (B\C);
C misses ((B\C)^b) by A1,A4,Th8;
then
A5: C,B\C are_separated by A4;
C \/ (B\C)=C \/ B by XBOOLE_1:39
.=B by A3,XBOOLE_1:12;
then C = B or B\C = B by A1,A2,A5,Th12;
hence thesis by A3,XBOOLE_1:37,38;
end;
hence thesis;
end;
thus not (ex C being Subset of FT st C<>{} & B\C <>{} & C c= B & (C^b)
misses (B\C)) implies B is connected
proof
assume
A6: not (ex C being Subset of FT st C<>{} & B\C <>{} & C c= B & (C^b)
misses (B\C));
for A, B2 being Subset of FT st B = A \/ B2 & A,B2 are_separated
holds A = B or B2 = B
proof
let A, B2 be Subset of FT;
assume that
A7: B = A \/ B2 and
A8: A,B2 are_separated;
A9: (A \/ B2) \A =B2\A by XBOOLE_1:40;
A^b misses B2 by A8;
then A^b misses (B\A) by A7,A9,XBOOLE_1:36,63;
then A={} or B\A={} by A6,A7,XBOOLE_1:7;
then
A10: B=B2 or B c= A by A7,XBOOLE_1:37;
A c= B by A7,XBOOLE_1:7;
hence thesis by A10,XBOOLE_0:def 10;
end;
hence thesis by A1,Th12;
end;
end;
definition
let FT1,FT2 be non empty RelStr, f be Function of FT1, FT2, n be Nat;
pred f is_continuous n means
for x being Element of FT1,y being
Element of FT2 st x in the carrier of FT1 & y=f.x holds f.:(U_FT(x,0)) c= U_FT(
y,n);
end;
theorem
for FT1 being non empty RelStr, FT2 being filled non empty RelStr, n
being Element of NAT, f being Function of FT1, FT2 st f is_continuous 0 holds f
is_continuous n
proof
let FT1 be non empty RelStr, FT2 be filled non empty RelStr,n be Element
of NAT, f be Function of FT1, FT2;
assume
A1: f is_continuous 0;
for x being Element of FT1,y being Element of FT2 st x in the carrier of
FT1 & y=f.x holds f.:( U_FT(x,0)) c= U_FT(y,n)
proof
let x be Element of FT1,y be Element of FT2;
assume that
x in the carrier of FT1 and
A2: y=f.x;
U_FT y =U_FT(y,0) & U_FT(y,n)=Finf((U_FT y),n) by FINTOPO3:47,def 10;
then
A3: U_FT(y,0) c= U_FT(y,n) by FINTOPO3:36;
f.:( U_FT(x,0)) c= U_FT(y,0) by A1,A2;
hence thesis by A3;
end;
hence thesis;
end;
theorem
for FT1 being non empty RelStr, FT2 being filled non empty RelStr,
n0,n being Element of NAT, f being Function of FT1, FT2 st f is_continuous n0 &
n0<=n holds f is_continuous n
proof
let FT1 be non empty RelStr, FT2 be filled non empty RelStr,n0,n be
Element of NAT, f be Function of FT1, FT2;
assume that
A1: f is_continuous n0 and
A2: n0<=n;
for x being Element of FT1,y being Element of FT2 st x in the carrier of
FT1 & y=f.x holds f.:( U_FT(x,0)) c= U_FT(y,n)
proof
let x be Element of FT1,y be Element of FT2;
assume that
x in the carrier of FT1 and
A3: y=f.x;
U_FT(y,n0)=Finf((U_FT y),n0) & U_FT(y,n)=Finf((U_FT y),n) by
FINTOPO3:def 10;
then
A4: U_FT(y,n0) c= U_FT(y,n) by A2,Th1;
f.:( U_FT(x,0)) c= U_FT(y,n0) by A1,A3;
hence thesis by A4;
end;
hence thesis;
end;
theorem Th16:
for FT1,FT2 being non empty RelStr, A being Subset of FT1,B
being Subset of FT2, f being Function of FT1, FT2 st f is_continuous 0 & B=f.:A
holds f.:(A^b) c= B^b
proof
let FT1,FT2 be non empty RelStr,A be Subset of FT1, B be Subset of FT2, f be
Function of FT1, FT2;
assume that
A1: f is_continuous 0 and
A2: B=f.:A;
thus f.:(A^b) c= B^b
proof
let y be object;
assume y in f.:(A^b);
then consider x being object such that
A3: x in dom f and
A4: x in A^b and
A5: y=f.x by FUNCT_1:def 6;
reconsider x0=x as Element of FT1 by A3;
reconsider y0=y as Element of FT2 by A3,A5,FUNCT_2:5;
f.:( U_FT(x0,0)) c= U_FT(y0,0) by A1,A5;
then f.:(U_FT x0) c= U_FT(y0,0) by FINTOPO3:47;
then f.:(U_FT x0) c= U_FT y0 by FINTOPO3:47;
then
A6: f.:((U_FT x0) /\ A) c= (f.:((U_FT x0)))/\ (f.:A) & (f.:((U_FT x0)))/\
(f.:A) c= (U_FT y0) /\ (f.:A) by RELAT_1:121,XBOOLE_1:26;
ex z being Element of FT1 st z=x & U_FT z meets A by A4;
then
A7: U_FT x0 /\ A<>{} by XBOOLE_0:def 7;
dom f=the carrier of FT1 by FUNCT_2:def 1;
then f.:((U_FT x0) /\ A)<>{} by A7,RELAT_1:119;
then (U_FT y0) /\ (f.:A)<>{} by A6;
then U_FT y0 meets B by A2,XBOOLE_0:def 7;
hence thesis;
end;
end;
theorem
for FT1,FT2 being non empty RelStr,A being Subset of FT1, B being
Subset of FT2, f being Function of FT1, FT2 st A is connected & f is_continuous
0 & B=f.:A holds B is connected
proof
let FT1,FT2 be non empty RelStr,A be Subset of FT1, B be Subset of FT2, f be
Function of FT1, FT2;
assume that
A1: A is connected and
A2: f is_continuous 0 and
A3: B=f.:A;
for B2,C2 being Subset of FT2 st B = B2 \/ C2 & B2 <> {} & C2 <> {} & B2
misses C2 holds B2^b meets C2
proof
let B2,C2 be Subset of FT2;
assume that
A4: B = B2 \/ C2 and
A5: B2 <> {} and
A6: C2 <> {} and
A7: B2 misses C2;
reconsider C1=f"C2 as Subset of FT1;
reconsider C10=C1 /\ A as Subset of FT1;
reconsider B1 = f"B2 as Subset of FT1;
reconsider B10=B1/\A as Subset of FT1;
A8: C10 c= C1 by XBOOLE_1:17;
set x6 = the Element of C2;
x6 in B by A4,A6,XBOOLE_0:def 3;
then consider z6 being object such that
A9: z6 in dom f and
A10: z6 in A and
A11: x6=f.z6 by A3,FUNCT_1:def 6;
z6 in f"C2 by A6,A9,A11,FUNCT_1:def 7;
then
A12: C10<>{} by A10,XBOOLE_0:def 4;
set x5 = the Element of B2;
x5 in B by A4,A5,XBOOLE_0:def 3;
then consider z5 being object such that
A13: z5 in dom f and
A14: z5 in A and
A15: x5=f.z5 by A3,FUNCT_1:def 6;
A c= the carrier of FT1;
then
A16: A c= dom f by FUNCT_2:def 1;
B2 /\ C2 = {} by A7,XBOOLE_0:def 7;
then f"(B2 /\ C2) = {};
then B10 c= B1 & (f"B2) /\ (f"C2) = {} by FUNCT_1:68,XBOOLE_1:17;
then B10 /\ C10= {} by A8,XBOOLE_1:3,27;
then
A17: B10 misses C10 by XBOOLE_0:def 7;
(f"B2) \/ (f"C2)=f"(f.:A) by A3,A4,RELAT_1:140;
then A c= B1 \/ C1 by A16,FUNCT_1:76;
then A c= A/\(B1\/C1) by XBOOLE_1:19;
then
A18: A c= B10 \/ C10 by XBOOLE_1:23;
B10 c= A & C10 c= A by XBOOLE_1:17;
then B10 \/ C10 c= A by XBOOLE_1:8;
then
A19: A=B10 \/ C10 by A18,XBOOLE_0:def 10;
z5 in f"B2 by A5,A13,A15,FUNCT_1:def 7;
then B10<>{} by A14,XBOOLE_0:def 4;
then B10^b meets C10 by A1,A19,A12,A17;
then
A20: B10^b /\ C10 <> {} by XBOOLE_0:def 7;
reconsider B20 = f.:B1 as Subset of FT2;
A21: dom f=the carrier of FT1 by FUNCT_2:def 1;
f.:B1 c= B2
proof
let y be object;
assume y in f.:B1;
then ex x2 being object st x2 in dom f & x2 in B1 & y=f.x2
by FUNCT_1:def 6;
hence thesis by FUNCT_1:def 7;
end;
then
A22: B20^b c= B2^b by FIN_TOPO:14;
f.:(B1^b) c= B20^b by A2,Th16;
then f.:(B1^b) c= B2^b by A22;
then
A23: (f.:(B1^b)) /\ (f.:C1) c= (f.:(B1^b)) /\ C2 & (f.:(B1^b)) /\ C2 c= B2
^b /\ C2 by FUNCT_1:75,XBOOLE_1:26;
B10^b c= B1^b by FIN_TOPO:14,XBOOLE_1:17;
then B1^b /\ C1 <> {} by A8,A20,XBOOLE_1:3,27;
then f.:(B1^b /\ C1) <> {} by A21,RELAT_1:119;
then (f.:(B1^b)) /\ (f.:C1) <> {} by RELAT_1:121,XBOOLE_1:3;
then B2^b /\ C2 <>{} by A23;
hence thesis by XBOOLE_0:def 7;
end;
hence thesis;
end;
::1 dimensional linear FT_Str
definition
let n be Nat;
func Nbdl1 n -> Relation of Seg n means
:Def3:
for i being Element of NAT st
i in Seg n holds Im(it,i)={i,max(i-'1,1),min(i+1,n)};
existence
proof
deffunc F(Nat) = {$1,max($1-'1,1),min($1+1,n)};
A1: for x being Element of NAT st x in Seg n holds F(x) c= Seg n
proof
let i be Element of NAT;
set y0={i,max(i-'1,1),min(i+1,n)};
assume
A2: i in Seg n;
then Seg n <> {};
then n>0;
then
A3: 0+1<=n by NAT_1:13;
thus y0 c=Seg n
proof
let z1 be object;
assume
A4: z1 in y0;
then z1=i or z1=max(i-'1,1) or z1=min(i+1,n) by ENUMSET1:def 1;
then reconsider z2=z1 as Element of NAT by ORDINAL1:def 12;
A5: now
i-'1<=i & i<=n by A2,FINSEQ_1:1,NAT_D:35;
then i-'1<=n by XXREAL_0:2;
then
A6: 1<= max(i-'1,1) & max(i-'1,1)<=n by A3,XXREAL_0:28,30;
assume z1=max(i-'1,1);
hence thesis by A6;
end;
now
1<=i+1 by NAT_1:12;
then
A7: 1<=min(i+1,n) by A3,XXREAL_0:20;
A8: min(i+1,n)<=n by XXREAL_0:17;
assume z1=min(i+1,n);
hence z2 in Seg n by A7,A8;
end;
hence thesis by A2,A4,A5,ENUMSET1:def 1;
end;
end;
consider f being Relation of Seg n such that
A9: for x3 being Element of NAT st x3 in Seg n holds Im(f,x3) = F(x3)
from RELSET_1:sch 3(A1);
take f;
thus thesis by A9;
end;
uniqueness
proof
thus for f1,f2 being Relation of Seg n st (for i being Element of NAT st i
in Seg n holds Im(f1,i)={i,max(i-'1,1),min(i+1,n)})& (for i being Element of
NAT st i in Seg n holds Im(f2,i)={i,max(i-'1,1),min(i+1,n)}) holds f1=f2
proof
let f1,f2 be Relation of Seg n;
assume that
A10: for i being Element of NAT st i in Seg n holds Im(f1,i)={i,max(
i-'1,1) ,min(i+1,n)} and
A11: for i being Element of NAT st i in Seg n holds Im(f2,i)={i,max(
i-' 1,1),min(i+1,n)};
for x being set st x in Seg n holds Im(f1,x)=Im(f2,x)
proof
let x be set;
assume
A12: x in Seg n;
then reconsider i2=x as Element of NAT;
Im(f1,i2)={i2,max(i2-'1,1),min(i2+1,n)} by A10,A12;
hence thesis by A11,A12;
end;
hence thesis by RELSET_1:31;
end;
end;
end;
definition
let n be Nat;
assume
A1: n>0;
func FTSL1 n -> non empty RelStr equals
:Def4:
RelStr(# Seg n,Nbdl1 n #);
correctness by A1;
end;
theorem
for n being Nat st n>0 holds FTSL1 n is filled
proof
let n be Nat;
assume n>0;
then
A1: FTSL1 n=RelStr(# Seg n,Nbdl1 n #) by Def4;
let x be Element of FTSL1 n;
x in Seg n by A1;
then reconsider i=x as Element of NAT;
U_FT x= {i,max(i-'1,1),min(i+1,n)} by A1,Def3;
hence thesis by ENUMSET1:def 1;
end;
theorem
for n being Nat st n>0 holds FTSL1 n is symmetric
proof
let n be Nat;
assume n>0;
then
A1: FTSL1 n=RelStr(# Seg n,Nbdl1 n #) by Def4;
let x, y be Element of FTSL1 n;
x in Seg n by A1;
then reconsider i=x as Element of NAT;
A2: 1<=i by A1,FINSEQ_1:1;
A3: i<=n by A1,FINSEQ_1:1;
y in Seg n by A1;
then reconsider j=y as Element of NAT;
A4: U_FT y= {j,max(j-'1,1),min(j+1,n)} by A1,Def3;
A5: U_FT x= {i,max(i-'1,1),min(i+1,n)} by A1,Def3;
now
A6: now
assume
A7: y=max(i-'1,1);
now
per cases;
case
A8: i-'1>=1;
then
A9: y=i-'1 by A7,XXREAL_0:def 10;
now
per cases;
case
i-1>=0;
then j=i-1 by A9,XREAL_0:def 2;
hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A3,XXREAL_0:def 9
;
end;
case
i-1<0;
hence contradiction by A8,XREAL_0:def 2;
end;
end;
hence x =j or x=max(j-'1,1) or x= min(j+1,n);
end;
case
A10: i-'1<1;
A11: now
assume i>1;
then
A12: i-1>0 by XREAL_1:50;
then i-'1=i-1 by XREAL_0:def 2;
then i-'1>=0+1 by A12,NAT_1:13;
hence contradiction by A10;
end;
y=1 by A7,A10,XXREAL_0:def 10;
hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A2,A11,XXREAL_0:1;
end;
end;
hence x in U_FT y by A4,ENUMSET1:def 1;
end;
assume
A13: y in U_FT x;
A14: now
assume y=min(i+1,n);
now
per cases by A5,A13,ENUMSET1:def 1;
case
y=i;
hence x =j or x=max(j-'1,1) or x= min(j+1,n);
end;
case
A15: y=max(i-'1,1);
now
per cases;
case
A16: i-'1>=1;
then
A17: y=i-'1 by A15,XXREAL_0:def 10;
now
per cases;
case
i-1>=0;
then j=i-1 by A17,XREAL_0:def 2;
hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A3,
XXREAL_0:def 9;
end;
case
i-1<0;
hence contradiction by A16,XREAL_0:def 2;
end;
end;
hence x =j or x=max(j-'1,1) or x= min(j+1,n);
end;
case
A18: i-'1<1;
A19: now
assume i>1;
then
A20: i-1>0 by XREAL_1:50;
then i-'1=i-1 by XREAL_0:def 2;
then i-'1>=0+1 by A20,NAT_1:13;
hence contradiction by A18;
end;
y=1 by A15,A18,XXREAL_0:def 10;
hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A2,A19,XXREAL_0:1
;
end;
end;
hence x =j or x=max(j-'1,1) or x= min(j+1,n);
end;
case
A21: y=min(i+1,n);
now
per cases;
case
i+1<=n;
then
A22: y=i+1 by A21,XXREAL_0:def 9;
then
A23: j-1=j-'1 by XREAL_0:def 2;
now
per cases;
case
j-1>=1;
hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A22,A23,
XXREAL_0:def 10;
end;
case
j-1<1;
hence contradiction by A1,A22,FINSEQ_1:1;
end;
end;
hence x =j or x=max(j-'1,1) or x= min(j+1,n);
end;
case
A24: i+1>n;
then y=n by A21,XXREAL_0:def 9;
then j+1>n by NAT_1:13;
then
A25: min(j+1,n)=n by XXREAL_0:def 9;
i>=n by A24,NAT_1:13;
hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A3,A25,XXREAL_0:1
;
end;
end;
hence x =j or x=max(j-'1,1) or x= min(j+1,n);
end;
end;
hence x in U_FT y by A4,ENUMSET1:def 1;
end;
y=i or y=max(i-'1,1) or y=min(i+1,n) by A5,A13,ENUMSET1:def 1;
hence x in U_FT y by A13,A6,A14;
end;
hence thesis;
end;
::1 dimensional cyclic FT_Str
definition
let n be Nat;
func Nbdc1 n -> Relation of Seg n means
:Def5:
for i being Element of NAT st
i in Seg n holds (1<i & i<n implies Im(it,i)={i,i-'1,i+1})& (i=1 & i<n implies
Im(it,i)={i,n,i+1}) & (1<i & i=n implies Im(it,i)={i,i-'1,1}) & (i=1 & i=n
implies Im(it,i)={i});
existence
proof
defpred P[object,object] means
for i being Element of NAT st i=$1 holds (1<i & i
<n implies $2={i,i-'1,i+1})& (i=1 & i<n implies $2={i,n,i+1}) & (1<i & i=n
implies $2={i,i-'1,1}) & (i=1 & i=n implies $2={i});
A1: for x being object st x in Seg n
ex y being object st y in bool Seg n & P[x, y]
proof
let x be object;
assume
A2: x in Seg n;
then reconsider i2=x as Element of NAT;
A3: 1<=i2 & i2<=n by A2,FINSEQ_1:1;
now
per cases by A3,XXREAL_0:1;
case
A4: 1<i2 & i2<n;
i2<=i2+1 by NAT_1:12;
then
A5: 1<i2+1 by A4,XXREAL_0:2;
i2+1<=n by A4,NAT_1:13;
then
A6: i2+1 in Seg n by A5;
set y0={i2,i2-'1,i2+1};
i2-1>0 by A4,XREAL_1:50;
then i2-'1>0 by XREAL_0:def 2;
then
A7: i2-'1>=0+1 by NAT_1:13;
i2-'1<=i2 by NAT_D:35;
then i2-'1<n by A4,XXREAL_0:2;
then
A8: i2-'1 in Seg n by A7;
A9: y0 c= Seg n
by A2,A8,A6,ENUMSET1:def 1;
P[x,y0] by A4;
hence thesis by A9;
end;
case
A10: i2=1 & i2<n;
then i2+1<=n by NAT_1:13;
then
A11: i2+1 in Seg n by A10;
set y0={i2,n,i2+1};
A12: n in Seg n by A10;
A13: y0 c= Seg n
by A2,A12,A11,ENUMSET1:def 1;
P[x,y0] by A10;
hence thesis by A13;
end;
case
A14: 1<i2 & i2=n;
then i2-1>0 by XREAL_1:50;
then i2-'1>0 by XREAL_0:def 2;
then
A15: i2-'1>=0+1 by NAT_1:13;
set y0={i2,i2-'1,1};
A16: 1 in Seg n by A14;
i2-'1<=n by A14,NAT_D:35;
then
A17: i2-'1 in Seg n by A15;
A18: y0 c= Seg n
by A2,A17,A16,ENUMSET1:def 1;
P[x,y0] by A14;
hence thesis by A18;
end;
case
A19: i2=1 & i2=n;
set y0={i2};
A20: y0 c= Seg n
by A2,TARSKI:def 1;
P[x,y0] by A19;
hence thesis by A20;
end;
end;
hence thesis;
end;
consider f2 being Function of Seg n,bool Seg n such that
A21: for x3 being object st x3 in Seg n holds P[x3,f2.x3] from FUNCT_2:
sch 1(A1 );
consider R being Relation of Seg n such that
A22: for i being set st i in Seg n holds Im(R,i) = f2.i by FUNCT_2:93;
take R;
let i being Element of NAT;
assume
A23: i in Seg n;
then Im(R,i) = f2.i by A22;
hence thesis by A21,A23;
end;
uniqueness
proof
let f1,f2 be Relation of Seg n;
assume that
A24: for i being Element of NAT st i in Seg n holds (1<i & i<n implies
Im( f1,i)={i,i-'1,i+1})& (i=1 & i<n implies Im(f1,i)={i,n,i+1}) & (1<i & i=n
implies Im(f1,i)={i,i-'1,1}) & (i=1 & i=n implies Im(f1,i)={i}) and
A25: for i being Element of NAT st i in Seg n holds (1<i & i<n implies
Im(f2,i)={i,i-'1,i+1})& (i=1 & i<n implies Im(f2,i)={i,n,i+1}) & (1<i & i=n
implies Im(f2,i)={i,i-'1,1}) & (i=1 & i=n implies Im(f2,i)={i});
for x being set st x in Seg n holds Im(f1,x)=Im(f2,x)
proof
let x be set;
assume
A26: x in Seg n;
then reconsider i2=x as Element of NAT;
A27: 1<=i2 & i2<=n by A26,FINSEQ_1:1;
per cases by A27,XXREAL_0:1;
suppose
A28: 1<i2 & i2<n;
set y0={i2,i2-'1,i2+1};
Im(f1,x)=y0 by A24,A26,A28;
hence thesis by A25,A26,A28;
end;
suppose
A29: i2=1 & i2<n;
set y0={i2,n,i2+1};
Im(f1,x)=y0 by A24,A26,A29;
hence thesis by A25,A26,A29;
end;
suppose
A30: 1<i2 & i2=n;
set y0={i2,i2-'1,1};
Im(f1,x)=y0 by A24,A26,A30;
hence thesis by A25,A26,A30;
end;
suppose
A31: i2=1 & i2=n;
set y0={i2};
Im(f1,x)=y0 by A24,A26,A31;
hence thesis by A25,A26,A31;
end;
end;
hence f1=f2 by RELSET_1:31;
end;
end;
definition
let n be Nat;
assume
A1: n>0;
func FTSC1 n -> non empty RelStr equals
:Def6:
RelStr(# Seg n,Nbdc1 n #);
correctness by A1;
end;
theorem
for n being Element of NAT st n>0 holds FTSC1 n is filled
proof
let n be Element of NAT;
set f=Nbdc1 n;
assume n>0;
then
A1: FTSC1 n=RelStr(# Seg n,Nbdc1 n #) by Def6;
let x be Element of FTSC1 n;
x in Seg n by A1;
then reconsider i=x as Element of NAT;
A2: 1<=i & i<=n by A1,FINSEQ_1:1;
A3: i=1 & i<n implies Im(f,i)={i,n,i+1} by A1,Def5;
A4: 1<i & i<n implies Im(f,i)={i,i-'1,i+1} by A1,Def5;
A5: i=1 & i=n implies Im(f,i)={i} by A1,Def5;
A6: 1<i & i=n implies Im(f,i)={i,i-'1,1} by A1,Def5;
per cases by A2,XXREAL_0:1;
suppose
1<i & i<n;
hence thesis by A1,A4,ENUMSET1:def 1;
end;
suppose
i=1 & i<n;
hence thesis by A1,A3,ENUMSET1:def 1;
end;
suppose
1<i & i=n;
hence thesis by A1,A6,ENUMSET1:def 1;
end;
suppose
i=1 & i=n;
hence thesis by A1,A5,TARSKI:def 1;
end;
end;
theorem
for n being Element of NAT st n>0 holds FTSC1 n is symmetric
proof
let n be Element of NAT;
set f=Nbdc1 n;
assume n>0;
then
A1: FTSC1 n=RelStr(# Seg n,Nbdc1 n #) by Def6;
let x, y be Element of FTSC1 n;
x in Seg n by A1;
then reconsider i=x as Element of NAT;
A2: 1<=i by A1,FINSEQ_1:1;
A3: i=1 & i<n implies Im(f,i)={i,n,i+1} by A1,Def5;
A4: i=1 & i=n implies Im(f,i)={i} by A1,Def5;
A5: i<=n by A1,FINSEQ_1:1;
y in Seg n by A1;
then reconsider j=y as Element of NAT;
A6: 1<=j by A1,FINSEQ_1:1;
A7: 1<i & i=n implies Im(f,i)={i,i-'1,1} by A1,Def5;
A8: 1<i & i<n implies Im(f,i)={i,i-'1,i+1} by A1,Def5;
assume
A9: y in U_FT x;
A10: j<=n by A1,FINSEQ_1:1;
per cases by A2,A5,XXREAL_0:1;
suppose
A11: 1<i & i<n;
A12: now
i-1>0 by A11,XREAL_1:50;
then
A13: i-'1=i-1 by XREAL_0:def 2;
assume
A14: y=i-'1;
per cases by A14,A13;
suppose
A15: x=j;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A11,Def5;
hence thesis by A15,ENUMSET1:def 1;
end;
suppose
A16: x=j-'1;
then
A17: i=(i-'1)-'1 by A14;
now
assume i<>0;
then
A18: i>=0+1 by NAT_1:13;
then i-1>=1-1 by XREAL_1:9;
then
A19: i-1=i-'1 by XREAL_0:def 2;
now
assume
A20: i=1;
then i-'1-1<0 by A19;
hence contradiction by A14,A16,A20,XREAL_0:def 2;
end;
then i>1 by A18,XXREAL_0:1;
then i-1>1-1 by XREAL_1:9;
then i-'1>=0+1 by A19,NAT_1:13;
then i-'1-1>=0 by XREAL_1:48;
then i-'1-'1=i-'1-1 by XREAL_0:def 2;
hence contradiction by A17,A19;
end;
hence thesis by A11;
end;
suppose
A21: x=j+1;
then
A22: j<n by A5,NAT_1:13;
A23: now
assume j<>1;
then j>1 by A6,XXREAL_0:1;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A22,Def5;
hence thesis by A21,ENUMSET1:def 1;
end;
now
assume j=1;
then Im(the InternalRel of FTSC1 n,y)={j,n,j+1} by A1,A22,Def5;
hence thesis by A21,ENUMSET1:def 1;
end;
hence thesis by A23;
end;
end;
A24: now
assume
A25: y=i+1;
then
A26: j-1=x;
now
per cases by A11,A26,XREAL_0:def 2;
case
A27: x=j;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A11,Def5;
hence thesis by A27,ENUMSET1:def 1;
end;
case
A28: x=j-'1;
now
assume j=1;
then j-1=0;
hence contradiction by A11,A28,XREAL_0:def 2;
end;
then
A29: j>1 by A6,XXREAL_0:1;
A30: now
assume j<>n;
then j<n by A10,XXREAL_0:1;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A29,Def5;
hence thesis by A28,ENUMSET1:def 1;
end;
now
assume j=n;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,1} by A1,A29,Def5;
hence thesis by A28,ENUMSET1:def 1;
end;
hence thesis by A30;
end;
case
x=j+1;
hence contradiction by A25;
end;
end;
hence thesis;
end;
y=i or y=i-'1 or y=i+1 by A1,A8,A9,A11,ENUMSET1:def 1;
hence thesis by A9,A12,A24;
end;
suppose
A31: i=1 & i<n;
per cases by A1,A3,A9,A31,ENUMSET1:def 1;
suppose
y=i & y<>n;
hence thesis by A1,A3,A31,ENUMSET1:def 1;
end;
suppose
y=n;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,1} by A1,A31,Def5;
hence thesis by A31,ENUMSET1:def 1;
end;
suppose
A32: y=i+1 & y<>n;
then j-1=i;
then
A33: j-'1=i by XREAL_0:def 2;
j<n by A10,A32,XXREAL_0:1;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A31,A32,Def5;
hence thesis by A33,ENUMSET1:def 1;
end;
end;
suppose
A34: 1<i & i=n;
per cases by A1,A7,A9,A34,ENUMSET1:def 1;
suppose
y=i & y<>1;
hence thesis by A1,A7,A34,ENUMSET1:def 1;
end;
suppose
y=1;
then Im(the InternalRel of FTSC1 n,y)={j,n,j+1} by A1,A34,Def5;
hence thesis by A34,ENUMSET1:def 1;
end;
suppose
A35: y=i-'1 & y<>1;
then
A36: 1<j by A6,XXREAL_0:1;
n-1>0 by A34,XREAL_1:50;
then
A37: n-1=n-'1 by XREAL_0:def 2;
n-1+1=n;
then j<n by A34,A35,A37,NAT_1:13;
then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A36,Def5;
hence thesis by A34,A35,A37,ENUMSET1:def 1;
end;
end;
suppose
i=1 & i=n;
then j=i by A1,A4,A9,TARSKI:def 1;
hence thesis by A9;
end;
end;