:: Metric Spaces as Topological Spaces - Fundamental Concepts
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991 Association of Mizar Users

theorem Th1: :: 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 12;

theorem :: TOPMETR:2

canceled;

theorem :: TOPMETR:3

for T being non empty TopSpace
for A being non empty SubSpace of T st T is T_2 holds
A is T_2

proof end;

theorem Th4: :: TOPMETR:4

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

proof end;

theorem Th5: :: TOPMETR:5

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

proof end;

theorem :: TOPMETR:6

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 p' being Point of (T | P)
for Q' being Subset of (T | P) st Q' = Q /\ P & p' = p holds
Q' is a_neighborhood of p'

proof end;

theorem :: TOPMETR:7

canceled;

theorem :: TOPMETR:8

canceled;

theorem :: TOPMETR:9

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

proof end;

theorem :: TOPMETR:10

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

proof end;

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

proof end;

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 b₁ being MetrSpace st
( the carrier of b₁ c= the carrier of M & ( for x, y being Point of b₁ holds the distance of b₁ . x,y = the distance of M . x,y ) )

proof end;

end;

:: deftheorem Def1 defines SubSpace TOPMETR:def 1 :

for M, b₂ being MetrSpace holds
( b₂ is SubSpace of M iff ( the carrier of b₂ c= the carrier of M & ( for x, y being Point of b₂ holds the distance of b₂ . x,y = the distance of M . x,y ) ) );

registration

let M be MetrSpace;
cluster strict SubSpace of M;
existence
ex b₁ being SubSpace of M st b₁ is strict

proof end;

end;

registration

let M be non empty MetrSpace;
cluster non empty strict SubSpace of M;
existence
ex b₁ being SubSpace of M st
( b₁ is strict & not b₁ is empty )

proof end;

end;

theorem :: TOPMETR:11

canceled;

theorem Th12: :: TOPMETR:12

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

proof end;

theorem Th13: :: TOPMETR:13

for r being real number
for M being MetrSpace
for A being SubSpace of M
for x being Point of M
for x' being Point of A st x = x' holds
Ball x',r = (Ball x,r) /\ the carrier of A

proof end;

definition

let M be non empty MetrSpace;
let A be non empty Subset of M;
func M | A -> strict SubSpace of M means :Def2: :: TOPMETR:def 2
the carrier of it = A;
existence
ex b₁ being strict SubSpace of M st the carrier of b₁ = A

proof end;

uniqueness
for b₁, b₂ being strict SubSpace of M st the carrier of b₁ = A & the carrier of b₂ = A holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines | TOPMETR:def 2 :

for M being non empty MetrSpace
for A being non empty Subset of M
for b₃ being strict SubSpace of M holds
( b₃ = M | A iff the carrier of b₃ = A );

registration

let M be non empty MetrSpace;
let A be non empty Subset of M;
cluster M | 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 b₁ being non empty strict SubSpace of RealSpace st
for P being non empty Subset of RealSpace st P = [.a,b.] holds
b₁ = RealSpace | P

proof end;

uniqueness
for b₁, b₂ being non empty strict SubSpace of RealSpace st ( for P being non empty Subset of RealSpace st P = [.a,b.] holds
b₁ = RealSpace | P ) & ( for P being non empty Subset of RealSpace st P = [.a,b.] holds
b₂ = RealSpace | P ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Closed-Interval-MSpace TOPMETR:def 3 :

for a, b being real number st a <= b holds
for b₃ being non empty strict SubSpace of RealSpace holds
( b₃ = Closed-Interval-MSpace a,b iff for P being non empty Subset of RealSpace st P = [.a,b.] holds
b₃ = RealSpace | P );

theorem Th14: :: TOPMETR:14

for a, b being real number st a <= b holds
the carrier of (Closed-Interval-MSpace a,b) = [.a,b.]

proof end;

definition

let M be MetrStruct ;
let F be Subset-Family of M;
attr F 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 Th15: :: TOPMETR:15

for p, q being Point of RealSpace
for x, y being real number st x = p & y = q holds
dist p,q = abs (x - y)

proof end;

theorem Th16: :: 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 )

proof end;

theorem :: TOPMETR:17

canceled;

theorem :: TOPMETR:18

canceled;

theorem Th19: :: TOPMETR:19

for M being non empty MetrSpace
for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M

proof end;

theorem :: TOPMETR:20

canceled;

theorem Th21: :: TOPMETR:21

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

proof end;

theorem Th22: :: TOPMETR:22

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 & Ball p,r c= P ) )

proof end;

definition

canceled;
let M be MetrStruct ;
attr M is compact means :Def6: :: TOPMETR:def 6
TopSpaceMetr M is compact;

end;

:: deftheorem TOPMETR:def 5 :

canceled;

:: deftheorem Def6 defines compact TOPMETR:def 6 :

for M being MetrStruct holds
( M is compact iff TopSpaceMetr M is compact );

theorem :: TOPMETR:23

for M being non empty MetrSpace holds
( M is compact iff for F being Subset-Family of M st F is being_ball-family & F is Cover of M holds
ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) )

proof end;

definition

func R^1 -> strict TopSpace equals :: TOPMETR:def 7
TopSpaceMetr RealSpace ;
correctness
coherence
TopSpaceMetr RealSpace is strict TopSpace;
;

end;

:: deftheorem defines R^1 TOPMETR:def 7 :

R^1 = TopSpaceMetr RealSpace ;

registration

cluster R^1 -> non empty strict ;
coherence
not R^1 is empty ;

end;

theorem Th24: :: TOPMETR:24

the carrier of R^1 = REAL

proof end;

registration

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

proof end;

end;

definition

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

end;

:: deftheorem defines Closed-Interval-TSpace TOPMETR:def 8 :

for a, b being real number holds Closed-Interval-TSpace a,b = TopSpaceMetr (Closed-Interval-MSpace a,b);

theorem Th25: :: TOPMETR:25

for a, b being real number st a <= b holds
the carrier of (Closed-Interval-TSpace a,b) = [.a,b.]

proof end;

theorem Th26: :: TOPMETR:26

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

proof end;

theorem Th27: :: TOPMETR:27

Closed-Interval-TSpace 0 ,1 = I[01]

proof end;

definition

:: original: I[01]
redefine func I[01] -> strict SubSpace of R^1 ;
coherence
I[01] is strict SubSpace of R^1 by Th27;

end;

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

proof end;

theorem :: TOPMETR:28

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

theorem :: TOPMETR:29

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

proof end;

theorem Th30: :: TOPMETR:30

for a, b, d, e being real number
for 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 end;

theorem :: TOPMETR:31

for a, b being real number
for 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 Th27, Th30;