:: FINTOPO2 semantic presentation

theorem :: FINTOPO2:1

for FT being non empty FT_Space_Str
for A, B being Subset of FT st A c= B holds
A ^i c= B ^i

proof end;

theorem Th2: :: FINTOPO2:2

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

proof end;

theorem :: FINTOPO2:3

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

proof end;

theorem :: FINTOPO2:4

for FT being non empty FT_Space_Str
for A being Subset of FT st A ` is open holds
A is closed

proof end;

theorem :: FINTOPO2:5

for FT being non empty FT_Space_Str
for A being Subset of FT st A ` is closed holds
A is open

proof end;

definition

let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
let A be Subset of FT;
func P_1 x,y,A -> Element of BOOLEAN equals :Def1: :: FINTOPO2:def 1
TRUE if ( y in U_FT x & y in A )
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :

definition

let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
let A be Subset of FT;
func P_2 x,y,A -> Element of BOOLEAN equals :Def2: :: FINTOPO2:def 2
TRUE if ( y in U_FT x & y in A ` )
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :

theorem :: FINTOPO2:6

for FT being non empty FT_Space_Str
for x, y being Element of FT
for A being Subset of FT holds
( P_1 x,y,A = TRUE iff ( y in U_FT x & y in A ) ) by Def1, MARGREL1:38;

theorem :: FINTOPO2:7

for FT being non empty FT_Space_Str
for x, y being Element of FT
for A being Subset of FT holds
( P_2 x,y,A = TRUE iff ( y in U_FT x & y in A ` ) ) by Def2, MARGREL1:38;

theorem Th8: :: FINTOPO2:8

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) )

proof end;

definition

let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
func P_0 x,y -> Element of BOOLEAN equals :Def3: :: FINTOPO2:def 3
TRUE if y in U_FT x
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :

theorem :: FINTOPO2:9

for FT being non empty FT_Space_Str
for x, y being Element of FT holds
( P_0 x,y = TRUE iff y in U_FT x ) by Def3, MARGREL1:38;

theorem :: FINTOPO2:10

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff for y being Element of FT st P_0 x,y = TRUE holds
P_1 x,y,A = TRUE )

proof end;

theorem :: FINTOPO2:11

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff ex y1 being Element of FT st P_1 x,y1,A = TRUE )

proof end;

definition

let FT be non empty FT_Space_Str ;
let x be Element of FT;
let A be Subset of FT;
func P_A x,A -> Element of BOOLEAN equals :Def4: :: FINTOPO2:def 4
TRUE if x in A
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def4 defines P_A FINTOPO2:def 4 :

theorem :: FINTOPO2:12

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( P_A x,A = TRUE iff x in A ) by Def4, MARGREL1:38;

theorem :: FINTOPO2:13

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^deltai iff ( ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = TRUE ) )

proof end;

theorem :: FINTOPO2:14

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE ) )

proof end;

definition

let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
func P_e x,y -> Element of BOOLEAN equals :Def5: :: FINTOPO2:def 5
TRUE if x = y
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def5 defines P_e FINTOPO2:def 5 :

theorem :: FINTOPO2:15

for FT being non empty FT_Space_Str
for x, y being Element of FT holds
( P_e x,y = TRUE iff x = y ) by Def5, MARGREL1:38;

theorem :: FINTOPO2:16

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) )

proof end;

theorem :: FINTOPO2:17

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( P_A x,A = TRUE & ex y being Element of FT st
( P_1 x,y,A = TRUE & P_e x,y = FALSE ) ) )

proof end;

theorem :: FINTOPO2:18

for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) )

proof end;

definition

attr c₁ 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 c₁, bool (bool the carrier of c₁);

end;

registration

cluster non empty strict FMT_Space_Str ;
existence

proof end;

end;

definition

let FMT be non empty FMT_Space_Str ;
let x be Element of FMT;
func U_FMT x -> Subset-Family of FMT equals :: FINTOPO2:def 6
the BNbd of FMT . x;
correctness ;

end;

:: deftheorem defines U_FMT FINTOPO2:def 6 :

definition

let T be non empty TopStruct ;
func NeighSp T -> non empty strict FMT_Space_Str means :: FINTOPO2:def 7
( the carrier of it = the carrier of T & ( for x being Point of it holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines NeighSp FINTOPO2:def 7 :

definition

let IT be non empty FMT_Space_Str ;
attr IT is Fo_filled means :Def8: :: FINTOPO2:def 8
for x being Element of IT
for D being Subset of IT st D in U_FMT x holds
x in D;

end;

:: deftheorem Def8 defines Fo_filled FINTOPO2:def 8 :

definition

let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fodelta -> Subset of FMT equals :: FINTOPO2:def 9
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) } ;
coherence

