:: Topological Spaces and Continuous Functions :: by Beata Padlewska and Agata Darmochwa\l :: :: Received April 14, 1989 :: Copyright (c) 1990-2021 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;