:: 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


begin

:: Topological spaces
theorem :: TOPMETR:1
for T being TopStruct
for 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;

theorem :: TOPMETR:2
for T being non empty TopSpace
for A being non empty SubSpace of T st T is T_2 holds
A is T_2
proofend;

theorem Th3: :: TOPMETR:3
for T being TopSpace
for A, B being SubSpace of T st the carrier of A c= the carrier of B holds
A is SubSpace of B
proofend;

theorem Th4: :: TOPMETR:4
for T being non empty TopSpace
for P, Q being Subset of T holds
( T | P is SubSpace of T | (P \/ Q) & T | Q is SubSpace of T | (P \/ Q) )
proofend;

theorem :: TOPMETR:5
for T being non empty TopSpace
for p being Point of T
for P being non empty Subset of T st p in P holds
for Q being a_neighborhood of p
for p9 being Point of (T | P)
for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds
Q9 is a_neighborhood of p9
proofend;

theorem :: TOPMETR:6
for A, B being TopSpace
for f being Function of A,B
for C being Subset of B st f is continuous holds
for h being Function of A,(B | C) st h = f holds
h is continuous
proofend;

theorem :: TOPMETR:7
for X being TopStruct
for Y being non empty TopStruct
for K0 being Subset of X
for f being Function of X,Y
for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds
g is continuous
proofend;

Lm1:  for M being MetrSpace holds MetrStruct(# the carrier of M, the distance of M #) is MetrSpace
proofend;

definition
let M be MetrSpace;
mode SubSpace of M ->  MetrSpace means :Def1: :: 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) ) );
existence
 ex b1 being MetrSpace st
( the carrier of b1 c= the carrier of M & ( for x, y being Point of b1 holds the distance of b1 . (x,y) = the distance of M . (x,y) ) )
proofend;
end;

:: deftheorem Def1 defines SubSpace TOPMETR:def_1_:_
 for M, b2 being MetrSpace holds
( b2 is SubSpace of M iff ( the carrier of b2 c= the carrier of M & ( for x, y being Point of b2 holds the distance of b2 . (x,y) = the distance of M . (x,y) ) ) );

registration
let M be MetrSpace;
cluster strict Reflexive discerning V122() triangle for SubSpace of M;
existence
 ex b1 being SubSpace of M st b1 is strict
proofend;
end;

registration
let M be non empty MetrSpace;
cluster non empty strict Reflexive discerning V122() triangle for SubSpace of M;
existence
 ex b1 being SubSpace of M st
( b1 is strict & not b1 is empty )
proofend;
end;

theorem Th8: :: TOPMETR:8
for M being non empty MetrSpace
for A being non empty SubSpace of M
for p being Point of A holds p is Point of M
proofend;

theorem Th9: :: TOPMETR:9
for r being real number
for M being MetrSpace
for A being SubSpace of M
for x being Point of M
for x9 being Point of A st x = x9 holds
Ball (x9,r) = (Ball (x,r)) /\ the carrier of A
proofend;

definition
let M be non empty MetrSpace;
let A be non empty Subset of M;
funcM | A ->  strict SubSpace of M means :Def2: :: TOPMETR:def 2
 the carrier of it = A;
existence
 ex b1 being strict SubSpace of M st the carrier of b1 = A
proofend;
uniqueness
 for b1, b2 being strict SubSpace of M st the carrier of b1 = A & the carrier of b2 = A holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines | TOPMETR:def_2_:_
 for M being non empty MetrSpace
for A being non empty Subset of M
for b3 being strict SubSpace of M holds
( b3 = M | A iff the carrier of b3 = A );

registration
let M be non empty MetrSpace;
let A be non empty Subset of M;
clusterM | A ->  non empty strict ;
coherence
 not M | A is empty by Def2;
end;

definition
let a, b be real number ;
assume A1: a <= b ;
func Closed-Interval-MSpace (a,b) ->  non empty strict SubSpace of RealSpace  means :Def3: :: TOPMETR:def 3
 for P being non empty Subset of RealSpace st P = [.a,b.] holds
it = RealSpace | P;
existence
 ex b1 being non empty strict SubSpace of RealSpace st
for P being non empty Subset of RealSpace st P = [.a,b.] holds
b1 = RealSpace | P
proofend;
uniqueness
 for b1, b2 being non empty strict SubSpace of RealSpace st ( for P being non empty Subset of RealSpace st P = [.a,b.] holds
b1 = RealSpace | P ) &amp; ( for P being non empty Subset of RealSpace st P = [.a,b.] holds
b2 = RealSpace | P ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Closed-Interval-MSpace TOPMETR:def_3_:_
 for a, b being real number st a <= b holds
for b3 being non empty strict SubSpace of RealSpace holds
( b3 = Closed-Interval-MSpace (a,b) iff for P being non empty Subset of RealSpace st P = [.a,b.] holds
b3 = RealSpace | P );

theorem Th10: :: TOPMETR:10
for a, b being real number st a <= b holds
the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.]
proofend;

definition
let M be MetrStruct ;
let F be Subset-Family of M;
attrF is being_ball-family  means :Def4: :: TOPMETR:def 4
 for P being set st P in F holds
