:: Metric Spaces as Topological Spaces - Fundamental Concepts
::  by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991-2012 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, XREAL_0, ORDINAL1, 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;
 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;
 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;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions STRUCT_0, PRE_TOPC, TARSKI, TOPS_2, XREAL_0, BINOP_1, REALSET1,
      MEMBERED, PCOMPS_1, METRIC_1;
 theorems ABSVALUE, BINOP_1, BORSUK_1, COMPTS_1, CONNSP_2, FINSET_1, FUNCT_1,
      FUNCT_2, METRIC_1, PCOMPS_1, PRE_TOPC, TARSKI, TOPS_1, TOPS_2, ZFMISC_1,
      TBSP_1, RELAT_1, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1,
      XREAL_1, COMPLEX1, XXREAL_0, SETFAM_1, XXREAL_1, XXREAL_2;
 schemes FUNCT_2;

begin

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

:: Topological spaces

theorem
  for T being TopStruct, F being Subset-Family of T holds F is Cover of
  T iff the carrier of T c= union F by SETFAM_1:def 11;

reserve A for non empty SubSpace of T;

theorem
  T is T_2 implies A is T_2
proof
  assume
A1: T is T_2;
  for p,q being Point of A st not p = q ex W,V being Subset of A st W is
  open & V is open & p in W & q in V & W misses V
  proof
    let p,q be Point of A such that
A2: not p = q;
    reconsider p9 = p, q9 = q as Point of T by PRE_TOPC:25;
    consider W,V being Subset of T such that
