:: Formal topological spaces
:: by Gang Liu , Yasushi Fuwa and Masayoshi Eguchi
::
:: Received October 13, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users


theorem :: FINTOPO2:1
for FT being non empty RelStr
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 RelStr
for A being Subset of FT holds A ^delta = (A ^b) /\ ((A ^i) `)
proof end;

theorem :: FINTOPO2:3
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) \ (A ^i)
proof end;

theorem :: FINTOPO2:4
for FT being non empty RelStr
for A being Subset of FT st A ` is open holds
A is closed
proof end;

theorem :: FINTOPO2:5
for FT being non empty RelStr
for A being Subset of FT st A ` is closed holds
A is open
proof end;

definition
let FT be non empty RelStr ;
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
coherence
( ( y in U_FT x & y in A implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ) implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;

:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :
for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( ( y in U_FT x & y in A implies P_1 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ) implies P_1 (x,y,A) = FALSE ) );

definition
let FT be non empty RelStr ;
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
coherence
( ( y in U_FT x & y in A ` implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ` ) implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;

:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :
for FT being non empty RelStr
for x, y being Element of FT
for A being Subset of FT holds
( ( y in U_FT x & y in A ` implies P_2 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ` ) implies P_2 (x,y,A) = FALSE ) );

theorem :: FINTOPO2:6
for FT being non empty RelStr
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;

theorem :: FINTOPO2:7
for FT being non empty RelStr
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;

theorem Th8: :: FINTOPO2:8
for FT being non empty RelStr
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 RelStr ;
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
coherence
( ( y in U_FT x implies TRUE is Element of BOOLEAN ) & ( not y in U_FT x implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;

:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :
for FT being non empty RelStr
for x, y being Element of FT holds
( ( y in U_FT x implies P_0 (x,y) = TRUE ) & ( not y in U_FT x implies P_0 (x,y) = FALSE ) );

theorem :: FINTOPO2:9
for FT being non empty RelStr
for x, y being Element of FT holds
( P_0 (x,y) = TRUE iff y in U_FT x ) by Def3;

theorem :: FINTOPO2:10
for FT being non empty RelStr
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 RelStr
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 RelStr ;
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
coherence
( ( x in A implies TRUE is Element of BOOLEAN ) & ( not x in A implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;

:: deftheorem Def4 defines P_A FINTOPO2:def 4 :
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( ( x in A implies P_A (x,A) = TRUE ) & ( not x in A implies P_A (x,A) = FALSE ) );

theorem :: FINTOPO2:12
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( P_A (x,A) = TRUE iff x in A ) by Def4;

theorem :: FINTOPO2:13
for FT being non empty RelStr
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 RelStr
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 RelStr ;
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
coherence
( ( x = y implies TRUE is Element of BOOLEAN ) & ( not x = y implies FALSE is Element of BOOLEAN ) );
consistency
for b1 being Element of BOOLEAN holds verum;
;
end;

:: deftheorem Def5 defines P_e FINTOPO2:def 5 :
for FT being non empty RelStr
for x, y being Element of FT holds
( ( x = y implies P_e (x,y) = TRUE ) & ( not x = y implies P_e (x,y) = FALSE ) );

theorem :: FINTOPO2:15
for FT being non empty RelStr
for x, y being Element of FT holds
( P_e (x,y) = TRUE iff x = y ) by Def5;

theorem :: FINTOPO2:16
for FT being non empty RelStr
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 RelStr
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 RelStr
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;

::
:: SECTION2: Formal Topological Spaces
::
definition
attr c1 is strict ;
struct FMT_Space_Str -> 1-sorted ;
aggr FMT_Space_Str(# carrier, BNbd #) -> FMT_Space_Str ;
sel BNbd c1 -> Function of the carrier of c1,(bool (bool the carrier of c1));
end;

registration
cluster non empty strict for FMT_Space_Str ;
existence
ex b1 being FMT_Space_Str st
( not b1 is empty & b1 is strict )
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
coherence
the BNbd of FMT . x is Subset-Family of FMT;
;
end;

:: deftheorem defines U_FMT FINTOPO2:def 6 :
for FMT being non empty FMT_Space_Str
for x being Element of FMT holds U_FMT x = the BNbd of FMT . x;

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
ex b1 being non empty strict FMT_Space_Str st
( the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )
proof end;
uniqueness
for b1, b2 being non empty strict FMT_Space_Str st the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) holds
b1 = b2
proof end;
end;

:: deftheorem defines NeighSp FINTOPO2:def 7 :
for T being non empty TopStruct
for b2 being non empty strict FMT_Space_Str holds
( b2 = NeighSp T iff ( the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) );

definition
let IT be non empty FMT_Space_Str ;
attr IT is Fo_filled means :: 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 defines Fo_filled FINTOPO2:def 8 :
for IT being non empty FMT_Space_Str holds
( IT is Fo_filled iff for x being Element of IT
for D being Subset of IT st D in U_FMT x holds
x in D );

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
{ 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 ` ) } is Subset of FMT
proof end;
end;

