:: FINTOPO2 semantic presentation

theorem Th1: :: FINTOPO2:1

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^i c= b₃ ^i

proof end;

theorem Th2: :: FINTOPO2:2

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^delta = (b₂ ^b ) /\ ((b₂ ^i ) ` )

proof end;

theorem Th3: :: FINTOPO2:3

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^delta = (b₂ ^b ) \ (b₂ ^i )

proof end;

theorem Th4: :: FINTOPO2:4

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₂ ` is open holds
b₂ is closed

proof end;

theorem Th5: :: FINTOPO2:5

for b₁ being non empty FT_Space_Str
for b₂ being Subset of b₁ st b₂ ` is closed holds
b₂ is open

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂, c₃ be Element of c₁;
let c₄ be Subset of c₁;
func P_1 c₂,c₃,c₄ -> Element of BOOLEAN equals :Def1: :: FINTOPO2:def 1
TRUE if ( a₃ in U_FT a₂ & a₃ in a₄ )
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :

definition

let c₁ be non empty FT_Space_Str ;
let c₂, c₃ be Element of c₁;
let c₄ be Subset of c₁;
func P_2 c₂,c₃,c₄ -> Element of BOOLEAN equals :Def2: :: FINTOPO2:def 2
TRUE if ( a₃ in U_FT a₂ & a₃ in a₄ ` )
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :

theorem Th6: :: FINTOPO2:6

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ holds
( P_1 b₂,b₃,b₄ = TRUE iff ( b₃ in U_FT b₂ & b₃ in b₄ ) ) by Def1, MARGREL1:38;

