FINTOPO4: Continuous Mappings between Finite and One-Dimensional Finite Topological Spaces

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

end;

:: deftheorem Def1 defines are_separated FINTOPO4:def 1 :

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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Nbdl1 FINTOPO4:def 3 :

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 by A1;

end;

:: deftheorem Def4 defines FTSL1 FINTOPO4:def 4 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Nbdc1 FINTOPO4:def 5 :

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 by A1;

end;

:: deftheorem Def6 defines FTSC1 FINTOPO4:def 6 :

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;