:: TOPMETR semantic presentation
begin
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
proof
let T be non empty TopSpace; ::_thesis: for A being non empty SubSpace of T st T is T_2 holds
A is T_2
let A be non empty SubSpace of T; ::_thesis: ( T is T_2 implies A is T_2 )
assume A1: T is T_2 ; ::_thesis: A is T_2
for p, q being Point of A st not p = q holds
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; ::_thesis: ( not p = q implies ex W, V being Subset of A st
( W is open & V is open & p in W & q in V & W misses V ) )
assume A2: not p = q ; ::_thesis: ex W, V being Subset of A st
( W is open & V is open & p in W & q in V & W misses V )
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 ; ::_thesis: ex V being Subset of A st
( W9 is open & V is open & p in W9 & q in V & W9 misses V )
take V9 ; ::_thesis: ( W9 is open & V9 is open & p in W9 & q in V9 & W9 misses 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; ::_thesis: ( p in W9 & q in V9 & W9 misses V9 )
thus ( p in W9 & q in V9 ) by A5, XBOOLE_0:def_4; ::_thesis: W9 misses V9
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 W9 misses V9 by XBOOLE_0:def_7; ::_thesis: verum
end;
hence A is T_2 by PRE_TOPC:def_10; ::_thesis: verum
end;
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
proof
let T be TopSpace; ::_thesis: for A, B being SubSpace of T st the carrier of A c= the carrier of B holds
A is SubSpace of B
let A, B be SubSpace of T; ::_thesis: ( the carrier of A c= the carrier of B implies A is SubSpace of B )
assume A1: the carrier of A c= the carrier of B ; ::_thesis: A is SubSpace 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; ::_thesis: ( P in the topology of A iff ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] 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) ) ) ::_thesis: ( ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) ) implies P in the topology of A )
proof
assume P in the topology of A ; ::_thesis: ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] 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 ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) ) by A5; ::_thesis: verum
end;
given Q being Subset of B such that A6: Q in the topology of B and
A7: P = Q /\ ([#] A) ; ::_thesis: P in the topology of 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 P in the topology of A by A8, PRE_TOPC:def_4; ::_thesis: verum
end;
the carrier of A c= [#] B by A1;
hence A is SubSpace of B by A2, PRE_TOPC:def_4; ::_thesis: verum
end;
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) )
proof
let T be non empty TopSpace; ::_thesis: for P, Q being Subset of T holds
( T | P is SubSpace of T | (P \/ Q) & T | Q is SubSpace of T | (P \/ Q) )
let P, Q be Subset of T; ::_thesis: ( T | P is SubSpace of T | (P \/ Q) & T | Q is SubSpace of T | (P \/ Q) )
( [#] (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; ::_thesis: T | Q is SubSpace of T | (P \/ Q)
( [#] (T | Q) = Q & [#] (T | (P \/ Q)) = P \/ Q ) by PRE_TOPC:def_5;
hence T | Q is SubSpace of T | (P \/ Q) by Th3, XBOOLE_1:7; ::_thesis: verum
end;
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
proof
let T be non empty TopSpace; ::_thesis: 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
let p be Point of T; ::_thesis: 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
let P be non empty Subset of T; ::_thesis: ( p in P implies 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 )
assume A1: p in P ; ::_thesis: 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
let Q be a_neighborhood of p; ::_thesis: 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
let p9 be Point of (T | P); ::_thesis: for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds
Q9 is a_neighborhood of p9
let Q9 be Subset of (T | P); ::_thesis: ( Q9 = Q /\ P & p9 = p implies Q9 is a_neighborhood of p9 )
assume that
A2: Q9 = Q /\ P and
A3: p9 = p ; ::_thesis: Q9 is a_neighborhood of p9
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 Q9 is a_neighborhood of p9 by CONNSP_2:def_1; ::_thesis: verum
end;
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
proof
let A, B be TopSpace; ::_thesis: 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
let f be Function of A,B; ::_thesis: 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
let C be Subset of B; ::_thesis: ( f is continuous implies for h being Function of A,(B | C) st h = f holds
h is continuous )
assume A1: f is continuous ; ::_thesis: for h being Function of A,(B | C) st h = f holds
h is continuous
A2: the carrier of (B | C) = [#] (B | C)
.= C by PRE_TOPC:def_5 ;
let h be Function of A,(B | C); ::_thesis: ( h = f implies h is continuous )
assume A3: h = f ; ::_thesis: h is continuous
A4: rng f c= the carrier of (B | C) by A3, RELAT_1:def_19;
for P being Subset of (B | C) st P is closed holds
h " P is closed
proof
let P be Subset of (B | C); ::_thesis: ( P is closed implies h " P is closed )
assume P is closed ; ::_thesis: h " 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 h " P is closed by A1, A5, PRE_TOPC:def_6; ::_thesis: verum
end;
hence h is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;
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
proof
let X be TopStruct ; ::_thesis: 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
let Y be non empty TopStruct ; ::_thesis: 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
let K0 be Subset of X; ::_thesis: 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
let f be Function of X,Y; ::_thesis: for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds
g is continuous
let g be Function of (X | K0),Y; ::_thesis: ( f is continuous & g = f | K0 implies g is continuous )
assume that
A1: f is continuous and
A2: g = f | K0 ; ::_thesis: g is continuous
A3: [#] Y <> {} ;
for G being Subset of Y st G is open holds
g " G is open
proof
let G be Subset of Y; ::_thesis: ( G is open implies g " G is open )
[#] (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 ; ::_thesis: g " G is open
then f " G is open by A3, A1, TOPS_2:43;
hence g " G is open by A4, TOPS_2:24; ::_thesis: verum
end;
hence g is continuous by A3, TOPS_2:43; ::_thesis: verum
end;
Lm1: for M being MetrSpace holds MetrStruct(# the carrier of M, the distance of M #) is MetrSpace
proof
let M be MetrSpace; ::_thesis: MetrStruct(# the carrier of M, the distance of M #) is MetrSpace
now__::_thesis:_for_a,_b,_c_being_Element_of_MetrStruct(#_the_carrier_of_M,_the_distance_of_M_#)_holds_
(_(_dist_(a,b)_=_0_implies_a_=_b_)_&_(_a_=_b_implies_dist_(a,b)_=_0_)_&_dist_(a,b)_=_dist_(b,a)_&_dist_(a,c)_<=_(dist_(a,b))_+_(dist_(b,c))_)
let a, b, c be Element of MetrStruct(# the carrier of M, the distance of M #); ::_thesis: ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
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, METRIC_1:2; ::_thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
dist (b,a) = the distance of M . (b,a)
.= dist (b9,a9) ;
hence dist (a,b) = dist (b,a) by A2; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
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; ::_thesis: verum
end;
hence MetrStruct(# the carrier of M, the distance of M #) is MetrSpace by METRIC_1:6; ::_thesis: verum
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 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) ) )
proof
reconsider MM = MetrStruct(# the carrier of M, the distance of M #) as MetrSpace by Lm1;
take MM ; ::_thesis: ( the carrier of MM c= the carrier of M & ( for x, y being Point of MM holds the distance of MM . (x,y) = the distance of M . (x,y) ) )
thus the carrier of MM c= the carrier of M ; ::_thesis: for x, y being Point of MM holds the distance of MM . (x,y) = the distance of M . (x,y)
let x, y be Point of MM; ::_thesis: the distance of MM . (x,y) = the distance of M . (x,y)
thus the distance of MM . (x,y) = the distance of M . (x,y) ; ::_thesis: verum
end;
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
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 ex b1 being SubSpace of M st b1 is strict ; ::_thesis: verum
end;
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 )
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 ex b1 being SubSpace of M st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
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
proof
let M be non empty MetrSpace; ::_thesis: for A being non empty SubSpace of M
for p being Point of A holds p is Point of M
let A be non empty SubSpace of M; ::_thesis: for p being Point of A holds p is Point of M
let p be Point of A; ::_thesis: p is Point of M
( p in the carrier of A & the carrier of A c= the carrier of M ) by Def1;
hence p is Point of M ; ::_thesis: verum
end;
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
proof
let r be real number ; ::_thesis: 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
let M be MetrSpace; ::_thesis: 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
let A be SubSpace of M; ::_thesis: 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
let x be Point of M; ::_thesis: for x9 being Point of A st x = x9 holds
Ball (x9,r) = (Ball (x,r)) /\ the carrier of A
let x9 be Point of A; ::_thesis: ( x = x9 implies Ball (x9,r) = (Ball (x,r)) /\ the carrier of A )
assume A1: x = x9 ; ::_thesis: Ball (x9,r) = (Ball (x,r)) /\ the carrier of A
now__::_thesis:_for_a_being_set_st_a_in_Ball_(x9,r)_holds_
a_in_(Ball_(x,r))_/\_the_carrier_of_A
let a be set ; ::_thesis: ( a in Ball (x9,r) implies a in (Ball (x,r)) /\ the carrier of A )
assume A2: a in Ball (x9,r) ; ::_thesis: a in (Ball (x,r)) /\ the carrier of A
then reconsider y9 = a as Point of A ;
the carrier of A c= the carrier of M by Def1;
then A3: not M is empty by A2;
not A is 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; ::_thesis: verum
end;
then A4: Ball (x9,r) c= (Ball (x,r)) /\ the carrier of A by TARSKI:def_3;
now__::_thesis:_for_a_being_set_st_a_in_(Ball_(x,r))_/\_the_carrier_of_A_holds_
a_in_Ball_(x9,r)
let a be set ; ::_thesis: ( a in (Ball (x,r)) /\ the carrier of A implies a in Ball (x9,r) )
assume A5: a in (Ball (x,r)) /\ the carrier of A ; ::_thesis: a in Ball (x9,r)
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 ;
not the carrier of A is empty by A5;
then not A is empty ;
hence a in Ball (x9,r) by A6, METRIC_1:11; ::_thesis: verum
end;
then (Ball (x,r)) /\ the carrier of A c= Ball (x9,r) by TARSKI:def_3;
hence Ball (x9,r) = (Ball (x,r)) /\ the carrier of A by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
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
proof
reconsider B = A as non empty set ;
set d = the distance of M || A;
A1: dom ( the distance of M || A) = (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 ;
the distance of M || A = the distance of M | [:A,A:] ;
then rng ( the distance of M || A) c= REAL by RELAT_1:def_19;
then reconsider d = the distance of M || A as Function of [:B,B:],REAL by A1, FUNCT_2:def_1, RELSET_1:4;
set MM = MetrStruct(# B,d #);
A2: now__::_thesis:_for_a,_b_being_Element_of_MetrStruct(#_B,d_#)_holds_dist_(a,b)_=_the_distance_of_M_._(a,b)
let a, b be Element of MetrStruct(# B,d #); ::_thesis: dist (a,b) = the distance of M . (a,b)
thus dist (a,b) = the distance of MetrStruct(# B,d #) . (a,b)
.= the distance of M . [a,b] by A1, FUNCT_1:47
.= the distance of M . (a,b) ; ::_thesis: verum
end;
now__::_thesis:_for_a,_b,_c_being_Element_of_MetrStruct(#_B,d_#)_holds_
(_(_dist_(a,b)_=_0_implies_a_=_b_)_&_(_a_=_b_implies_dist_(a,b)_=_0_)_&_dist_(a,b)_=_dist_(b,a)_&_dist_(a,c)_<=_(dist_(a,b))_+_(dist_(b,c))_)
let a, b, c be Element of MetrStruct(# B,d #); ::_thesis: ( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
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, METRIC_1:2; ::_thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
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 ; ::_thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
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; ::_thesis: verum
end;
then reconsider MM = MetrStruct(# B,d #) as MetrSpace by METRIC_1:6;
now__::_thesis:_for_x,_y_being_Point_of_MM_holds_the_distance_of_MM_._(x,y)_=_the_distance_of_M_._(x,y)
let x, y be Point of MM; ::_thesis: the distance of MM . (x,y) = the distance of M . (x,y)
thus the distance of MM . (x,y) = dist (x,y)
.= the distance of M . (x,y) by A2 ; ::_thesis: verum
end;
then reconsider MM = MM as strict SubSpace of M by Def1;
take MM ; ::_thesis: the carrier of MM = A
thus the carrier of MM = A ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict SubSpace of M st the carrier of b1 = A & the carrier of b2 = A holds
b1 = b2
proof
let S1, S2 be strict SubSpace of M; ::_thesis: ( the carrier of S1 = A & the carrier of S2 = A implies S1 = S2 )
assume that
A5: the carrier of S1 = A and
A6: the carrier of S2 = A ; ::_thesis: S1 = S2
now__::_thesis:_for_a,_b_being_Element_of_A_holds_the_distance_of_S1_._(a,b)_=_the_distance_of_S2_._(a,b)
let a, b be Element of A; ::_thesis: the distance of S1 . (a,b) = the distance of S2 . (a,b)
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 ; ::_thesis: verum
end;
hence S1 = S2 by A5, A6, BINOP_1:2; ::_thesis: verum
end;
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
proof
reconsider P = [.a,b.] as Subset of RealSpace ;
reconsider P = P as non empty Subset of RealSpace by A1, XXREAL_1:1;
take RealSpace | P ; ::_thesis: for P being non empty Subset of RealSpace st P = [.a,b.] holds
RealSpace | P = RealSpace | P
thus for P being non empty Subset of RealSpace st P = [.a,b.] holds
RealSpace | P = RealSpace | P ; ::_thesis: verum
end;
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 ) & ( for P being non empty Subset of RealSpace st P = [.a,b.] holds
b2 = RealSpace | P ) holds
b1 = b2
proof
reconsider P = [.a,b.] as Subset of RealSpace ;
reconsider P = P as non empty Subset of RealSpace by A1, XXREAL_1:1;
let S1, S2 be non empty strict SubSpace of RealSpace ; ::_thesis: ( ( for P being non empty Subset of RealSpace st P = [.a,b.] holds
S1 = RealSpace | P ) & ( for P being non empty Subset of RealSpace st P = [.a,b.] holds
S2 = RealSpace | P ) implies S1 = S2 )
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 ; ::_thesis: S1 = S2
thus S1 = RealSpace | P by A2
.= S2 by A3 ; ::_thesis: verum
end;
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.]
proof
let a, b be real number ; ::_thesis: ( a <= b implies the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] )
assume A1: a <= b ; ::_thesis: the carrier of (Closed-Interval-MSpace (a,b)) = [.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 ; ::_thesis: verum
end;
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 & y = q holds
dist (p,q) = abs (x - y) by METRIC_1:def_12;
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 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
proof
let M be non empty MetrSpace; ::_thesis: for A being non empty SubSpace of M holds TopSpaceMetr A is SubSpace of TopSpaceMetr M
let A be non empty SubSpace of M; ::_thesis: TopSpaceMetr A is SubSpace of TopSpaceMetr M
set T = TopSpaceMetr M;
set R = TopSpaceMetr A;
thus [#] (TopSpaceMetr A) c= [#] (TopSpaceMetr M) by Def1; :: according to PRE_TOPC:def_4 ::_thesis: for b1 being Element of bool the carrier of (TopSpaceMetr A) holds
( ( not b1 in the topology of (TopSpaceMetr A) or ex b2 being Element of bool the carrier of (TopSpaceMetr M) st
( b2 in the topology of (TopSpaceMetr M) & b1 = b2 /\ ([#] (TopSpaceMetr A)) ) ) & ( for b2 being Element of bool the carrier of (TopSpaceMetr M) holds
( not b2 in the topology of (TopSpaceMetr M) or not b1 = b2 /\ ([#] (TopSpaceMetr A)) ) or b1 in the topology of (TopSpaceMetr A) ) )
let P be Subset of (TopSpaceMetr A); ::_thesis: ( ( not P in the topology of (TopSpaceMetr A) or ex b1 being Element of bool the carrier of (TopSpaceMetr M) st
( b1 in the topology of (TopSpaceMetr M) & P = b1 /\ ([#] (TopSpaceMetr A)) ) ) & ( for b1 being Element of bool the carrier of (TopSpaceMetr M) holds
( not b1 in the topology of (TopSpaceMetr M) or not P = b1 /\ ([#] (TopSpaceMetr A)) ) or P in the topology of (TopSpaceMetr A) ) )
thus ( P in the topology of (TopSpaceMetr A) implies ex Q being Subset of (TopSpaceMetr M) st
( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) ) ) ::_thesis: ( for b1 being Element of bool the carrier of (TopSpaceMetr M) holds
( not b1 in the topology of (TopSpaceMetr M) or not P = b1 /\ ([#] (TopSpaceMetr A)) ) or P in the topology of (TopSpaceMetr A) )
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 { (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 ) } holds
X c= the carrier of M
proof
let X be set ; ::_thesis: ( X in { (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 ) } implies X c= the carrier of M )
assume X in { (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 ) } ; ::_thesis: X c= the carrier of M
then ex x being Point of M ex r being Real st
( X = Ball (x,r) & x in P & r > 0 & (Ball (x,r)) /\ the carrier of A c= P ) ;
hence X c= the carrier of M ; ::_thesis: verum
end;
then reconsider Q = union { (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 ) } as Subset of M by ZFMISC_1:76;
reconsider Q9 = Q as Subset of (TopSpaceMetr M) ;
assume P in the topology of (TopSpaceMetr A) ; ::_thesis: ex Q being Subset of (TopSpaceMetr M) st
( Q in the topology of (TopSpaceMetr M) & P = Q /\ ([#] (TopSpaceMetr A)) )
then A1: P in Family_open_set A ;
A2: P c= Q9 /\ ([#] (TopSpaceMetr A))
proof
reconsider P9 = P as Subset of A ;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in P or a in Q9 /\ ([#] (TopSpaceMetr A)) )
assume A3: a in P ; ::_thesis: a in Q9 /\ ([#] (TopSpaceMetr A))
then reconsider x = a as Point of A ;
reconsider x9 = x as Point of M by Th8;
consider r being Real 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 { (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 ) } by A3, A4, A5;
x9 in Ball (x9,r) by A4, TBSP_1:11;
then a in Q9 by A6, TARSKI:def_4;
hence a in Q9 /\ ([#] (TopSpaceMetr A)) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
take Q9 ; ::_thesis: ( Q9 in the topology of (TopSpaceMetr M) & P = Q9 /\ ([#] (TopSpaceMetr A)) )
for x being Point of M st x in Q holds
ex r being Real st
( r > 0 & Ball (x,r) c= Q )
proof
let x be Point of M; ::_thesis: ( x in Q implies ex r being Real st
( r > 0 & Ball (x,r) c= Q ) )
assume x in Q ; ::_thesis: ex r being Real st
( r > 0 & Ball (x,r) c= Q )
then consider Y being set such that
A7: x in Y and
A8: Y in { (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 ) } 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 ; ::_thesis: ( p > 0 & Ball (x,p) c= Q )
thus p > 0 by A10; ::_thesis: Ball (x,p) c= Q
Y c= Q by A8, ZFMISC_1:74;
hence Ball (x,p) c= Q by A9, A11, XBOOLE_1:1; ::_thesis: verum
end;
then Q in Family_open_set M by PCOMPS_1:def_4;
hence Q9 in the topology of (TopSpaceMetr M) ; ::_thesis: P = Q9 /\ ([#] (TopSpaceMetr A))
Q9 /\ ([#] (TopSpaceMetr A)) c= P
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Q9 /\ ([#] (TopSpaceMetr A)) or a in P )
assume A12: a in Q9 /\ ([#] (TopSpaceMetr A)) ; ::_thesis: a in P
then a in Q9 by XBOOLE_0:def_4;
then consider Y being set such that
A13: a in Y and
A14: Y in { (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 ) } 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 a in P by A16; ::_thesis: verum
end;
hence P = Q9 /\ ([#] (TopSpaceMetr A)) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
reconsider P9 = P as Subset of A ;
given Q being Subset of (TopSpaceMetr M) such that A17: Q in the topology of (TopSpaceMetr M) and
A18: P = Q /\ ([#] (TopSpaceMetr A)) ; ::_thesis: P in the topology of (TopSpaceMetr A)
reconsider Q9 = Q as Subset of M ;
for p being Point of A st p in P9 holds
ex r being Real st
( r > 0 & Ball (p,r) c= P9 )
proof
let p be Point of A; ::_thesis: ( p in P9 implies ex r being Real st
( r > 0 & Ball (p,r) c= P9 ) )
reconsider p9 = p as Point of M by Th8;
assume p in P9 ; ::_thesis: ex r being Real st
( r > 0 & Ball (p,r) c= P9 )
then A19: p9 in Q9 by A18, XBOOLE_0:def_4;
Q9 in Family_open_set M by A17;
then consider r being Real 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 (TopSpaceMetr A) ;
hence ex r being Real st
( r > 0 & Ball (p,r) c= P9 ) by A18, A20; ::_thesis: verum
end;
then P in Family_open_set A by PCOMPS_1:def_4;
hence P in the topology of (TopSpaceMetr A) ; ::_thesis: verum
end;
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
proof
let r be real number ; ::_thesis: 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
let M be triangle MetrStruct ; ::_thesis: for p being Point of M
for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds
P is open
let p be Point of M; ::_thesis: for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds
P is open
let P be Subset of (TopSpaceMetr M); ::_thesis: ( P = Ball (p,r) implies P is open )
assume P = Ball (p,r) ; ::_thesis: P is open
then A1: P in Family_open_set M by PCOMPS_1:29;
thus P is open by A1, PRE_TOPC:def_2; ::_thesis: verum
end;
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 & Ball (p,r) c= P ) )
proof
let M be non empty MetrSpace; ::_thesis: 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 ) )
let P be Subset of (TopSpaceMetr M); ::_thesis: ( 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 ) )
reconsider P9 = P as Subset of M ;
thus ( P is open implies for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball (p,r) c= P ) ) ::_thesis: ( ( for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball (p,r) c= P ) ) implies P is open )
proof
assume P is open ; ::_thesis: for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball (p,r) c= P )
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; ::_thesis: ( p in P implies ex r being real number st
( r > 0 & Ball (p,r) c= P ) )
assume p in P ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= P )
then ex r being Real st
( r > 0 & Ball (p,r) c= P ) by A1, PCOMPS_1:def_4;
hence ex r being real number st
( r > 0 & Ball (p,r) c= P ) ; ::_thesis: verum
end;
assume A2: for p being Point of M st p in P holds
ex r being real number st
( r > 0 & Ball (p,r) c= P ) ; ::_thesis: P is open
for p being Point of M st p in P holds
ex r being Real st
( r > 0 & Ball (p,r) c= P )
proof
let p be Point of M; ::_thesis: ( p in P implies ex r being Real st
( r > 0 & Ball (p,r) c= P ) )
assume p in P ; ::_thesis: ex r being Real st
( r > 0 & Ball (p,r) c= P )
then consider r being real number such that
A3: ( r > 0 & Ball (p,r) c= P ) by A2;
reconsider r = r as Element of REAL by XREAL_0:def_1;
take r ; ::_thesis: ( r > 0 & Ball (p,r) c= P )
thus ( r > 0 & Ball (p,r) c= P ) by A3; ::_thesis: verum
end;
then P9 in Family_open_set M by PCOMPS_1:def_4;
hence P in the topology of (TopSpaceMetr M) ; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
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 & 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
let M be non empty MetrSpace; ::_thesis: ( 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 ) )
thus ( M is compact implies 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 ) ) ::_thesis: ( ( 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 ) ) implies M is compact )
proof
set TM = TopSpaceMetr M;
assume M is compact ; ::_thesis: 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 )
then A1: TopSpaceMetr M is compact by Def5;
let F be Subset-Family of M; ::_thesis: ( F is being_ball-family & F is Cover of M implies ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite ) )
reconsider TF = F as Subset-Family of (TopSpaceMetr M) ;
assume that
A2: F is being_ball-family and
A3: F is Cover of M ; ::_thesis: ex G being Subset-Family of M st
( G c= F & G is Cover of M & G is finite )
A4: TF is open
proof
let P be Subset of (TopSpaceMetr M); :: according to TOPS_2:def_1 ::_thesis: ( not P in TF or P is open )
reconsider P9 = P as Subset of M ;
assume P in TF ; ::_thesis: P is open
then ex p being Point of M ex r being Real st P9 = Ball (p,r) by A2, Def4;
hence P is open by Th14; ::_thesis: verum
end;
the carrier of M c= union F by A3, SETFAM_1:def_11;
then the carrier of (TopSpaceMetr M) c= union TF ;
then TF is Cover of (TopSpaceMetr M) by SETFAM_1:def_11;
then consider TG being Subset-Family of (TopSpaceMetr M) such that
A5: TG c= TF and
A6: TG is Cover of (TopSpaceMetr M) and
A7: TG is finite by A1, A4, COMPTS_1:def_1;
reconsider G = TG as Subset-Family of M ;
take G ; ::_thesis: ( G c= F & G is Cover of M & G is finite )
the carrier of (TopSpaceMetr M) c= union TG by A6, SETFAM_1:def_11;
then the carrier of M c= union G ;
hence ( G c= F & G is Cover of M & G is finite ) by A5, A7, SETFAM_1:def_11; ::_thesis: verum
end;
thus ( ( 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 ) ) implies M is compact ) ::_thesis: verum
proof
set TM = TopSpaceMetr M;
assume A8: 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 ) ; ::_thesis: M is compact
now__::_thesis:_for_F_being_Subset-Family_of_(TopSpaceMetr_M)_st_F_is_Cover_of_(TopSpaceMetr_M)_&_F_is_open_holds_
ex_GG_being_Subset-Family_of_(TopSpaceMetr_M)_st_
(_GG_c=_F_&_GG_is_Cover_of_(TopSpaceMetr_M)_&_GG_is_finite_)
let F be Subset-Family of (TopSpaceMetr M); ::_thesis: ( F is Cover of (TopSpaceMetr M) & F is open implies ex GG being Subset-Family of (TopSpaceMetr M) st
( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite ) )
set Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } ;
{ (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } c= bool the carrier of M
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } or a in bool the carrier of M )
assume a in { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } ; ::_thesis: a in bool the carrier of M
then ex p being Point of M ex r being Real st
( a = Ball (p,r) & ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) ) ;
hence a in bool the carrier of M ; ::_thesis: verum
end;
then reconsider Z = { (Ball (p,r)) where p is Point of M, r is Real : ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) } as Subset-Family of M ;
assume that
A9: F is Cover of (TopSpaceMetr M) and
A10: F is open ; ::_thesis: ex GG being Subset-Family of (TopSpaceMetr M) st
( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )
the carrier of M c= union Z
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of M or a in union Z )
assume a in the carrier of M ; ::_thesis: a in union Z
then reconsider p = a as Point of M ;
( the carrier of (TopSpaceMetr M) c= union F & the carrier of (TopSpaceMetr M) = 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 = P as Subset of (TopSpaceMetr M) 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 a in union Z by A15, TARSKI:def_4; ::_thesis: verum
end;
then A16: Z is Cover of M by SETFAM_1:def_11;
reconsider F9 = F as non empty Subset-Family of (TopSpaceMetr M) by A9, TOPS_2:3;
defpred S1[ set , set ] means $1 c= $2;
Z is being_ball-family
proof
let P be set ; :: according to TOPMETR:def_4 ::_thesis: ( P in Z implies ex p being Point of M ex r being Real st P = Ball (p,r) )
assume P in Z ; ::_thesis: ex p being Point of M ex r being Real st P = Ball (p,r)
then ex p being Point of M ex r being Real st
( P = Ball (p,r) & ex P being Subset of (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) ) ;
hence ex p being Point of M ex r being Real st P = Ball (p,r) ; ::_thesis: verum
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 holds
ex u being set st
( u in F9 & S1[a,u] )
proof
let a be set ; ::_thesis: ( a in G implies ex u being set st
( u in F9 & S1[a,u] ) )
assume a in G ; ::_thesis: ex u being set st
( u in F9 & S1[a,u] )
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 (TopSpaceMetr M) st
( P in F & Ball (p,r) c= P ) ;
consider P being Subset of (TopSpaceMetr M) such that
A23: ( P in F & Ball (p,r) c= P ) by A22;
take P ; ::_thesis: ( P in F9 & S1[a,P] )
thus ( P in F9 & S1[a,P] ) by A21, A23; ::_thesis: verum
end;
consider f being Function of G,F9 such that
A24: for a being set st a in G holds
S1[a,f . a] from FUNCT_2:sch_1(A20);
reconsider GG = rng f as Subset-Family of (TopSpaceMetr M) by TOPS_2:2;
take GG = GG; ::_thesis: ( GG c= F & GG is Cover of (TopSpaceMetr M) & GG is finite )
thus GG c= F ; ::_thesis: ( GG is Cover of (TopSpaceMetr M) & GG is finite )
the carrier of (TopSpaceMetr M) c= union GG
proof
A25: ( the carrier of (TopSpaceMetr M) = the carrier of M & the carrier of M c= union G ) by A18, SETFAM_1:def_11;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of (TopSpaceMetr M) or a in union GG )
assume a in the carrier of (TopSpaceMetr M) ; ::_thesis: a in union GG
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 a in union GG by A26, A28, TARSKI:def_4; ::_thesis: verum
end;
hence GG is Cover of (TopSpaceMetr M) by SETFAM_1:def_11; ::_thesis: GG is finite
dom f = G by FUNCT_2:def_1;
hence GG is finite by A19, FINSET_1:8; ::_thesis: verum
end;
then TopSpaceMetr M is compact by COMPTS_1:def_1;
hence M is compact by Def5; ::_thesis: verum
end;
end;
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 & 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
proof
let a, b be real number ; ::_thesis: ( a <= b implies for P being Subset of R^1 st P = [.a,b.] holds
Closed-Interval-TSpace (a,b) = R^1 | P )
assume A1: a <= b ; ::_thesis: for P being Subset of R^1 st P = [.a,b.] holds
Closed-Interval-TSpace (a,b) = R^1 | P
let P be Subset of R^1; ::_thesis: ( P = [.a,b.] implies Closed-Interval-TSpace (a,b) = R^1 | P )
assume P = [.a,b.] ; ::_thesis: Closed-Interval-TSpace (a,b) = R^1 | P
then [#] (Closed-Interval-TSpace (a,b)) = P by A1, Th18;
hence Closed-Interval-TSpace (a,b) = R^1 | P by PRE_TOPC:def_5; ::_thesis: verum
end;
theorem Th20: :: TOPMETR:20
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 (TopSpaceMetr RealSpace) ;
thus Closed-Interval-TSpace (0,1) = (TopSpaceMetr RealSpace) | P9 by Th19
.= I[01] by BORSUK_1:def_13 ; ::_thesis: verum
end;
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 & a + r <= b holds
a <= b
proof
let a, b, r be real number ; ::_thesis: ( r >= 0 & a + r <= b implies a <= b )
assume ( r >= 0 & a + r <= b ) ; ::_thesis: a <= b
then ( (a + r) - r <= b - r & b - r <= b ) by XREAL_1:9, XREAL_1:43;
hence a <= b by XXREAL_0:2; ::_thesis: verum
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
proof
let f be Function of R^1,R^1; ::_thesis: ( ex a, b being Real st
for x being Real holds f . x = (a * x) + b implies f is continuous )
given a, b being Real such that A1: for x being Real holds f . x = (a * x) + b ; ::_thesis: f is continuous
for W being Point of R^1
for 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; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
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__::_thesis:_ex_H_being_a_neighborhood_of_W_st_f_.:_H_c=_G
percases ( a = 0 or a <> 0 ) ;
supposeA8: a = 0 ; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
set H = [#] R^1;
W in [#] R^1 ;
then W in Int ([#] R^1) by TOPS_1:23;
then reconsider H = [#] R^1 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 ; ::_thesis: ( y in {b} iff ex x being set st
( x in dom f & x in H & y = f . x ) )
thus ( y in {b} implies ex x being set st
( x in dom f & x in H & y = f . x ) ) ::_thesis: ( ex x being set st
( x in dom f & x in H & y = f . x ) implies y in {b} )
proof
assume A9: y in {b} ; ::_thesis: ex x being set st
( x in dom f & x in H & y = f . x )
take 0 ; ::_thesis: ( 0 in dom f & 0 in H & y = f . 0 )
dom f = the carrier of R^1 by FUNCT_2:def_1;
hence ( 0 in dom f & 0 in H ) ; ::_thesis: y = f . 0
thus f . 0 = (0 * 0) + b by A1, A8
.= y by A9, TARSKI:def_1 ; ::_thesis: verum
end;
given x being set such that A10: x in dom f and
x in H and
A11: y = f . x ; ::_thesis: y in {b}
reconsider x = x as Real by A10;
y = (0 * x) + b by A1, A8, A11
.= b ;
hence y in {b} by TARSKI:def_1; ::_thesis: verum
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 ex H being a_neighborhood of W st f .: H c= G ; ::_thesis: verum
end;
supposeA14: a <> 0 ; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
reconsider W9 = W as Point of RealSpace ;
set d = r / (2 * (abs a));
reconsider H = Ball (W9,(r / (2 * (abs a)))) 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 = 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 ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: H or y in Ball (Y,r) )
reconsider Y9 = Y as Real ;
assume y in f .: H ; ::_thesis: y in Ball (Y,r)
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) < r / (2 * (abs a)) by A18, METRIC_1:11;
then abs (W99 - x99) < r / (2 * (abs a)) by Th11;
then (abs a) * (abs (W99 - x99)) < (abs a) * (r / (2 * (abs a))) by A20, XREAL_1:68;
then abs (a * (W99 - x99)) < (abs a) * (r / (2 * (abs a))) by COMPLEX1:65;
then abs (((a * W99) + b) - ((a * x99) + b)) < (abs a) * (r / (2 * (abs a))) ;
then abs (Y9 - ((a * x99) + b)) < (abs a) * (r / (2 * (abs a))) by A1;
then A21: abs (Y9 - y9) < (abs a) * (r / (2 * (abs a))) by A1, A19;
abs a <> 0 by A14, ABSVALUE:2;
then A22: (abs a) * (r / (2 * (abs a))) = 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 y in Ball (Y,r) by METRIC_1:11; ::_thesis: verum
end;
Ball (Y,r) c= G by A4, A7, XBOOLE_1:1;
hence ex H being a_neighborhood of W st f .: H c= G by A16, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence ex H being a_neighborhood of W st f .: H c= G ; ::_thesis: verum
end;
hence f is continuous by BORSUK_1:def_1; ::_thesis: verum
end;
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
proof
let T be non empty TopSpace; ::_thesis: for A, B being Subset of T st A c= B holds
T | A is SubSpace of T | B
let A, B be Subset of T; ::_thesis: ( A c= B implies T | A is SubSpace of T | B )
assume A c= B ; ::_thesis: T | A is SubSpace of T | B
then A \/ B = B by XBOOLE_1:12;
hence T | A is SubSpace of T | B by Th4; ::_thesis: verum
end;
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 & 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 ; ::_thesis: 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
let B be Subset of (Closed-Interval-TSpace (d,e)); ::_thesis: ( d <= a & a <= b & b <= e & B = [.a,b.] implies Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B )
assume that
A1: d <= a and
A2: a <= b and
A3: b <= e and
A4: B = [.a,b.] ; ::_thesis: Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | 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 Closed-Interval-TSpace (a,b) = (Closed-Interval-TSpace (d,e)) | B by A4, A8, A7, PRE_TOPC:7; ::_thesis: verum
end;
theorem :: TOPMETR:24
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 Th20, Th23;
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
proof
thus the carrier of I[01] is real-membered by BORSUK_1:40; :: according to TOPMETR:def_8 ::_thesis: verum
end;
end;
registration
cluster non empty real-membered for 1-sorted ;
existence
ex b1 being 1-sorted st
( not b1 is empty & b1 is real-membered )
proof
take I[01] ; ::_thesis: ( not I[01] is empty & I[01] is real-membered )
thus ( not I[01] is empty & I[01] is real-membered ) ; ::_thesis: verum
end;
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;
registration
cluster R^1 -> real-membered ;
coherence
R^1 is real-membered
proof
let x be set ; :: according to MEMBERED:def_3,TOPMETR:def_8 ::_thesis: ( not x in the carrier of R^1 or x is real )
assume x in the carrier of R^1 ; ::_thesis: x is real
hence x is real ; ::_thesis: verum
end;
end;
registration
cluster non empty strict TopSpace-like real-membered for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & not b1 is empty & b1 is real-membered )
proof
take I[01] ; ::_thesis: ( I[01] is strict & not I[01] is empty & I[01] is real-membered )
thus ( I[01] is strict & not I[01] is empty & I[01] is real-membered ) ; ::_thesis: verum
end;
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
proof
let R be SubSpace of T; ::_thesis: R is real-membered
let x be set ; :: according to MEMBERED:def_3,TOPMETR:def_8 ::_thesis: ( not x in the carrier of R or x is real )
the carrier of R c= the carrier of T by BORSUK_1:1;
hence ( not x in the carrier of R or x is real ) ; ::_thesis: verum
end;
end;
registration
cluster RealSpace -> real-membered ;
coherence
RealSpace is real-membered
proof
thus the carrier of RealSpace is real-membered ; :: according to TOPMETR:def_8 ::_thesis: verum
end;
end;