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

theorem Th1: :: FIN_TOPO:1

for A being set
for f being FinSequence of bool A st ( for i being Nat st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being 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 Nat st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Nat st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Nat st i <= k & k <= j holds
f /. j = f /. k

proof end;

scheme :: FIN_TOPO:sch 1
MaxFinSeqEx{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> Subset of F₁(), F₄( Subset of F₁()) -> Subset of F₁() } :

ex f being FinSequence of bool F₁() st
( len f > 0 & f /. 1 = F₃() & ( for i being Nat st i > 0 & i < len f holds
f /. (i + 1) = F₄((f /. i)) ) & F₄((f /. (len f))) = f /. (len f) & ( for i, j being Nat st i > 0 & i < j & j <= len f holds
( f /. i c= F₂() & f /. i c< f /. j ) ) )

provided

A1: F₂() is finite and
A2: F₃() c= F₂() and
A3: for A being Subset of F₁() st A c= F₂() holds
( A c= F₄(A) & F₄(A) c= F₂() )

proof end;

registration

cluster non empty strict for RelStr ;

existence
ex b₁ being RelStr st
( not b₁ is empty & b₁ 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 b₁ being non empty RelStr st
( b₁ is finite & b₁ is filled & b₁ 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 :: 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 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 :: FIN_TOPO:def 14
IT = IT ^i ;

attr IT is closed means :: FIN_TOPO:def 15
IT = IT ^b ;

attr IT is connected means :: 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 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 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 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;