theorem Th7: :: FINTOPO2:7

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Element of b₁
for b₄ being Subset of b₁ holds
( P_2 b₂,b₃,b₄ = TRUE iff ( b₃ in U_FT b₂ & b₃ in b₄ ` ) ) by Def2, MARGREL1:38;

theorem Th8: :: FINTOPO2:8

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^delta iff ex b₄, b₅ being Element of b₁ st
( P_1 b₂,b₄,b₃ = TRUE & P_2 b₂,b₅,b₃ = TRUE ) )

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂, c₃ be Element of c₁;
func P_0 c₂,c₃ -> Element of BOOLEAN equals :Def3: :: FINTOPO2:def 3
TRUE if a₃ in U_FT a₂
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :

theorem Th9: :: FINTOPO2:9

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Element of b₁ holds
( P_0 b₂,b₃ = TRUE iff b₃ in U_FT b₂ ) by Def3, MARGREL1:38;

theorem Th10: :: FINTOPO2:10

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^i iff for b₄ being Element of b₁ st P_0 b₂,b₄ = TRUE holds
P_1 b₂,b₄,b₃ = TRUE )

proof end;

theorem Th11: :: FINTOPO2:11

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^b iff ex b₄ being Element of b₁ st P_1 b₂,b₄,b₃ = TRUE )

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂ be Element of c₁;
let c₃ be Subset of c₁;
func P_A c₂,c₃ -> Element of BOOLEAN equals :Def4: :: FINTOPO2:def 4
TRUE if a₂ in a₃
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def4 defines P_A FINTOPO2:def 4 :

theorem Th12: :: FINTOPO2:12

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( P_A b₂,b₃ = TRUE iff b₂ in b₃ ) by Def4, MARGREL1:38;

theorem Th13: :: FINTOPO2:13

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^deltai iff ( ex b₄, b₅ being Element of b₁ st
( P_1 b₂,b₄,b₃ = TRUE & P_2 b₂,b₅,b₃ = TRUE ) & P_A b₂,b₃ = TRUE ) )

proof end;

theorem Th14: :: FINTOPO2:14

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^deltao iff ( ex b₄, b₅ being Element of b₁ st
( P_1 b₂,b₄,b₃ = TRUE & P_2 b₂,b₅,b₃ = TRUE ) & P_A b₂,b₃ = FALSE ) )

proof end;

definition

let c₁ be non empty FT_Space_Str ;
let c₂, c₃ be Element of c₁;
func P_e c₂,c₃ -> Element of BOOLEAN equals :Def5: :: FINTOPO2:def 5
TRUE if a₂ = a₃
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def5 defines P_e FINTOPO2:def 5 :

theorem Th15: :: FINTOPO2:15

for b₁ being non empty FT_Space_Str
for b₂, b₃ being Element of b₁ holds
( P_e b₂,b₃ = TRUE iff b₂ = b₃ ) by Def5, MARGREL1:38;

theorem Th16: :: FINTOPO2:16

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^s iff ( P_A b₂,b₃ = TRUE & ( for b₄ being Element of b₁ holds
( not P_1 b₂,b₄,b₃ = TRUE or not P_e b₂,b₄ = FALSE ) ) ) )

proof end;

theorem Th17: :: FINTOPO2:17

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^n iff ( P_A b₂,b₃ = TRUE & ex b₄ being Element of b₁ st
( P_1 b₂,b₄,b₃ = TRUE & P_e b₂,b₄ = FALSE ) ) )

proof end;

theorem Th18: :: FINTOPO2:18

for b₁ being non empty FT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^f iff ex b₄ being Element of b₁ st
( P_A b₄,b₃ = TRUE & P_0 b₄,b₂ = TRUE ) )

proof end;

definition

attr a₁ is strict;
struct FMT_Space_Str -> 1-sorted ;
aggr FMT_Space_Str(# carrier, BNbd #) -> FMT_Space_Str ;
sel BNbd c₁ -> Function of the carrier of a₁, bool (bool the carrier of a₁);

end;

registration

cluster non empty strict FMT_Space_Str ;
existence

proof end;

end;

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Element of c₁;
func U_FMT c₂ -> Subset-Family of a₁ equals :: FINTOPO2:def 6
the BNbd of a₁ . a₂;
correctness ;

end;

:: deftheorem Def6 defines U_FMT FINTOPO2:def 6 :

definition

let c₁ be non empty TopStruct ;
func NeighSp c₁ -> non empty strict FMT_Space_Str means :: FINTOPO2:def 7
( the carrier of a₂ = the carrier of a₁ & ( for b₁ being Point of a₂ holds U_FMT b₁ = { b₂ where B is Subset of a₁ : ( b₂ in the topology of a₁ & b₁ in b₂ ) } ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines NeighSp FINTOPO2:def 7 :

definition

let c₁ be non empty FMT_Space_Str ;
attr a₁ is Fo_filled means :Def8: :: FINTOPO2:def 8
for b₁ being Element of a₁
for b₂ being Subset of a₁ st b₂ in U_FMT b₁ holds
b₁ in b₂;

end;

:: deftheorem Def8 defines Fo_filled FINTOPO2:def 8 :

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^Fodelta -> Subset of a₁ equals :: FINTOPO2:def 9
{ b₁ where B is Element of a₁ : for b₁ being Subset of a₁ st b₂ in U_FMT b₁ holds
( b₂ meets a₂ & b₂ meets a₂ ` ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines ^Fodelta FINTOPO2:def 9 :

theorem Th19: :: FINTOPO2:19

canceled;

theorem Th20: :: FINTOPO2:20

for b₁ being non empty FMT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^Fodelta iff for b₄ being Subset of b₁ st b₄ in U_FMT b₂ holds
( b₄ meets b₃ & b₄ meets b₃ ` ) )

proof end;

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^Fob -> Subset of a₁ equals :: FINTOPO2:def 10
{ b₁ where B is Element of a₁ : for b₁ being Subset of a₁ st b₂ in U_FMT b₁ holds
b₂ meets a₂ } ;
coherence

proof end;

end;

:: deftheorem Def10 defines ^Fob FINTOPO2:def 10 :

theorem Th21: :: FINTOPO2:21

for b₁ being non empty FMT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^Fob iff for b₄ being Subset of b₁ st b₄ in U_FMT b₂ holds
b₄ meets b₃ )

proof end;

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^Foi -> Subset of a₁ equals :: FINTOPO2:def 11
{ b₁ where B is Element of a₁ : ex b₁ being Subset of a₁ st
( b₂ in U_FMT b₁ & b₂ c= a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def11 defines ^Foi FINTOPO2:def 11 :

theorem Th22: :: FINTOPO2:22

for b₁ being non empty FMT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^Foi iff ex b₄ being Subset of b₁ st
( b₄ in U_FMT b₂ & b₄ c= b₃ ) )

proof end;

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^Fos -> Subset of a₁ equals :: FINTOPO2:def 12
{ b₁ where B is Element of a₁ : ( b₁ in a₂ & ex b₁ being Subset of a₁ st
( b₂ in U_FMT b₁ & b₂ \ {b₁} misses a₂ ) ) } ;
coherence

proof end;

end;

:: deftheorem Def12 defines ^Fos FINTOPO2:def 12 :

theorem Th23: :: FINTOPO2:23

for b₁ being non empty FMT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^Fos iff ( b₂ in b₃ & ex b₄ being Subset of b₁ st
( b₄ in U_FMT b₂ & b₄ \ {b₂} misses b₃ ) ) )

proof end;

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^Fon -> Subset of a₁ equals :: FINTOPO2:def 13
a₂ \ (a₂ ^Fos );
coherence ;

end;

:: deftheorem Def13 defines ^Fon FINTOPO2:def 13 :

theorem Th24: :: FINTOPO2:24

for b₁ being non empty FMT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^Fon iff ( b₂ in b₃ & ( for b₄ being Subset of b₁ st b₄ in U_FMT b₂ holds
b₄ \ {b₂} meets b₃ ) ) )

proof end;

theorem Th25: :: FINTOPO2:25

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^Fob c= b₃ ^Fob

proof end;

theorem Th26: :: FINTOPO2:26

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
b₂ ^Foi c= b₃ ^Foi

proof end;

theorem Th27: :: FINTOPO2:27

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ ^Fob ) \/ (b₃ ^Fob ) c= (b₂ \/ b₃) ^Fob

proof end;

theorem Th28: :: FINTOPO2:28

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ /\ b₃) ^Fob c= (b₂ ^Fob ) /\ (b₃ ^Fob )

proof end;

theorem Th29: :: FINTOPO2:29

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ ^Foi ) \/ (b₃ ^Foi ) c= (b₂ \/ b₃) ^Foi

proof end;

theorem Th30: :: FINTOPO2:30

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ holds (b₂ /\ b₃) ^Foi c= (b₂ ^Foi ) /\ (b₃ ^Foi )

proof end;

theorem Th31: :: FINTOPO2:31

for b₁ being non empty FMT_Space_Str holds
( ( for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ in U_FMT b₂ & b₄ in U_FMT b₂ holds
ex b₅ being Subset of b₁ st
( b₅ in U_FMT b₂ & b₅ c= b₃ /\ b₄ ) ) iff for b₂, b₃ being Subset of b₁ holds (b₂ \/ b₃) ^Fob = (b₂ ^Fob ) \/ (b₃ ^Fob ) )

proof end;

theorem Th32: :: FINTOPO2:32

proof end;

theorem Th33: :: FINTOPO2:33

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ st ( for b₄ being Element of b₁
for b₅, b₆ being Subset of b₁ st b₅ in U_FMT b₄ & b₆ in U_FMT b₄ holds
ex b₇ being Subset of b₁ st
( b₇ in U_FMT b₄ & b₇ c= b₅ /\ b₆ ) ) holds
(b₂ \/ b₃) ^Fodelta c= (b₂ ^Fodelta ) \/ (b₃ ^Fodelta )

proof end;

theorem Th34: :: FINTOPO2:34

for b₁ being non empty FMT_Space_Str st b₁ is Fo_filled & ( for b₂, b₃ being Subset of b₁ holds (b₂ \/ b₃) ^Fodelta = (b₂ ^Fodelta ) \/ (b₃ ^Fodelta ) ) holds
for b₂ being Element of b₁
for b₃, b₄ being Subset of b₁ st b₃ in U_FMT b₂ & b₄ in U_FMT b₂ holds
ex b₅ being Subset of b₁ st
( b₅ in U_FMT b₂ & b₅ c= b₃ /\ b₄ )

proof end;

theorem Th35: :: FINTOPO2:35

for b₁ being non empty FMT_Space_Str
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds
( b₂ in b₃ ^Fos iff ( b₂ in b₃ & not b₂ in (b₃ \ {b₂}) ^Fob ) )

proof end;

theorem Th36: :: FINTOPO2:36

for b₁ being non empty FMT_Space_Str holds
( b₁ is Fo_filled iff for b₂ being Subset of b₁ holds b₂ c= b₂ ^Fob )

proof end;

theorem Th37: :: FINTOPO2:37

for b₁ being non empty FMT_Space_Str holds
( b₁ is Fo_filled iff for b₂ being Subset of b₁ holds b₂ ^Foi c= b₂ )

proof end;

theorem Th38: :: FINTOPO2:38

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ holds ((b₂ ` ) ^Fob ) ` = b₂ ^Foi

proof end;

theorem Th39: :: FINTOPO2:39

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ holds ((b₂ ` ) ^Foi ) ` = b₂ ^Fob

proof end;

theorem Th40: :: FINTOPO2:40

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^Fodelta = (b₂ ^Fob ) /\ ((b₂ ` ) ^Fob )

