Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### Formal Topological Spaces

by
Gang Liu,
Yasushi Fuwa, and
Masayoshi Eguchi

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

```environ

vocabulary FIN_TOPO, BOOLE, SUBSET_1, PRE_TOPC, MARGREL1, FUNCT_1, FINTOPO2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, FUNCT_1, FUNCT_2,
FIN_TOPO, PRE_TOPC, MARGREL1;
constructors DOMAIN_1, FIN_TOPO, PRE_TOPC, MARGREL1;
clusters SUBSET_1, RELSET_1, STRUCT_0, FIN_TOPO, PRE_TOPC, XBOOLE_0;
requirements SUBSET, BOOLE;

begin
::
::     SECTION1 : Some Useful Theorems on Finite Topological Spaces
::

reserve FT for non empty FT_Space_Str;
reserve A for Subset of FT;

theorem :: FINTOPO2:1
for FT being non empty FT_Space_Str,
A,B being Subset of FT holds
A c= B implies A^i c= B^i;

theorem :: FINTOPO2:2
A^delta = (A^b) /\ ((A^i)`);

theorem :: FINTOPO2:3
A^delta = A^b \ A^i;

theorem :: FINTOPO2:4
A` is open implies A is closed;

theorem :: FINTOPO2:5
A` is closed implies A is open;

definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
let A be Subset of FT;
func P_1(x,y,A) -> Element of BOOLEAN equals
:: FINTOPO2:def 1

TRUE if (y in U_FT x) & (y in A)
otherwise FALSE;
end;

definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
let A be Subset of FT;
func P_2(x,y,A) -> Element of BOOLEAN equals
:: FINTOPO2:def 2

TRUE if (y in U_FT x) & (y in A`)
otherwise FALSE;
end;

theorem :: FINTOPO2:6
for x,y be Element of FT, A be Subset of FT
holds P_1(x,y,A) = TRUE iff (y in U_FT x) & (y in A);

theorem :: FINTOPO2:7
for x,y be Element of FT, A be Subset of FT
holds P_2(x,y,A) = TRUE iff (y in U_FT x) & (y in A`);

theorem :: FINTOPO2:8
for x be Element of FT, A be 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;

definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
func P_0(x,y) -> Element of BOOLEAN equals
:: FINTOPO2:def 3

TRUE if y in U_FT x
otherwise FALSE;
end;

theorem :: FINTOPO2:9
for x,y be Element of FT holds
P_0(x,y)=TRUE iff y in U_FT x;

theorem :: FINTOPO2:10
for x be Element of FT, A be Subset of FT
holds x in A^i iff (for y be Element of FT holds
(P_0(x,y)=TRUE implies P_1(x,y,A)=TRUE));

theorem :: FINTOPO2:11
for x be Element of FT, A be Subset of FT
holds
x in A^b iff
ex y1 being Element of FT
st P_1(x,y1,A)=TRUE;

definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let A be Subset of FT;
func P_A(x,A) -> Element of BOOLEAN equals
:: FINTOPO2:def 4

TRUE if x in A
otherwise FALSE;
end;

theorem :: FINTOPO2:12
for x be Element of FT, A be Subset of FT
holds P_A(x,A)=TRUE iff x in A;

theorem :: FINTOPO2:13
for x be Element of FT, A be 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;

theorem :: FINTOPO2:14
for x be Element of FT, A be 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;

definition
let FT be non empty FT_Space_Str;
let x be Element of FT;
let y be Element of FT;
func P_e(x,y) -> Element of BOOLEAN equals
:: FINTOPO2:def 5

TRUE if x = y
otherwise FALSE;
end;

theorem :: FINTOPO2:15
for x,y be Element of FT
holds P_e(x,y)=TRUE iff x = y;

theorem :: FINTOPO2:16
for x be Element of FT, A be Subset of FT
holds
x in A^s iff
P_A(x,A)=TRUE &
not(ex y being Element of FT
st (P_1(x,y,A)=TRUE & P_e(x,y)=FALSE));

theorem :: FINTOPO2:17
for x be Element of FT, A be 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);

theorem :: FINTOPO2:18
for x be Element of FT, A be 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);

begin
::
::          SECTION2: Formal Topological Spaces
::

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

definition
cluster non empty strict FMT_Space_Str;
end;

reserve T for non empty TopStruct;
reserve FMT for non empty FMT_Space_Str;
reserve x, y for Element of FMT;

definition
let FMT;
let x be Element of FMT;
func U_FMT x -> Subset of bool the carrier of FMT equals
:: FINTOPO2:def 6

( the BNbd of FMT ).x;
end;

definition
let T;
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};
end;

reserve A, B, W, V for Subset of FMT;

definition let IT be non empty FMT_Space_Str;
attr IT is Fo_filled means
:: 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;