ex p being Point of M ex r being Real st P = Ball (p,r);
end;

:: deftheorem Def4 defines being_ball-family TOPMETR:def_4_:_
 for M being MetrStruct
for F being Subset-Family of M holds
( F is being_ball-family iff for P being set st P in F holds
ex p being Point of M ex r being Real st P = Ball (p,r) );

theorem Th11: :: TOPMETR:11
for p, q being Point of RealSpace
for x, y being real number st x = p &amp; y = q holds
dist (p,q) = abs (x - y) by METRIC_1:def_12;

:: Metric spaces and topology
theorem :: TOPMETR:12
for M being MetrStruct holds
( the carrier of M = the carrier of (TopSpaceMetr M) &amp; the topology of (TopSpaceMetr M) = Family_open_set M ) ;

theorem Th13: :: TOPMETR:13
for M being non empty MetrSpace
for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M
proofend;

theorem Th14: :: TOPMETR:14
for r being real number
for M being triangle MetrStruct
for p being Point of M
for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds
P is open
proofend;

theorem Th15: :: TOPMETR:15
for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) holds
( P is open iff for p being Point of M st p in P holds
ex r being real number st
( r > 0 &amp; Ball (p,r) c= P ) )
proofend;

definition
let M be MetrStruct ;
attrM is compact  means :Def5: :: TOPMETR:def 5
 TopSpaceMetr M is compact ;
end;

:: deftheorem Def5 defines compact TOPMETR:def_5_:_
 for M being MetrStruct holds
( M is compact iff TopSpaceMetr M is compact );

theorem :: TOPMETR:16
for M being non empty MetrSpace holds
( M is compact iff for F being Subset-Family of M st F is being_ball-family &amp; F is Cover of M holds
ex G being Subset-Family of M st
( G c= F &amp; G is Cover of M &amp; G is finite ) )
proofend;

:: REAL as topological space
definition
func R^1  ->  TopSpace equals :: TOPMETR:def 6
 TopSpaceMetr RealSpace;
correctness
coherence
TopSpaceMetr RealSpace is TopSpace;
;
end;

:: deftheorem  defines R^1 TOPMETR:def_6_:_
 R^1 = TopSpaceMetr RealSpace;

registration
cluster R^1  ->  non empty strict ;
coherence
 ( R^1 is strict &amp; not R^1 is empty ) ;
end;

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

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

:: deftheorem  defines Closed-Interval-TSpace TOPMETR:def_7_:_
 for a, b being real number holds Closed-Interval-TSpace (a,b) = TopSpaceMetr (Closed-Interval-MSpace (a,b));

theorem Th18: :: TOPMETR:18
for a, b being real number st a <= b holds
the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by Th10;

theorem Th19: :: TOPMETR:19
for a, b being real number st a <= b holds
for P being Subset of R^1 st P = [.a,b.] holds
Closed-Interval-TSpace (a,b) = R^1 | P
proofend;

theorem Th20: :: TOPMETR:20
Closed-Interval-TSpace (0,1) = I[01]
proofend;

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

Lm2:  for a, b, r being real number st r >= 0 &amp; a + r <= b holds
a <= b
proofend;

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
proofend;

::Moved from JORDAN16:6, AK 20.02.2006
theorem :: TOPMETR:22
for T being non empty TopSpace
for A, B being Subset of T st A c= B holds
T | A is SubSpace of T | B
proofend;

::Moved from JGRAPH_5:6,7, AK 20.02.2006
theorem Th23: :: TOPMETR:23
for a, b, d, e being real number
for B being Subset of (Closed-Interval-TSpace (d,e)) st d <= a &amp; a <= b &amp; b <= e &amp; B = [.a,b.] holds
Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B
proofend;

theorem :: TOPMETR:24
for a, b being real number
for B being Subset of I[01] st 0 <= a &amp; a <= b &amp; b <= 1 &amp; 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 ;
attrT is real-membered  means :Def8: :: TOPMETR:def 8
 the carrier of T is real-membered ;
end;

:: deftheorem Def8 defines real-membered TOPMETR:def_8_:_
 for T being 1-sorted holds
( T is real-membered iff the carrier of T is real-membered );

registration
cluster I[01]  ->  real-membered ;
coherence
 I[01] is real-membered
proofend;
end;

:: from RCOMP_3, 2007.04.08, A,T.
registration
cluster non empty real-membered for 1-sorted ;
existence
 ex b1 being 1-sorted st
( not b1 is empty &amp; b1 is real-membered )
proofend;
end;

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

:: from BORSUK_6, 2010.03.07, A.T.
registration
cluster R^1  ->  real-membered ;
coherence
 R^1 is real-membered
proofend;
end;

:: from BORSUK_6, 2010.05.31, A.K.
registration
cluster non empty strict TopSpace-like real-membered for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is strict &amp; not b1 is empty &amp; b1 is real-membered )
proofend;
end;

registration
let T be real-membered TopStruct ;
cluster  ->  real-membered for SubSpace of T;
coherence
 for b1 being SubSpace of T holds b1 is real-membered
proofend;
end;

:: from EUCLID_9, 2010.10.05, A.K.
registration
cluster RealSpace  ->  real-membered ;
coherence
 RealSpace is real-membered
proofend;
end;