:: deftheorem defines ^Fodelta FINTOPO2:def 9 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = { 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 ` ) } ;

theorem Th19: :: FINTOPO2:19
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
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } is Subset of FMT
proof end;
end;

:: deftheorem defines ^Fob FINTOPO2:def 10 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fob = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A } ;

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 ^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
{ x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } is Subset of FMT
proof end;
end;

:: deftheorem defines ^Foi FINTOPO2:def 11 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Foi = { x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A ) } ;

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 ^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
{ 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 ) ) } is Subset of FMT
proof end;
end;

:: deftheorem defines ^Fos FINTOPO2:def 12 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fos = { 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 ) ) } ;

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 ^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
A \ (A ^Fos) is Subset of FMT ;
end;

:: deftheorem defines ^Fon FINTOPO2:def 13 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fon = A \ (A ^Fos);

theorem :: 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 ^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 Th24: :: FINTOPO2:24
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 Th25: :: FINTOPO2:25
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 Th26: :: FINTOPO2:26
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:27
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:28
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 Th29: :: FINTOPO2:29
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:30
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: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 ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi )
proof end;

theorem :: FINTOPO2:32
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:33
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:34
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 Th35: :: FINTOPO2:35
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 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 ^Foi c= A )
proof end;

theorem Th37: :: FINTOPO2:37
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A `) ^Fob) ` = A ^Foi
proof end;

theorem Th38: :: FINTOPO2:38
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A `) ^Foi) ` = A ^Fob
proof end;

theorem Th39: :: FINTOPO2:39
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:40
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:41
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A `) ^Fodelta
proof end;

theorem :: FINTOPO2:42
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
A /\ (A ^Fodelta) is Subset of FMT ;
func A ^Fodel_o -> Subset of FMT equals :: FINTOPO2:def 15
(A `) /\ (A ^Fodelta);
coherence
(A `) /\ (A ^Fodelta) is Subset of FMT ;
end;

:: deftheorem defines ^Fodel_i FINTOPO2:def 14 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodel_i = A /\ (A ^Fodelta);

:: deftheorem defines ^Fodel_o FINTOPO2:def 15 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodel_o = (A `) /\ (A ^Fodelta);

theorem :: FINTOPO2:43
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 :: FINTOPO2:def 16
G = G ^Foi ;
attr G is Fo_closed means :: FINTOPO2:def 17
G = G ^Fob ;
end;

:: deftheorem defines Fo_open FINTOPO2:def 16 :
for FMT being non empty FMT_Space_Str
for G being Subset of FMT holds
( G is Fo_open iff G = G ^Foi );

:: deftheorem defines Fo_closed FINTOPO2:def 17 :
for FMT being non empty FMT_Space_Str
for G being Subset of FMT holds
( G is Fo_closed iff G = G ^Fob );

theorem :: FINTOPO2:44
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:45
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:46
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: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 ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi
proof end;