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

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;
let A, B be Subset of FT;

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

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

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)

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)

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)

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)

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 ;

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

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 ) )

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

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

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 )

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 )

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 )

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 ) )

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

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

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

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

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

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;

ex b_{1} being Relation of (Seg n) st

for i being Element of NAT st i in Seg n holds

Im (b_{1},i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}

for b_{1}, b_{2} being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds

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

Im (b_{2},i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds

b_{1} = b_{2}

end;
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 for i being Element of NAT st i in Seg n holds

Im (it,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))};

ex b

for i being Element of NAT st i in Seg n holds

Im (b

proof end;

uniqueness for b

Im (b

Im (b

b

proof end;

:: deftheorem Def3 defines Nbdl1 FINTOPO4:def 3 :

for n being Nat

for b_{2} being Relation of (Seg n) holds

( b_{2} = Nbdl1 n iff for i being Element of NAT st i in Seg n holds

Im (b_{2},i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} );

for n being Nat

for b

( b

Im (b

definition

let n be Nat;

assume A1: n > 0 ;

correctness

coherence

RelStr(# (Seg n),(Nbdl1 n) #) is non empty RelStr ;

by A1;

end;
assume A1: n > 0 ;

correctness

coherence

RelStr(# (Seg n),(Nbdl1 n) #) is non empty RelStr ;

by A1;

:: deftheorem Def4 defines FTSL1 FINTOPO4:def 4 :

for n being Nat st n > 0 holds

FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #);

for n being Nat st n > 0 holds

FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #);

::1 dimensional cyclic FT_Str

definition

let n be Nat;

ex b_{1} 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_{1},i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b_{1},i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b_{1},i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b_{1},i) = {i} ) )

for b_{1}, b_{2} 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_{1},i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b_{1},i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b_{1},i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b_{1},i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds

( ( 1 < i & i < n implies Im (b_{2},i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b_{2},i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b_{2},i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b_{2},i) = {i} ) ) ) holds

b_{1} = b_{2}

end;
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 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} ) );

ex b

for i being Element of NAT st i in Seg n holds

( ( 1 < i & i < n implies Im (b

proof end;

uniqueness for b

( ( 1 < i & i < n implies Im (b

( ( 1 < i & i < n implies Im (b

b

proof end;

:: deftheorem Def5 defines Nbdc1 FINTOPO4:def 5 :

for n being Nat

for b_{2} being Relation of (Seg n) holds

( b_{2} = Nbdc1 n iff for i being Element of NAT st i in Seg n holds

( ( 1 < i & i < n implies Im (b_{2},i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b_{2},i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b_{2},i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b_{2},i) = {i} ) ) );

for n being Nat

for b

( b

( ( 1 < i & i < n implies Im (b

definition

let n be Nat;

assume A1: n > 0 ;

correctness

coherence

RelStr(# (Seg n),(Nbdc1 n) #) is non empty RelStr ;

by A1;

end;
assume A1: n > 0 ;

correctness

coherence

RelStr(# (Seg n),(Nbdc1 n) #) is non empty RelStr ;

by A1;

:: deftheorem Def6 defines FTSC1 FINTOPO4:def 6 :

for n being Nat st n > 0 holds

FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #);

for n being Nat st n > 0 holds

FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #);