The abstract of the Mizar article:

Metric Spaces as Topological Spaces --- Fundamental Concepts

by

Agata Darmochwal, and

Yatsuka Nakamura

Received November 21, 1991

MML identifier: TOPMETR

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, PRE_TOPC, SETFAM_1, TARSKI, SUBSET_1, COMPTS_1, BOOLE,
      RELAT_1, CONNSP_2, TOPS_1, ORDINAL2, FUNCT_1, METRIC_1, RCOMP_1,
      ABSVALUE, ARYTM_1, PCOMPS_1, EUCLID, FINSET_1, BORSUK_1, ARYTM_3,
      TOPMETR, PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, NAT_1, REAL_1, DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FINSET_1, BINOP_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2,
      COMPTS_1, PCOMPS_1, CONNSP_2, RCOMP_1, ABSVALUE, BORSUK_1, EUCLID;
 constructors REAL_1, DOMAIN_1, TOPS_1, TOPS_2, COMPTS_1, RCOMP_1, ABSVALUE,
      BORSUK_1, EUCLID, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, PRE_TOPC, PCOMPS_1, STRUCT_0, METRIC_3, METRIC_1,
      RELSET_1, EUCLID, TOPS_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

reserve r for Real, n for Nat;
reserve a, b for real number;
reserve T for non empty TopSpace;

:: Topological spaces

theorem :: TOPMETR:1
 for T being TopStruct,
     F being Subset-Family of T holds
   F is_a_cover_of T iff the carrier of T c= union F;

reserve A for non empty SubSpace of T;

theorem :: TOPMETR:2
for p being Point of A holds p is Point of T;

theorem :: TOPMETR:3
T is_T2 implies A is_T2;

theorem :: TOPMETR:4
for 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:5
T|P is SubSpace of T|(P \/ Q) & T|Q is SubSpace of T|(P \/ Q);

theorem :: TOPMETR:6
   for P being non empty Subset of T st p in P
 for Q being a_neighborhood of p holds
 for p' being Point of T|P, Q' being Subset of T|P
 st Q' = Q /\ P & p'= p
   holds Q' is a_neighborhood of p';

theorem :: TOPMETR:7
for A,B,C being TopSpace
    for f being map of A,C holds
     f is continuous & C is SubSpace of B implies
    for h being map of A,B st h = f holds h is continuous;

theorem :: TOPMETR:8
for A being TopSpace, B being non empty TopSpace
 for f being map of A,B
  for C being SubSpace of B holds f is continuous
 implies for h being map of A,C st h = f holds h is continuous;

theorem :: TOPMETR:9
  for A,B being TopSpace for f being map of A,B
  for C being Subset of B holds f is continuous
  implies
  for h being map of A,B|C st h = f holds h is continuous;

theorem :: TOPMETR:10
    for X being TopStruct, Y being non empty TopStruct,
      K0 being Subset of X,
      f being map of X,Y, g being map 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;

definition let M be MetrSpace;
 cluster strict SubSpace of M;
end;

definition let M be non empty MetrSpace;
 cluster strict non empty SubSpace of M;
end;

reserve A for non empty SubSpace of M;

canceled;

theorem :: TOPMETR:12
for p being Point of A holds p is Point of M;

theorem :: TOPMETR:13
 for r being real number
 for M being MetrSpace, A being SubSpace of M
 for x being Point of M, x' being Point of A st x = x' holds
    Ball(x',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;

definition 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 number;
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:14
 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);
  synonym F is_ball-family;
 pred F is_a_cover_of M means
:: TOPMETR:def 5
   the carrier of M c= union F;
end;

theorem :: TOPMETR:15
for p,q being Point of RealSpace, x,y being real number holds
  x=p & y=q implies dist(p,q) = abs(x-y);

:: Metric spaces and topology

theorem :: TOPMETR:16
  for M being MetrStruct holds
   the carrier of M = the carrier of TopSpaceMetr M &
   the topology of TopSpaceMetr M = Family_open_set M;

canceled 2;

theorem :: TOPMETR:19
TopSpaceMetr(A) is SubSpace of TopSpaceMetr(M);

theorem :: TOPMETR:20
   for P being Subset of TOP-REAL n,
 Q being non empty Subset of Euclid n holds
  P = Q implies (TOP-REAL n)|P = TopSpaceMetr((Euclid n)|Q);

theorem :: TOPMETR:21
 for r being real number
 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:22
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 number st r>0 & Ball(p,r) c= P;

definition let M be MetrStruct;
 attr M is compact means
:: TOPMETR:def 6
   TopSpaceMetr(M) is compact;
end;

theorem :: TOPMETR:23
M is compact iff
 for F st F is_ball-family & F is_a_cover_of M
  ex G st G c= F & G is_a_cover_of M & G is finite;

:: REAL as topological space

definition
 func R^1 -> strict TopSpace equals
:: TOPMETR:def 7
   TopSpaceMetr(RealSpace);
end;

definition
 cluster R^1 -> non empty;
end;

theorem :: TOPMETR:24
the carrier of R^1 = REAL;

definition let C be set, f be PartFunc of C, the carrier of R^1, x be set;
 cluster f.x -> real;
end;

definition let a,b be real number;
 func Closed-Interval-TSpace(a,b) -> strict non empty SubSpace of R^1 equals
:: TOPMETR:def 8
    TopSpaceMetr(Closed-Interval-MSpace(a,b));
end;

theorem :: TOPMETR:25
 a <= b implies the carrier of Closed-Interval-TSpace(a,b) = [. a,b .];

theorem :: TOPMETR:26
 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:27
Closed-Interval-TSpace(0,1) = I[01];

definition
 redefine func I[01] -> strict SubSpace of R^1;
end;

theorem :: TOPMETR:28
   for f being map 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;