:: FINTOPO4 semantic presentation

definition

let c₁ be non empty FT_Space_Str ;
let c₂, c₃ be Subset of c₁;
pred c₂,c₃ are_separated means :Def1: :: FINTOPO4:def 1
( a₂ ^b misses a₃ & a₂ misses a₃ ^b );

end;

:: deftheorem Def1 defines are_separated FINTOPO4:def 1 :

theorem Th1: :: FINTOPO4:1

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
Finf b₂,b₃ c= Finf b₂,b₄

proof end;

theorem Th2: :: FINTOPO4:2

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
Fcl b₂,b₃ c= Fcl b₂,b₄

proof end;

theorem Th3: :: FINTOPO4:3

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
Fdfl b₂,b₄ c= Fdfl b₂,b₃

proof end;

theorem Th4: :: FINTOPO4:4

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
Fint b₂,b₄ c= Fint b₂,b₃

proof end;

theorem Th5: :: FINTOPO4:5

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂,b₃ are_separated holds
b₃,b₂ are_separated

proof end;

theorem Th6: :: FINTOPO4:6

for b₁ being non empty filled FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂,b₃ are_separated holds
b₂ misses b₃

proof end;

theorem Th7: :: FINTOPO4:7

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₁ is symmetric holds
( b₂,b₃ are_separated iff ( b₂ ^f misses b₃ & b₂ misses b₃ ^f ) )

proof end;

theorem Th8: :: FINTOPO4:8

for b₁ being non empty filled FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₁ is symmetric & b₂ ^b misses b₃ holds
b₂ misses b₃ ^b

proof end;

theorem Th9: :: FINTOPO4:9

for b₁ being non empty filled FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₁ is symmetric & b₂ misses b₃ ^b holds
b₂ ^b misses b₃ by Th8;

theorem Th10: :: FINTOPO4:10

for b₁ being non empty filled FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₁ is symmetric holds
( b₂,b₃ are_separated iff b₂ ^b misses b₃ )

proof end;

theorem Th11: :: FINTOPO4:11

for b₁ being non empty filled FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₁ is symmetric holds
( b₂,b₃ are_separated iff b₂ misses b₃ ^b )

proof end;

theorem Th12: :: FINTOPO4:12

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁ st b₁ is symmetric holds
( b₂ is connected iff for b₃, b₄ being Subset of b₁ st b₂ = b₃ \/ b₄ & b₃,b₄ are_separated & not b₃ = b₂ holds
b₄ = b₂ )

proof end;

theorem Th13: :: FINTOPO4:13

for b₁ being non empty filled FT_Space_Str
for b₂ being Subset of b₁ st b₁ is symmetric holds
( b₂ is connected iff for b₃ being Subset of b₁ holds
( not b₃ <> {} or not b₂ \ b₃ <> {} or not b₃ c= b₂ or not b₃ ^b misses b₂ \ b₃ ) )

proof end;

definition

let c₁, c₂ be non empty FT_Space_Str ;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
let c₄ be Nat;
pred c₃ is_continuous c₄ means :Def2: :: FINTOPO4:def 2
for b₁ being Element of a₁
for b₂ being Element of a₂ st b₁ in the carrier of a₁ & b₂ = a₃ . b₁ holds
a₃ .: (U_FT b₁,0) c= U_FT b₂,a₄;

end;

:: deftheorem Def2 defines is_continuous FINTOPO4:def 2 :

theorem Th14: :: FINTOPO4:14

for b₁ being non empty FT_Space_Str
for b₂ being non empty filled FT_Space_Str
for b₃ being Nat
for b₄ being Function of the carrier of b₁,the carrier of b₂ st b₄ is_continuous 0 holds
b₄ is_continuous b₃

proof end;

theorem Th15: :: FINTOPO4:15

for b₁ being non empty FT_Space_Str
for b₂ being non empty filled FT_Space_Str
for b₃, b₄ being Nat
for b₅ being Function of the carrier of b₁,the carrier of b₂ st b₅ is_continuous b₃ & b₃ <= b₄ holds
b₅ is_continuous b₄

proof end;

theorem Th16: :: FINTOPO4:16

for b₁, b₂ being non empty FT_Space_Str
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Function of the carrier of b₁,the carrier of b₂ st b₅ is_continuous 0 & b₄ = b₅ .: b₃ holds
b₅ .: (b₃ ^b ) c= b₄ ^b

proof end;

theorem Th17: :: FINTOPO4:17

for b₁, b₂ being non empty FT_Space_Str
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Function of the carrier of b₁,the carrier of b₂ st b₃ is connected & b₅ is_continuous 0 & b₄ = b₅ .: b₃ holds
b₄ is connected

proof end;

definition

let c₁ be Nat;
func Nbdl1 c₁ -> Function of Seg a₁, bool (Seg a₁) means :Def3: :: FINTOPO4:def 3
( dom a₂ = Seg a₁ & ( for b₁ being Nat st b₁ in Seg a₁ holds
a₂ . b₁ = {b₁,(max (b₁ -' 1),1),(min (b₁ + 1),a₁)} ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Nbdl1 FINTOPO4:def 3 :

definition

let c₁ be Nat;
assume E10: c₁ > 0 ;
func FTSL1 c₁ -> non empty FT_Space_Str equals :Def4: :: FINTOPO4:def 4
FT_Space_Str(# (Seg a₁),(Nbdl1 a₁) #);
correctness

proof end;

end;

:: deftheorem Def4 defines FTSL1 FINTOPO4:def 4 :

theorem Th18: :: FINTOPO4:18

for b₁ being Nat st b₁ > 0 holds
FTSL1 b₁ is filled

proof end;

theorem Th19: :: FINTOPO4:19

for b₁ being Nat st b₁ > 0 holds
FTSL1 b₁ is symmetric

proof end;

definition

let c₁ be Nat;
func Nbdc1 c₁ -> Function of Seg a₁, bool (Seg a₁) means :Def5: :: FINTOPO4:def 5
( dom a₂ = Seg a₁ & ( for b₁ being Nat st b₁ in Seg a₁ holds
( ( 1 < b₁ & b₁ < a₁ implies a₂ . b₁ = {b₁,(b₁ -' 1),(b₁ + 1)} ) & ( b₁ = 1 & b₁ < a₁ implies a₂ . b₁ = {b₁,a₁,(b₁ + 1)} ) & ( 1 < b₁ & b₁ = a₁ implies a₂ . b₁ = {b₁,(b₁ -' 1),1} ) & ( b₁ = 1 & b₁ = a₁ implies a₂ . b₁ = {b₁} ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Nbdc1 FINTOPO4:def 5 :

definition

let c₁ be Nat;
assume E12: c₁ > 0 ;
func FTSC1 c₁ -> non empty FT_Space_Str equals :Def6: :: FINTOPO4:def 6
FT_Space_Str(# (Seg a₁),(Nbdc1 a₁) #);
correctness

proof end;

end;

:: deftheorem Def6 defines FTSC1 FINTOPO4:def 6 :

theorem Th20: :: FINTOPO4:20

for b₁ being Nat st b₁ > 0 holds
FTSC1 b₁ is filled

proof end;

theorem Th21: :: FINTOPO4:21

for b₁ being Nat st b₁ > 0 holds
FTSC1 b₁ is symmetric

proof end;