:: 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-2012 Association of Mizar Users


begin

definition
let FT be non empty RelStr ;
let A, B be Subset of FT;
pred A,B are_separated means :Def1: :: FINTOPO4:def 1
( A ^b misses B & A misses B ^b );
symmetry
for A, B being Subset of FT st A ^b misses B & A misses B ^b holds
( B ^b misses A & B misses A ^b )
;
end;

:: deftheorem Def1 defines are_separated FINTOPO4:def 1 :
for FT being non empty RelStr
for A, B being Subset of FT holds
( A,B are_separated iff ( A ^b misses B & A misses B ^b ) );

theorem Th1: :: FINTOPO4:1
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Finf (A,n) c= Finf (A,m)
proof end;

theorem :: FINTOPO4:2
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fcl (A,n) c= Fcl (A,m)
proof end;

theorem :: FINTOPO4:3
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fdfl (A,m) c= Fdfl (A,n)
proof end;

theorem :: FINTOPO4:4
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fint (A,m) c= Fint (A,n)
proof end;

theorem :: FINTOPO4:5
for FT being non empty RelStr
for A, B being Subset of FT st A,B are_separated holds
B,A are_separated ;

theorem Th6: :: FINTOPO4:6
for FT being non empty filled RelStr
for A, B being Subset of FT st A,B are_separated holds
A misses B
proof end;

theorem :: FINTOPO4:7
for FT being non empty RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff ( A ^f misses B & A misses B ^f ) )
proof end;

theorem Th8: :: FINTOPO4:8
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b
proof end;

theorem :: FINTOPO4:9
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric & A misses B ^b holds
A ^b misses B by Th8;

theorem :: FINTOPO4:10
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A ^b misses B )
proof end;

theorem :: FINTOPO4:11
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A misses B ^b )
proof end;

theorem Th12: :: FINTOPO4:12
for FT being non empty filled RelStr
for 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 & not A = IT holds
B = IT )
proof end;

theorem :: FINTOPO4:13
for FT being non empty filled RelStr
for B being Subset of FT st FT is symmetric holds
( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) )
proof end;

definition
let FT1, FT2 be non empty RelStr ;
let f be Function of FT1,FT2;
let n be Element of NAT ;
pred f is_continuous n means :Def2: :: FINTOPO4:def 2
for x being Element of FT1
for 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;

:: deftheorem Def2 defines is_continuous FINTOPO4:def 2 :
for FT1, FT2 being non empty RelStr
for f being Function of FT1,FT2
for n being Element of NAT holds
( f is_continuous n iff for x being Element of FT1
for 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) );

theorem :: FINTOPO4:14
for FT1 being non empty RelStr
for FT2 being non empty filled RelStr
for n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
proof end;

theorem :: FINTOPO4:15
for FT1 being non empty RelStr
for FT2 being non empty filled RelStr
for n0, n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds
f is_continuous n
proof end;

theorem Th16: :: FINTOPO4:16
for FT1, FT2 being non empty RelStr
for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
proof end;

theorem :: FINTOPO4:17
for FT1, FT2 being non empty RelStr
for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
proof end;

::1 dimensional linear FT_Str
definition
let n be Nat;
func Nbdl1 n -> Relation of (Seg n) means :Def3: :: FINTOPO4:def 3
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
ex b1 being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}
proof end;
uniqueness
for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (b2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Nbdl1 FINTOPO4:def 3 :
for n being Nat
for b2 being Relation of (Seg n) holds
( b2 = Nbdl1 n iff for i being Element of NAT st i in Seg n holds
Im (b2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} );

definition
let n be Nat;
assume A1: n > 0 ;
func FTSL1 n -> non empty RelStr equals :Def4: :: FINTOPO4:def 4
RelStr(# (Seg n),(Nbdl1 n) #);
correctness
coherence
RelStr(# (Seg n),(Nbdl1 n) #) is non empty RelStr
;
by A1;
end;

:: deftheorem Def4 defines FTSL1 FINTOPO4:def 4 :
for n being Nat st n > 0 holds
FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #);

theorem :: FINTOPO4:18
for n being Nat st n > 0 holds
FTSL1 n is filled
proof end;

theorem :: FINTOPO4:19
for n being Nat st n > 0 holds
FTSL1 n is symmetric
proof end;

::1 dimensional cyclic FT_Str
definition
let n be Nat;
func Nbdc1 n -> Relation of (Seg n) means :Def5: :: FINTOPO4:def 5
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
ex b1 being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) )
proof end;
uniqueness
for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Nbdc1 FINTOPO4:def 5 :
for n being Nat
for b2 being Relation of (Seg n) holds
( b2 = Nbdc1 n iff for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) );

definition
let n be Nat;
assume A1: n > 0 ;
func FTSC1 n -> non empty RelStr equals :Def6: :: FINTOPO4:def 6
RelStr(# (Seg n),(Nbdc1 n) #);
correctness
coherence
RelStr(# (Seg n),(Nbdc1 n) #) is non empty RelStr
;
by A1;
end;

:: deftheorem Def6 defines FTSC1 FINTOPO4:def 6 :
for n being Nat st n > 0 holds
FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #);

theorem :: FINTOPO4:20
for n being Element of NAT st n > 0 holds
FTSC1 n is filled
proof end;

theorem :: FINTOPO4:21
for n being Element of NAT st n > 0 holds
FTSC1 n is symmetric
proof end;