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


begin

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
proofend;

theorem Th2: :: FINTOPO2:2
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) /\ ((A ^i) `)
proofend;

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

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

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

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 ) )
proofend;

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 )
proofend;

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 )
proofend;

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 ) )
proofend;

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 ) )
proofend;

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 ) ) ) )
proofend;

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 ) ) )
proofend;

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 ) )
proofend;

begin

::
:: SECTION2: Formal Topological Spaces
::
definition
attrc1 is strict ;
struct FMT_Space_Str  ->  1-sorted ;
aggrFMT_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 )
proofend;
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 )  }  ) )
proofend;
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
proofend;
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 ;
attrIT 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_:_
 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;
funcA ^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
proofend;
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 ` ) )
proofend;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^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
proofend;
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 )
proofend;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^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
proofend;
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 ) )
proofend;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^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
proofend;
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 ) ) )
proofend;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^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 ) ) )
proofend;

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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
proofend;

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)
proofend;

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) )
proofend;

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 )
proofend;

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)
proofend;

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 )
proofend;

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 ) )
proofend;

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 )
proofend;

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 )
proofend;

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

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

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)
proofend;

theorem :: FINTOPO2:40
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)
proofend;

theorem :: FINTOPO2:41
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A `) ^Fodelta
proofend;

theorem :: FINTOPO2:42
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob) \ (A ^Foi)
proofend;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
funcA ^Fodel_i  ->  Subset of FMT equals :: FINTOPO2:def 14
A /\ (A ^Fodelta);
coherence
 A /\ (A ^Fodelta) is Subset of FMT ;
funcA ^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)
proofend;

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

:: deftheorem Def16 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 Def17 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
proofend;

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
proofend;

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)
proofend;

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
proofend;