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