proof end;

end;

:: deftheorem defines ^Fodelta FINTOPO2:def 9 :

theorem :: FINTOPO2:19

canceled;

theorem Th20: :: FINTOPO2:20

for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )

proof end;

definition

let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fob -> Subset of FMT equals :: FINTOPO2:def 10
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } ;
coherence

proof end;

end;

:: deftheorem defines ^Fob FINTOPO2:def 10 :

theorem Th21: :: FINTOPO2:21

for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds
W meets A )

proof end;

definition

let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Foi -> Subset of FMT equals :: FINTOPO2:def 11
{ x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } ;
coherence

proof end;

end;

:: deftheorem defines ^Foi FINTOPO2:def 11 :

theorem Th22: :: FINTOPO2:22

for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Foi iff ex V being Subset of FMT st
( V in U_FMT x & V c= A ) )

proof end;

definition

let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fos -> Subset of FMT equals :: FINTOPO2:def 12
{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) } ;
coherence

proof end;

end;

:: deftheorem defines ^Fos FINTOPO2:def 12 :

theorem Th23: :: FINTOPO2:23

for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) )

proof end;

definition

let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fon -> Subset of FMT equals :: FINTOPO2:def 13
A \ (A ^Fos );
coherence ;

end;

:: deftheorem defines ^Fon FINTOPO2:def 13 :

theorem :: FINTOPO2:24

for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) )

proof end;

theorem Th25: :: FINTOPO2:25

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st A c= B holds
A ^Fob c= B ^Fob

proof end;

theorem Th26: :: FINTOPO2:26

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st A c= B holds
A ^Foi c= B ^Foi

proof end;

theorem Th27: :: FINTOPO2:27

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A ^Fob ) \/ (B ^Fob ) c= (A \/ B) ^Fob

proof end;

theorem :: FINTOPO2:28

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob ) /\ (B ^Fob )

proof end;

theorem :: FINTOPO2:29

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A ^Foi ) \/ (B ^Foi ) c= (A \/ B) ^Foi

proof end;

theorem Th30: :: FINTOPO2:30

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi ) /\ (B ^Foi )

proof end;

theorem :: FINTOPO2:31

for FMT being non empty FMT_Space_Str holds
( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob ) \/ (B ^Fob ) )

proof end;

theorem :: FINTOPO2:32

proof end;

theorem :: FINTOPO2:33

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) holds
(A \/ B) ^Fodelta c= (A ^Fodelta ) \/ (B ^Fodelta )

proof end;

theorem :: FINTOPO2:34

for FMT being non empty FMT_Space_Str st FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta ) \/ (B ^Fodelta ) ) holds
for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 )

proof end;

theorem :: FINTOPO2:35

for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )

proof end;

theorem Th36: :: FINTOPO2:36

for FMT being non empty FMT_Space_Str holds
( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob )

proof end;

theorem Th37: :: FINTOPO2:37

for FMT being non empty FMT_Space_Str holds
( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A )

proof end;

theorem Th38: :: FINTOPO2:38

for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A ` ) ^Fob ) ` = A ^Foi

proof end;

theorem Th39: :: FINTOPO2:39

for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A ` ) ^Foi ) ` = A ^Fob

proof end;

theorem Th40: :: FINTOPO2:40

for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) /\ ((A ` ) ^Fob )

proof end;

theorem :: FINTOPO2:41

for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) /\ ((A ^Foi ) ` )

proof end;

theorem :: FINTOPO2:42

for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ` ) ^Fodelta

proof end;

theorem :: FINTOPO2:43

for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) \ (A ^Foi )

proof end;

definition

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

end;

:: deftheorem defines ^Fodel_i FINTOPO2:def 14 :

:: deftheorem defines ^Fodel_o FINTOPO2:def 15 :

theorem :: FINTOPO2:44

for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i ) \/ (A ^Fodel_o )

proof end;

definition

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

end;

:: deftheorem Def16 defines Fo_open FINTOPO2:def 16 :

:: deftheorem Def17 defines Fo_closed FINTOPO2:def 17 :

theorem :: FINTOPO2:45

for FMT being non empty FMT_Space_Str
for A being Subset of FMT st A ` is Fo_open holds
A is Fo_closed

proof end;

theorem :: FINTOPO2:46

for FMT being non empty FMT_Space_Str
for A being Subset of FMT st A ` is Fo_closed holds
A is Fo_open

proof end;

theorem :: FINTOPO2:47

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A /\ B) ^Fob = (A ^Fob ) /\ (B ^Fob )

proof end;

theorem :: FINTOPO2:48

for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A ^Foi ) \/ (B ^Foi ) = (A \/ B) ^Foi

proof end;