:: Topological Spaces and Continuous Functions
:: by Beata Padlewska and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, SETFAM_1, TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1,
RCOMP_1, RELAT_1, FUNCT_1, ORDINAL2, FUNCOP_1, CARD_5, PRE_TOPC;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELSET_1, STRUCT_0;
constructors SETFAM_1, PARTFUN1, STRUCT_0, FUNCOP_1, CARD_1, DOMAIN_1,
RELSET_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, RELSET_1;
requirements BOOLE, SUBSET;
definitions TARSKI, STRUCT_0;
equalities STRUCT_0, SUBSET_1;
expansions TARSKI;
theorems TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1, XBOOLE_0, XBOOLE_1, FUNCT_1,
FUNCT_2, RELAT_1, FUNCOP_1;
schemes SUBSET_1;
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;
registration
cluster non empty strict TopSpace-like for TopStruct;
existence
proof
now
take X={{}};
set T={{},X};
T c= bool X
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in T;
then x= {} or x = X by TARSKI:def 2;
then xx c= X;
hence thesis;
end;
then reconsider T as Subset-Family of X;
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:36;
then union a={} or union a=X or union a = {} \/ X by ZFMISC_1:2,25,75;
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;
A3: b={} or b=X by A2,TARSKI:def 2;
a={} or a=X by A1,TARSKI:def 2;
hence a /\ b in the topology of Y by A3,TARSKI:def 2;
end;
then consider X being non empty set, T being Subset-Family of X such that
A4: ( 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;
thus thesis by A4;
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;
registration
let T be TopSpace;
cluster the topology of T -> non empty;
coherence by Def1;
end;
reserve GX for TopSpace;
theorem Th1:
{} in the topology of GX
proof
reconsider A = {} as Subset-Family of GX by XBOOLE_1:2;
A c= the topology of GX;
hence thesis by Def1,ZFMISC_1:2;
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:10
.= the carrier of T;
hence thesis;
end;
theorem Th3:
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) = P /\ [#]T by XBOOLE_1:48;
hence thesis by XBOOLE_1:28;
end;
theorem Th4:
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 that
A1: P <> [#]T and
A2: [#]T \ P = {};
[#]T c= P by A2,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 & P
misses Q holds Q = [#]T \ P
proof
let T be 1-sorted, P,Q be Subset of T;
assume that
A1: [#]T = P \/ Q and
A2: P misses Q;
[#]T \ P = Q \ P by A1,XBOOLE_1:40
.= Q by A2,XBOOLE_1:83;
hence thesis;
end;
theorem
for T being 1-sorted holds [#]T = ({}T)`;
definition
let T be TopStruct, P be Subset of T;
attr P is open means
:Def2:
P in the topology of T;
end;
definition
let T be TopStruct, P be Subset of T;
attr P is closed means
:Def3:
[#]T \ P is open;
end;
definition
let T be TopStruct;
mode SubSpace of T -> TopStruct means
:Def4:
[#]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 XBOOLE_1:28;
end;
given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]T;
thus thesis by A2,XBOOLE_1:28;
end;
end;
Lm1: the TopStruct of T is SubSpace of T
proof
set S = the TopStruct of T;
thus [#]S c= [#]T;
let P be Subset of S;
hereby
reconsider Q = P as Subset of T;
assume
A1: P in the topology of S;
take Q;
thus Q in the topology of T by A1;
thus P = Q /\ [#]S by XBOOLE_1:28;
end;
given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]S;
thus thesis by A2,XBOOLE_1:28;
end;
registration
let T be TopStruct;
cluster strict for SubSpace of T;
existence
proof
the TopStruct of T is SubSpace of T by Lm1;
hence thesis;
end;
end;
registration
let T be non empty TopStruct;
cluster strict non empty for SubSpace of T;
existence
proof
the TopStruct of T is SubSpace of T & the TopStruct of T is non empty
by Lm1;
hence thesis;
end;
end;
registration
let T be TopSpace;
cluster -> TopSpace-like for SubSpace of T;
coherence
proof
let S be SubSpace of T;
S is TopSpace-like
proof
set P = the carrier of S;
A1: [#]T in the topology of T by Def1;
A2: P = [#] S;
then P c= [#] T by Def4;
then [#]T /\ P = P by XBOOLE_1:28;
hence the carrier of S in the topology of S by A2,A1,Def4;
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
A3: 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
A4: for Z being Subset of T holds Z in b iff Q[Z] from SUBSET_1:
sch 3;
A5: union b /\ P c= union a
proof
let x be object;
assume
A6: x in union b /\ P;
then x in union b by XBOOLE_0:def 4;
then consider Z being set such that
A7: x in Z and
A8: Z in b by TARSKI:def 4;
x in P by A6,XBOOLE_0:def 4;
then
A9: x in Z /\ P by A7,XBOOLE_0:def 4;
Z /\ P in a by A4,A8;
hence thesis by A9,TARSKI:def 4;
end;
b c= the topology of T
by A4;
then
A10: union b in the topology of T by Def1;
union a c= union b /\ P
proof
let x be object;
assume
A11: x in union a;
then consider Z1 being set such that
A12: x in Z1 and
A13: Z1 in a by TARSKI:def 4;
consider Z3 being Subset of T such that
A14: Z3 in the topology of T & Z1 = Z3 /\ P by A2,A3,A13,Def4;
Z3 in b & x in Z3 by A4,A12,A13,A14,XBOOLE_0:def 4;
then x in union b by TARSKI:def 4;
hence thesis by A11,XBOOLE_0:def 4;
end;
then union a = union b /\ P by A5,XBOOLE_0:def 10;
hence thesis by A2,A10,Def4;
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 that
A15: V in the topology of S and
A16: Q in the topology of S;
consider P1 being Subset of T such that
A17: P1 in the topology of T and
A18: V = P1 /\ P by A2,A15,Def4;
consider Q1 being Subset of T such that
A19: Q1 in the topology of T and
A20: Q = Q1 /\ P by A2,A16,Def4;
A21: V /\ Q = P1 /\ ((Q1 /\ P) /\ P) by A18,A20,XBOOLE_1:16
.= P1 /\ (Q1 /\ (P /\ P)) by XBOOLE_1:16
.= (P1 /\ Q1) /\ P by XBOOLE_1:16;
P1 /\ Q1 in the topology of T by A17,A19,Def1;
hence thesis by A2,A21,Def4;
end;
end;
hence thesis;
end;
end;
definition
let T be TopStruct, P be Subset of T;
func T|P -> strict SubSpace of T means
:Def5:
[#]it = P;
existence
proof
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
A1: for Z being Subset of P holds Z in top1 iff Q[Z] from SUBSET_1:sch
3;
reconsider top1 as Subset-Family of P;
set Y = TopStruct(#P,top1#);
A2: for Z being Subset of Y holds Z in top1 iff ex Q being Subset of T st
Q in the topology of T & Z = Q /\ [#]Y
proof
let Z be Subset of Y;
thus Z in top1 implies ex Q being Subset of T st Q in the topology of T
& Z = Q /\ [#]Y
proof
assume Z in top1;
then Q[Z] by A1;
hence thesis;
end;
thus thesis by A1;
end;
[#]Y c= [#]T;
then reconsider Y as strict SubSpace of T by A2,Def4;
take Y;
thus thesis;
end;
uniqueness
proof
let Z1,Z2 be strict SubSpace of T;
assume
A3: [#] Z1 = P & [#] Z2 = P;
A4: the topology of Z2 c= the topology of Z1
proof
let x be object;
assume x in the topology of Z2;
then ex Q being Subset of T st Q in the topology of T & x = Q /\ [#]Z1
by A3,Def4;
hence thesis by Def4;
end;
the topology of Z1 c= the topology of Z2
proof
let x be object;
assume x in the topology of Z1;
then ex Q being Subset of T st Q in the topology of T & x = Q /\ [#]Z2
by A3,Def4;
hence thesis by Def4;
end;
hence thesis by A3,A4,XBOOLE_0:def 10;
end;
end;
registration
let T be non empty TopStruct, P be non empty Subset of T;
cluster T|P -> non empty;
coherence
proof
[#](T|P) = P by Def5;
hence the carrier of T|P is non empty;
end;
end;
registration
let T be TopSpace;
cluster TopSpace-like strict for SubSpace of T;
existence
proof
set X = the strict SubSpace of T;
take X;
thus thesis;
end;
end;
registration
let T be TopSpace, P be Subset of T;
cluster T|P -> TopSpace-like;
coherence;
end;
theorem
for S being TopSpace, P1,P2 being Subset of S, P19 being Subset of S|
P2 st P1=P19 & P1 c= P2 holds S|P1=(S|P2)|P19
proof
let S be TopSpace, P1,P2 be Subset of S, P19 be Subset of S|P2;
assume that
A1: P1=P19 and
A2: P1 c= P2;
A3: [#]((S|P2)|P19)=P1 by A1,Def5;
A4: [#](S|P2)=P2 by Def5;
A5: for R being Subset of (S|P2)|P19 holds R in the topology of (S|P2)|P19
iff ex Q being Subset of S st Q in the topology of S & R=Q/\[#]((S|P2)|P19)
proof
let R be Subset of (S|P2)|P19;
A6: now
given Q being Subset of S such that
A7: Q in the topology of S and
A8: R=Q/\[#]((S|P2)|P19);
reconsider R9=Q/\[#](S|P2) as Subset of S|P2;
A9: R9 in the topology of (S|P2) by A7,Def4;
R9/\[#]((S|P2)|P19)=Q/\(P2/\P1) by A4,A3,XBOOLE_1:16
.=R by A2,A3,A8,XBOOLE_1:28;
hence R in the topology of (S|P2)|P19 by A9,Def4;
end;
now
assume R in the topology of (S|P2)|P19;
then consider Q0 being Subset of S|P2 such that
A10: Q0 in the topology of S|P2 and
A11: R=Q0/\[#]((S|P2)|P19) by Def4;
consider Q1 being Subset of S such that
A12: Q1 in the topology of S and
A13: Q0=Q1/\[#](S|P2) by A10,Def4;
R=Q1/\(P2/\P1) by A4,A3,A11,A13,XBOOLE_1:16
.=Q1/\[#]((S|P2)|P19) by A2,A3,XBOOLE_1:28;
hence
ex Q being Subset of S st Q in the topology of S & R=Q/\[#]((S|P2)|
P19) by A12;
end;
hence thesis by A6;
end;
[#]((S|P2)|P19) c= [#](S) by A3;
then (S|P2)|P19 is SubSpace of S by A5,Def4;
hence thesis by A3,Def5;
end;
theorem Th8: :: JORDAN1:1, AK, 20.02.2006
for GX being TopStruct, A being Subset of GX holds the carrier of (GX|A) = A
proof
let GX be TopStruct, A be Subset of GX;
A=[#](GX|A) by Def5;
hence thesis;
end;
theorem :: JGRAPH_3:12, AK, 20.02.2006
for X being TopStruct,Y being non empty TopStruct, f being Function of
X,Y, P being Subset of X holds f|P is Function of X|P,Y
proof
let X be TopStruct,Y be non empty TopStruct,f be Function of X,Y, P be
Subset of X;
P = the carrier of (X|P) by Th8;
hence thesis by FUNCT_2:32;
end;
definition
let S, T be TopStruct, f be Function of S,T;
attr f is continuous means
for P1 being Subset of T st P1 is closed holds f" P1 is closed;
end;
theorem
for T1, T2, S1, S2 being TopStruct st the TopStruct of T1 = the
TopStruct of T2 & the TopStruct of S1 = the TopStruct of S2 holds S1 is
SubSpace of T1 implies S2 is SubSpace of T2
proof
let T1, T2, S1, S2 be TopStruct such that
A1: the TopStruct of T1 = the TopStruct of T2 & the TopStruct of S1 =
the TopStruct of S2;
assume that
A2: [#]S1 c= [#]T1 and
A3: for P being Subset of S1 holds P in the topology of S1 iff ex Q
being Subset of T1 st Q in the topology of T1 & P = Q /\ [#]S1;
thus [#]S2 c= [#]T2 by A1,A2;
thus thesis by A1,A3;
end;
theorem Th11:
for X9 being SubSpace of T, A being Subset of X9 holds A is Subset of T
proof
let X9 be SubSpace of T, A be Subset of X9;
[#]X9 c= [#]T by Def4;
hence thesis by XBOOLE_1:1;
end;
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;
set x = the Element of A;
assume
A1: A <> {}T;
then x is Point of T by TARSKI:def 3;
hence thesis by A1;
end;
registration
let T be TopSpace;
cluster [#]T -> closed;
coherence
proof
{}T in the topology of T by Th1;
then
A1: {}T is open;
[#]T \ [#]T = {}T by Th4;
hence thesis by A1;
end;
end;
registration
let T be TopSpace;
cluster closed for Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster non empty closed for Subset of T;
existence
proof
take [#]T;
thus thesis;
end;
end;
theorem Th13:
for X9 being SubSpace of T, B being Subset of X9 holds B is
closed iff ex C being Subset of T st C is closed & C /\ [#](X9) = B
proof
let X9 be SubSpace of T, B be Subset of X9;
A1: [#]X9 is Subset of T by Th11;
A2: now
assume B is closed;
then [#](X9) \ B is open;
then [#](X9) \ B in the topology of X9;
then consider V being Subset of T such that
A3: V in the topology of T and
A4: [#](X9) \ B = V /\ [#]X9 by Def4;
A5: ([#](T) \ V) /\ ([#]X9) = [#]X9 /\ V` .= ([#](X9)) \ V by A1,SUBSET_1:13
.= [#](X9) \ (([#](X9)) /\ V) by XBOOLE_1:47
.= B by A4,Th3;
reconsider V1 = V as Subset of T;
A6: [#](T) \ ([#](T) \ V) = V by Th3;
V1 is open by A3;
then [#](T) \ V is closed by A6;
hence ex C being Subset of T st C is closed & C /\ ([#]X9) = B by A5;
end;
now
given C being Subset of T such that
A7: C is closed and
A8: C /\ [#]X9 = B;
[#]T \ C is open by A7;
then [#]T \ C in the topology of T;
then
A9: ([#]T \ C) /\ [#]X9 in the topology of X9 by Def4;
[#]X9 \ B = [#]X9 \ C by A8,XBOOLE_1:47
.= ([#]X9) /\ C` by A1,SUBSET_1:13
.= ([#]T \ C) /\ ([#]X9);
then [#]X9 \ B is open by A9;
hence B is closed;
end;
hence thesis by A2;
end;
theorem Th14:
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 SUBSET_1:sch
3;
A4: 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
A5: x in the carrier of GX;
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
A6: 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 A6;
hence thesis by XBOOLE_0:def 5;
end;
assume
A7: for Z being Subset of GX st Z in R1 holds not x in Z;
let A be Subset of GX such that
A8: A in F;
[#]GX \ ([#]GX \ A) = A by Th3;
then [#]GX \ A in R1 by A3,A8;
then not x in [#]GX \ A by A7;
hence thesis by A5,XBOOLE_0:def 5;
end;
A9: for x being object holds x in [#]GX \ (union R1) iff x in meet F
proof
let x be object;
thus x in [#]GX \ (union R1) implies x in meet F
proof
assume
A10: x in [#]GX \ union R1;
then not x in union R1 by XBOOLE_0:def 5;
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 A4,A10;
hence thesis by A2,SETFAM_1:def 1;
end;
assume
A11: x in meet F;
then for A being Subset of GX st A in F holds x in A by SETFAM_1:def 1;
then for Z being set st x in Z holds not Z in R1 by A4;
then not x in union R1 by TARSKI:def 4;
hence thesis by A11,XBOOLE_0:def 5;
end;
now
let B be object;
assume
A12: B in R1;
then reconsider B1=B as Subset of GX;
B1 in R1 iff [#]GX \ B1 in F by A3;
then
A13: [#]GX \ B1 is closed by A1,A12;
[#]GX \ ([#]GX \ B1) = B1 by Th3;
then B1 is open by A13;
hence B in the topology of GX;
end;
then R1 c= the topology of GX;
then union R1 in the topology of GX by Def1;
then
A14: union R1 is open;
[#]GX \ ([#]GX \ (union R1)) = union R1 by Th3;
then [#]GX \ union R1 is closed by A14;
hence thesis by A9,TARSKI:2;
end;
suppose
A15: F = {};
the carrier of GX in the topology of GX by Def1;
then
A16: [#]GX is open;
{}GX is closed by A16;
hence thesis by A15,SETFAM_1:def 1;
end;
end;
::
:: The closure of a set
::
definition
let GX be TopStruct, A be Subset of GX;
func Cl A -> Subset of GX means
:Def7:
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 holds x in P iff x in the carrier of GX & P[x]
from SUBSET_1:sch 1;
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 object holds x in C1 iff x in C2
proof
let x be object;
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 thesis 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 thesis by A2,A5;
end;
hence thesis by TARSKI:2;
end;
projectivity
proof
let r, A be Subset of GX;
assume
A6: for p being set st p in the carrier of GX holds p in r iff for G
being Subset of GX st G is open holds p in G implies A meets G;
let p be set such that
A7: p in the carrier of GX;
thus p in r implies for G being Subset of GX st G is open & p in G holds r
meets G by XBOOLE_0:3;
assume
A8: for G being Subset of GX st G is open holds p in G implies r meets G;
A9: now
let C be Subset of GX;
assume C is closed;
then
A10: [#]GX \ C is open;
now
assume p in [#]GX \ C;
then r meets [#]GX \ C by A8,A10;
then ex x being object st x in r & x in [#]GX \ C by XBOOLE_0:3;
hence A meets [#]GX \ C by A6,A10;
end;
then A c= ([#]GX \ C)` implies p in C or not p in [#]GX by SUBSET_1:23
,XBOOLE_0:def 5;
hence A c= C implies p in C by A7,Th3;
end;
for G being Subset of GX st G is open holds p in G implies A meets G
proof
let G be Subset of GX such that
A11: G is open;
[#]GX \ ([#]GX \ G) = G by Th3;
then [#]GX \ G is closed by A11;
then A c= G` implies p in [#]GX \ G by A9;
hence thesis by SUBSET_1:23,XBOOLE_0:def 5;
end;
hence thesis by A6,A7;
end;
end;
theorem Th15:
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: 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
A4: G is open;
[#]T \ ([#]T \ G) = G by Th3;
then [#]T \ G is closed by A4;
then A c= G` implies p in [#]T \ G by A3;
hence thesis by SUBSET_1:23,XBOOLE_0:def 5;
end;
hence p in Cl A by A1,Def7;
end;
now
assume
A5: p in Cl A;
let C be Subset of T;
assume C is closed;
then [#]T \ C is open;
then p in [#]T \ C implies A meets ([#]T \ C) by A5,Def7;
then A c= ([#]T \ C)` implies (p in C or not p in [#]T) by SUBSET_1:23
,XBOOLE_0:def 5;
hence A c= C implies p in C by A1,Th3;
end;
hence thesis by A2;
end;
theorem Th16:
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 F9 being Subset-Family of GX such that
A1: for C being Subset of GX holds C in F9 iff Q[C] from SUBSET_1:sch 3;
take F=F9;
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;
then
A2: F <> {} by A1;
for p being object holds p in Cl A iff p in meet F
proof
let p be object;
A3: now
assume
A4: 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 A4,SETFAM_1:def 1;
end;
hence p in Cl A by A4,Th15;
end;
now
assume
A5: p in Cl A;
now
let C be set;
assume C in F;
then
ex C1 being Subset of GX st C1 = C & C1 is closed & A c= C by A1;
hence p in C by A5,Th15;
end;
hence p in meet F by A2,SETFAM_1:def 1;
end;
hence thesis by A3;
end;
hence thesis by TARSKI:2;
end;
theorem
for X9 being SubSpace of T, A being Subset of T, A1 being Subset of X9
st A = A1 holds Cl A1 = (Cl A) /\ ([#]X9)
proof
let X9 be SubSpace of T, A be Subset of T, A1 be Subset of X9 such that
A1: A = A1;
for p being object holds p in Cl A1 iff p in (Cl A) /\ ([#]X9)
proof
let p be object;
thus p in Cl A1 implies p in (Cl A) /\ ([#]X9)
proof
reconsider DD = Cl A1 as Subset of T by Th11;
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;
set D3 = D1 /\ [#]X9;
assume A c= D1;
then
A5: A1 c= D1 /\ [#]X9 by A1,XBOOLE_1:19;
D3 is closed by A4,Th13;
then p in D3 by A2,A5,Th15;
hence thesis by XBOOLE_0:def 4;
end;
p in DD by A2;
then p in Cl A by A3,Th15;
hence thesis by A2,XBOOLE_0:def 4;
end;
assume
A6: p in (Cl A) /\ ([#]X9);
then
A7: p in Cl A by XBOOLE_0:def 4;
now
let D1 be Subset of X9;
assume D1 is closed;
then consider D2 being Subset of T such that
A8: D2 is closed and
A9: D1 = D2 /\ [#]X9 by Th13;
A10: D2 /\ [#]X9 c= D2 by XBOOLE_1:17;
assume A1 c= D1;
then A c= D2 by A1,A9,A10;
then p in D2 by A7,A8,Th15;
hence p in D1 by A6,A9,XBOOLE_0:def 4;
end;
hence thesis by A6,Th15;
end;
hence thesis by TARSKI:2;
end;
theorem Th18:
for A being Subset of T holds A c= Cl A
proof
let A be Subset of T;
now
let x be object;
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,Th15
;
hence contradiction by A1;
end;
hence thesis;
end;
theorem Th19:
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;
let x be object;
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;
hence x in D1 by A2,A3,Th15;
end;
hence x in Cl B by A2,Th15;
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 object;
assume
A1: x in Cl(A \/ B);
assume
A2: not x in Cl A \/ Cl B;
then not x in Cl A by XBOOLE_0:def 3;
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,Def7;
A6: A /\ G1 = {} by A5,XBOOLE_0:def 7;
not x in Cl B by A2,XBOOLE_0:def 3;
then consider G2 being Subset of GX such that
A7: G2 is open and
A8: x in G2 and
A9: B misses G2 by A1,Def7;
A10: G2 in the topology of GX by A7;
A11: B /\ G2 = {} by A9,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 A6,A11,XBOOLE_1:16
.= {}GX;
then
A12: (A \/ B) misses (G1 /\ G2) by XBOOLE_0:def 7;
G1 in the topology of GX by A3;
then G1 /\ G2 in the topology of GX by A10,Def1;
then
A13: G1 /\ G2 is open;
x in G1 /\ G2 by A4,A8,XBOOLE_0:def 4;
hence contradiction by A1,A13,A12,Def7;
end;
then
A14: Cl(A \/ B) c= Cl A \/ Cl B;
Cl A c= Cl(A \/ B) & Cl B c= Cl(A \/ B) by Th19,XBOOLE_1:7;
then Cl A \/ Cl B c= Cl(A \/ B) by XBOOLE_1:8;
hence thesis by A14,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;
Cl(A /\ B) c= Cl A & Cl(A /\ B) c= Cl B by Th19,XBOOLE_1:17;
hence thesis by XBOOLE_1:19;
end;
theorem Th22:
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 A is closed;
then for x be object st x in Cl A holds x in A by Th15;
then
A1: Cl A c= A;
A c= Cl A by Th18;
hence thesis by A1,XBOOLE_0:def 10;
end;
assume
A2: T is TopSpace-like;
then consider F being Subset-Family of T such that
A3: for C being Subset of T holds C in F iff C is closed & A c= C and
A4: Cl A = meet F by Th16;
assume
A5: Cl A = A;
for C being Subset of T st C in F holds C is closed by A3;
hence thesis by A2,A5,A4,Th14;
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 Th3;
then
A1: A is open iff [#]T \ A is closed;
hence A is open implies Cl ([#]T \ A) = [#]T \ A by Th22;
assume T is TopSpace-like & Cl([#]T \ A) = [#]T \ A;
hence thesis by A1,Th22;
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
by Def7;
begin ::Addenda
:: from TOPMETR, 2008.07.06, A.T.
theorem
for T being non empty TopStruct, A being non empty SubSpace of T for p
being Point of A holds p is Point of T
proof
let T be non empty TopStruct,A be non empty SubSpace of T;
[#] A c= [#] T by Def4;
hence thesis;
end;
theorem
for A,B,C being TopSpace for f being Function of A,C holds f is
continuous & C is SubSpace of B implies for h being Function of A,B st h = f
holds h is continuous
proof
let A,B,C be TopSpace, f be Function of A,C;
assume that
A1: f is continuous and
A2: C is SubSpace of B;
let h be Function of A,B such that
A3: h = f;
for P being Subset of B holds P is closed implies h"P is closed
proof
let P be Subset of B such that
A4: P is closed;
A5: rng h c= the carrier of C by A3,RELAT_1:def 19;
A6: h"P = h"(rng h /\ P) by RELAT_1:133
.= h"(rng h /\ [#] C /\ P) by A5,XBOOLE_1:28
.= h"(rng h /\ ([#] C /\ P)) by XBOOLE_1:16
.= h"(P /\ [#] C) by RELAT_1:133;
reconsider C as SubSpace of B by A2;
reconsider Q = P /\ [#] C as Subset of C;
Q is closed by A4,Th13;
hence thesis by A1,A3,A6;
end;
hence thesis;
end;
theorem
for A being TopSpace, B being non empty TopSpace for f being Function
of A,B for C being SubSpace of B holds f is continuous implies for h being
Function of A,C st h = f holds h is continuous
proof
let A be TopSpace, B be non empty TopSpace, f be Function of A,B, C be
SubSpace of B;
assume
A1: f is continuous;
let h be Function of A,C such that
A2: h = f;
A3: rng f c= the carrier of C by A2,RELAT_1:def 19;
for P being Subset of C holds P is closed implies h"P is closed
proof
let P be Subset of C;
assume P is closed;
then consider Q being Subset of B such that
A4: Q is closed and
A5: Q /\ ([#] C) = P by Th13;
h"P = f"Q /\ f"([#] C) by A2,A5,FUNCT_1:68
.= f"Q /\ f"(rng f /\ [#] C) by RELAT_1:133
.= f"Q /\ f"(rng f) by A3,XBOOLE_1:28
.= f"Q /\ dom f by RELAT_1:134
.= f"Q by RELAT_1:132,XBOOLE_1:28;
hence thesis by A1,A4;
end;
hence thesis;
end;
registration
let T be TopSpace;
cluster empty -> closed for Subset of T;
coherence
proof let S be Subset of T;
assume S is empty;
then
A1: S = {}T;
the carrier of T in the topology of T by Def1;
hence [#] T \ S is open by A1;
end;
end;
:: from BORSUK_1, 2008.07.07, A.T.
registration
let X be TopSpace, Y be non empty TopStruct;
let y be Point of Y;
cluster X --> y -> continuous;
coherence
proof
let P1 being Subset of Y such that
P1 is closed;
set F = X --> y, H = [#] X;
per cases;
suppose
y in P1;
then F"P1 = H by FUNCOP_1:14;
hence thesis;
end;
suppose
not y in P1;
then F"P1 = {}X by FUNCOP_1:16;
hence thesis;
end;
end;
end;
registration
let S be TopSpace;
let T be non empty TopSpace;
cluster continuous for Function of S, T;
existence
proof
set a = the Point of T;
S --> a is continuous;
hence thesis;
end;
end;
reserve T for TopStruct,
x,y for Point of T;
:: from TSP_1, T_0TOPSP, COMPTS_1, URYSOHN1 2008.07.16, A.T.
definition
let T;
attr T is T_0 means
for x,y st for G being Subset of T st G is open holds x
in G iff y in G holds x = y;
attr T is T_1 means
for p,q being Point of T st p <> q ex G being
Subset of T st G is open & p in G & q in G`;
attr T is T_2 means
for p, q being Point of T st p <> q ex G1,G2
being Subset of T st G1 is open &G2 is open & p in G1 & q in G2 & G1 misses G2;
attr T is regular means
for p being Point of T, F being Subset of T st F is
closed & p in F` ex G1,G2 being Subset of T st G1 is open & G2 is open & p in
G1 & F c= G2 & G1 misses G2;
attr T is normal means
for F1,F2 being Subset of T st F1 is closed & F2 is
closed & F1 misses F2 ex G1,G2 being Subset of T st G1 is open & G2 is open &
F1 c= G1 & F2 c= G2 & G1 misses G2;
end;
definition
let T;
attr T is T_3 means
T is T_1 regular;
attr T is T_4 means
T is T_1 normal;
end;
registration
cluster T_3 -> T_1 regular for TopStruct;
coherence;
cluster T_1 regular -> T_3 for TopStruct;
coherence;
cluster T_4 -> T_1 normal for TopStruct;
coherence;
cluster T_1 normal -> T_4 for TopStruct;
coherence;
end;
registration
cluster T_1 for non empty TopSpace;
existence
proof
set T = TopStruct(#{{}},[#]bool {{}}#);
A1: [#]the carrier of T = the carrier of T & for a being Subset-Family of
T st a c= the topology of T holds union a in the topology of T;
for a,b being Subset of T st a in the topology of T & b in the
topology of T holds a /\ b in the topology of T;
then reconsider T as non empty TopSpace by A1,Def1;
take T;
let p,q be Point of T;
p = {} by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
end;
registration
cluster T_1 -> T_0 for TopStruct;
coherence
proof
let T;
assume
A1: T is T_1;
let x,y;
assume
A2: for G being Subset of T st G is open holds x in G iff y in G;
assume x <> y;
then consider G being Subset of T such that
A3: G is open & x in G and
A4: y in G` by A1;
not y in G by A4,XBOOLE_0:def 5;
hence contradiction by A2,A3;
end;
cluster T_2 -> T_1 for TopStruct;
coherence
proof
let T;
assume
A5: T is T_2;
let p,q being Point of T;
assume p <> q;
then consider G1,G2 being Subset of T such that
A6: G1 is open and
G2 is open and
A7: p in G1 and
A8: q in G2 and
A9: G1 misses G2 by A5;
take G1;
thus G1 is open by A6;
thus p in G1 by A7;
G2 c= G1` by A9,SUBSET_1:23;
hence thesis by A8;
end;
end;
:: missing, 2009.02.14, A.T.
registration
let T be TopSpace;
cluster the TopStruct of T -> TopSpace-like;
coherence
by Def1;
end;
registration
let T be non empty TopStruct;
cluster the TopStruct of T -> non empty;
coherence;
end;
theorem
for T being TopStruct st the TopStruct of T is TopSpace-like holds T
is TopSpace-like;
theorem
for T being TopStruct, S being SubSpace of the TopStruct of T holds S
is SubSpace of T
proof
let T be TopStruct, S be SubSpace of the TopStruct of T;
[#]S c= [#]the TopStruct of T by Def4;
hence
[#]S c= [#]T & for P being Subset of S holds P in the topology of S iff
ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]S by Def4;
end;
registration
let T be TopSpace;
cluster open for Subset of T;
existence
proof
take {}T;
thus {}T in the topology of T by Th1;
end;
end;
theorem
for T being TopSpace, X being set holds X is open Subset of T iff X is
open Subset of the TopStruct of T
proof
let T be TopSpace, X be set;
X in the topology of T iff X in the topology of the TopStruct of T;
hence thesis by Def2;
end;
theorem Th31:
for T being TopSpace, X being set holds X is closed Subset of T
iff X is closed Subset of the TopStruct of T
proof
let T be TopSpace, X be set;
[#]T \ X is open iff ([#]the TopStruct of T) \ X is open;
hence thesis by Def3;
end;
theorem Th32:
for S,T being TopSpace, f being Function of S,T, g being
Function of the TopStruct of S, T st f = g holds f is continuous iff g is
continuous
proof
let S,T be TopSpace, f be Function of S,T, g be Function of the TopStruct of
S, T such that
A1: f = g;
thus f is continuous implies g is continuous
by A1,Th31;
assume
A2: g is continuous;
let P1 being Subset of T;
assume P1 is closed;
then g"P1 is closed by A2;
hence f" P1 is closed by A1,Th31;
end;
theorem Th33:
for S,T being TopSpace, f being Function of S,T, g being
Function of S, the TopStruct of T st f = g holds f is continuous iff g is
continuous
proof
let S,T be TopSpace, f be Function of S,T, g be Function of S, the TopStruct
of T such that
A1: f = g;
thus f is continuous implies g is continuous
by Th31,A1;
assume
A2: g is continuous;
let P1 being Subset of T;
reconsider P = P1 as Subset of the TopStruct of T;
assume P1 is closed;
then P is closed by Th31;
hence f" P1 is closed by A1,A2;
end;
theorem
for S,T being TopSpace, f being Function of S,T, g being Function of
the TopStruct of S, the TopStruct of T st f = g holds f is continuous iff g is
continuous
proof
let S,T be TopSpace, f be Function of S,T, g be Function of the TopStruct of
S, the TopStruct of T such that
A1: f = g;
reconsider h = f as Function of S, the TopStruct of T;
h is continuous iff g is continuous by A1,Th32;
hence f is continuous iff g is continuous by Th33;
end;
:: from BORSUK_3, 2009.03.15, A.T.
registration
let T be TopStruct, P be empty Subset of T;
cluster T | P -> empty;
coherence by Th8;
end;
theorem Th35:
for S,T being TopStruct holds S is SubSpace of T iff S is
SubSpace of the TopStruct of T
proof
let S,T be TopStruct;
thus S is SubSpace of T implies S is SubSpace of the TopStruct of T
proof
assume
A1: S is SubSpace of T;
then [#]S c= [#]T by Def4;
hence [#]S c= [#]the TopStruct of T;
let P be Subset of S;
thus P in the topology of S implies ex Q being Subset of the TopStruct of
T st Q in the topology of the TopStruct of T & P = Q /\ [#]S by A1,Def4;
given Q being Subset of the TopStruct of T such that
A2: Q in the topology of the TopStruct of T & P = Q /\ [#]S;
thus P in the topology of S by A1,A2,Def4;
end;
assume
A3: S is SubSpace of the TopStruct of T;
then [#]S c= [#]the TopStruct of T by Def4;
hence [#]S c= [#]T;
let P be Subset of S;
thus P in the topology of S implies ex Q being Subset of T st Q in the
topology of T & P = Q /\ [#]S by A3,Def4;
given Q being Subset of T such that
A4: Q in the topology of T & P = Q /\ [#]S;
thus P in the topology of S by A3,A4,Def4;
end;
theorem
for X being Subset of T, Y being Subset of the TopStruct of T st X = Y
holds the TopStruct of T|X = (the TopStruct of T)|Y
proof
let X be Subset of T, Y be Subset of the TopStruct of T;
assume X = Y;
then
A1: [#](the TopStruct of T|X) = Y by Def5;
the TopStruct of T|X is strict SubSpace of the TopStruct of T by Th35;
hence the TopStruct of T|X = (the TopStruct of T)|Y by A1,Def5;
end;
:: missing, 2009.05.26, A.T.
registration
cluster strict empty for TopStruct;
existence
proof
set T = the TopStruct;
take T | {}T;
thus thesis;
end;
end;
:: from COMPLSP1, 2010.02.25, A.T.
registration
let A be non empty set, t be Subset-Family of A;
cluster TopStruct(#A,t#) -> non empty;
coherence;
end;
:: from BORSUK_3, 2011.07.08. A.T.
registration
cluster empty -> T_0 for TopStruct;
coherence
proof let T be TopStruct such that
A1: T is empty;
let x,y be Point of T such that
for G being Subset of T st G is open holds x in G iff y in G;
thus x = {} by A1,SUBSET_1:def 1 .= y by A1,SUBSET_1:def 1;
end;
end;
registration
cluster strict empty for TopSpace;
existence
proof
set T = the TopSpace;
take T | {}T;
thus thesis;
end;
end;