:: Topological Spaces and Continuous Functions
:: by Beata Padlewska and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990-2016 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;
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
:: PRE_TOPC:def 1
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;
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;
end;
reserve GX for TopSpace;
theorem :: PRE_TOPC:1
{} in the topology of GX;
theorem :: PRE_TOPC:2
for T being 1-sorted, P being Subset of T holds P \/ P` = [#]T;
theorem :: PRE_TOPC:3
for T being 1-sorted, P being Subset of T holds [#]T \ ([#]T \ P ) = P;
theorem :: PRE_TOPC:4
for T being 1-sorted, P being Subset of T holds P <> [#]T iff [#]T \ P <> {};
theorem :: PRE_TOPC:5
for T being 1-sorted, P,Q being Subset of T st [#]T = P \/ Q & P
misses Q holds Q = [#]T \ P;
theorem :: PRE_TOPC:6
for T being 1-sorted holds [#]T = ({}T)`;
definition
let T be TopStruct, P be Subset of T;
attr P is open means
:: PRE_TOPC:def 2
P in the topology of T;
end;
definition
let T be TopStruct, P be Subset of T;
attr P is closed means
:: PRE_TOPC:def 3
[#]T \ P is open;
end;
definition
let T be TopStruct;
mode SubSpace of T -> TopStruct means
:: PRE_TOPC:def 4
[#]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;
end;
registration
let T be TopStruct;
cluster strict for SubSpace of T;
end;
registration
let T be non empty TopStruct;
cluster strict non empty for SubSpace of T;
end;
registration
let T be TopSpace;
cluster -> TopSpace-like for SubSpace of T;
end;
definition
let T be TopStruct, P be Subset of T;
func T|P -> strict SubSpace of T means
:: PRE_TOPC:def 5
[#]it = P;
end;
registration
let T be non empty TopStruct, P be non empty Subset of T;
cluster T|P -> non empty;
end;
registration
let T be TopSpace;
cluster TopSpace-like strict for SubSpace of T;
end;
registration
let T be TopSpace, P be Subset of T;
cluster T|P -> TopSpace-like;
end;
theorem :: PRE_TOPC:7
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;
theorem :: PRE_TOPC:8 :: JORDAN1:1, AK, 20.02.2006
for GX being TopStruct, A being Subset of GX holds the carrier of (GX|A) = A;
theorem :: PRE_TOPC:9 :: 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;
definition
let S, T be TopStruct, f be Function of S,T;
attr f is continuous means
:: PRE_TOPC:def 6
for P1 being Subset of T st P1 is closed holds f" P1 is closed;
end;
theorem :: PRE_TOPC:10
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;
theorem :: PRE_TOPC:11
for X9 being SubSpace of T, A being Subset of X9 holds A is Subset of T;
theorem :: PRE_TOPC:12
for A being Subset of T st A <> {}T ex x being Point of T st x in A;
registration
let T be TopSpace;
cluster [#]T -> closed;
end;
registration
let T be TopSpace;
cluster closed for Subset of T;
end;
registration
let T be non empty TopSpace;
cluster non empty closed for Subset of T;
end;
theorem :: PRE_TOPC:13
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;
theorem :: PRE_TOPC:14
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;
::
:: The closure of a set
::
definition
let GX be TopStruct, A be Subset of GX;
func Cl A -> Subset of GX means
:: PRE_TOPC:def 7
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;
projectivity;
end;
theorem :: PRE_TOPC:15
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);
theorem :: PRE_TOPC:16
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;
theorem :: PRE_TOPC:17
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);
theorem :: PRE_TOPC:18
for A being Subset of T holds A c= Cl A;
theorem :: PRE_TOPC:19
for A,B being Subset of T st A c= B holds Cl A c= Cl B;
theorem :: PRE_TOPC:20
for A,B being Subset of GX holds Cl(A \/ B) = Cl A \/ Cl B;
theorem :: PRE_TOPC:21
for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ Cl B;
theorem :: PRE_TOPC:22
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);
theorem :: PRE_TOPC:23
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);
theorem :: PRE_TOPC:24
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
;
begin ::Addenda
:: from TOPMETR, 2008.07.06, A.T.
theorem :: PRE_TOPC:25
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;
theorem :: PRE_TOPC:26
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;
theorem :: PRE_TOPC:27
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;
registration
let T be TopSpace;
cluster empty -> closed for Subset of T;
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;
end;
registration
let S be TopSpace;
let T be non empty TopSpace;
cluster continuous for Function of S, T;
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
:: PRE_TOPC:def 8
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
:: PRE_TOPC:def 9
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
:: PRE_TOPC:def 10
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
:: PRE_TOPC:def 11
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
:: PRE_TOPC:def 12
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
:: PRE_TOPC:def 13
T is T_1 regular;
attr T is T_4 means
:: PRE_TOPC:def 14
T is T_1 normal;
end;
registration
cluster T_3 -> T_1 regular for TopStruct;
cluster T_1 regular -> T_3 for TopStruct;
cluster T_4 -> T_1 normal for TopStruct;
cluster T_1 normal -> T_4 for TopStruct;
end;
registration
cluster T_1 for non empty TopSpace;
end;
registration
cluster T_1 -> T_0 for TopStruct;
cluster T_2 -> T_1 for TopStruct;
end;
:: missing, 2009.02.14, A.T.
registration
let T be TopSpace;
cluster the TopStruct of T -> TopSpace-like;
end;
registration
let T be non empty TopStruct;
cluster the TopStruct of T -> non empty;
end;
theorem :: PRE_TOPC:28
for T being TopStruct st the TopStruct of T is TopSpace-like holds T
is TopSpace-like;
theorem :: PRE_TOPC:29
for T being TopStruct, S being SubSpace of the TopStruct of T holds S
is SubSpace of T;
registration
let T be TopSpace;
cluster open for Subset of T;
end;
theorem :: PRE_TOPC:30
for T being TopSpace, X being set holds X is open Subset of T iff X is
open Subset of the TopStruct of T;
theorem :: PRE_TOPC:31
for T being TopSpace, X being set holds X is closed Subset of T
iff X is closed Subset of the TopStruct of T;
theorem :: PRE_TOPC:32
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;
theorem :: PRE_TOPC:33
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;
theorem :: PRE_TOPC:34
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;
:: from BORSUK_3, 2009.03.15, A.T.
registration
let T be TopStruct, P be empty Subset of T;
cluster T | P -> empty;
end;
theorem :: PRE_TOPC:35
for S,T being TopStruct holds S is SubSpace of T iff S is
SubSpace of the TopStruct of T;
theorem :: PRE_TOPC:36
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;
:: missing, 2009.05.26, A.T.
registration
cluster strict empty for TopStruct;
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;
end;
:: from BORSUK_3, 2011.07.08. A.T.
registration
cluster empty -> T_0 for TopStruct;
end;
registration
cluster strict empty for TopSpace;
end;