:: Finite Topological Spaces. Finite Topology Concepts and Neighbourhoods
:: by Hiroshi Imura and Masayoshi Eguchi
::
:: Received November 27, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem Th1: :: FIN_TOPO:1
for A being set
for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i &amp; i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st i <= j &amp; 1 <= i &amp; j <= len f holds
f /. i c= f /. j
proofend;

theorem Th2: :: FIN_TOPO:2
for A being set
for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i &amp; i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st 1 <= i &amp; j <= len f &amp; f /. j c= f /. i holds
for k being Element of NAT st i <= k &amp; k <= j holds
f /. j = f /. k
proofend;

scheme :: FIN_TOPO:sch 1
MaxFinSeqEx{ F1() ->  non empty set , F2() ->  Subset of F1(), F3() ->  Subset of F1(), F4( Subset of F1()) ->  Subset of F1() } :
 ex f being FinSequence of bool F1() st
( len f > 0 &amp; f /. 1 = F3() &amp; ( for i being Element of NAT st i > 0 &amp; i < len f holds
f /. (i + 1) = F4((f /. i)) ) &amp; F4((f /. (len f))) = f /. (len f) &amp; ( for i, j being Element of NAT st i > 0 &amp; i < j &amp; j <= len f holds
( f /. i c= F2() &amp; f /. i c< f /. j ) ) )
provided
A1: F2() is finite and
A2: F3() c= F2() and
A3: for A being Subset of F1() st A c= F2() holds
( A c= F4(A) &amp; F4(A) c= F2() )
proofend;

registration
cluster non empty strict for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is empty &amp; b1 is strict )
proofend;
end;

definition
let FT be RelStr ;
let x be Element of FT;
func U_FT x ->  Subset of FT equals :: FIN_TOPO:def 1
 Class ( the InternalRel of FT,x);
coherence
 Class ( the InternalRel of FT,x) is Subset of FT ;
end;

:: deftheorem  defines U_FT FIN_TOPO:def_1_:_
 for FT being RelStr
for x being Element of FT holds U_FT x = Class ( the InternalRel of FT,x);

definition
let x be set ;
let y be Subset of {x};
:: original:.-->
redefine funcx .--> y ->  Function of {x},(bool {x});
coherence
 x .--> y is Function of {x},(bool {x})
proofend;
end;

definition
let x be set ;
func SinglRel x ->  Relation of {x} equals :: FIN_TOPO:def 2
{[x,x]};
coherence
 {[x,x]} is Relation of {x}
proofend;
end;

:: deftheorem  defines SinglRel FIN_TOPO:def_2_:_
 for x being set holds SinglRel x = {[x,x]};

