:: Metric Spaces as Topological Spaces - Fundamental Concepts :: by Agata Darmochwa{\l} and Yatsuka Nakamura :: :: Received November 21, 1991 :: Copyright (c) 1991-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 NUMBERS, REAL_1, XBOOLE_0, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI, SUBSET_1, RCOMP_1, RELAT_1, CONNSP_2, TOPS_1, FUNCT_1, ORDINAL2, METRIC_1, CARD_1, XXREAL_0, ARYTM_3, REALSET1, ZFMISC_1, XXREAL_1, COMPLEX1, ARYTM_1, PCOMPS_1, FINSET_1, BORSUK_1, TOPMETR, MEMBERED, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XCMPLX_0, XREAL_0, REAL_1, NAT_1, DOMAIN_1, RELAT_1, REALSET1, FUNCT_1, PARTFUN1, RELSET_1, XXREAL_0, FUNCT_2, FINSET_1, BINOP_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, PCOMPS_1, CONNSP_2, RCOMP_1, BORSUK_1, COMPLEX1; constructors SETFAM_1, REAL_1, COMPLEX1, RCOMP_1, REALSET1, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, FINSET_1, MEMBERED, XXREAL_2, PCOMPS_1, BINOP_1, BINOP_2, VALUED_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, XREAL_0, MEMBERED, REALSET1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, METRIC_3, PCOMPS_1, XXREAL_2, BORSUK_1, BINOP_2, VALUED_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve r for Real; reserve a, b for Real; reserve T for non empty TopSpace; :: Topological spaces theorem :: TOPMETR:1 for T being TopStruct, F being Subset-Family of T holds F is Cover of T iff the carrier of T c= union F; reserve A for non empty SubSpace of T; theorem :: TOPMETR:2 T is T_2 implies A is T_2; theorem :: TOPMETR:3 for T being TopSpace, A,B being SubSpace of T st the carrier of A c= the carrier of B holds A is SubSpace of B; reserve P,Q for Subset of T, p for Point of T; theorem :: TOPMETR:4 T|P is SubSpace of T|(P \/ Q) & T|Q is SubSpace of T|(P \/ Q); theorem :: TOPMETR:5 for P being non empty Subset of T st p in P for Q being a_neighborhood of p holds for p9 being Point of T|P, Q9 being Subset of T|P st Q9 = Q /\ P & p9= p holds Q9 is a_neighborhood of p9; theorem :: TOPMETR:6 for A,B being TopSpace for f being Function of A,B for C being Subset of B holds f is continuous implies for h being Function of A,B|C st h = f holds h is continuous; theorem :: TOPMETR:7 for X being TopStruct, Y being non empty TopStruct, K0 being Subset of X, f being Function of X,Y, g being Function of X|K0,Y st f is continuous & g = f|K0 holds g is continuous; :: Some definitions & theorems about metrical spaces reserve M for non empty MetrSpace, p for Point of M; definition let M be MetrSpace; mode SubSpace of M -> MetrSpace means :: TOPMETR:def 1 the carrier of it c= the carrier of M & for x,y being Point of it holds (the distance of it).(x,y) = ( the distance of M).(x,y); end; registration let M be MetrSpace; cluster strict for SubSpace of M; end; registration let M be non empty MetrSpace; cluster strict non empty for SubSpace of M; end; reserve A for non empty SubSpace of M; theorem :: TOPMETR:8 for p being Point of A holds p is Point of M; theorem :: TOPMETR:9 for r being Real for M being MetrSpace, A being SubSpace of M for x being Point of M, x9 being Point of A st x = x9 holds Ball(x9,r) = Ball(x,r) /\ the carrier of A; definition let M be non empty MetrSpace, A be non empty Subset of M; func M|A -> strict SubSpace of M means :: TOPMETR:def 2 the carrier of it = A; end; registration let M be non empty MetrSpace, A be non empty Subset of M; cluster M|A -> non empty; end; definition let a,b be Real; assume a <= b; func Closed-Interval-MSpace(a,b) -> strict non empty SubSpace of RealSpace means :: TOPMETR:def 3 for P being non empty Subset of RealSpace st P = [. a,b .] holds it = RealSpace | P; end; theorem :: TOPMETR:10 a <= b implies the carrier of Closed-Interval-MSpace(a,b) = [. a ,b .]; reserve F,G for Subset-Family of M; definition let M be MetrStruct, F be Subset-Family of M; attr F is being_ball-family means :: TOPMETR:def 4 for P being set holds P in F implies ex p being Point of M, r st P = Ball(p,r); end; theorem :: TOPMETR:11 for p,q being Point of RealSpace, x,y being Real holds x= p & y=q implies dist(p,q) = |.x-y.|; :: Metric spaces and topology theorem :: TOPMETR:12 for M being MetrStruct holds the carrier of M = the carrier of TopSpaceMetr M & the topology of TopSpaceMetr M = Family_open_set M; theorem :: TOPMETR:13 TopSpaceMetr(A) is SubSpace of TopSpaceMetr(M); theorem :: TOPMETR:14 for r being Real for M being triangle MetrStruct, p being Point of M for P being Subset of TopSpaceMetr(M) st P = Ball(p,r) holds P is open; theorem :: TOPMETR:15 for P being Subset of TopSpaceMetr(M) holds P is open iff for p being Point of M st p in P ex r being Real st r>0 & Ball(p,r) c= P; definition let M be MetrStruct; attr M is compact means :: TOPMETR:def 5 TopSpaceMetr(M) is compact; end; theorem :: TOPMETR:16 M is compact iff for F st F is being_ball-family & F is Cover of M ex G st G c= F & G is Cover of M & G is finite; :: REAL as topological space definition func R^1 -> TopSpace equals :: TOPMETR:def 6 TopSpaceMetr(RealSpace); end; registration cluster R^1 -> strict non empty; end; theorem :: TOPMETR:17 the carrier of R^1 = REAL; definition let a,b be Real; func Closed-Interval-TSpace(a,b) -> strict non empty SubSpace of R^1 equals :: TOPMETR:def 7 TopSpaceMetr(Closed-Interval-MSpace(a,b)); end; theorem :: TOPMETR:18 a <= b implies the carrier of Closed-Interval-TSpace(a,b) = [. a,b .]; theorem :: TOPMETR:19 a <= b implies for P being Subset of R^1 st P = [. a,b .] holds Closed-Interval-TSpace(a,b) = R^1|P; theorem :: TOPMETR:20 Closed-Interval-TSpace(0,1) = I[01]; definition redefine func I[01] -> SubSpace of R^1; end; theorem :: TOPMETR:21 for f being Function of R^1,R^1 st ex a,b being Real st for x being Real holds f.x = a*x + b holds f is continuous; ::Moved from JORDAN16:6, AK 20.02.2006 theorem :: TOPMETR:22 for T being non empty TopSpace, A,B being Subset of T st A c= B holds T|A is SubSpace of T|B; ::Moved from JGRAPH_5:6,7, AK 20.02.2006 theorem :: TOPMETR:23 for a,b,d,e being Real, B being Subset of Closed-Interval-TSpace(d,e) st d<=a & a<=b & b<=e & B=[.a,b.] holds Closed-Interval-TSpace(a,b)=Closed-Interval-TSpace(d,e)|B; theorem :: TOPMETR:24 for a,b being Real, B being Subset of I[01] st 0<=a & a<=b & b <=1 & B=[.a,b.] holds Closed-Interval-TSpace(a,b)=I[01]|B; :: from BORSUK_6, 2007.04.08, A,T. definition let T be 1-sorted; attr T is real-membered means :: TOPMETR:def 8 the carrier of T is real-membered; end; registration cluster I[01] -> real-membered; end; :: from RCOMP_3, 2007.04.08, A,T. registration cluster non empty real-membered for 1-sorted; end; registration let S be real-membered 1-sorted; cluster the carrier of S -> real-membered; end; :: from BORSUK_6, 2010.03.07, A.T. registration cluster R^1 -> real-membered; end; :: from BORSUK_6, 2010.05.31, A.K. registration cluster strict non empty real-membered for TopSpace; end; registration let T be real-membered TopStruct; cluster -> real-membered for SubSpace of T; end; :: from EUCLID_9, 2010.10.05, A.K. registration cluster RealSpace -> real-membered; end;