:: FINTOPO4 semantic presentation

definition

let FT be non empty FT_Space_Str ;
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 );

end;

:: deftheorem Def1 defines are_separated FINTOPO4:def 1 :

theorem Th1: :: FINTOPO4:1

for FT being non empty filled FT_Space_Str
for A being Subset of FT
for n, m being Nat st n <= m holds
Finf A,n c= Finf A,m

proof end;

theorem :: FINTOPO4:2

for FT being non empty filled FT_Space_Str
for A being Subset of FT
for n, m being Nat st n <= m holds
Fcl A,n c= Fcl A,m

proof end;

theorem :: FINTOPO4:3

for FT being non empty filled FT_Space_Str
for A being Subset of FT
for n, m being Nat st n <= m holds
Fdfl A,m c= Fdfl A,n

proof end;

theorem :: FINTOPO4:4

for FT being non empty filled FT_Space_Str
for A being Subset of FT
for n, m being Nat st n <= m holds
Fint A,m c= Fint A,n

proof end;

theorem :: FINTOPO4:5

for FT being non empty FT_Space_Str
for A, B being Subset of FT st A,B are_separated holds
B,A are_separated

proof end;

theorem Th6: :: FINTOPO4:6

for FT being non empty filled FT_Space_Str
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 FT_Space_Str
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 FT_Space_Str
for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b

proof end;

theorem Th9: :: FINTOPO4:9

for FT being non empty filled FT_Space_Str
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 FT_Space_Str
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 FT_Space_Str
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 FT_Space_Str
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 FT_Space_Str
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 FT_Space_Str ;
let f be Function of the carrier of FT1,the carrier of FT2;
let n be 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 FT_Space_Str
for FT2 being non empty filled FT_Space_Str
for n being Nat
for f being Function of the carrier of FT1,the carrier of FT2 st f is_continuous 0 holds
f is_continuous n

proof end;

theorem :: FINTOPO4:15

for FT1 being non empty FT_Space_Str
for FT2 being non empty filled FT_Space_Str
for n0, n being Nat
for f being Function of the carrier of FT1,the carrier of 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 FT_Space_Str
for A being Subset of FT1
for B being Subset of FT2
for f being Function of the carrier of FT1,the carrier of 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 FT_Space_Str
for A being Subset of FT1
for B being Subset of FT2
for f being Function of the carrier of FT1,the carrier of FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected

proof end;

definition

let n be Nat;
func Nbdl1 n -> Function of Seg n, bool (Seg n) means :Def3: :: FINTOPO4:def 3
( dom it = Seg n & ( for i being Nat st i in Seg n holds
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 FT_Space_Str equals :Def4: :: FINTOPO4:def 4
FT_Space_Str(# (Seg n),(Nbdl1 n) #);
correctness

proof end;

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;

definition

let n be Nat;
func Nbdc1 n -> Function of Seg n, bool (Seg n) means :Def5: :: FINTOPO4:def 5
( dom it = Seg n & ( for i being Nat st i in Seg n holds
( ( 1 < i & i < n implies it . i = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies it . i = {i,n,(i + 1)} ) & ( 1 < i & i = n implies it . i = {i,(i -' 1),1} ) & ( i = 1 & i = n implies 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 FT_Space_Str equals :Def6: :: FINTOPO4:def 6
FT_Space_Str(# (Seg n),(Nbdc1 n) #);
correctness

proof end;

end;

:: deftheorem Def6 defines FTSC1 FINTOPO4:def 6 :

theorem :: FINTOPO4:20

for n being Nat st n > 0 holds
FTSC1 n is filled

proof end;

theorem :: FINTOPO4:21

for n being Nat st n > 0 holds
FTSC1 n is symmetric

proof end;