definition
func FT{0}  ->  strict RelStr  equals :: FIN_TOPO:def 3
 RelStr(# {0},(SinglRel 0) #);
coherence
 RelStr(# {0},(SinglRel 0) #) is strict RelStr ;
end;

:: deftheorem  defines FT{0} FIN_TOPO:def_3_:_
 FT{0} = RelStr(# {0},(SinglRel 0) #);

registration
cluster FT{0}  ->  non empty strict ;
coherence
 not FT{0} is empty ;
end;

notation
let IT be non empty RelStr ;
synonym  filled IT for  reflexive ;
end;

definition
let IT be non empty RelStr ;
redefine attr IT is reflexive  means :Def4: :: FIN_TOPO:def 4
 for x being Element of IT holds x in U_FT x;
compatibility
 ( IT is filled iff for x being Element of IT holds x in U_FT x )
proofend;
end;

:: deftheorem Def4 defines filled FIN_TOPO:def_4_:_
 for IT being non empty RelStr holds
( IT is filled iff for x being Element of IT holds x in U_FT x );

theorem Th3: :: FIN_TOPO:3
FT{0} is filled
proofend;

registration
cluster FT{0}  ->  finite strict filled ;
coherence
 ( FT{0} is filled &amp; FT{0} is finite ) by Th3;
end;

registration
cluster non empty finite strict filled for RelStr ;
existence
 ex b1 being non empty RelStr st
( b1 is finite &amp; b1 is filled &amp; b1 is strict ) by Th3;
end;

theorem :: FIN_TOPO:4
for FT being non empty filled RelStr holds  {  (U_FT x) where x is Element of FT : verum  }  is Cover of FT
proofend;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^delta  ->  Subset of FT equals :: FIN_TOPO:def 5
 {  x where x is Element of FT : ( U_FT x meets A &amp; U_FT x meets A ` )  }  ;
coherence
  {  x where x is Element of FT : ( U_FT x meets A &amp; U_FT x meets A ` )  }  is Subset of FT
proofend;
end;

:: deftheorem  defines ^delta FIN_TOPO:def_5_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^delta =  {  x where x is Element of FT : ( U_FT x meets A &amp; U_FT x meets A ` )  }  ;

theorem Th5: :: FIN_TOPO:5
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A &amp; U_FT x meets A ` ) )
proofend;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^deltai  ->  Subset of FT equals :: FIN_TOPO:def 6
A /\ (A ^delta);
coherence
 A /\ (A ^delta) is Subset of FT ;
funcA ^deltao  ->  Subset of FT equals :: FIN_TOPO:def 7
(A `) /\ (A ^delta);
coherence
 (A `) /\ (A ^delta) is Subset of FT ;
end;

:: deftheorem  defines ^deltai FIN_TOPO:def_6_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^deltai = A /\ (A ^delta);

:: deftheorem  defines ^deltao FIN_TOPO:def_7_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^deltao = (A `) /\ (A ^delta);

theorem :: FIN_TOPO:6
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^deltai) \/ (A ^deltao)
proofend;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^i  ->  Subset of FT equals :: FIN_TOPO:def 8
 {  x where x is Element of FT : U_FT x c= A  }  ;
coherence
  {  x where x is Element of FT : U_FT x c= A  }  is Subset of FT
proofend;
funcA ^b  ->  Subset of FT equals :: FIN_TOPO:def 9
 {  x where x is Element of FT : U_FT x meets A  }  ;
coherence
  {  x where x is Element of FT : U_FT x meets A  }  is Subset of FT
proofend;
funcA ^s  ->  Subset of FT equals :: FIN_TOPO:def 10
 {  x where x is Element of FT : ( x in A &amp; (U_FT x) \ {x} misses A )  }  ;
coherence
  {  x where x is Element of FT : ( x in A &amp; (U_FT x) \ {x} misses A )  }  is Subset of FT
proofend;
end;

:: deftheorem  defines ^i FIN_TOPO:def_8_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^i =  {  x where x is Element of FT : U_FT x c= A  }  ;

:: deftheorem  defines ^b FIN_TOPO:def_9_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^b =  {  x where x is Element of FT : U_FT x meets A  }  ;

:: deftheorem  defines ^s FIN_TOPO:def_10_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^s =  {  x where x is Element of FT : ( x in A &amp; (U_FT x) \ {x} misses A )  }  ;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^n  ->  Subset of FT equals :: FIN_TOPO:def 11
A \ (A ^s);
coherence
 A \ (A ^s) is Subset of FT ;
funcA ^f  ->  Subset of FT equals :: FIN_TOPO:def 12
 {  x where x is Element of FT : ex y being Element of FT st
( y in A &amp; x in U_FT y )  }  ;
coherence
  {  x where x is Element of FT : ex y being Element of FT st
( y in A &amp; x in U_FT y )  }  is Subset of FT
proofend;
end;

:: deftheorem  defines ^n FIN_TOPO:def_11_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^n = A \ (A ^s);

:: deftheorem  defines ^f FIN_TOPO:def_12_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^f =  {  x where x is Element of FT : ex y being Element of FT st
( y in A &amp; x in U_FT y )  }  ;

definition
let IT be non empty RelStr ;
attrIT is symmetric  means :Def13: :: FIN_TOPO:def 13
 for x, y being Element of IT st y in U_FT x holds
x in U_FT y;
end;

:: deftheorem Def13 defines symmetric FIN_TOPO:def_13_:_
 for IT being non empty RelStr holds
( IT is symmetric iff for x, y being Element of IT st y in U_FT x holds
x in U_FT y );

theorem Th7: :: FIN_TOPO:7
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )
proofend;

theorem Th8: :: FIN_TOPO:8
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
proofend;

theorem Th9: :: FIN_TOPO:9
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( x in A &amp; (U_FT x) \ {x} misses A ) )
proofend;

theorem :: FIN_TOPO:10
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A &amp; (U_FT x) \ {x} meets A ) )
proofend;

theorem Th11: :: FIN_TOPO:11
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
( y in A &amp; x in U_FT y ) )
proofend;

theorem :: FIN_TOPO:12
for FT being non empty RelStr holds
( FT is symmetric iff for A being Subset of FT holds A ^b = A ^f )
proofend;

definition
let FT be non empty RelStr ;
let IT be Subset of FT;
attrIT is open  means :Def14: :: FIN_TOPO:def 14
IT = IT ^i ;
attrIT is closed  means :Def15: :: FIN_TOPO:def 15
IT = IT ^b ;
attrIT is connected  means :Def16: :: FIN_TOPO:def 16
 for B, C being Subset of FT st IT = B \/ C &amp; B <> {} &amp; C <> {} &amp; B misses C holds
B ^b meets C;
end;

:: deftheorem Def14 defines open FIN_TOPO:def_14_:_
 for FT being non empty RelStr
for IT being Subset of FT holds
( IT is open iff IT = IT ^i );

:: deftheorem Def15 defines closed FIN_TOPO:def_15_:_
 for FT being non empty RelStr
for IT being Subset of FT holds
( IT is closed iff IT = IT ^b );

:: deftheorem Def16 defines connected FIN_TOPO:def_16_:_
 for FT being non empty RelStr
for IT being Subset of FT holds
( IT is connected iff for B, C being Subset of FT st IT = B \/ C &amp; B <> {} &amp; C <> {} &amp; B misses C holds
B ^b meets C );

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^fb  ->  Subset of FT equals :: FIN_TOPO:def 17
 meet  {  F where F is Subset of FT : ( A c= F &amp; F is closed )  }  ;
coherence
 meet  {  F where F is Subset of FT : ( A c= F &amp; F is closed )  }  is Subset of FT
proofend;
funcA ^fi  ->  Subset of FT equals :: FIN_TOPO:def 18
 union  {  F where F is Subset of FT : ( A c= F &amp; F is open )  }  ;
coherence
 union  {  F where F is Subset of FT : ( A c= F &amp; F is open )  }  is Subset of FT
proofend;
end;

:: deftheorem  defines ^fb FIN_TOPO:def_17_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^fb = meet  {  F where F is Subset of FT : ( A c= F &amp; F is closed )  }  ;

:: deftheorem  defines ^fi FIN_TOPO:def_18_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^fi = union  {  F where F is Subset of FT : ( A c= F &amp; F is open )  }  ;

theorem Th13: :: FIN_TOPO:13
for FT being non empty filled RelStr
for A being Subset of FT holds A c= A ^b
proofend;

theorem Th14: :: FIN_TOPO:14
for FT being non empty RelStr
for A, B being Subset of FT st A c= B holds
A ^b c= B ^b
proofend;

theorem :: FIN_TOPO:15
for FT being non empty finite filled RelStr
for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 &amp; S /. 1 = {x} &amp; ( for i being Element of NAT st i > 0 &amp; i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) &amp; A c= S /. (len S) ) )
proofend;

theorem Th16: :: FIN_TOPO:16
for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^i) ` = A ^b
proofend;

theorem Th17: :: FIN_TOPO:17
for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^b) ` = A ^i
proofend;

theorem :: FIN_TOPO:18
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) /\ ((A `) ^b)
proofend;

theorem :: FIN_TOPO:19
for FT being non empty RelStr
for A being Subset of FT holds (A `) ^delta = A ^delta
proofend;

theorem :: FIN_TOPO:20
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
proofend;

theorem :: FIN_TOPO:21
for FT being non empty RelStr
for A being Subset of FT st A ^s <> {} &amp; card A <> 1 holds
not A is connected
proofend;

theorem :: FIN_TOPO:22
for FT being non empty filled RelStr
for A being Subset of FT holds A ^i c= A
proofend;

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

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