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

definition

let FT be non empty RelStr ;
let A, B be Subset of FT;

pred A,B are_separated means :: 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 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 by FIN_TOPO:13, XBOOLE_1:63;

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 ) ) by FIN_TOPO:12;

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 ) by Th8;

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 ) by Th8;

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 Nat;

pred f is_continuous n means :: 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 defines is_continuous FINTOPO4:def 2 :
for FT1, FT2 being non empty RelStr
for f being Function of FT1,FT2
for n being 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 b₁ being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
Im (b₁,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}

proof end;

uniqueness
for b₁, b₂ being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
Im (b₁,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (b₂,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Nbdl1 FINTOPO4:def 3 :
for n being Nat
for b₂ being Relation of (Seg n) holds
( b₂ = Nbdl1 n iff for i being Element of NAT st i in Seg n holds
Im (b₂,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 b₁ being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b₁,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b₁,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b₁,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b₁,i) = {i} ) )

proof end;

uniqueness
for b₁, b₂ being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b₁,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b₁,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b₁,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b₁,i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b₂,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b₂,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b₂,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b₂,i) = {i} ) ) ) holds
b₁ = b₂

proof end;

end;

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