A3: W is open and
A4: V is open and
A5: p9 in W & q9 in V and
A6: W misses V by A1,A2,PRE_TOPC:def 10;
    reconsider W9 = W /\ [#] A, V9 = V /\ [#] A as Subset of A;
    V in the topology of T by A4,PRE_TOPC:def 2;
    then
A7: V9 in the topology of A by PRE_TOPC:def 4;
    take W9, V9;
    W in the topology of T by A3,PRE_TOPC:def 2;
    then W9 in the topology of A by PRE_TOPC:def 4;
    hence W9 is open & V9 is open by A7,PRE_TOPC:def 2;
    thus p in W9 & q in V9 by A5,XBOOLE_0:def 4;
A8: W /\ V = {} by A6,XBOOLE_0:def 7;
    W9 /\ V9 = W /\ (V /\ [#] A) /\ [#] A by XBOOLE_1:16
      .= {} /\ [#] A by A8,XBOOLE_1:16
      .= {};
    hence thesis by XBOOLE_0:def 7;
  end;
  hence thesis by PRE_TOPC:def 10;
end;

theorem Th3:
  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
proof
  let T be TopSpace, A,B be SubSpace of T;
  assume
A1: the carrier of A c= the carrier of B;
A2: for P being Subset of A holds P in the topology of A iff ex Q being
  Subset of B st Q in the topology of B & P = Q /\ [#] A
  proof
    let P be Subset of A;
    thus P in the topology of A implies ex Q being Subset of B st Q in the
    topology of B & P = Q /\ [#] A
    proof
      assume P in the topology of A;
      then consider Q9 being Subset of T such that
A3:   Q9 in the topology of T and
A4:   P = Q9 /\ [#] A by PRE_TOPC:def 4;
      reconsider Q = Q9 /\ [#] B as Subset of B;
A5:   Q in the topology of B by A3,PRE_TOPC:def 4;
      P = Q9 /\ ([#] B /\ [#] A) by A1,A4,XBOOLE_1:28
        .= Q /\ [#] A by XBOOLE_1:16;
      hence thesis by A5;
    end;
    given Q being Subset of B such that
A6: Q in the topology of B and
A7: P = Q /\ [#] A;
    consider P9 being Subset of T such that
A8: P9 in the topology of T and
A9: Q = P9 /\ [#] B by A6,PRE_TOPC:def 4;
    P = P9 /\ ([#] B /\ [#] A) by A7,A9,XBOOLE_1:16
      .= P9 /\ [#] A by A1,XBOOLE_1:28;
    hence thesis by A8,PRE_TOPC:def 4;
  end;
  the carrier of A c= [#] B by A1;
  hence thesis by A2,PRE_TOPC:def 4;
end;

reserve P,Q for Subset of T,
  p for Point of T;

theorem Th4:
  T|P is SubSpace of T|(P \/ Q) & T|Q is SubSpace of T|(P \/ Q)
proof
  [#](T|P) = P & [#](T|(P \/ Q)) = P \/ Q by PRE_TOPC:def 5;
  hence T|P is SubSpace of T|(P \/ Q) by Th3,XBOOLE_1:7;
  [#](T|Q) = Q & [#](T|(P \/ Q)) = P \/ Q by PRE_TOPC:def 5;
  hence thesis by Th3,XBOOLE_1:7;
end;

theorem
  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
proof
  let P be non empty Subset of T;
  assume
A1: p in P;
  let Q be a_neighborhood of p;
  let p9 be Point of T|P, Q9 be Subset of T|P such that
A2: Q9 = Q /\ P and
A3: p9= p;
  p in Int Q by CONNSP_2:def 1;
  then consider S being Subset of T such that
A4: S is open and
A5: S c= Q and
A6: p in S by TOPS_1:22;
  reconsider R = S /\ P as Subset of T|P by TOPS_2:29;
A7: R c= Q9 by A5,A2,XBOOLE_1:26;
  S /\ [#](T|P) = S /\ P by PRE_TOPC:def 5;
  then
A8: R is open by A4,TOPS_2:24;
  p9 in R by A1,A6,A3,XBOOLE_0:def 4;
  then p9 in Int Q9 by A8,A7,TOPS_1:22;
  hence thesis by CONNSP_2:def 1;
end;

theorem
  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
proof
  let A,B be TopSpace, f be Function of A,B, C be Subset of B;
  assume
A1: f is continuous;
A2: the carrier of B|C = [#](B|C) .= C by PRE_TOPC:def 5;
  let h be Function of A,B|C such that
A3: h = f;
A4: rng f c= the carrier of B|C by A3,RELAT_1:def 19;
  for P being Subset of B|C holds P is closed implies h"P is closed
  proof
    let P be Subset of B|C;
    assume P is closed;
    then consider Q being Subset of B such that
A5: Q is closed and
A6: Q /\ ([#](B|C)) = P by PRE_TOPC:13;
    h"P = f"(Q /\ C) by A3,A6,PRE_TOPC:def 5
      .= f"Q /\ f"C by FUNCT_1:68
      .= f"Q /\ f"(rng f /\ C) by RELAT_1:133
      .= f"Q /\ f"(rng f) by A2,A4,XBOOLE_1:28
      .= f"Q /\ dom f by RELAT_1:134
      .= f"Q by RELAT_1:132,XBOOLE_1:28;
    hence thesis by A1,A5,PRE_TOPC:def 6;
  end;
  hence thesis by PRE_TOPC:def 6;
end;

theorem
  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
proof
  let X be TopStruct,Y be non empty TopStruct, K0 be Subset of X, f be
  Function of X,Y,g be Function of X|K0,Y;
  assume that
A1: f is continuous and
A2: g=f|K0;
A3: [#]Y <> {};
  for G being Subset of Y st G is open holds g"G is open
  proof
    let G be Subset of Y;
    [#](X|K0)=K0 by PRE_TOPC:def 5;
    then
A4: g"G= [#](X|K0) /\ f"G by A2,FUNCT_1:70;
    assume G is open;
    then f"G is open by A3,A1,TOPS_2:43;
    hence thesis by A4,TOPS_2:24;
  end;
  hence thesis by A3,TOPS_2:43;
end;

:: Some definitions & theorems about metrical spaces

reserve M for non empty MetrSpace,
  p for Point of M;

Lm1: for M be MetrSpace holds MetrStruct (#the carrier of M, the distance of M
#) is MetrSpace
proof
  let M be MetrSpace;
  now
    let a,b,c be Element of MetrStruct (#the carrier of M, the
      distance of M#);
    reconsider a9=a, b9=b, c9=c as Element of M;
A1: dist(a,c) = (the distance of M).(a,c)
      .= dist(a9,c9);
A2: dist(a,b) = (the distance of M).(a,b)
      .= dist(a9,b9);
    hence dist(a,b) = 0 iff a=b by METRIC_1:1,2;
    dist(b,a) = (the distance of M).(b,a)
      .= dist(b9,a9);
    hence dist(a,b) = dist(b,a) by A2;
    dist(b,c) = (the distance of M).(b,c)
      .= dist(b9,c9);
    hence dist(a,c)<=dist(a,b)+dist(b,c) by A2,A1,METRIC_1:4;
  end;
  hence thesis by METRIC_1:6;
end;

definition
  let M be MetrSpace;
  mode SubSpace of M -> MetrSpace means
    :Def1:
    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);
  existence
  proof
    reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as
    MetrSpace by Lm1;
    take MM;
    thus the carrier of MM c= the carrier of M;
    let x,y be Point of MM;
    thus thesis;
  end;
end;

registration
  let M be MetrSpace;
  cluster strict for SubSpace of M;
  existence
  proof
    reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as
    MetrSpace by Lm1;
    for x,y being Point of MM holds (the distance of MM).(x,y) = (the
    distance of M).(x,y);
    then MM is SubSpace of M by Def1;
    hence thesis;
  end;
end;

registration
  let M be non empty MetrSpace;
  cluster strict non empty for SubSpace of M;
  existence
  proof
    reconsider MM = MetrStruct (#the carrier of M, the distance of M#) as
    MetrSpace by Lm1;
    for x,y being Point of MM holds (the distance of MM).(x,y) = (the
    distance of M).(x,y);
    then MM is SubSpace of M by Def1;
    hence thesis;
  end;
end;

reserve A for non empty SubSpace of M;

theorem Th8:
  for p being Point of A holds p is Point of M
proof
  let p be Point of A;
  p in the carrier of A & the carrier of A c= the carrier of M by Def1;
  hence thesis;
end;

theorem Th9:
  for r being real number 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
proof
  let r be real number;
  let M be MetrSpace, A be SubSpace of M;
  let x be Point of M, x9 be Point of A;
  assume
A1: x = x9;
  now
    let a be set;
    assume
A2: a in Ball(x9,r);
    then reconsider y9 = a as Point of A;
    the carrier of A c= the carrier of M by Def1;
    then
A3: M is non empty by A2;
    A is non empty by A2;
    then reconsider y = y9 as Point of M by A3,Th8;
    dist(x9,y9) < r by A2,METRIC_1:11;
    then (the distance of A).(x9,y9) < r;
    then (the distance of M).(x,y) < r by A1,Def1;
    then dist(x,y) < r;
    then a in Ball(x,r) by A3,METRIC_1:11;
    hence a in Ball(x,r) /\ the carrier of A by A2,XBOOLE_0:def 4;
  end;
  then
A4: Ball(x9,r) c= Ball(x,r) /\ the carrier of A by TARSKI:def 3;
  now
    let a be set;
    assume
A5: a in Ball(x,r) /\ the carrier of A;
    then reconsider y9 = a as Point of A by XBOOLE_0:def 4;
    reconsider y = y9 as Point of M by A5;
    a in Ball(x,r) by A5,XBOOLE_0:def 4;
    then dist(x,y) < r by METRIC_1:11;
    then (the distance of M).(x,y) < r;
    then (the distance of A).(x9,y9) < r by A1,Def1;
    then
A6: dist(x9,y9) < r;
    the carrier of A is non empty by A5;
    then A is non empty;
    hence a in Ball(x9,r) by A6,METRIC_1:11;
  end;
  then Ball(x,r) /\ the carrier of A c= Ball(x9,r) by TARSKI:def 3;
  hence thesis by A4,XBOOLE_0:def 10;
end;

definition
  let M be non empty MetrSpace, A be non empty Subset of M;
  func M|A -> strict SubSpace of M means
  :Def2:
  the carrier of it = A;
  existence
  proof
    reconsider B=A as non empty set;
    set d = (the distance of M)||A;
A1: dom d = dom (the distance of M) /\ [:A,A:] by RELAT_1:61
      .= [:the carrier of M,the carrier of M:] /\ [:A,A:] by FUNCT_2:def 1
      .= [: (the carrier of M) /\ A, (the carrier of M) /\ A:] by ZFMISC_1:100
      .= [: (the carrier of M) /\ A, A:] by XBOOLE_1:28
      .= [: A, A :] by XBOOLE_1:28;
    d = (the distance of M)| [:A,A:];
    then rng d c= REAL by RELAT_1:def 19;
    then reconsider d as Function of [:B,B:],REAL by A1,FUNCT_2:def 1
,RELSET_1:4;
    set MM = MetrStruct (# B, d #);
A2: now
      let a,b be Element of MM;
      thus dist(a,b) = (the distance of MM).(a,b)
        .= (the distance of M) . [a,b] by A1,FUNCT_1:47
        .= (the distance of M).(a,b);
    end;
    now
      let a,b,c be Element of MM;
      reconsider a9=a, b9=b, c9=c as Point of M by TARSKI:def 3;
A3:   dist(a,c) = (the distance of M).(a,c) by A2
        .= dist(a9,c9);
      dist(a,b) = (the distance of M).(a,b) by A2
        .= dist(a9,b9);
      hence dist(a,b) = 0 iff a=b by METRIC_1:1,2;
A4:   dist(b,c) = (the distance of M).(b,c) by A2
        .= dist(b9,c9);
      thus dist(a,b) = (the distance of M).(a9,b9) by A2
        .= dist(b9,a9) by METRIC_1:def 1
        .= (the distance of M).(b9,a9)
        .= dist(b,a) by A2;
      dist(a,b) = (the distance of M).(a,b) by A2
        .= dist(a9,b9);
      hence dist(a,c)<=dist(a,b)+dist(b,c) by A3,A4,METRIC_1:4;
    end;
    then reconsider MM as MetrSpace by METRIC_1:6;
    now
      let x, y be Point of MM;
      thus (the distance of MM).(x,y) = dist(x,y)
        .= (the distance of M).(x,y) by A2;
    end;
    then reconsider MM as strict SubSpace of M by Def1;
    take MM;
    thus thesis;
  end;
  uniqueness
  proof
    let S1,S2 be strict SubSpace of M;
    assume that
A5: the carrier of S1 = A and
A6: the carrier of S2 = A;
    now
      let a,b be Element of A;
      thus (the distance of S1).(a,b) = (the distance of M).(a,b) by A5,Def1
        .= (the distance of S2).(a,b) by A6,Def1;
    end;
    hence thesis by A5,A6,BINOP_1:2;
  end;
end;

registration
  let M be non empty MetrSpace, A be non empty Subset of M;
  cluster M|A -> non empty;
  coherence by Def2;
end;

definition
  let a,b be real number;
  assume
A1: a <= b;
  func Closed-Interval-MSpace(a,b) -> strict non empty SubSpace of RealSpace
  means
  :Def3:
  for P being non empty Subset of RealSpace st P = [. a,b .] holds
  it = RealSpace | P;
  existence
  proof
    reconsider P = [. a,b .] as Subset of RealSpace;
    reconsider P as non empty Subset of RealSpace by A1,XXREAL_1:1;
    take RealSpace | P;
    thus thesis;
  end;
  uniqueness
  proof
    reconsider P = [. a,b .] as Subset of RealSpace;
    reconsider P as non empty Subset of RealSpace by A1,XXREAL_1:1;
    let S1,S2 be strict non empty SubSpace of RealSpace;
    assume that
A2: for P being non empty Subset of RealSpace st P = [. a,b .] holds
    S1 = RealSpace | P and
A3: for P being non empty Subset of RealSpace st P = [. a,b .] holds
    S2 = RealSpace | P;
    thus S1 = RealSpace | P by A2
      .= S2 by A3;
  end;
end;

theorem Th10:
  a <= b implies the carrier of Closed-Interval-MSpace(a,b) = [. a ,b .]
proof
  assume
A1: a <= b;
  then reconsider P = [. a,b .] as non empty Subset of RealSpace by XXREAL_1:1;
  thus the carrier of Closed-Interval-MSpace(a,b) = the carrier of RealSpace |
  P by A1,Def3
    .= [. a,b .] by Def2;
end;

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
  :Def4:
  for P being set holds P in F
  implies ex p being Point of M, r st P = Ball(p,r);
end;

theorem Th11:
  for p,q being Point of RealSpace, x,y being real number holds x=
  p & y=q implies dist(p,q) = abs(x-y)
   by METRIC_1:def 12;

:: Metric spaces and topology

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

theorem Th13:
  TopSpaceMetr(A) is SubSpace of TopSpaceMetr(M)
proof
  set T = TopSpaceMetr M, R = TopSpaceMetr A;
  thus [#](R) c= [#](T) by Def1;
  let P be Subset of R;
  thus P in the topology of R implies ex Q being Subset of T st Q in the
  topology of T & P = Q /\ [#](R)
  proof
    set QQ = {Ball(x,r) where x is Point of M, r is Real : x in P & r > 0 &
    Ball(x,r) /\ the carrier of A c= P};
    for X being set st X in QQ holds X c= the carrier of M
    proof
      let X be set;
      assume X in QQ;
      then
      ex x being Point of M, r being Real st X = Ball(x,r) & x in P & r >
      0 & Ball(x,r) /\ the carrier of A c= P;
      hence thesis;
    end;
    then reconsider Q = union QQ as Subset of M by ZFMISC_1:76;
    reconsider Q9 = Q as Subset of T;
    assume P in the topology of R;
    then
A1: P in Family_open_set A;
A2: P c= Q9 /\ [#](R)
    proof
      reconsider P9 = P as Subset of A;
      let a be set;
      assume
A3:   a in P;
      then reconsider x = a as Point of A;
      reconsider x9 = x as Point of M by Th8;
      consider r such that
A4:   r > 0 and
A5:   Ball(x,r) c= P9 by A1,A3,PCOMPS_1:def 4;
      Ball(x,r) = Ball(x9,r) /\ the carrier of A by Th9;
      then
A6:   Ball(x9,r) in QQ by A3,A4,A5;
      x9 in Ball(x9,r) by A4,TBSP_1:11;
      then a in Q9 by A6,TARSKI:def 4;
      hence thesis by A3,XBOOLE_0:def 4;
    end;
    take Q9;
    for x being Point of M st x in Q ex r st r > 0 & Ball(x,r) c= Q
    proof
      let x be Point of M;
      assume x in Q;
      then consider Y being set such that
A7:   x in Y and
A8:   Y in QQ by TARSKI:def 4;
      consider x9 being Point of M, r being Real such that
A9:  Y = Ball(x9,r) and
      x9 in P and
      r > 0 and
      Ball(x9,r) /\ the carrier of A c= P by A8;
      consider p being Real such that
A10:  p > 0 and
A11:  Ball(x,p) c= Ball(x9,r) by A7,A9,PCOMPS_1:27;
      take p;
      thus p > 0 by A10;
      Y c= Q by A8,ZFMISC_1:74;
      hence thesis by A9,A11,XBOOLE_1:1;
    end;
    then Q in Family_open_set M by PCOMPS_1:def 4;
    hence Q9 in the topology of T;
    Q9 /\ [#](R) c= P
    proof
      let a be set;
      assume
A12:  a in Q9 /\ [#](R);
      then a in Q9 by XBOOLE_0:def 4;
      then consider Y being set such that
A13:  a in Y and
A14:  Y in QQ by TARSKI:def 4;
      consider x being Point of M, r being Real such that
A15:  Y = Ball(x,r) and
      x in P and
      r > 0 and
A16:  Ball(x,r) /\ the carrier of A c= P by A14;
      a in Ball(x,r) /\ the carrier of A by A12,A13,A15,XBOOLE_0:def 4;
      hence thesis by A16;
    end;
    hence P = Q9 /\ [#](R) by A2,XBOOLE_0:def 10;
  end;
  reconsider P9 = P as Subset of A;
  given Q being Subset of T such that
A17: Q in the topology of T and
A18: P = Q /\ [#](R);
  reconsider Q9 = Q as Subset of M;
  for p being Point of A st p in P9 ex r st r>0 & Ball(p,r) c= P9
  proof
    let p be Point of A;
    reconsider p9 = p as Point of M by Th8;
    assume p in P9;
    then
A19: p9 in Q9 by A18,XBOOLE_0:def 4;
    Q9 in Family_open_set M by A17;
    then consider r such that
A20: r>0 and
A21: Ball(p9,r) c= Q9 by A19,PCOMPS_1:def 4;
    Ball(p,r) = Ball(p9,r) /\ the carrier of A by Th9;
    then Ball(p,r) c= Q /\ the carrier of A by A21,XBOOLE_1:26;
    then Ball(p,r) c= Q /\ the carrier of R;
    hence thesis by A18,A20;
  end;
  then P in Family_open_set A by PCOMPS_1:def 4;
  hence thesis;
end;

theorem Th14:
  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
proof
  let r be real number;
  let M be triangle MetrStruct, p be Point of M;
  let P be Subset of TopSpaceMetr(M);
  assume P = Ball(p,r);
  then
A1: P in Family_open_set(M) by PCOMPS_1:29;
  thus thesis by A1,PRE_TOPC:def 2;
end;

theorem Th15:
  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
proof
  let P be Subset of TopSpaceMetr(M);
  reconsider P9 = P as Subset of M;
  thus P is open implies for p being Point of M st p in P ex r being real
  number st r>0 & Ball(p,r) c= P
  proof
    assume P is open;
    then P in the topology of TopSpaceMetr M by PRE_TOPC:def 2;
    then
A1: P9 in Family_open_set M;
    let p be Point of M;
    assume p in P;
    then ex r being Real st r>0 & Ball(p,r) c= P by A1,PCOMPS_1:def 4;
    hence thesis;
  end;
  assume
A2: for p being Point of M st p in P ex r being real number st r>0 &
  Ball(p,r) c= P;
  for p being Point of M st p in P ex r being Real st r>0 & Ball(p,r) c= P
  proof
    let p be Point of M;
    assume p in P;
    then consider r being real number such that
A3: r>0 & Ball(p,r) c= P by A2;
    reconsider r as Element of REAL by XREAL_0:def 1;
    take r;
    thus thesis by A3;
  end;
  then P9 in Family_open_set M by PCOMPS_1:def 4;
  hence P in the topology of TopSpaceMetr M;
end;

definition

  let M be MetrStruct;
  attr M is compact means
  :Def5:
  TopSpaceMetr(M) is compact;
end;

theorem
  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
proof
  thus M is compact implies 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
  proof
    set TM = TopSpaceMetr(M);
    assume M is compact;
    then
A1: TopSpaceMetr(M) is compact by Def5;
    let F;
    reconsider TF = F as Subset-Family of TM;
    assume that
A2: F is being_ball-family and
A3: F is Cover of M;
A4: TF is open
    proof
      let P be Subset of TM;
      reconsider P9 = P as Subset of M;
      assume P in TF;
      then ex p,r st P9 = Ball(p,r) by A2,Def4;
      hence thesis by Th14;
    end;
    the carrier of M c= union F by A3,SETFAM_1:def 11;
    then the carrier of TM c= union TF;
    then TF is Cover of TM by SETFAM_1:def 11;
    then consider TG being Subset-Family of TM such that
A5: TG c= TF and
A6: TG is Cover of TM and
A7: TG is finite by A1,A4,COMPTS_1:def 1;
    reconsider G = TG as Subset-Family of M;
    take G;
    the carrier of TM c= union TG by A6,SETFAM_1:def 11;
    then the carrier of M c= union G;
    hence thesis by A5,A7,SETFAM_1:def 11;
  end;
  thus (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) implies M is compact
  proof
    set TM = TopSpaceMetr(M);
    assume
A8: 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;
    now
      let F be Subset-Family of TM;
      set Z = { Ball(p,r) where p is Point of M, r is Real: ex P being Subset
      of TM st P in F & Ball(p,r) c= P};
      Z c= bool the carrier of M
      proof
        let a be set;
        assume a in Z;
        then
        ex p being Point of M, r being Real st a = Ball(p,r) & ex P being
        Subset of TM st P in F & Ball(p,r) c= P;
        hence thesis;
      end;
      then reconsider Z as Subset-Family of M;
      assume that
A9:   F is Cover of TM and
A10:  F is open;
      the carrier of M c= union Z
      proof
        let a be set;
        assume a in the carrier of M;
        then reconsider p = a as Point of M;
        the carrier of TM c= union F & the carrier of TM = the carrier of
        M by A9,SETFAM_1:def 11;
        then p in union F by TARSKI:def 3;
        then consider P being set such that
A11:    p in P and
A12:    P in F by TARSKI:def 4;
        reconsider P as Subset of TM by A12;
        P is open by A10,A12,TOPS_2:def 1;
        then consider r being real number such that
A13:    r>0 and
A14:    Ball(p,r) c= P by A11,Th15;
        reconsider r9 = r as Element of REAL by XREAL_0:def 1;
A15:    a in Ball(p,r) by A13,TBSP_1:11;
        Ball(p,r9) in Z by A12,A14;
        hence thesis by A15,TARSKI:def 4;
      end;
      then
A16:  Z is Cover of M by SETFAM_1:def 11;
      reconsider F9 = F as non empty Subset-Family of TM by A9,TOPS_2:3;
      defpred X[set,set] means $1 c= $2;
      Z is being_ball-family
      proof
        let P be set;
        assume P in Z;
        then
        ex p being Point of M, r being Real st P = Ball(p,r) & ex P being
        Subset of TM st P in F & Ball(p,r) c= P;
        hence thesis;
      end;
      then consider G being Subset-Family of M such that
A17:  G c= Z and
A18:  G is Cover of M and
A19:  G is finite by A8,A16;
A20:  for a being set st a in G ex u being set st u in F9 & X[a,u]
      proof
        let a be set;
        assume a in G;
        then a in Z by A17;
        then consider p being Point of M, r being Real such that
A21:    Ball(p,r) = a and
A22:    ex P being Subset of TM st P in F & Ball(p,r) c= P;
        consider P being Subset of TM such that
A23:    P in F & Ball(p,r) c= P by A22;
        take P;
        thus thesis by A21,A23;
      end;
      consider f being Function of G,F9 such that
A24:  for a being set st a in G holds X[a,f.a] from FUNCT_2:sch 1(A20
      );
      reconsider GG = rng f as Subset-Family of TM by TOPS_2:2;
      take GG;
      thus GG c= F;
      the carrier of TM c= union GG
      proof
A25:    the carrier of TM = the carrier of M & the carrier of M c= union
        G by A18,SETFAM_1:def 11;
        let a be set;
        assume a in the carrier of TM;
        then consider P being set such that
A26:    a in P and
A27:    P in G by A25,TARSKI:def 4;
A28:    P c= f.P by A24,A27;
        dom f = G by FUNCT_2:def 1;
        then f.P in GG by A27,FUNCT_1:def 3;
        hence thesis by A26,A28,TARSKI:def 4;
      end;
      hence GG is Cover of TM by SETFAM_1:def 11;
      dom f = G by FUNCT_2:def 1;
      hence GG is finite by A19,FINSET_1:8;
    end;
    then TM is compact by COMPTS_1:def 1;
    hence thesis by Def5;
  end;
end;

:: REAL as topological space

definition
  func R^1 -> TopSpace equals
  TopSpaceMetr(RealSpace);
  correctness;
end;

registration
  cluster R^1 -> strict non empty;
  coherence;
end;

theorem
  the carrier of R^1 = REAL;

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

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

theorem Th19:
  a <= b implies for P being Subset of R^1 st P = [. a,b .] holds
  Closed-Interval-TSpace(a,b) = R^1|P
proof
  assume
A1: a <= b;
  let P be Subset of R^1;
  assume P = [. a,b .];
  then [#](Closed-Interval-TSpace(a,b)) = P by A1,Th18;
  hence thesis by PRE_TOPC:def 5;
end;

theorem Th20:
  Closed-Interval-TSpace(0,1) = I[01]
proof
  reconsider P = [.0,1.] as Subset of R^1;
  set TR = TopSpaceMetr(RealSpace);
  reconsider P9 = P as Subset of TR;
  thus Closed-Interval-TSpace(0,1) = TR|P9 by Th19
    .= I[01] by BORSUK_1:def 13;
end;

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

Lm2: for r be real number holds r >= 0 & a + r <= b implies a <= b
proof
  let r be real number;
  assume r >= 0 & a + r <= b;
  then a + r - r <= b - r & b - r <= b by XREAL_1:9,43;
  hence thesis by XXREAL_0:2;
end;

theorem
  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
proof
  let f be Function of R^1,R^1;
  given a,b being Real such that
A1: for x being Real holds f.x = a*x + b;
  for W being Point of R^1, G being a_neighborhood of f.W ex H being
  a_neighborhood of W st f.:H c= G
  proof
    let W be Point of R^1, G be a_neighborhood of f.W;
    reconsider Y = f.W as Point of RealSpace;
A2: f.W in Int G by CONNSP_2:def 1;
    then consider Q being Subset of R^1 such that
A3: Q is open and
A4: Q c= G and
A5: f.W in Q by TOPS_1:22;
    consider r being real number such that
A6: r>0 and
A7: Ball(Y,r) c= Q by A3,A5,Th15;
    now
      per cases;
      suppose
A8:     a = 0;
        set H = [#](R^1);
        W in H;
        then W in Int H by TOPS_1:23;
        then reconsider H as a_neighborhood of W by CONNSP_2:def 1;
        for y being set holds y in {b} iff ex x being set st x in dom f &
        x in H & y = f.x
        proof
          let y be set;
          thus y in {b} implies ex x being set st x in dom f & x in H & y = f.
          x
          proof
            assume
A9:         y in {b};
            take 0;
            dom f = the carrier of R^1 by FUNCT_2:def 1;
            hence 0 in dom f & 0 in H;
            thus f.0 = 0 * 0 + b by A1,A8
              .= y by A9,TARSKI:def 1;
          end;
          given x being set such that
A10:      x in dom f and
          x in H and
A11:      y = f.x;
          reconsider x as Real by A10;
          y = 0 * x + b by A1,A8,A11
            .= b;
          hence thesis by TARSKI:def 1;
        end;
        then
A12:    f.:H = {b} by FUNCT_1:def 6;
        reconsider W9 = W as Real;
A13:    Int G c= G by TOPS_1:16;
        f.W = 0 * W9 + b by A1,A8
          .= b;
        then f.:H c= G by A2,A12,A13,ZFMISC_1:31;
        hence thesis;
      end;
      suppose
A14:    a <> 0;
        reconsider W9 = W as Point of RealSpace;
        set d = r/(2* abs(a));
        reconsider H = Ball(W9,d) as Subset of R^1;
        H is open by Th14;
        then
A15:    Int H = H by TOPS_1:23;
        abs(a) > 0 by A14,COMPLEX1:47;
        then 2*abs(a) > 0 by XREAL_1:129;
        then W in Int H by A6,A15,TBSP_1:11,XREAL_1:139;
        then reconsider H as a_neighborhood of W by CONNSP_2:def 1;
A16:    f.:H c= Ball(Y,r)
        proof
          reconsider W99 = W9 as Real;
          let y be set;
          reconsider Y9 = Y as Real;
          assume y in f.:H;
          then consider x being set such that
A17:      x in dom f and
A18:      x in H and
A19:      y = f.x by FUNCT_1:def 6;
          reconsider x9=x as Point of RealSpace by A18;
          reconsider y9=y as Real by A17,A19,FUNCT_2:5;
          reconsider x99 = x9 as Real;
          reconsider yy=y9 as Point of RealSpace;
A20:      abs(a) > 0 by A14,COMPLEX1:47;
          dist(W9,x9) < d by A18,METRIC_1:11;
          then abs( W99 - x99 ) < d by Th11;
          then abs(a)*abs( W99 - x99 ) < abs(a)*d by A20,XREAL_1:68;
          then abs(a*(W99 - x99)) < abs(a)*d by COMPLEX1:65;
          then abs((a*W99+b) - (a*x99+b)) < abs(a)*d;
          then abs(Y9 - (a*x99+b)) < abs(a)*d by A1;
          then
A21:      abs(Y9 - y9) < abs(a)*d by A1,A19;
          abs(a) <> 0 by A14,ABSVALUE:2;
          then
A22:      abs(a)*d = r/2 by XCMPLX_1:92;
          r/2+r/2 = r & r/2>=0 by A6,XREAL_1:136;
          then abs(Y9-y9) < r by A21,A22,Lm2;
          then dist(Y,yy) < r by Th11;
          hence thesis by METRIC_1:11;
        end;
        Ball(Y,r) c= G by A4,A7,XBOOLE_1:1;
        hence thesis by A16,XBOOLE_1:1;
      end;
    end;
    hence thesis;
  end;
  hence thesis by BORSUK_1:def 1;
end;

::Moved from JORDAN16:6, AK 20.02.2006

theorem
  for T being non empty TopSpace, A,B being Subset of T st A c= B holds
  T|A is SubSpace of T|B
proof
  let T be non empty TopSpace, A,B be Subset of T;
  assume A c= B;
  then A \/ B = B by XBOOLE_1:12;
  hence thesis by Th4;
end;

::Moved from JGRAPH_5:6,7, AK 20.02.2006

theorem Th23:
  for a,b,d,e being real number, 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
proof
  let a,b,d,e be real number, B be Subset of Closed-Interval-TSpace(d,e);
  assume that
A1: d<=a and
A2: a<=b and
A3: b<=e and
A4: B=[.a,b.];
  a<=e by A2,A3,XXREAL_0:2;
  then
A5: a in [.d,e.] by A1,XXREAL_1:1;
A6: d<=b by A1,A2,XXREAL_0:2;
  then reconsider A=[.d,e.] as non empty Subset of R^1 by A3,XXREAL_1:1;
  b in [.d,e.] by A3,A6,XXREAL_1:1;
  then
A7: [.a,b.] c= [.d,e.] by A5,XXREAL_2:def 12;
  reconsider B2=[.a,b.] as non empty Subset of R^1 by A2,XXREAL_1:1;
A8: Closed-Interval-TSpace(a,b)=R^1|B2 by A2,Th19;
  Closed-Interval-TSpace(d,e)=R^1|A by A3,A6,Th19,XXREAL_0:2;
  hence thesis by A4,A8,A7,PRE_TOPC:7;
end;

theorem
  for a,b being real number, 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 by Th20,Th23;

:: from BORSUK_6, 2007.04.08, A,T.

definition
  let T be 1-sorted;
  attr T is real-membered means
  :Def8:
  the carrier of T is real-membered;
end;

registration
  cluster I[01] -> real-membered;
  coherence
  proof
    thus the carrier of I[01] is real-membered by BORSUK_1:40;
  end;
end;

:: from RCOMP_3, 2007.04.08, A,T.

registration
  cluster non empty real-membered for 1-sorted;
  existence
  proof
    take I[01];
    thus thesis;
  end;
end;

registration
  let S be real-membered 1-sorted;
  cluster the carrier of S -> real-membered;
  coherence by Def8;
end;

:: from BORSUK_6, 2010.03.07, A.T.

registration
  cluster R^1 -> real-membered;
  coherence
  proof let x be set;
   assume x in the carrier of R^1;
   hence x is real;
  end;
end;

:: from BORSUK_6, 2010.05.31, A.K.

registration
  cluster strict non empty real-membered for TopSpace;
  existence
  proof
    take I[01];
    thus thesis;
  end;
end;

registration
  let T be real-membered TopStruct;
  cluster -> real-membered for SubSpace of T;
  coherence
  proof
    let R be SubSpace of T;
    let x be set;
    the carrier of R c= the carrier of T by BORSUK_1:1;
    hence thesis;
  end;
end;

:: from EUCLID_9, 2010.10.05, A.K.

registration
  cluster RealSpace -> real-membered;
  coherence
  proof
    thus the carrier of RealSpace is real-membered;
  end;
end;