Copyright (c) 1989 Association of Mizar Users
environ
vocabulary SETFAM_1, TARSKI, BOOLE, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL2,
PRE_TOPC;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_2, SETFAM_1,
STRUCT_0;
constructors STRUCT_0, FUNCT_2, MEMBERED;
clusters STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1;
requirements BOOLE, SUBSET;
definitions TARSKI, STRUCT_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1, STRUCT_0, XBOOLE_0, XBOOLE_1;
schemes SETFAM_1, XBOOLE_0;
begin
definition
struct(1-sorted) TopStruct (# carrier -> set,
topology -> Subset-Family of the carrier #);
end;
reserve T for TopStruct;
::
:: The topological space
::
definition let IT be TopStruct;
attr IT is TopSpace-like means
:Def1:
the carrier of IT in the topology of IT &
(for a being Subset-Family of IT
st a c= the topology of IT
holds union a in the topology of IT) &
(for a,b being Subset of IT st
a in the topology of IT & b in the topology of IT
holds a /\ b in the topology of IT);
end;
definition
cluster non empty strict TopSpace-like TopStruct;
existence
proof
now
take X={{}};
set T={{},X};
T c= bool X
proof
let x be set;
assume x in T;
then x= {} or x = X by TARSKI:def 2;
then x c= X by XBOOLE_1:2;
hence thesis;
end;
then reconsider T as Subset-Family of X by SETFAM_1:def 7;
take T;
set Y=TopStruct(#X,T#);
thus the carrier of Y in the topology of Y by TARSKI:def 2;
thus for a being Subset-Family of Y st
a c= the topology of Y holds union a in the topology of Y
proof
let a be Subset-Family of Y; assume
a c= the topology of Y;
then a={} or a={{}} or a={X} or a={{},X} by ZFMISC_1:42;
then union a={} or union a=X or union a = {} \/ X by ZFMISC_1:2,31,93
;
hence thesis by TARSKI:def 2;
end;
let a,b be Subset of Y such that
A1:a in the topology of Y and A2:b in the topology of Y;
(a={} or a=X) & (b={} or b=X) by A1,A2,TARSKI:def 2;
hence a /\ b in the topology of Y by TARSKI:def 2;
end;
then consider X being non empty set, T being Subset-Family of X such that
A3: the carrier of TopStruct(#X,T#) in the topology of TopStruct(#X,T#) &
(for a being Subset-Family of TopStruct(#X,T#)
st a c= the topology of TopStruct(#X,T#)
holds union a in the topology of TopStruct(#X,T#)) &
(for a,b being Subset of TopStruct(#X,T#) st
a in the topology of TopStruct(#X,T#) &
b in the topology of TopStruct(#X,T#)
holds a /\ b in the topology of TopStruct(#X,T#));
take TopStruct(#X,T#);
thus TopStruct(#X,T#) is non empty by STRUCT_0:def 1;
thus thesis by A3,Def1;
end;
end;
definition
mode TopSpace is TopSpace-like TopStruct;
end;
definition let S be 1-sorted;
mode Point of S is Element of S;
end;
reserve GX for TopSpace;
canceled 4;
theorem Th5:
{} in the topology of GX
proof
{} c= bool the carrier of GX by XBOOLE_1:2;
then reconsider A = {} as Subset-Family of GX by SETFAM_1:def
7;
A c= the topology of GX & union A = {} by XBOOLE_1:2,ZFMISC_1:2;
hence thesis by Def1;
end;
definition let T be 1-sorted;
func {}T -> Subset of T equals
:Def2: {};
coherence
proof
{} = {}the carrier of T;
hence thesis;
end;
func [#]T -> Subset of T equals
:Def3: the carrier of T;
coherence
proof
the carrier of T = [#] the carrier of T by SUBSET_1:def 4;
hence thesis;
end;
end;
definition let T be 1-sorted;
cluster {}T -> empty;
coherence by Def2;
end;
canceled 6;
theorem
for T being 1-sorted holds [#]T = the carrier of T by Def3;
definition let T be non empty 1-sorted;
cluster [#]T -> non empty;
coherence by Def3;
end;
theorem Th13:
for T being non empty 1-sorted, p being Point of T holds p in [#]T
proof let T be non empty 1-sorted, p be Point of T;
p in the carrier of T;
hence p in [#]T by Def3;
end;
theorem Th14:
for T being 1-sorted, P being Subset of T holds P c= [#]T
proof let T be 1-sorted, P be Subset of T;
the carrier of T = [#]T by Def3;
hence P c= [#]T;
end;
theorem Th15:
for T being 1-sorted, P being Subset of T holds P /\ [#]T = P
proof let T be 1-sorted, P be Subset of T;
P /\ the carrier of T = P by XBOOLE_1:28;
hence P /\ [#]T = P by Def3;
end;
theorem Th16:
for T being 1-sorted
for A being set st A c= [#]T holds A is Subset of T by Def3;
theorem Th17:
for T being 1-sorted, P being Subset of T holds P` = [#]T \ P
proof let T be 1-sorted, P be Subset of T;
P` = (the carrier of T) \ P by SUBSET_1:def 5;
hence thesis by Def3;
end;
theorem
for T being 1-sorted, P being Subset of T holds P \/ P` =
[#]
T
proof let T be 1-sorted, P be Subset of T;
P \/ P` = [#] the carrier of T by SUBSET_1:25
.= the carrier of T by SUBSET_1:def 4;
hence thesis by Def3;
end;
theorem
for T being 1-sorted, P,Q being Subset of T
holds P c= Q iff Q` c= P` by SUBSET_1:31;
theorem
for T being 1-sorted, P being Subset of T
holds P = P``;
theorem Th21:
for T being 1-sorted
for P,Q being Subset of T holds P c= Q` iff P misses Q by SUBSET_1:43;
theorem Th22:
for T being 1-sorted, P being Subset of T
holds [#]T \ ([#]T \ P) = P
proof let T be 1-sorted, P be Subset of T;
[#]T \ ([#]T \ P) = (the carrier of T) \ ([#]T \ P) by Def3
.= (the carrier of T) \ ((the carrier of T) \ P) by Def3
.= (the carrier of T) /\ P by XBOOLE_1:48
.= P /\ [#]T by Def3;
hence thesis by Th15;
end;
theorem Th23:
for T being 1-sorted, P being Subset of T
holds P <> [#]T iff [#]T \ P <> {}
proof let T be 1-sorted, P be Subset of T;
now
assume A1:P <> [#]T & [#]T \ P = {};
then [#]T c= P & P c= [#]T by Th14,XBOOLE_1:37;
hence contradiction by A1,XBOOLE_0:def 10;
end;
hence thesis by XBOOLE_1:37;
end;
theorem
for T being 1-sorted, P,Q being Subset of T st [#]T \ P = Q
holds [#]T = P \/ Q
proof let T be 1-sorted, P,Q be Subset of T;
assume ([#]T) \ P = Q;
then (the carrier of T) \ P = Q by Def3;
then P \/ Q = the carrier of T by XBOOLE_1:45;
hence [#]T = P \/ Q by Def3;
end;
theorem
for T being 1-sorted, P,Q being Subset of T
st [#]T = P \/ Q & P misses Q
holds Q = [#]T \ P
proof let T be 1-sorted, P,Q be Subset of T;
assume A1:[#]T = P \/ Q & P misses Q;
then [#]T \ P = Q \ P by XBOOLE_1:40
.= Q by A1,XBOOLE_1:83;
hence Q = [#]T \ P;
end;
theorem
for T being 1-sorted, P being Subset of T holds P misses P`
by SUBSET_1:26;
theorem
for T being 1-sorted holds [#]T = ({}T)`
proof let T be 1-sorted;
[#]T = the carrier of T by Def3 .= [#]the carrier of T by SUBSET_1:def 4;
then [#]T = ({} the carrier of T)` &
{} the carrier of T = {} by SUBSET_1:22;
hence [#]T = ({}T)`;
end;
definition let T be TopStruct, P be Subset of T;
canceled;
attr P is open means :Def5: P in the topology of T;
end;
definition let T be TopStruct, P be Subset of T;
attr P is closed means :Def6: [#]T \ P is open;
end;
definition let T be 1-sorted, F be Subset-Family of T;
redefine func union F -> Subset of T;
coherence
proof
thus union F is Subset of T;
end;
end;
definition let T be 1-sorted, F be Subset-Family of T;
redefine func meet F -> Subset of T;
coherence
proof
thus meet F is Subset of T;
end;
end;
definition let T be 1-sorted, F be Subset-Family of T;
canceled;
pred F is_a_cover_of T means
[#]T = union F;
end;
definition let T be TopStruct;
mode SubSpace of T -> TopStruct means :Def9:
[#]it c= [#]T &
for P being Subset of it
holds P in the topology of it iff
ex Q being Subset of T st Q in the topology of T &
P = Q /\ [#]it;
existence
proof take T;
thus [#]T c= [#]T;
let P be Subset of T;
hereby assume
A1: P in the topology of T;
take Q = P;
thus Q in the topology of T by A1;
thus P = Q /\ [#]T by Th15;
end;
given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]T;
thus thesis by A2,Th15;
end;
end;
Lm2:
the TopStruct of T is SubSpace of T
proof
set S = the TopStruct of T;
[#]S = the carrier of S by Def3;
hence [#]S c= [#]T by Def3;
let P be Subset of S;
hereby assume
A1: P in the topology of S;
reconsider Q = P as Subset of T;
take Q;
thus Q in the topology of T by A1;
thus P = Q /\ [#]S by Th15;
end;
given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]S;
thus P in the topology of S by A2,Th15;
end;
definition let T be TopStruct;
cluster strict SubSpace of T;
existence
proof
the TopStruct of T is SubSpace of T by Lm2;
hence thesis;
end;
end;
definition let T be non empty TopStruct;
cluster strict non empty SubSpace of T;
existence
proof
A1: the TopStruct of T is SubSpace of T by Lm2;
the TopStruct of T is non empty by STRUCT_0:def 1;
hence thesis by A1;
end;
end;
scheme SubFamExS {A() -> TopStruct, P[Subset of A()]}:
ex F being Subset-Family of A() st
for B being Subset of A() holds B in F iff P[B]
proof
defpred Q[Subset of A()] means P[$1];
consider F being Subset-Family of A() such that
A1: for B being Subset of A() holds B in F iff Q[B]
from SubFamEx;
reconsider F as Subset-Family of A();
take F;
thus thesis by A1;
end;
definition let T be TopSpace;
cluster -> TopSpace-like SubSpace of T;
coherence
proof let S be SubSpace of T;
S is TopSpace-like
proof
set P = the carrier of S;
A1: P = [#] S by Def3;
then A2: P c= [#] T by Def9;
A3: [#]T = the carrier of T by Def3;
then A4:[#]T in the topology of T by Def1;
[#]T /\ P = P by A2,A3,Th15;
hence the carrier of S in the topology of S by A1,A4,Def9;
thus for a being Subset-Family of S st
a c= the topology of S
holds union a in the topology of S
proof
let a be Subset-Family of S such that
A5:a c= the topology of S;
defpred Q[set] means
$1 /\ the carrier of S in a & $1 in the topology of T;
consider b being Subset-Family of T such that
A6:for Z being Subset of T holds Z in b iff Q[Z]
from SubFamExS;
b c= the topology of T
proof
let y be set;
assume y in b;
hence thesis by A6;
end;
then A7:union b in the topology of T by Def1;
union a = union b /\ P
proof
A8:union a c= union b /\ P
proof
let x be set;
assume A9:x in union a;
then consider Z1 being set such that A10:x in Z1 & Z1 in a
by TARSKI:def 4;
consider Z3 being Subset of T such that
A11:Z3 in the topology of T & Z1 = Z3 /\ P by A1,A5,A10,Def9;
A12:Z3 in b by A6,A10,A11;
x in Z3 by A10,A11,XBOOLE_0:def 3;
then x in union b by A12,TARSKI:def 4;
hence x in union b /\ P by A9,XBOOLE_0:def 3;
end;
union b /\ P c= union a
proof
let x be set;
assume x in union b /\ P;
then A13:x in union b & x in P by XBOOLE_0:def 3;
then consider Z being set such that
A14:x in Z & Z in b by TARSKI:def 4;
A15:Z /\ P in a by A6,A14;
x in Z /\ P by A13,A14,XBOOLE_0:def 3;
hence x in union a by A15,TARSKI:def 4;
end;
hence union a = union b /\ P by A8,XBOOLE_0:def 10;
end;
hence union a in the topology of S by A1,A7,Def9;
end;
thus for V,Q being Subset of S st
V in the topology of S & Q in the topology of S holds
V /\ Q in the topology of S
proof
let V,Q be Subset of S; assume
A16:V in the topology of S & Q in the topology of S;
then consider P1 being Subset of T such that
A17:P1 in the topology of T & V = P1 /\ P by A1,Def9;
consider Q1 being Subset of T such that
A18:Q1 in the topology of T & Q = Q1 /\ P by A1,A16,Def9;
A19:P1 /\ Q1 in the topology of T by A17,A18,Def1;
V /\ Q = P1 /\ ((Q1 /\ P) /\ P) by A17,A18,XBOOLE_1:16
.= P1 /\ (Q1 /\ (P /\ P)) by XBOOLE_1:16
.= (P1 /\ Q1) /\ P by XBOOLE_1:16;
hence V /\ Q in the topology of S by A1,A19,Def9;
end;
end;
hence thesis;
end;
end;
definition let T be TopStruct, P be Subset of T;
func T|P -> strict SubSpace of T means :Def10:
[#]it = P;
existence
proof
A1: P c= [#] T by Th14;
defpred Q[set] means ex Q being Subset of T st
Q in the topology of T & $1 = Q /\ P;
consider top1 being Subset-Family of P such that
A2:for Z being Subset of P holds Z in top1 iff Q[Z] from SubFamEx;
reconsider top1 as Subset-Family of P;
set Y = TopStruct(#P,top1#);
A3:[#]Y c= [#]T by A1,Def3;
for P being Subset of Y holds P in the topology of Y iff
ex Q being Subset of T st Q in the topology of T &
P = Q /\ [#]Y
proof
let P be Subset of Y;
[#] Y = the carrier of Y by Def3;
hence P in the topology of Y iff
ex Q being Subset of T st Q in the topology of T &
P = Q /\ [#]Y by A2;
end;
then reconsider Y as strict SubSpace of T by A3,Def9;
take Y;
thus thesis by Def3;
end;
uniqueness
proof
let Z1,Z2 be strict SubSpace of T;
assume that A4:[#] Z1 = P and A5:[#] Z2 = P;
A6: [#] Z1 = the carrier of Z1 & [#] Z2 = the carrier of Z2 by Def3;
A7:the topology of Z1 c= the topology of Z2
proof
let x be set;
assume A8:x in the topology of Z1;
then A9:ex Q being Subset of T st Q in
the topology of T &
x = Q /\ [#]Z2 by A4,A5,Def9;
x c= [#]Z2 by A4,A5,A8,Th14;
then x is Subset of Z2 by Th16;
hence thesis by A9,Def9;
end;
the topology of Z2 c= the topology of Z1
proof
let x be set;
assume A10:x in the topology of Z2;
then A11:ex Q being Subset of T st Q in the topology of
T &
x = Q /\ [#]Z1 by A4,A5,Def9;
x c= [#]Z1 by A4,A5,A10,Th14;
then x is Subset of Z1 by Th16;
hence thesis by A11,Def9;
end;
hence Z1 = Z2 by A4,A5,A6,A7,XBOOLE_0:def 10;
end;
end;
definition let T be non empty TopStruct,
P be non empty Subset of T;
cluster T|P -> non empty;
coherence
proof
[#](T|P) = P by Def10;
hence the carrier of T|P is non empty by Def3;
end;
end;
definition let T be TopSpace;
cluster TopSpace-like strict SubSpace of T;
existence
proof consider X being strict SubSpace of T;
take X; thus thesis;
end;
end;
definition
let T be TopSpace, P be Subset of T;
cluster T|P -> TopSpace-like;
coherence;
end;
definition let S, T be 1-sorted;
mode map of S, T is Function of the carrier of S, the carrier of T;
canceled;
end;
definition let S, T be 1-sorted,
f be Function of the carrier of S, the carrier of T,
P be set;
redefine func f.:P -> Subset of T;
coherence
proof
thus f.:P is Subset of T;
end;
end;
definition let S, T be 1-sorted,
f be Function of the carrier of S, the carrier of T,
P be set;
redefine func f"P -> Subset of S;
coherence
proof
thus f"P is Subset of S;
end;
end;
definition let S, T be TopStruct, f be map of S,T;
attr f is continuous means
for P1 being Subset of T st P1 is closed holds f" P1 is closed;
end;
scheme TopAbstr{A() -> TopStruct,P[set]}:
ex P being Subset of A() st
for x being set st x in the carrier of A() holds x in P iff P[x]
proof
defpred Q[set] means ex y being Point of A() st $1=y & P[y];
consider Z being set such that
A1:for x being set holds x in Z iff x in the carrier of A() & Q[x]
from Separation;
for x being set holds x in Z implies x in the carrier of A() by A1;
then reconsider Z as Subset of A() by TARSKI:def 3;
take Z;
for x being set st x in the carrier of A() holds x in Z iff P[x]
proof
let x be set such that
A2: x in the carrier of A();
thus x in Z implies P[x]
proof
assume x in Z;
then ex y being Point of A() st x=y & P[y] by A1;
hence P[x];
end;
thus P[x] implies x in Z by A1,A2;
end;
hence thesis;
end;
canceled 11;
theorem Th39:
for X' being SubSpace of T, A being Subset of X'
holds A is Subset of T
proof
let X' be SubSpace of T, A be Subset of X';
A1:A c= [#]X' by Th14;
[#]X' c= [#]T by Def9;
then A c= [#]T by A1,XBOOLE_1:1;
hence A is Subset of T by Th16;
end;
canceled;
theorem
for A being Subset of T st A <> {}T
ex x being Point of T st x in A
proof
let A be Subset of T; assume
A1:A <> {}T;
consider x being Element of A;
x is Point of T by A1,TARSKI:def 3;
hence thesis by A1;
end;
theorem Th42:
[#]GX is closed
proof
A1:[#]GX \ [#]GX = {}GX by Th23;
{}GX in the topology of GX by Th5;
then {}GX is open by Def5;
hence [#]GX is closed by A1,Def6;
end;
definition let T be TopSpace;
cluster [#]T -> closed;
coherence by Th42;
end;
definition let T be TopSpace;
cluster closed Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
definition let T be non empty TopSpace;
cluster non empty closed Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
theorem Th43:
for X' being SubSpace of T,
B being Subset of X' holds
B is closed iff ex C being Subset of T st C is closed & C /\ [#](X') = B
proof
let X' be SubSpace of T, B be Subset of X';
A1:[#]X' is Subset of T by Th39;
A2:now
assume B is closed;
then [#](X') \ B is open by Def6;
then [#](X') \ B in the topology of X' by Def5;
then consider V being Subset of T such that
A3: V in the topology of T
and A4:[#](X') \ B = V /\ [#]X' by Def9;
reconsider V1 = V as Subset of T;
A5:V1 is open by A3,Def5;
[#](T) \ ([#](T) \ V) = V by Th22;
then A6:[#](T) \ V is closed by A5,Def6;
([#](T) \ V) /\ ([#]X') = [#]X' /\ V` by Th17
.= ([#](X')) \ V by A1,SUBSET_1:32
.= [#](X') \ (([#](X')) /\ V) by XBOOLE_1:47
.= B by A4,Th22;
hence ex C being Subset of T st C is closed &
C /\ ([#]X') = B by A6;
end;
now
given C being Subset of T such that A7:C is closed and
A8:C /\ [#]X' = B;
[#]T \ C is open by A7,Def6;
then A9:[#]T \ C in the topology of T by Def5;
A10:[#]X' \ B = [#]X' \ C by A8,XBOOLE_1:47
.= ([#]X') /\ C` by A1,SUBSET_1:32
.= ([#]T \ C) /\ ([#]X') by Th17;
([#]T \ C) /\ ([#]X') c= [#]X' by XBOOLE_1:17;
then ([#]T \ C) /\ [#]X' is Subset of X' by Th16;
then ([#]T \ C) /\ [#]X' in the topology of X' by A9,Def9;
then [#]X' \ B is open by A10,Def5;
hence B is closed by Def6;
end;
hence thesis by A2;
end;
theorem Th44:
for F being Subset-Family of GX st
for A being Subset of GX st A in F holds A is closed
holds meet F is closed
proof
let F be Subset-Family of GX such that
A1:for A being Subset of GX st A in F holds A is closed;
per cases;
suppose
A2: F <> {};
defpred Q[set] means [#]GX \ $1 in F;
consider R1 being Subset-Family of GX such that
A3:for B being Subset of GX holds B in R1 iff Q[B]
from SubFamExS;
now
let B be set;
assume A4:B in R1;
then reconsider B1=B as Subset of GX;
A5:[#]GX \ ([#]GX \ B1) = B1 by Th22;
B1 in R1 iff [#]GX \ B1 in F by A3;
then [#]GX \ B1 is closed by A1,A4;
then B1 is open by A5,Def6;
hence B in the topology of GX by Def5;
end;
then R1 c= the topology of GX by TARSKI:def 3;
then union R1 in the topology of GX by Def1;
then A6: union R1 is open by Def5;
[#]GX \ ([#]GX \ (union R1)) = union R1 by Th22;
then A7:[#]GX \ union R1 is closed by A6,Def6;
A8:for x being set st x in the carrier of GX holds
(for A being Subset of GX st A in F holds x in A) iff
(for Z being Subset of GX st Z in R1 holds not x in Z)
proof
let x be set;
assume
A9: x in the carrier of GX;
then A10: GX is non empty by STRUCT_0:def 1;
thus (for A being Subset of GX st A in F holds x in A)
implies (for Z being Subset of GX st Z in R1 holds not x in
Z)
proof
assume A11:for A being Subset of GX st A in F holds x in A;
let Z be Subset of GX; assume Z in R1;
then [#]GX \ Z in F by A3;
then x in [#]GX \ Z by A11;
hence not x in Z by XBOOLE_0:def 4;
end;
assume A12:for Z being Subset of GX st Z in R1 holds
not x in Z;
let A be Subset of GX such that A13:A in F;
[#]GX \ ([#]GX \ A) = A by Th22;
then [#]GX \ A in R1 by A3,A13;
then not x in [#]GX \ A by A12;
then (not x in [#]GX) or x in A by XBOOLE_0:def 4;
hence x in A by A9,A10,Th13;
end;
for x being set holds x in [#]GX \ (union R1) iff x in meet F
proof
let x be set;
thus x in [#]GX \ (union R1) implies x in meet F
proof
assume A14:x in [#]GX \ union R1;
then not x in union R1 by XBOOLE_0:def 4;
then for Z being Subset of GX st Z in R1 holds not x in Z
by TARSKI:def 4;
then for A be set st A in F holds x in A by A8,A14;
hence x in meet F by A2,SETFAM_1:def 1;
end;
assume A15:x in meet F;
then A16: GX is non empty by STRUCT_0:def 1;
for A being Subset of GX st A in F holds x in A
by A15,SETFAM_1:def 1;
then for Z being set st x in Z holds not Z in R1 by A8;
then A17:not x in union R1 by TARSKI:def 4;
x in [#]GX by A15,A16,Th13;
hence x in [#]GX \ union R1 by A17,XBOOLE_0:def 4;
end;
hence meet F is closed by A7,TARSKI:2;
suppose
A18: F = {};
{}GX is closed
proof
A19: [#]GX = the carrier of GX by Def3;
the carrier of GX in the topology of GX by Def1;
then A20: [#]GX is open by A19,Def5;
[#]GX = [#]GX \ {}GX;
hence {}GX is closed by A20,Def6;
end;
hence meet F is closed by A18,SETFAM_1:def 1;
end;
::
:: The closure of a set
::
definition
let GX be TopStruct, A be Subset of GX;
func Cl A -> Subset of GX means
:Def13:for p being set st p in the carrier of GX holds p in it iff
for G being Subset of GX st G is open holds
p in G implies A meets G;
existence
proof
defpred P[set] means
for G being Subset of GX st G is open holds $1 in G implies A meets G;
consider P being Subset of GX such that
A1: for x being set st x in the carrier of GX holds x in P iff P[x]
from TopAbstr;
reconsider P as Subset of GX;
take P;
thus thesis by A1;
end;
uniqueness
proof
let C1,C2 be Subset of GX;
assume that
A2:for p being set st p in the carrier of GX holds p in C1 iff
for G being Subset of GX st G is open holds
p in G implies A meets G and
A3:for p being set st p in the carrier of GX holds p in C2 iff
for V being Subset of GX st V is open holds
p in V implies A meets V;
for x being set holds x in C1 iff x in C2
proof
let x be set;
thus x in C1 implies x in C2
proof
assume A4:x in C1;
then for G being Subset of GX st G is open holds
x in G implies A meets G by A2;
hence x in C2 by A3,A4;
end;
assume A5:x in C2;
then for V being Subset of GX st V is open holds
x in V implies A meets V by A3;
hence x in C1 by A2,A5;
end;
hence C1 = C2 by TARSKI:2;
end;
end;
theorem Th45:
for A being Subset of T, p being set
st p in the carrier of T holds
p in Cl A iff for C being Subset of T st C is closed
holds (A c= C implies p in C)
proof
let A be Subset of T, p be set such that
A1: p in the carrier of T;
A2:now
assume A3: p in Cl A;
then A4: T is non empty by STRUCT_0:def 1;
let C be Subset of T; assume C is closed;
then [#]T \ C is open by Def6;
then p in [#]T \ C implies A meets ([#]T \ C) by A3,Def13;
then A c= ([#]T \ C)` implies (p in C or not p in [#]
T) by Th21,XBOOLE_0:def 4;
then A c= [#]T \ ([#]T \ C) implies p in C by A1,A4,Th13,Th17;
hence A c= C implies p in C by Th22;
end;
now
assume A5:for C being Subset of T st C is closed holds
(A c= C implies p in C);
for G being Subset of T st G is open holds
(p in G implies A meets G)
proof
let G be Subset of T such that A6:G is open;
[#]T \ ([#]T \ G) = G by Th22;
then A7:[#]T \ G is closed by A6,Def6;
[#]T \ G = G` by Th17;
then A c= G` implies p in [#]T \ G by A5,A7;
then A c= G` implies p in [#]T \ G;
hence p in G implies A meets G by Th21,XBOOLE_0:def 4;
end;
hence p in Cl A by A1,Def13;
end;
hence thesis by A2;
end;
theorem Th46:
for A being Subset of GX ex F being Subset-Family of GX st
(for C being Subset of GX holds C in F iff C is closed &
A c= C) & Cl A = meet F
proof
let A be Subset of GX;
defpred Q[set] means ex C1 being Subset of GX st C1 = $1 & C1 is closed &
A c= $1;
consider F' being Subset-Family of GX such that
A1:for C being Subset of GX holds C in F' iff Q[C]
from SubFamExS;
take F=F';
thus for C being Subset of GX holds C in F iff C is closed & A c= C
proof
let C be Subset of GX;
thus C in F implies C is closed & A c= C
proof
assume C in F;
then ex C1 being Subset of GX st C1 = C & C1 is closed & A c= C by A1;
hence thesis;
end;
thus thesis by A1;
end;
A c= [#]GX by Th14;
then A2:F <> {} by A1;
for p being set holds p in Cl A iff p in meet F
proof
let p be set;
A3:now
assume A4:p in Cl A;
now
let C be set; assume C in F;
then consider C1 being Subset of GX such that
A5: C1 = C & C1 is closed & A c= C by A1;
thus p in C by A4,A5,Th45;
end;
hence p in meet F by A2,SETFAM_1:def 1;
end;
now
assume A6:p in meet F;
now
let C be Subset of GX; assume C is closed & A c= C;
then C in F by A1;
hence p in C by A6,SETFAM_1:def 1;
end;
hence p in Cl A by A6,Th45;
end;
hence thesis by A3;
end;
hence Cl A = meet F by TARSKI:2;
end;
theorem
for X' being SubSpace of T, A being Subset of T,
A1 being Subset of X'
st A = A1 holds Cl A1 = (Cl A) /\ ([#]X')
proof
let X' be SubSpace of T, A be Subset of T,
A1 be Subset of X' such that A1:A = A1;
for p being set holds p in Cl A1 iff p in (Cl A) /\ ([#]X')
proof
let p be set;
thus p in Cl A1 implies p in (Cl A) /\ ([#]X')
proof
assume A2:p in Cl A1;
A3:for D1 being Subset of T st D1 is closed
holds A c= D1 implies p in D1
proof
let D1 be Subset of T such that A4:D1 is closed;
assume A5:A c= D1;
A1 c= [#]X' by Th14;
then A6:A1 c= D1 /\ [#]X' by A1,A5,XBOOLE_1:19;
D1 /\ [#]X' c= [#]X' by XBOOLE_1:17;
then reconsider D3 = D1 /\ [#]X' as Subset of X' by Th16;
D3 is closed by A4,Th43;
then p in D3 by A2,A6,Th45;
hence p in D1 by XBOOLE_0:def 3;
end;
reconsider DD = Cl A1 as Subset of T by Th39;
p in DD by A2;
then A7:p in Cl A by A3,Th45;
Cl A1 c= [#]X' by Th14;
hence p in (Cl A) /\ ([#]X') by A2,A7,XBOOLE_0:def 3;
end;
assume p in (Cl A) /\ ([#]X');
then A8:p in Cl A & p in [#]X' by XBOOLE_0:def 3;
now
let D1 be Subset of X' such that
A9:D1 is closed;
assume A10: A1 c= D1;
consider D2 being Subset of T such that
A11:D2 is closed and A12:D1 = D2 /\ [#]X'
by A9,Th43;
D2 /\ [#]X' c= D2 by XBOOLE_1:17;
then A c= D2 by A1,A10,A12,XBOOLE_1:1;
then p in D2 by A8,A11,Th45;
hence p in D1 by A8,A12,XBOOLE_0:def 3;
end;
hence p in Cl A1 by A8,Th45;
end;
hence Cl A1 = (Cl A) /\ ([#]X') by TARSKI:2;
end;
theorem Th48:
for A being Subset of T holds A c= Cl A
proof
let A be Subset of T;
now
let x be set;
assume A1:x in A;
assume not x in Cl A;
then ex C being Subset of T st
C is closed & A c= C & not x in C by A1,Th45;
hence contradiction by A1;
end;
hence A c= Cl A by TARSKI:def 3;
end;
theorem Th49:
for A,B being Subset of T st A c= B holds Cl A c= Cl B
proof
let A,B be Subset of T such that A1:A c= B;
now
let x be set;
assume A2:x in Cl A;
now
let D1 be Subset of T; assume A3:D1 is closed;
assume B c= D1;
then A c= D1 by A1,XBOOLE_1:1;
hence x in D1 by A2,A3,Th45;
end;
hence x in Cl B by A2,Th45;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for A,B being Subset of GX holds Cl(A \/ B) = Cl A \/ Cl B
proof
let A,B be Subset of GX;
now
let x be set;
assume A1:x in Cl(A \/ B);
assume not x in Cl A \/ Cl B;
then A2:not x in Cl A & not x in Cl B by XBOOLE_0:def 2;
then consider G1 being Subset of GX such that
A3:G1 is open and A4:x in G1 and A5: A misses G1 by A1,Def13;
consider G2 being Subset of GX such that
A6:G2 is open and A7:x in G2 and A8:B misses G2 by A1,A2,Def13;
G1 in the topology of GX & G2 in the topology of GX
by A3,A6,Def5;
then G1 /\ G2 in the topology of GX by Def1;
then A9:G1 /\ G2 is open by Def5;
A10:x in G1 /\ G2 by A4,A7,XBOOLE_0:def 3;
A11: A /\ G1 = {} & B /\ G2 = {} by A5,A8,XBOOLE_0:def 7;
(A \/ B) /\ (G1 /\ G2) = (A /\ (G1 /\ G2)) \/ (B /\ (G2 /\
G1)) by XBOOLE_1:23
.= ((A /\ G1) /\ G2) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:16
.= {} \/ ({} /\ G1) by A11,XBOOLE_1:16
.= {}GX;
then (A \/ B) misses (G1 /\ G2) by XBOOLE_0:def 7;
hence contradiction by A1,A9,A10,Def13;
end;
then A12:Cl(A \/ B) c= Cl A \/ Cl B by TARSKI:def 3;
A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
then Cl A c= Cl(A \/ B) & Cl B c= Cl(A \/ B) by Th49;
then Cl A \/ Cl B c= Cl(A \/ B) by XBOOLE_1:8;
hence Cl(A \/ B) = Cl A \/ Cl B by A12,XBOOLE_0:def 10;
end;
theorem
for A, B being Subset of T holds
Cl (A /\ B) c= (Cl A) /\ Cl B
proof
let A,B be Subset of T;
A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
then Cl(A /\ B) c= Cl A & Cl(A /\ B) c= Cl B by Th49;
hence Cl (A /\ B) c= (Cl A) /\ Cl B by XBOOLE_1:19;
end;
theorem Th52:
for A being Subset of T holds
(A is closed implies Cl A = A) &
(T is TopSpace-like & Cl A = A implies A is closed)
proof
let A be Subset of T;
thus A is closed implies Cl A = A
proof
assume A1:A is closed;
A2:A c= Cl A by Th48;
for x be set st x in Cl A holds x in A by A1,Th45;
then Cl A c= A by TARSKI:def 3;
hence Cl A = A by A2,XBOOLE_0:def 10;
end;
assume A3: T is TopSpace-like;
assume A4:Cl A = A;
consider F being Subset-Family of T such that
A5:for C being Subset of T holds C in F iff C is closed
& A c= C and A6:Cl A = meet F by A3,Th46;
for C being Subset of T st C in F holds C is closed by A5;
hence A is closed by A3,A4,A6,Th44;
end;
theorem
for A being Subset of T holds
(A is open implies Cl([#](T) \ A) = [#](T) \ A) &
(T is TopSpace-like & Cl([#](T) \ A) = [#](T) \ A implies A is open)
proof
let A be Subset of T;
[#](T) \([#]T \ A) = A by Th22;
then A1: A is open iff [#]T \ A is closed by Def6;
hence A is open implies Cl ([#]T \ A) = [#]T \ A by Th52;
assume T is TopSpace-like & Cl([#]T \ A) = [#]T \ A;
hence thesis by A1,Th52;
end;
theorem
for A being Subset of T,
p being Point of T holds
p in Cl A iff
T is non empty & for G being Subset of T st G is open holds
p in G implies A meets G
proof let A be Subset of T,
p be Point of T;
thus p in Cl A implies
T is non empty & for G being Subset of T
st G is open holds p in G implies A meets G by Def13,STRUCT_0:def 1;
assume T is non empty;
then A1: the carrier of T <> {} by STRUCT_0:def 1;
assume for G being Subset of T st G is open holds
p in G implies A meets G;
hence thesis by A1,Def13;
end;