proof end;

theorem Th41: :: FINTOPO2:41

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^Fodelta = (b₂ ^Fob ) /\ ((b₂ ^Foi ) ` )

proof end;

theorem Th42: :: FINTOPO2:42

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^Fodelta = (b₂ ` ) ^Fodelta

proof end;

theorem Th43: :: FINTOPO2:43

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^Fodelta = (b₂ ^Fob ) \ (b₂ ^Foi )

proof end;

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Subset of c₁;
func c₂ ^Fodel_i -> Subset of a₁ equals :: FINTOPO2:def 14
a₂ /\ (a₂ ^Fodelta );
coherence ;
func c₂ ^Fodel_o -> Subset of a₁ equals :: FINTOPO2:def 15
(a₂ ` ) /\ (a₂ ^Fodelta );
coherence ;

end;

:: deftheorem Def14 defines ^Fodel_i FINTOPO2:def 14 :

:: deftheorem Def15 defines ^Fodel_o FINTOPO2:def 15 :

theorem Th44: :: FINTOPO2:44

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ holds b₂ ^Fodelta = (b₂ ^Fodel_i ) \/ (b₂ ^Fodel_o )

proof end;

definition

let c₁ be non empty FMT_Space_Str ;
let c₂ be Subset of c₁;
attr a₂ is Fo_open means :Def16: :: FINTOPO2:def 16
a₂ = a₂ ^Foi ;
attr a₂ is Fo_closed means :Def17: :: FINTOPO2:def 17
a₂ = a₂ ^Fob ;

end;

:: deftheorem Def16 defines Fo_open FINTOPO2:def 16 :

:: deftheorem Def17 defines Fo_closed FINTOPO2:def 17 :

theorem Th45: :: FINTOPO2:45

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ st b₂ ` is Fo_open holds
b₂ is Fo_closed

proof end;

theorem Th46: :: FINTOPO2:46

for b₁ being non empty FMT_Space_Str
for b₂ being Subset of b₁ st b₂ ` is Fo_closed holds
b₂ is Fo_open

proof end;

theorem Th47: :: FINTOPO2:47

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ st b₁ is Fo_filled & ( for b₄ being Element of b₁ holds {b₄} in U_FMT b₄ ) holds
(b₂ /\ b₃) ^Fob = (b₂ ^Fob ) /\ (b₃ ^Fob )

proof end;

theorem Th48: :: FINTOPO2:48

for b₁ being non empty FMT_Space_Str
for b₂, b₃ being Subset of b₁ st b₁ is Fo_filled & ( for b₄ being Element of b₁ holds {b₄} in U_FMT b₄ ) holds
(b₂ ^Foi ) \/ (b₃ ^Foi ) = (b₂ \/ b₃) ^Foi

proof end;