definition
let FMT;
let A;
func A^Fodelta -> Subset of FMT equals
:: FINTOPO2:def 9
{x:for W st W in U_FMT x holds W meets A & W meets A`};
end;

canceled;

theorem :: FINTOPO2:20
x in A^Fodelta iff for W st W in U_FMT x holds W meets A & W meets A`;

definition
let FMT,A;
func A^Fob -> Subset of FMT equals
:: FINTOPO2:def 10

{x:for W st W in U_FMT x holds W meets A};
end;

theorem :: FINTOPO2:21
x in A^Fob iff for W st W in U_FMT x holds W meets A;

definition
let FMT,A;
func A^Foi -> Subset of FMT equals
:: FINTOPO2:def 11

{x:ex V st V in U_FMT x & V c= A};
end;

theorem :: FINTOPO2:22
x in A^Foi iff ex V st V in U_FMT x & V c= A;

definition
let FMT,A;
func A^Fos -> Subset of FMT equals
:: FINTOPO2:def 12

{x:x in A & (ex V st V in U_FMT x & V \ {x} misses A)};
end;

theorem :: FINTOPO2:23
x in A^Fos iff x in A & (ex V st V in U_FMT x & V \ {x} misses A);

definition
let FMT,A;
func A^Fon -> Subset of FMT equals
:: FINTOPO2:def 13

A\(A^Fos);
end;

theorem :: FINTOPO2:24
x in A^Fon iff x in A & (for V st V in U_FMT x holds (V \ {x}) meets A);

theorem :: FINTOPO2:25
for FMT being non empty FMT_Space_Str,
A, B being Subset of FMT holds
A c= B implies A^Fob c= B^Fob;

theorem :: FINTOPO2:26
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT holds
A c= B implies A^Foi c= B^Foi;

theorem :: FINTOPO2:27
((A^Fob) \/ (B^Fob)) c= (A \/ B)^Fob;

theorem :: FINTOPO2:28
(A /\ B)^Fob c= (A^Fob) /\ (B^Fob);

theorem :: FINTOPO2:29
((A^Foi) \/ (B^Foi)) c= (A \/ B)^Foi;

theorem :: FINTOPO2:30
(A /\ B)^Foi c= ((A^Foi) /\ (B^Foi));

theorem :: FINTOPO2:31
for FMT being non empty FMT_Space_Str holds
(for x being Element of FMT,
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));

theorem :: FINTOPO2:32
for FMT being non empty FMT_Space_Str holds
(for x being Element of FMT,
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;

theorem :: FINTOPO2:33
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT holds
(for x being Element of FMT,
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))))
implies (A \/ B)^Fodelta c= ((A^Fodelta) \/ (B^Fodelta));

theorem :: FINTOPO2:34
for FMT being non empty FMT_Space_Str st FMT is Fo_filled
holds (for A,B being Subset of FMT holds
(A \/ B)^Fodelta = ((A^Fodelta) \/ (B^Fodelta)))
implies (for x being Element of FMT,
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)));

theorem :: FINTOPO2:35
for x be Element of FMT, A being Subset of
FMT
holds x in A^Fos iff x in A & not x in (A\{x})^Fob;

theorem :: FINTOPO2:36
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;

theorem :: FINTOPO2:37
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;

theorem :: FINTOPO2:38
((A`)^Fob)` =A^Foi;

theorem :: FINTOPO2:39
((A`)^Foi)` = A^Fob;

theorem :: FINTOPO2:40
A^Fodelta = (A^Fob) /\ ((A`)^Fob);

theorem :: FINTOPO2:41
A^Fodelta = (A^Fob) /\ (A^Foi)`;

theorem :: FINTOPO2:42
A^Fodelta = (A`)^Fodelta;

theorem :: FINTOPO2:43
A^Fodelta = A^Fob \ A^Foi;

definition
let FMT;
let A;
func A^Fodel_i -> Subset of FMT equals
:: FINTOPO2:def 14

A /\ (A^Fodelta);

func A^Fodel_o -> Subset of FMT equals
:: FINTOPO2:def 15

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

theorem :: FINTOPO2:44
A^Fodelta = (A^Fodel_i) \/ (A^Fodel_o);

definition let FMT;
let G be Subset of FMT;
attr G is Fo_open means
:: FINTOPO2:def 16

G = G^Foi;

attr G is Fo_closed means
:: FINTOPO2:def 17

G = G^Fob;
end;

theorem :: FINTOPO2:45
A` is Fo_open implies A is Fo_closed;

theorem :: FINTOPO2:46
A` is Fo_closed implies A is Fo_open;

theorem :: FINTOPO2:47
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT st FMT is Fo_filled
holds (for x being Element of FMT holds
{x} in U_FMT x )
implies (A /\ B)^Fob = ((A^Fob) /\ (B^Fob));

theorem :: FINTOPO2:48
for FMT being non empty FMT_Space_Str,
A,B being Subset of FMT st FMT is Fo_filled
holds (for x being Element of FMT holds
{x} in U_FMT x )
implies (A^Foi) \/ (B^Foi) = (A \/ B)^Foi;

```