Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Finite Topological Spaces

by
Hiroshi Imura, and
Masayoshi Eguchi

MML identifier: FIN_TOPO
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, FINSET_1, BOOLE, ZFMISC_1, FUNCT_1, RELAT_1, ABSVALUE,
ARYTM_1, CAT_1, FUNCT_2, SUBSET_1, PRE_TOPC, TARSKI, RELAT_2, SETFAM_1,
CARD_1, FIN_TOPO, HAHNBAN, FINSEQ_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, FINSET_1, NAT_1, SETFAM_1, STRUCT_0, RELSET_1, RELAT_1, FUNCT_1,
FUNCT_2, CQC_LANG, DOMAIN_1, GROUP_1, FINSEQ_1, FINSEQ_4, CARD_1;
constructors NAT_1, CQC_LANG, DOMAIN_1, GROUP_1, FINSEQ_4, MEMBERED, XBOOLE_0;
clusters SUBSET_1, INT_1, RELSET_1, STRUCT_0, CQC_LANG, FINSEQ_1, NAT_1,
XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

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

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

theorem :: FIN_TOPO:3
for F being set st
F is finite &
F <> {} & F is c=-linear
ex m being set st m in F &
for C being set st C in F holds C c= m;

canceled;

theorem :: FIN_TOPO:5
for f being Function st
(for i being Nat holds f.i c= f.(i+1))
for i, j being Nat st
i <= j holds f.i c= f.j;

scheme MaxFinSeqEx {X() -> non empty set,
A() -> Subset of X(),
B() -> Subset of X(),
F(Subset of X()) -> Subset of X()}:
ex f being FinSequence of bool X() st
len f > 0 &
f/.1=B() &
(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= A() & f/.i c< f/.j)
provided
A() is finite and
B() c= A() and
for A being Subset of X() st A c= A() holds A c= F(A) & F(A) c= A();

definition
struct ( 1-sorted ) FT_Space_Str
(# carrier -> set,
Nbd -> Function of the carrier, bool the carrier #);
end;

definition
cluster non empty strict FT_Space_Str;
end;

reserve FT for non empty FT_Space_Str;
reserve x, y, z for Element of FT;

definition
let FT be non empty FT_Space_Str;
let x be Element of FT;

func U_FT x -> Subset of FT equals
:: FIN_TOPO:def 1

( the Nbd of FT ).x;
end;

definition
let x be set,
y be Subset of {x};

redefine func x.-->y -> Function of {x}, bool {x};
end;

definition
func FT{0} -> strict FT_Space_Str equals
:: FIN_TOPO:def 2

FT_Space_Str (#{0},0.-->[#]{0}#);
end;

definition
cluster FT{0} -> non empty;
end;

definition let IT be non empty FT_Space_Str;
attr IT is filled means
:: FIN_TOPO:def 3

for x being Element of IT holds x in U_FT x;
end;

canceled;

theorem :: FIN_TOPO:7
FT{0} is filled;

theorem :: FIN_TOPO:8
FT{0} is finite;

definition
cluster finite filled strict (non empty FT_Space_Str);
end;

definition
let T be 1-sorted,
F be set;
canceled;

pred F is_a_cover_of T means
:: FIN_TOPO:def 5
the carrier of T c= union F;
end;

theorem :: FIN_TOPO:9
for FT being filled (non empty FT_Space_Str) holds
{U_FT x where x is Element of FT : not contradiction}
is_a_cover_of FT;

reserve A for Subset of FT;

definition
let FT;
let A be Subset of FT;

func A^delta -> Subset of FT equals
:: FIN_TOPO:def 6

{x:U_FT x meets A & U_FT x meets A` };
end;

theorem :: FIN_TOPO:10
x in A^delta iff U_FT x meets A & U_FT x meets A`;

definition let FT;
let A be Subset of FT;
func A^deltai -> Subset of FT equals
:: FIN_TOPO:def 7

A /\ (A^delta);

func A^deltao -> Subset of FT equals
:: FIN_TOPO:def 8

A` /\ (A^delta);
end;

theorem :: FIN_TOPO:11
A^delta = A^deltai \/ A^deltao;

definition let FT;
let A be Subset of FT;
func A^i -> Subset of FT equals
:: FIN_TOPO:def 9
{x:U_FT x c= A};

func A^b -> Subset of FT equals
:: FIN_TOPO:def 10

{x:U_FT x meets A};

func A^s -> Subset of FT equals
:: FIN_TOPO:def 11

{x:x in A & U_FT x \ {x} misses A };
end;

definition
let FT;
let A be Subset of FT;

func A^n -> Subset of FT equals
:: FIN_TOPO:def 12

A \ A^s;

func A^f -> Subset of FT equals
:: FIN_TOPO:def 13

{x:ex y st y in A & x in U_FT y};
end;

definition let IT be non empty FT_Space_Str;
attr IT is symmetric means
:: FIN_TOPO:def 14

for x, y being Element of IT holds
y in U_FT x implies x in U_FT y;
end;

theorem :: FIN_TOPO:12
x in A^i iff U_FT x c= A;

theorem :: FIN_TOPO:13
x in A^b iff U_FT x meets A;

theorem :: FIN_TOPO:14
x in A^s iff x in A & U_FT x \ {x} misses A;

theorem :: FIN_TOPO:15
x in A^n iff x in A & U_FT x \ {x} meets A;

theorem :: FIN_TOPO:16
x in A^f iff ex y st y in A & x in U_FT y;

theorem :: FIN_TOPO:17
FT is symmetric iff for A holds A^b = A^f;

reserve F for Subset of FT;

definition let FT;
let IT be Subset of FT;
attr IT is open means
:: FIN_TOPO:def 15
IT = IT^i;

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

attr IT is connected means
:: FIN_TOPO:def 17
for B,C being Subset of FT st
IT = B \/ C & B <> {} & C <> {} & B misses C holds B^b meets C;
end;

definition let FT; let A be Subset of FT;
func A^fb -> Subset of FT equals
:: FIN_TOPO:def 18
meet{F:A c= F & F is closed};

func A^fi -> Subset of FT equals
:: FIN_TOPO:def 19
union{F:A c= F & F is open};
end;

theorem :: FIN_TOPO:18
for FT being filled (non empty FT_Space_Str),
A being Subset of FT holds
A c= A^b;

theorem :: FIN_TOPO:19
for FT being non empty FT_Space_Str,
A, B being Subset of FT holds
A c= B implies A^b c= B^b;

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

theorem :: FIN_TOPO:21
for E being non empty set,
A being Subset of E,
x being Element of E holds
x in A` iff not x in A;

theorem :: FIN_TOPO:22
((A`)^i)` = A^b;

theorem :: FIN_TOPO:23
((A`)^b)` = A^i;

theorem :: FIN_TOPO:24
A^delta = (A^b) /\ ((A`)^b);

theorem :: FIN_TOPO:25
(A`)^delta = A^delta;

theorem :: FIN_TOPO:26
x in A^s implies not x in (A \ {x})^b;

theorem :: FIN_TOPO:27
A^s <> {} & Card A <> 1 implies A is not connected;

theorem :: FIN_TOPO:28
for FT being filled (non empty FT_Space_Str),
A being Subset of FT holds
A^i c= A;

theorem :: FIN_TOPO:29
for E being set,
A, B being Subset of E holds
A = B iff A` = B`;

theorem :: FIN_TOPO:30
A is open implies A` is closed;

theorem :: FIN_TOPO:31
A is closed implies A` is open;
```