:: 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 & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
proof end;

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 & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
proof end;

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 & f /. 1 = F3() & ( for i being Element of NAT st i > 0 & i < len f holds
f /. (i + 1) = F4((f /. i)) ) & F4((f /. (len f))) = f /. (len f) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len f holds
( f /. i c= F2() & 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) & F4(A) c= F2() )
proof end;

registration
cluster non empty strict for RelStr ;
existence
ex b1 being RelStr st
( not b1 is empty & b1 is strict )
proof end;
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 func x .--> y -> Function of {x},(bool {x});
coherence
x .--> y is Function of {x},(bool {x})
proof end;
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}
proof end;
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 )
proof end;
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
proof end;

registration
cluster FT{0} -> finite strict filled ;
coherence
( FT{0} is filled & 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 & b1 is filled & 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
proof end;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
func A ^delta -> Subset of FT equals :: FIN_TOPO:def 5
 { x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } ;
coherence
{ x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` ) } is Subset of FT
proof end;
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 & 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 & U_FT x meets A ` ) )
proof end;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
func A ^deltai -> Subset of FT equals :: FIN_TOPO:def 6
A /\ (A ^delta);
coherence
A /\ (A ^delta) is Subset of FT ;
func A ^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)
proof end;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
func A ^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
proof end;
func A ^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
proof end;
func A ^s -> Subset of FT equals :: FIN_TOPO:def 10
 { x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } ;
coherence
{ x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A ) } is Subset of FT
proof end;
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 & (U_FT x) \ {x} misses A ) } ;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
func A ^n -> Subset of FT equals :: FIN_TOPO:def 11
A \ (A ^s);
coherence
A \ (A ^s) is Subset of FT ;
func A ^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 & x in U_FT y ) } ;
coherence
{ x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y ) } is Subset of FT
proof end;
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 & x in U_FT y ) } ;

definition
let IT be non empty RelStr ;
attr IT 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 )
proof end;

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 )
proof end;

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 & (U_FT x) \ {x} misses A ) )
proof end;

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 & (U_FT x) \ {x} meets A ) )
proof end;

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 & x in U_FT y ) )
proof end;

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 )
proof end;

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

definition
let FT be non empty RelStr ;
let A be Subset of FT;
func A ^fb -> Subset of FT equals :: FIN_TOPO:def 17
 meet { F where F is Subset of FT : ( A c= F & F is closed ) } ;
coherence
meet { F where F is Subset of FT : ( A c= F & F is closed ) } is Subset of FT
proof end;
func A ^fi -> Subset of FT equals :: FIN_TOPO:def 18
 union { F where F is Subset of FT : ( A c= F & F is open ) } ;
coherence
union { F where F is Subset of FT : ( A c= F & F is open ) } is Subset of FT
proof end;
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 & 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 & 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
proof end;

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
proof end;

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 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
proof end;

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

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

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

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

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
proof end;

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

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

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

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