:: WEIERSTR semantic presentation begin theorem Th1: :: WEIERSTR:1 for M being MetrSpace for x1, x2 being Point of M for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) proof let M be MetrSpace; ::_thesis: for x1, x2 being Point of M for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) let x1, x2 be Point of M; ::_thesis: for r1, r2 being Real ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) let r1, r2 be Real; ::_thesis: ex x being Point of M ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) reconsider x = x1 as Point of M ; reconsider r = ((abs r1) + (abs r2)) + (dist (x1,x2)) as Real ; take x ; ::_thesis: ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) take r ; ::_thesis: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) for a being set st a in (Ball (x1,r1)) \/ (Ball (x2,r2)) holds a in Ball (x,r) proof let a be set ; ::_thesis: ( a in (Ball (x1,r1)) \/ (Ball (x2,r2)) implies a in Ball (x,r) ) assume A1: a in (Ball (x1,r1)) \/ (Ball (x2,r2)) ; ::_thesis: a in Ball (x,r) then reconsider a = a as Point of M ; now__::_thesis:_(_(_a_in_Ball_(x1,r1)_&_a_in_Ball_(x,r)_)_or_(_a_in_Ball_(x2,r2)_&_a_in_Ball_(x,r)_)_) percases ( a in Ball (x1,r1) or a in Ball (x2,r2) ) by A1, XBOOLE_0:def_3; caseA2: a in Ball (x1,r1) ; ::_thesis: a in Ball (x,r) ( r1 <= abs r1 & 0 <= abs r2 ) by ABSVALUE:4, COMPLEX1:46; then A3: r1 + 0 <= (abs r1) + (abs r2) by XREAL_1:7; A4: dist (x,a) < r1 by A2, METRIC_1:11; 0 <= dist (x1,x2) by METRIC_1:5; then r1 + 0 <= ((abs r1) + (abs r2)) + (dist (x1,x2)) by A3, XREAL_1:7; then (dist (x,a)) - r < r1 - r1 by A4, XREAL_1:14; then A5: ((dist (x,a)) - r) + r < 0 + r by XREAL_1:8; not M is empty by A2; hence a in Ball (x,r) by A5, METRIC_1:11; ::_thesis: verum end; caseA6: a in Ball (x2,r2) ; ::_thesis: a in Ball (x,r) then dist (x2,a) < r2 by METRIC_1:11; then (dist (x2,a)) - (abs r2) < r2 - r2 by ABSVALUE:4, XREAL_1:14; then ( dist (x,a) <= (dist (x1,x2)) + (dist (x2,a)) & ((dist (x2,a)) - (abs r2)) + (abs r2) < 0 + (abs r2) ) by METRIC_1:4, XREAL_1:8; then (dist (x,a)) - (abs r2) < ((dist (x1,x2)) + (dist (x2,a))) - (dist (x2,a)) by XREAL_1:15; then ((dist (x,a)) - (abs r2)) - (abs r1) < (dist (x1,x2)) - 0 by COMPLEX1:46, XREAL_1:14; then A7: ((dist (x,a)) - ((abs r1) + (abs r2))) + ((abs r1) + (abs r2)) < ((abs r1) + (abs r2)) + (dist (x1,x2)) by XREAL_1:8; not M is empty by A6; hence a in Ball (x,r) by A7, METRIC_1:11; ::_thesis: verum end; end; end; hence a in Ball (x,r) ; ::_thesis: verum end; hence (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by TARSKI:def_3; ::_thesis: verum end; theorem Th2: :: WEIERSTR:2 for M being MetrSpace for n being Nat for F being Subset-Family of M for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds ex G being Subset-Family of M st ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) proof let M be MetrSpace; ::_thesis: for n being Nat for F being Subset-Family of M for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds ex G being Subset-Family of M st ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) let n be Nat; ::_thesis: for F being Subset-Family of M for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds ex G being Subset-Family of M st ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) let F be Subset-Family of M; ::_thesis: for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds ex G being Subset-Family of M st ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) let p be FinSequence; ::_thesis: ( F is being_ball-family & rng p = F & dom p = Seg (n + 1) implies ex G being Subset-Family of M st ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) ) assume that A1: F is being_ball-family and A2: rng p = F and A3: dom p = Seg (n + 1) ; ::_thesis: ex G being Subset-Family of M st ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) n + 1 in dom p by A3, FINSEQ_1:4; then p . (n + 1) in F by A2, FUNCT_1:def_3; then consider x being Point of M such that A4: ex r being Real st p . (n + 1) = Ball (x,r) by A1, TOPMETR:def_4; consider r being Real such that A5: p . (n + 1) = Ball (x,r) by A4; reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15; A6: rng q c= rng p by RELAT_1:70; then reconsider G = rng q as Subset-Family of M by A2, XBOOLE_1:1; reconsider G = G as Subset-Family of M ; len p = n + 1 by A3, FINSEQ_1:def_3; then n <= len p by NAT_1:11; then A7: dom q = Seg n by FINSEQ_1:17; then A8: (dom q) \/ {(n + 1)} = dom p by A3, FINSEQ_1:9; A9: ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) proof take x ; ::_thesis: ex r being Real st union F c= (union G) \/ (Ball (x,r)) take r ; ::_thesis: union F c= (union G) \/ (Ball (x,r)) union F c= (union G) \/ (Ball (x,r)) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in union F or t in (union G) \/ (Ball (x,r)) ) assume t in union F ; ::_thesis: t in (union G) \/ (Ball (x,r)) then consider A being set such that A10: t in A and A11: A in F by TARSKI:def_4; consider s being set such that A12: s in dom p and A13: A = p . s by A2, A11, FUNCT_1:def_3; now__::_thesis:_(_(_s_in_dom_q_&_t_in_(union_G)_\/_(Ball_(x,r))_)_or_(_s_in_{(n_+_1)}_&_t_in_(union_G)_\/_(Ball_(x,r))_)_) percases ( s in dom q or s in {(n + 1)} ) by A8, A12, XBOOLE_0:def_3; case s in dom q ; ::_thesis: t in (union G) \/ (Ball (x,r)) then ( q . s in G & q . s = A ) by A13, FUNCT_1:47, FUNCT_1:def_3; then A14: t in union G by A10, TARSKI:def_4; union G c= (union G) \/ (Ball (x,r)) by XBOOLE_1:7; hence t in (union G) \/ (Ball (x,r)) by A14; ::_thesis: verum end; case s in {(n + 1)} ; ::_thesis: t in (union G) \/ (Ball (x,r)) then p . s = Ball (x,r) by A5, TARSKI:def_1; hence t in (union G) \/ (Ball (x,r)) by A10, A13, XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence t in (union G) \/ (Ball (x,r)) ; ::_thesis: verum end; hence union F c= (union G) \/ (Ball (x,r)) ; ::_thesis: verum end; take G ; ::_thesis: ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) for x being set st x in G holds ex y being Point of M ex r being Real st x = Ball (y,r) by A1, A2, A6, TOPMETR:def_4; hence ( G is finite & G is being_ball-family & ex q being FinSequence st ( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) by A7, A9, TOPMETR:def_4; ::_thesis: verum end; theorem Th3: :: WEIERSTR:3 for M being MetrSpace for F being Subset-Family of M st F is finite & F is being_ball-family holds ex x being Point of M ex r being Real st union F c= Ball (x,r) proof let M be MetrSpace; ::_thesis: for F being Subset-Family of M st F is finite & F is being_ball-family holds ex x being Point of M ex r being Real st union F c= Ball (x,r) let F be Subset-Family of M; ::_thesis: ( F is finite & F is being_ball-family implies ex x being Point of M ex r being Real st union F c= Ball (x,r) ) assume that A1: F is finite and A2: F is being_ball-family ; ::_thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r) consider p being FinSequence such that A3: rng p = F by A1, FINSEQ_1:52; A4: for F being Subset-Family of M st F is finite & F is being_ball-family holds for n being Nat for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) proof defpred S1[ Nat] means for F being Subset-Family of M st F is finite & F is being_ball-family holds for n being Nat st n = \$1 holds for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r); A5: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] let F be Subset-Family of M; ::_thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = k + 1 holds for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) ) assume that F is finite and A7: F is being_ball-family ; ::_thesis: for n being Nat st n = k + 1 holds for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) let n be Nat; ::_thesis: ( n = k + 1 implies for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) ) assume A8: n = k + 1 ; ::_thesis: for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) let p be FinSequence; ::_thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) ) assume ( rng p = F & dom p = Seg n ) ; ::_thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r) then consider F1 being Subset-Family of M such that A9: ( F1 is finite & F1 is being_ball-family ) and A10: ex p1 being FinSequence st ( rng p1 = F1 & dom p1 = Seg k & ex x2 being Point of M ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) ) by A7, A8, Th2; consider x1 being Point of M such that A11: ex r being Real st union F1 c= Ball (x1,r) by A6, A9, A10; consider x2 being Point of M such that A12: ex r2 being Real st union F c= (union F1) \/ (Ball (x2,r2)) by A10; consider r2 being Real such that A13: union F c= (union F1) \/ (Ball (x2,r2)) by A12; consider r1 being Real such that A14: union F1 c= Ball (x1,r1) by A11; consider x being Point of M such that A15: ex r being Real st (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by Th1; take x ; ::_thesis: ex r being Real st union F c= Ball (x,r) consider r being Real such that A16: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x,r) by A15; take r ; ::_thesis: union F c= Ball (x,r) (union F1) \/ (Ball (x2,r2)) c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A14, XBOOLE_1:9; then union F c= (Ball (x1,r1)) \/ (Ball (x2,r2)) by A13, XBOOLE_1:1; hence union F c= Ball (x,r) by A16, XBOOLE_1:1; ::_thesis: verum end; A17: S1[ 0 ] proof let F be Subset-Family of M; ::_thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = 0 holds for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) ) assume that F is finite and F is being_ball-family ; ::_thesis: for n being Nat st n = 0 holds for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) let n be Nat; ::_thesis: ( n = 0 implies for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) ) assume n = 0 ; ::_thesis: for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) then A18: Seg n = {} ; for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) proof set x = the Point of M; let p be FinSequence; ::_thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball (x,r) ) assume A19: ( rng p = F & dom p = Seg n ) ; ::_thesis: ex x being Point of M ex r being Real st union F c= Ball (x,r) take the Point of M ; ::_thesis: ex r being Real st union F c= Ball ( the Point of M,r) take 0 ; ::_thesis: union F c= Ball ( the Point of M,0) union F = {} by A19, A18, RELAT_1:42, ZFMISC_1:2; hence union F c= Ball ( the Point of M,0) by XBOOLE_1:2; ::_thesis: verum end; hence for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A17, A5); hence for F being Subset-Family of M st F is finite & F is being_ball-family holds for n being Nat for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M ex r being Real st union F c= Ball (x,r) ; ::_thesis: verum end; ex n being Nat st dom p = Seg n by FINSEQ_1:def_2; hence ex x being Point of M ex r being Real st union F c= Ball (x,r) by A2, A4, A3; ::_thesis: verum end; theorem Th4: :: WEIERSTR:4 for T, S being non empty TopSpace for f being Function of T,S for B being Subset-Family of S st f is continuous & B is open holds f " B is open proof let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S for B being Subset-Family of S st f is continuous & B is open holds f " B is open let f be Function of T,S; ::_thesis: for B being Subset-Family of S st f is continuous & B is open holds f " B is open let B be Subset-Family of S; ::_thesis: ( f is continuous & B is open implies f " B is open ) assume that A1: f is continuous and A2: B is open ; ::_thesis: f " B is open for P being Subset of T st P in f " B holds P is open proof let P be Subset of T; ::_thesis: ( P in f " B implies P is open ) assume A3: P in f " B ; ::_thesis: P is open thus P is open ::_thesis: verum proof consider C being Subset of S such that A4: C in B and A5: P = f " C by A3, FUNCT_2:def_9; reconsider C = C as Subset of S ; ( [#] S <> {} & C is open ) by A2, A4, TOPS_2:def_1; hence P is open by A1, A5, TOPS_2:43; ::_thesis: verum end; end; hence f " B is open by TOPS_2:def_1; ::_thesis: verum end; theorem :: WEIERSTR:5 for T, S being non empty TopSpace for f being Function of T,S for Q being Subset-Family of S st Q is finite holds f " Q is finite proof let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S for Q being Subset-Family of S st Q is finite holds f " Q is finite let f be Function of T,S; ::_thesis: for Q being Subset-Family of S st Q is finite holds f " Q is finite let Q be Subset-Family of S; ::_thesis: ( Q is finite implies f " Q is finite ) defpred S1[ Subset of ([#] S), Subset of ([#] T)] means for s, t being set st \$1 = s & \$2 = t holds t = f " s; assume Q is finite ; ::_thesis: f " Q is finite then consider s being FinSequence such that A1: rng s = Q by FINSEQ_1:52; A2: for x being Subset of ([#] S) ex y being Subset of ([#] T) st S1[x,y] proof let x be Subset of ([#] S); ::_thesis: ex y being Subset of ([#] T) st S1[x,y] reconsider x = x as set ; set y = f " x; reconsider y = f " x as Subset of ([#] T) ; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider F being Function of (bool ([#] S)),(bool ([#] T)) such that A3: for x being Subset of ([#] S) holds S1[x,F . x] from FUNCT_2:sch_3(A2); dom F = bool ([#] S) by FUNCT_2:def_1; then reconsider q = F * s as FinSequence by A1, FINSEQ_1:16; for x being set holds ( x in F .: Q iff x in f " Q ) proof let x be set ; ::_thesis: ( x in F .: Q iff x in f " Q ) A4: dom F = bool ([#] S) by FUNCT_2:def_1; thus ( x in F .: Q implies x in f " Q ) ::_thesis: ( x in f " Q implies x in F .: Q ) proof assume x in F .: Q ; ::_thesis: x in f " Q then consider y being set such that A5: y in dom F and A6: ( y in Q & x = F . y ) by FUNCT_1:def_6; reconsider y = y as Subset of S by A5; F . y = f " y by A3; hence x in f " Q by A6, FUNCT_2:def_9; ::_thesis: verum end; assume A7: x in f " Q ; ::_thesis: x in F .: Q then reconsider x = x as Subset of T ; consider y being Subset of S such that A8: y in Q and A9: x = f " y by A7, FUNCT_2:def_9; x = F . y by A3, A9; hence x in F .: Q by A8, A4, FUNCT_1:def_6; ::_thesis: verum end; then A10: F .: Q = f " Q by TARSKI:1; ex q being FinSequence st rng q = f " Q proof take q ; ::_thesis: rng q = f " Q thus rng q = f " Q by A1, A10, RELAT_1:127; ::_thesis: verum end; hence f " Q is finite ; ::_thesis: verum end; theorem :: WEIERSTR:6 for T, S being non empty TopSpace for f being Function of T,S for P being Subset-Family of T st P is finite holds f .: P is finite proof let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S for P being Subset-Family of T st P is finite holds f .: P is finite let f be Function of T,S; ::_thesis: for P being Subset-Family of T st P is finite holds f .: P is finite let P be Subset-Family of T; ::_thesis: ( P is finite implies f .: P is finite ) defpred S1[ Subset of ([#] T), Subset of ([#] S)] means for s, t being set st \$1 = s & \$2 = t holds t = f .: s; assume P is finite ; ::_thesis: f .: P is finite then consider s being FinSequence such that A1: rng s = P by FINSEQ_1:52; A2: for x being Subset of ([#] T) ex y being Subset of ([#] S) st S1[x,y] proof let x be Subset of ([#] T); ::_thesis: ex y being Subset of ([#] S) st S1[x,y] reconsider x = x as set ; set y = f .: x; reconsider y = f .: x as Subset of ([#] S) ; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider F being Function of (bool ([#] T)),(bool ([#] S)) such that A3: for x being Subset of ([#] T) holds S1[x,F . x] from FUNCT_2:sch_3(A2); dom F = bool ([#] T) by FUNCT_2:def_1; then reconsider q = F * s as FinSequence by A1, FINSEQ_1:16; for x being set holds ( x in F .: P iff x in f .: P ) proof let x be set ; ::_thesis: ( x in F .: P iff x in f .: P ) thus ( x in F .: P implies x in f .: P ) ::_thesis: ( x in f .: P implies x in F .: P ) proof assume x in F .: P ; ::_thesis: x in f .: P then consider y being set such that A4: y in dom F and A5: ( y in P & x = F . y ) by FUNCT_1:def_6; reconsider y = y as Subset of T by A4; F . y = f .: y by A3; hence x in f .: P by A5, FUNCT_2:def_10; ::_thesis: verum end; thus ( x in f .: P implies x in F .: P ) ::_thesis: verum proof assume A6: x in f .: P ; ::_thesis: x in F .: P then reconsider x = x as Subset of S ; consider y being Subset of T such that A7: y in P and A8: x = f .: y by A6, FUNCT_2:def_10; A9: dom F = bool ([#] T) by FUNCT_2:def_1; x = F . y by A3, A8; hence x in F .: P by A7, A9, FUNCT_1:def_6; ::_thesis: verum end; end; then A10: F .: P = f .: P by TARSKI:1; ex q being FinSequence st rng q = f .: P proof take q ; ::_thesis: rng q = f .: P thus rng q = f .: P by A1, A10, RELAT_1:127; ::_thesis: verum end; hence f .: P is finite ; ::_thesis: verum end; theorem Th7: :: WEIERSTR:7 for T, S being non empty TopSpace for f being Function of T,S for P being Subset of T for F being Subset-Family of S st ex B being Subset-Family of T st ( B c= f " F & B is Cover of P & B is finite ) holds ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) proof let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S for P being Subset of T for F being Subset-Family of S st ex B being Subset-Family of T st ( B c= f " F & B is Cover of P & B is finite ) holds ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) let f be Function of T,S; ::_thesis: for P being Subset of T for F being Subset-Family of S st ex B being Subset-Family of T st ( B c= f " F & B is Cover of P & B is finite ) holds ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) let P be Subset of T; ::_thesis: for F being Subset-Family of S st ex B being Subset-Family of T st ( B c= f " F & B is Cover of P & B is finite ) holds ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) let F be Subset-Family of S; ::_thesis: ( ex B being Subset-Family of T st ( B c= f " F & B is Cover of P & B is finite ) implies ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ) given B being Subset-Family of T such that A1: B c= f " F and A2: B is Cover of P and A3: B is finite ; ::_thesis: ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) A4: P c= union B by A2, SETFAM_1:def_11; now__::_thesis:_(_(_P_<>_{}_&_ex_G_being_Subset-Family_of_S_st_ (_G_c=_F_&_G_is_Cover_of_f_.:_P_&_G_is_finite_)_&_ex_G_being_Subset-Family_of_S_st_ (_G_c=_F_&_G_is_Cover_of_f_.:_P_&_G_is_finite_)_)_or_(_P_=_{}_&_ex_G_being_Subset-Family_of_S_st_ (_G_c=_F_&_G_is_Cover_of_f_.:_P_&_G_is_finite_)_)_) percases ( P <> {} or P = {} ) ; caseA5: P <> {} ; ::_thesis: ( ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) & ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ) thus ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ::_thesis: ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) proof consider s being FinSequence such that A6: rng s = B by A3, FINSEQ_1:52; B <> {} by A4, A5, ZFMISC_1:2; then consider D being non empty set such that A7: D = B ; defpred S1[ Element of D, Subset of ([#] S)] means for x being Element of D st \$1 = x holds for y being Subset of ([#] S) st \$2 = y holds ( y in F & x = f " y ); A8: for x being Element of D ex y being Subset of ([#] S) st S1[x,y] proof let x be Element of D; ::_thesis: ex y being Subset of ([#] S) st S1[x,y] A9: x in B by A7; then reconsider x = x as Subset of T ; consider y being Subset of S such that A10: ( y in F & x = f " y ) by A1, A9, FUNCT_2:def_9; reconsider y = y as Subset of ([#] S) ; take y ; ::_thesis: S1[x,y] thus S1[x,y] by A10; ::_thesis: verum end; consider F0 being Function of D,(bool ([#] S)) such that A11: for x being Element of D holds S1[x,F0 . x] from FUNCT_2:sch_3(A8); A12: for x being Element of D holds ( F0 . x in F & x = f " (F0 . x) ) by A11; reconsider F0 = F0 as Function of B,(bool ([#] S)) by A7; A13: dom F0 = B by FUNCT_2:def_1; then reconsider q = F0 * s as FinSequence by A6, FINSEQ_1:16; set G = rng q; A14: rng q c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q or x in F ) assume x in rng q ; ::_thesis: x in F then consider y being set such that A15: ( y in dom q & x = q . y ) by FUNCT_1:def_3; ( s . y in B & x = F0 . (s . y) ) by A13, A15, FUNCT_1:11, FUNCT_1:12; hence x in F by A7, A12; ::_thesis: verum end; then reconsider G = rng q as Subset-Family of S by XBOOLE_1:1; reconsider G = G as Subset-Family of S ; take G ; ::_thesis: ( G c= F & G is Cover of f .: P & G is finite ) for x being set st x in f .: P holds x in union G proof let x be set ; ::_thesis: ( x in f .: P implies x in union G ) assume A16: x in f .: P ; ::_thesis: x in union G ex A being set st ( x in A & A in G ) proof consider y being set such that A17: y in dom f and A18: y in P and A19: x = f . y by A16, FUNCT_1:def_6; consider C being set such that A20: y in C and A21: C in B by A4, A18, TARSKI:def_4; C = f " (F0 . C) by A7, A12, A21; then A22: x in f .: (f " (F0 . C)) by A17, A19, A20, FUNCT_1:def_6; set A = F0 . C; take F0 . C ; ::_thesis: ( x in F0 . C & F0 . C in G ) ( f .: (f " (F0 . C)) c= F0 . C & G = rng F0 ) by A6, A13, FUNCT_1:75, RELAT_1:28; hence ( x in F0 . C & F0 . C in G ) by A21, A22, FUNCT_2:4; ::_thesis: verum end; hence x in union G by TARSKI:def_4; ::_thesis: verum end; then f .: P c= union G by TARSKI:def_3; hence ( G c= F & G is Cover of f .: P & G is finite ) by A14, SETFAM_1:def_11; ::_thesis: verum end; hence ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ; ::_thesis: verum end; caseA23: P = {} ; ::_thesis: ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) proof set G = {} ; reconsider G = {} as Subset-Family of S by XBOOLE_1:2; reconsider G = G as Subset-Family of S ; take G ; ::_thesis: ( G c= F & G is Cover of f .: P & G is finite ) f .: P = {} proof assume f .: P <> {} ; ::_thesis: contradiction then consider x being set such that A24: x in f .: P by XBOOLE_0:def_1; ex z being set st ( z in dom f & z in P & x = f . z ) by A24, FUNCT_1:def_6; hence contradiction by A23; ::_thesis: verum end; hence ( G c= F & G is Cover of f .: P & G is finite ) by SETFAM_1:def_11, XBOOLE_1:2, ZFMISC_1:2; ::_thesis: verum end; hence ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ; ::_thesis: verum end; end; end; hence ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ; ::_thesis: verum end; begin theorem Th8: :: WEIERSTR:8 for T, S being non empty TopSpace for f being Function of T,S for P being Subset of T st P is compact & f is continuous holds f .: P is compact proof let T, S be non empty TopSpace; ::_thesis: for f being Function of T,S for P being Subset of T st P is compact & f is continuous holds f .: P is compact let f be Function of T,S; ::_thesis: for P being Subset of T st P is compact & f is continuous holds f .: P is compact let P be Subset of T; ::_thesis: ( P is compact & f is continuous implies f .: P is compact ) assume that A1: P is compact and A2: f is continuous ; ::_thesis: f .: P is compact P c= [#] T ; then A3: P c= dom f by FUNCT_2:def_1; for F0 being Subset-Family of S st F0 is Cover of f .: P & F0 is open holds ex G being Subset-Family of S st ( G c= F0 & G is Cover of f .: P & G is finite ) proof let F0 be Subset-Family of S; ::_thesis: ( F0 is Cover of f .: P & F0 is open implies ex G being Subset-Family of S st ( G c= F0 & G is Cover of f .: P & G is finite ) ) assume that A4: F0 is Cover of f .: P and A5: F0 is open ; ::_thesis: ex G being Subset-Family of S st ( G c= F0 & G is Cover of f .: P & G is finite ) set B0 = f " F0; A6: f .: P c= union F0 by A4, SETFAM_1:def_11; P c= union (f " F0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in union (f " F0) ) thus ( x in P implies x in union (f " F0) ) ::_thesis: verum proof A7: f " (union F0) c= union (f " F0) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f " (union F0) or y in union (f " F0) ) assume A8: y in f " (union F0) ; ::_thesis: y in union (f " F0) thus y in union (f " F0) ::_thesis: verum proof f . y in union F0 by A8, FUNCT_1:def_7; then consider Q being set such that A9: ( f . y in Q & Q in F0 ) by TARSKI:def_4; A10: y in dom f by A8, FUNCT_1:def_7; ex Z being set st ( y in Z & Z in f " F0 ) proof set Z = f " Q; take f " Q ; ::_thesis: ( y in f " Q & f " Q in f " F0 ) thus ( y in f " Q & f " Q in f " F0 ) by A10, A9, FUNCT_1:def_7, FUNCT_2:def_9; ::_thesis: verum end; hence y in union (f " F0) by TARSKI:def_4; ::_thesis: verum end; end; assume A11: x in P ; ::_thesis: x in union (f " F0) then A12: f . x in f .: P by A3, FUNCT_1:def_6; reconsider x = x as Point of T by A11; A13: f . x in union F0 by A6, A12; A14: f " {(f . x)} c= f " (union F0) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f " {(f . x)} or y in f " (union F0) ) assume A15: y in f " {(f . x)} ; ::_thesis: y in f " (union F0) then f . y in {(f . x)} by FUNCT_1:def_7; then A16: f . y in union F0 by A13, TARSKI:def_1; y in dom f by A15, FUNCT_1:def_7; hence y in f " (union F0) by A16, FUNCT_1:def_7; ::_thesis: verum end; f . x in {(f . x)} by TARSKI:def_1; then x in f " {(f . x)} by A3, A11, FUNCT_1:def_7; then x in f " (union F0) by A14; hence x in union (f " F0) by A7; ::_thesis: verum end; end; then A17: f " F0 is Cover of P by SETFAM_1:def_11; f " F0 is open by A2, A5, Th4; then ex B being Subset-Family of T st ( B c= f " F0 & B is Cover of P & B is finite ) by A1, A17, COMPTS_1:def_4; then consider G being Subset-Family of S such that A18: ( G c= F0 & G is Cover of f .: P & G is finite ) by Th7; take G ; ::_thesis: ( G c= F0 & G is Cover of f .: P & G is finite ) thus ( G c= F0 & G is Cover of f .: P & G is finite ) by A18; ::_thesis: verum end; hence f .: P is compact by COMPTS_1:def_4; ::_thesis: verum end; theorem :: WEIERSTR:9 for T being non empty TopSpace for f being Function of T,R^1 for P being Subset of T st P is compact & f is continuous holds f .: P is compact by Th8; theorem :: WEIERSTR:10 for f being Function of (TOP-REAL 2),R^1 for P being Subset of (TOP-REAL 2) st P is compact & f is continuous holds f .: P is compact by Th8; definition let P be Subset of R^1; func [#] P -> Subset of REAL equals :: WEIERSTR:def 1 P; correctness coherence P is Subset of REAL; by TOPMETR:17; end; :: deftheorem defines [#] WEIERSTR:def_1_:_ for P being Subset of R^1 holds [#] P = P; theorem Th11: :: WEIERSTR:11 for P being Subset of R^1 st P is compact holds [#] P is real-bounded proof let P be Subset of R^1; ::_thesis: ( P is compact implies [#] P is real-bounded ) assume A1: P is compact ; ::_thesis: [#] P is real-bounded thus [#] P is real-bounded ::_thesis: verum proof now__::_thesis:_(_(_[#]_P_<>_{}_&_[#]_P_is_real-bounded_)_or_(_[#]_P_=_{}_&_[#]_P_is_real-bounded_)_) percases ( [#] P <> {} or [#] P = {} ) ; case [#] P <> {} ; ::_thesis: [#] P is real-bounded set r0 = 1; defpred S1[ Subset of R^1] means ex x being Point of RealSpace st ( x in [#] P & \$1 = Ball (x,1) ); consider R being Subset-Family of R^1 such that A2: for A being Subset of R^1 holds ( A in R iff S1[A] ) from SUBSET_1:sch_3(); for x being set st x in [#] P holds x in union R proof let x be set ; ::_thesis: ( x in [#] P implies x in union R ) assume A3: x in [#] P ; ::_thesis: x in union R then reconsider x = x as Point of RealSpace by METRIC_1:def_13; consider A being Subset of RealSpace such that A4: A = Ball (x,1) ; R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def_5, TOPMETR:def_6; then reconsider A = A as Subset of R^1 ; ex A being set st ( x in A & A in R ) proof take A ; ::_thesis: ( x in A & A in R ) dist (x,x) = 0 by METRIC_1:1; hence ( x in A & A in R ) by A2, A3, A4, METRIC_1:11; ::_thesis: verum end; hence x in union R by TARSKI:def_4; ::_thesis: verum end; then [#] P c= union R by TARSKI:def_3; then A5: R is Cover of P by SETFAM_1:def_11; for A being Subset of R^1 st A in R holds A is open proof let A be Subset of R^1; ::_thesis: ( A in R implies A is open ) assume A in R ; ::_thesis: A is open then ex x being Point of RealSpace st ( x in [#] P & A = Ball (x,1) ) by A2; hence A is open by TOPMETR:14, TOPMETR:def_6; ::_thesis: verum end; then R is open by TOPS_2:def_1; then consider R0 being Subset-Family of R^1 such that A6: R0 c= R and A7: R0 is Cover of P and A8: R0 is finite by A1, A5, COMPTS_1:def_4; A9: P c= union R0 by A7, SETFAM_1:def_11; A10: for A being set st A in R0 holds ex x being Point of RealSpace ex r being Real st A = Ball (x,r) proof let A be set ; ::_thesis: ( A in R0 implies ex x being Point of RealSpace ex r being Real st A = Ball (x,r) ) assume A11: A in R0 ; ::_thesis: ex x being Point of RealSpace ex r being Real st A = Ball (x,r) then reconsider A = A as Subset of R^1 ; consider x being Point of RealSpace such that x in [#] P and A12: A = Ball (x,1) by A2, A6, A11; take x ; ::_thesis: ex r being Real st A = Ball (x,r) take 1 ; ::_thesis: A = Ball (x,1) thus A = Ball (x,1) by A12; ::_thesis: verum end; R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def_5, TOPMETR:def_6; then reconsider R0 = R0 as Subset-Family of RealSpace ; R0 is being_ball-family by A10, TOPMETR:def_4; then consider x1 being Point of RealSpace such that A13: ex r1 being Real st union R0 c= Ball (x1,r1) by A8, Th3; consider r1 being Real such that A14: union R0 c= Ball (x1,r1) by A13; A15: [#] P c= Ball (x1,r1) by A9, A14, XBOOLE_1:1; reconsider x1 = x1 as Real by METRIC_1:def_13; A16: for p being Real st p in [#] P holds ( x1 - r1 <= p & p <= x1 + r1 ) proof let p be Real; ::_thesis: ( p in [#] P implies ( x1 - r1 <= p & p <= x1 + r1 ) ) reconsider a = x1, b = p as Element of RealSpace by METRIC_1:def_13; assume p in [#] P ; ::_thesis: ( x1 - r1 <= p & p <= x1 + r1 ) then dist (a,b) < r1 by A15, METRIC_1:11; then A17: abs (x1 - p) < r1 by TOPMETR:11; then - r1 <= x1 - p by ABSVALUE:5; then (- r1) + p <= x1 by XREAL_1:19; then A18: p <= x1 - (- r1) by XREAL_1:19; x1 - p <= r1 by A17, ABSVALUE:5; then x1 <= p + r1 by XREAL_1:20; hence ( x1 - r1 <= p & p <= x1 + r1 ) by A18, XREAL_1:20; ::_thesis: verum end; x1 - r1 is LowerBound of [#] P proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in [#] P or x1 - r1 <= r ) thus ( not r in [#] P or x1 - r1 <= r ) by A16; ::_thesis: verum end; then A19: [#] P is bounded_below by XXREAL_2:def_9; x1 + r1 is UpperBound of [#] P proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in [#] P or r <= x1 + r1 ) thus ( not r in [#] P or r <= x1 + r1 ) by A16; ::_thesis: verum end; then [#] P is bounded_above by XXREAL_2:def_10; hence [#] P is real-bounded by A19, XXREAL_2:def_11; ::_thesis: verum end; caseA20: [#] P = {} ; ::_thesis: [#] P is real-bounded 0 is LowerBound of [#] P proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in [#] P or 0 <= r ) thus ( not r in [#] P or 0 <= r ) by A20; ::_thesis: verum end; then A21: [#] P is bounded_below by XXREAL_2:def_9; 0 is UpperBound of [#] P proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in [#] P or r <= 0 ) thus ( not r in [#] P or r <= 0 ) by A20; ::_thesis: verum end; then [#] P is bounded_above by XXREAL_2:def_10; hence [#] P is real-bounded by A21, XXREAL_2:def_11; ::_thesis: verum end; end; end; hence [#] P is real-bounded ; ::_thesis: verum end; end; theorem Th12: :: WEIERSTR:12 for P being Subset of R^1 st P is compact holds [#] P is closed proof let P be Subset of R^1; ::_thesis: ( P is compact implies [#] P is closed ) assume A1: P is compact ; ::_thesis: [#] P is closed now__::_thesis:_(_(_[#]_P_<>_{}_&_[#]_P_is_closed_)_or_(_[#]_P_=_{}_&_[#]_P_is_closed_)_) percases ( [#] P <> {} or [#] P = {} ) ; caseA2: [#] P <> {} ; ::_thesis: [#] P is closed A3: R^1 is T_2 by PCOMPS_1:34, TOPMETR:def_6; for s1 being Real_Sequence st rng s1 c= [#] P & s1 is convergent holds lim s1 in [#] P proof let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [#] P & s1 is convergent implies lim s1 in [#] P ) assume that A4: rng s1 c= [#] P and A5: s1 is convergent ; ::_thesis: lim s1 in [#] P set x = lim s1; reconsider x = lim s1 as Point of R^1 by TOPMETR:17; thus lim s1 in [#] P ::_thesis: verum proof assume not lim s1 in [#] P ; ::_thesis: contradiction then x in P ` by SUBSET_1:29; then consider Otx, OtP being Subset of R^1 such that A6: Otx is open and OtP is open and A7: x in Otx and A8: ( P c= OtP & Otx misses OtP ) by A1, A2, A3, COMPTS_1:6; A9: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def_5, TOPMETR:def_6; then reconsider x = x as Point of RealSpace ; consider r being real number such that A10: r > 0 and A11: Ball (x,r) c= Otx by A6, A7, TOPMETR:15, TOPMETR:def_6; reconsider r = r as Real by XREAL_0:def_1; A12: Ball (x,r) = { q where q is Element of RealSpace : dist (x,q) < r } by METRIC_1:17; rng s1 misses Otx by A4, A8, XBOOLE_1:1, XBOOLE_1:63; then A13: Ball (x,r) misses rng s1 by A11, XBOOLE_1:63; for n being Element of NAT ex m being Element of NAT st ( n <= m & not abs ((s1 . m) - (lim s1)) < r ) proof given n being Element of NAT such that A14: for m being Element of NAT st n <= m holds abs ((s1 . m) - (lim s1)) < r ; ::_thesis: contradiction set m = n + 1; abs ((s1 . (n + 1)) - (lim s1)) < r by A14, NAT_1:11; then real_dist . ((s1 . (n + 1)),(lim s1)) < r by METRIC_1:def_12; then A15: real_dist . ((lim s1),(s1 . (n + 1))) < r by METRIC_1:9; reconsider y = s1 . (n + 1) as Element of RealSpace by A9, TOPMETR:17; A16: s1 . (n + 1) in rng s1 by FUNCT_2:4; dist (x,y) = the distance of RealSpace . (x,y) by METRIC_1:def_1; then y in Ball (x,r) by A12, A15, METRIC_1:def_13; then y in (Ball (x,r)) /\ (rng s1) by A16, XBOOLE_0:def_4; hence contradiction by A13, XBOOLE_0:def_7; ::_thesis: verum end; hence contradiction by A5, A10, SEQ_2:def_7; ::_thesis: verum end; end; hence [#] P is closed by RCOMP_1:def_4; ::_thesis: verum end; caseA17: [#] P = {} ; ::_thesis: [#] P is closed for s1 being Real_Sequence st rng s1 c= [#] P & s1 is convergent holds lim s1 in [#] P proof let s1 be Real_Sequence; ::_thesis: ( rng s1 c= [#] P & s1 is convergent implies lim s1 in [#] P ) assume that A18: rng s1 c= [#] P and s1 is convergent ; ::_thesis: lim s1 in [#] P ex x being set st x in NAT by XBOOLE_0:def_1; hence lim s1 in [#] P by A17, A18, FUNCT_2:4; ::_thesis: verum end; hence [#] P is closed by RCOMP_1:def_4; ::_thesis: verum end; end; end; hence [#] P is closed ; ::_thesis: verum end; theorem Th13: :: WEIERSTR:13 for P being Subset of R^1 st P is compact holds [#] P is compact proof let P be Subset of R^1; ::_thesis: ( P is compact implies [#] P is compact ) assume A1: P is compact ; ::_thesis: [#] P is compact now__::_thesis:_(_(_[#]_P_<>_{}_&_[#]_P_is_compact_)_or_(_[#]_P_=_{}_&_(_not_[#]_P_is_compact_implies_[#]_P_is_compact_)_)_) percases ( [#] P <> {} or [#] P = {} ) ; case [#] P <> {} ; ::_thesis: [#] P is compact [#] P is real-bounded by A1, Th11; hence [#] P is compact by A1, Th12, RCOMP_1:11; ::_thesis: verum end; caseA2: [#] P = {} ; ::_thesis: ( not [#] P is compact implies [#] P is compact ) assume not [#] P is compact ; ::_thesis: [#] P is compact then A3: ex s1 being Real_Sequence st ( rng s1 c= [#] P & ( for s2 being Real_Sequence holds ( not s2 is subsequence of s1 or not s2 is convergent or not lim s2 in [#] P ) ) ) by RCOMP_1:def_3; ex x being set st x in NAT by XBOOLE_0:def_1; hence [#] P is compact by A2, A3, FUNCT_2:4; ::_thesis: verum end; end; end; hence [#] P is compact ; ::_thesis: verum end; Lm1: for T being non empty TopSpace for f being Function of T,R^1 for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x1, x2 being Point of T st ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x1, x2 being Point of T st ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) let f be Function of T,R^1; ::_thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x1, x2 being Point of T st ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) let P be Subset of T; ::_thesis: ( P <> {} & P is compact & f is continuous implies ex x1, x2 being Point of T st ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) ) assume that A1: P <> {} and A2: ( P is compact & f is continuous ) ; ::_thesis: ex x1, x2 being Point of T st ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) A3: [#] (f .: P) <> {} proof consider x being set such that A4: x in P by A1, XBOOLE_0:def_1; dom f = the carrier of T by FUNCT_2:def_1; then f . x in f .: P by A4, FUNCT_1:def_6; hence [#] (f .: P) <> {} ; ::_thesis: verum end; consider y1, y2 being Real such that A5: y1 = upper_bound ([#] (f .: P)) and A6: y2 = lower_bound ([#] (f .: P)) ; A7: [#] (f .: P) is compact by A2, Th8, Th13; then y1 in [#] (f .: P) by A3, A5, RCOMP_1:14; then consider x1 being set such that A8: x1 in dom f and A9: ( x1 in P & y1 = f . x1 ) by FUNCT_1:def_6; y2 in [#] (f .: P) by A3, A6, A7, RCOMP_1:14; then consider x2 being set such that A10: x2 in dom f and A11: ( x2 in P & y2 = f . x2 ) by FUNCT_1:def_6; reconsider x1 = x1, x2 = x2 as Point of T by A8, A10; take x1 ; ::_thesis: ex x2 being Point of T st ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) take x2 ; ::_thesis: ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) thus ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) by A5, A6, A9, A11; ::_thesis: verum end; definition let P be Subset of R^1; func upper_bound P -> Real equals :: WEIERSTR:def 2 upper_bound ([#] P); correctness coherence upper_bound ([#] P) is Real; ; func lower_bound P -> Real equals :: WEIERSTR:def 3 lower_bound ([#] P); correctness coherence lower_bound ([#] P) is Real; ; end; :: deftheorem defines upper_bound WEIERSTR:def_2_:_ for P being Subset of R^1 holds upper_bound P = upper_bound ([#] P); :: deftheorem defines lower_bound WEIERSTR:def_3_:_ for P being Subset of R^1 holds lower_bound P = lower_bound ([#] P); theorem Th14: :: WEIERSTR:14 for T being non empty TopSpace for f being Function of T,R^1 for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x1 being Point of T st ( x1 in P & f . x1 = upper_bound (f .: P) ) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x1 being Point of T st ( x1 in P & f . x1 = upper_bound (f .: P) ) let f be Function of T,R^1; ::_thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x1 being Point of T st ( x1 in P & f . x1 = upper_bound (f .: P) ) let P be Subset of T; ::_thesis: ( P <> {} & P is compact & f is continuous implies ex x1 being Point of T st ( x1 in P & f . x1 = upper_bound (f .: P) ) ) assume ( P <> {} & P is compact & f is continuous ) ; ::_thesis: ex x1 being Point of T st ( x1 in P & f . x1 = upper_bound (f .: P) ) then consider x1, x2 being Point of T such that A1: x1 in P and x2 in P and A2: f . x1 = upper_bound ([#] (f .: P)) and f . x2 = lower_bound ([#] (f .: P)) by Lm1; take x1 ; ::_thesis: ( x1 in P & f . x1 = upper_bound (f .: P) ) thus ( x1 in P & f . x1 = upper_bound (f .: P) ) by A1, A2; ::_thesis: verum end; theorem Th15: :: WEIERSTR:15 for T being non empty TopSpace for f being Function of T,R^1 for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x2 being Point of T st ( x2 in P & f . x2 = lower_bound (f .: P) ) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x2 being Point of T st ( x2 in P & f . x2 = lower_bound (f .: P) ) let f be Function of T,R^1; ::_thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds ex x2 being Point of T st ( x2 in P & f . x2 = lower_bound (f .: P) ) let P be Subset of T; ::_thesis: ( P <> {} & P is compact & f is continuous implies ex x2 being Point of T st ( x2 in P & f . x2 = lower_bound (f .: P) ) ) assume ( P <> {} & P is compact & f is continuous ) ; ::_thesis: ex x2 being Point of T st ( x2 in P & f . x2 = lower_bound (f .: P) ) then consider x1, x2 being Point of T such that x1 in P and A1: x2 in P and f . x1 = upper_bound ([#] (f .: P)) and A2: f . x2 = lower_bound ([#] (f .: P)) by Lm1; take x2 ; ::_thesis: ( x2 in P & f . x2 = lower_bound (f .: P) ) thus ( x2 in P & f . x2 = lower_bound (f .: P) ) by A1, A2; ::_thesis: verum end; begin definition let M be non empty MetrSpace; let x be Point of M; func dist x -> Function of (TopSpaceMetr M),R^1 means :Def4: :: WEIERSTR:def 4 for y being Point of M holds it . y = dist (y,x); existence ex b1 being Function of (TopSpaceMetr M),R^1 st for y being Point of M holds b1 . y = dist (y,x) proof defpred S1[ Element of M, Element of R^1] means for s being Element of M for t being Element of R^1 st \$1 = s & \$2 = t holds t = dist (s,x); A1: for s being Element of M ex t being Element of R^1 st S1[s,t] proof let s be Element of M; ::_thesis: ex t being Element of R^1 st S1[s,t] consider t being Real such that A2: t = dist (s,x) ; reconsider t = t as Element of R^1 by TOPMETR:17; take t ; ::_thesis: S1[s,t] thus S1[s,t] by A2; ::_thesis: verum end; consider F being Function of the carrier of M, the carrier of R^1 such that A3: for x being Element of M holds S1[x,F . x] from FUNCT_2:sch_3(A1); A4: for y being Point of M holds F . y = dist (y,x) by A3; TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider F = F as Function of (TopSpaceMetr M),R^1 ; take F ; ::_thesis: for y being Point of M holds F . y = dist (y,x) thus for y being Point of M holds F . y = dist (y,x) by A4; ::_thesis: verum end; uniqueness for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for y being Point of M holds b1 . y = dist (y,x) ) & ( for y being Point of M holds b2 . y = dist (y,x) ) holds b1 = b2 proof let F1, F2 be Function of (TopSpaceMetr M),R^1; ::_thesis: ( ( for y being Point of M holds F1 . y = dist (y,x) ) & ( for y being Point of M holds F2 . y = dist (y,x) ) implies F1 = F2 ) assume A5: for y being Point of M holds F1 . y = dist (y,x) ; ::_thesis: ( ex y being Point of M st not F2 . y = dist (y,x) or F1 = F2 ) assume A6: for y being Point of M holds F2 . y = dist (y,x) ; ::_thesis: F1 = F2 for y being set st y in the carrier of (TopSpaceMetr M) holds F1 . y = F2 . y proof let y be set ; ::_thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y ) A7: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; assume y in the carrier of (TopSpaceMetr M) ; ::_thesis: F1 . y = F2 . y then reconsider y = y as Point of M by A7; F1 . y = dist (y,x) by A5 .= F2 . y by A6 ; hence F1 . y = F2 . y ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def4 defines dist WEIERSTR:def_4_:_ for M being non empty MetrSpace for x being Point of M for b3 being Function of (TopSpaceMetr M),R^1 holds ( b3 = dist x iff for y being Point of M holds b3 . y = dist (y,x) ); theorem Th16: :: WEIERSTR:16 for M being non empty MetrSpace for x being Point of M holds dist x is continuous proof let M be non empty MetrSpace; ::_thesis: for x being Point of M holds dist x is continuous let x be Point of M; ::_thesis: dist x is continuous A1: for P being Subset of R^1 st P is open holds (dist x) " P is open proof let P be Subset of R^1; ::_thesis: ( P is open implies (dist x) " P is open ) assume A2: P is open ; ::_thesis: (dist x) " P is open for p being Point of M st p in (dist x) " P holds ex r being real number st ( r > 0 & Ball (p,r) c= (dist x) " P ) proof let p be Point of M; ::_thesis: ( p in (dist x) " P implies ex r being real number st ( r > 0 & Ball (p,r) c= (dist x) " P ) ) consider y being Point of RealSpace such that A3: y = dist (p,x) by METRIC_1:def_13; assume p in (dist x) " P ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (dist x) " P ) then A4: (dist x) . p in P by FUNCT_1:def_7; reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6; y in P by A4, A3, Def4; then consider r being real number such that A5: r > 0 and A6: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def_6; reconsider r = r as Real by XREAL_0:def_1; take r ; ::_thesis: ( r > 0 & Ball (p,r) c= (dist x) " P ) Ball (p,r) c= (dist x) " P proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball (p,r) or z in (dist x) " P ) assume A7: z in Ball (p,r) ; ::_thesis: z in (dist x) " P then reconsider z = z as Point of M ; consider q being Point of RealSpace such that A8: q = dist (z,x) by METRIC_1:def_13; dist (p,z) < r by A7, METRIC_1:11; then (abs ((dist (p,x)) - (dist (z,x)))) + (dist (p,z)) < r + (dist (p,z)) by METRIC_6:1, XREAL_1:8; then abs ((dist (p,x)) - (dist (z,x))) < r by XREAL_1:6; then dist (y,q) < r by A3, A8, TOPMETR:11; then q in Ball (y,r) by METRIC_1:11; then q in P by A6; then A9: (dist x) . z in P by A8, Def4; dom (dist x) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then dom (dist x) = the carrier of M by TOPMETR:12; hence z in (dist x) " P by A9, FUNCT_1:def_7; ::_thesis: verum end; hence ( r > 0 & Ball (p,r) c= (dist x) " P ) by A5; ::_thesis: verum end; hence (dist x) " P is open by TOPMETR:15; ::_thesis: verum end; [#] R^1 <> {} ; hence dist x is continuous by A1, TOPS_2:43; ::_thesis: verum end; theorem :: WEIERSTR:17 for M being non empty MetrSpace for x being Point of M for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds ex x1 being Point of (TopSpaceMetr M) st ( x1 in P & (dist x) . x1 = upper_bound ((dist x) .: P) ) by Th14, Th16; theorem :: WEIERSTR:18 for M being non empty MetrSpace for x being Point of M for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds ex x2 being Point of (TopSpaceMetr M) st ( x2 in P & (dist x) . x2 = lower_bound ((dist x) .: P) ) by Th15, Th16; definition let M be non empty MetrSpace; let P be Subset of (TopSpaceMetr M); func dist_max P -> Function of (TopSpaceMetr M),R^1 means :Def5: :: WEIERSTR:def 5 for x being Point of M holds it . x = upper_bound ((dist x) .: P); existence ex b1 being Function of (TopSpaceMetr M),R^1 st for x being Point of M holds b1 . x = upper_bound ((dist x) .: P) proof defpred S1[ Element of M, Element of R^1] means for s being Element of M for t being Element of R^1 st \$1 = s & \$2 = t holds t = upper_bound ((dist s) .: P); A1: for s being Element of M ex t being Element of R^1 st S1[s,t] proof let s be Element of M; ::_thesis: ex t being Element of R^1 st S1[s,t] consider t being Real such that A2: t = upper_bound ((dist s) .: P) ; reconsider t = t as Element of R^1 by TOPMETR:17; take t ; ::_thesis: S1[s,t] thus S1[s,t] by A2; ::_thesis: verum end; consider F being Function of the carrier of M, the carrier of R^1 such that A3: for x being Element of M holds S1[x,F . x] from FUNCT_2:sch_3(A1); A4: for y being Point of M holds F . y = upper_bound ((dist y) .: P) by A3; TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider F = F as Function of (TopSpaceMetr M),R^1 ; take F ; ::_thesis: for x being Point of M holds F . x = upper_bound ((dist x) .: P) thus for x being Point of M holds F . x = upper_bound ((dist x) .: P) by A4; ::_thesis: verum end; uniqueness for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b1 . x = upper_bound ((dist x) .: P) ) & ( for x being Point of M holds b2 . x = upper_bound ((dist x) .: P) ) holds b1 = b2 proof let F1, F2 be Function of (TopSpaceMetr M),R^1; ::_thesis: ( ( for x being Point of M holds F1 . x = upper_bound ((dist x) .: P) ) & ( for x being Point of M holds F2 . x = upper_bound ((dist x) .: P) ) implies F1 = F2 ) assume A5: for y being Point of M holds F1 . y = upper_bound ((dist y) .: P) ; ::_thesis: ( ex x being Point of M st not F2 . x = upper_bound ((dist x) .: P) or F1 = F2 ) assume A6: for y being Point of M holds F2 . y = upper_bound ((dist y) .: P) ; ::_thesis: F1 = F2 for y being set st y in the carrier of (TopSpaceMetr M) holds F1 . y = F2 . y proof let y be set ; ::_thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y ) A7: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; assume y in the carrier of (TopSpaceMetr M) ; ::_thesis: F1 . y = F2 . y then reconsider y = y as Point of M by A7; F1 . y = upper_bound ((dist y) .: P) by A5 .= F2 . y by A6 ; hence F1 . y = F2 . y ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:12; ::_thesis: verum end; func dist_min P -> Function of (TopSpaceMetr M),R^1 means :Def6: :: WEIERSTR:def 6 for x being Point of M holds it . x = lower_bound ((dist x) .: P); existence ex b1 being Function of (TopSpaceMetr M),R^1 st for x being Point of M holds b1 . x = lower_bound ((dist x) .: P) proof defpred S1[ Element of M, Element of R^1] means for s being Element of M for t being Element of R^1 st \$1 = s & \$2 = t holds t = lower_bound ((dist s) .: P); A8: for s being Element of M ex t being Element of R^1 st S1[s,t] proof let s be Element of M; ::_thesis: ex t being Element of R^1 st S1[s,t] consider t being Real such that A9: t = lower_bound ((dist s) .: P) ; reconsider t = t as Element of R^1 by TOPMETR:17; take t ; ::_thesis: S1[s,t] thus S1[s,t] by A9; ::_thesis: verum end; consider F being Function of the carrier of M, the carrier of R^1 such that A10: for x being Element of M holds S1[x,F . x] from FUNCT_2:sch_3(A8); A11: for y being Point of M holds F . y = lower_bound ((dist y) .: P) by A10; TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider F = F as Function of (TopSpaceMetr M),R^1 ; take F ; ::_thesis: for x being Point of M holds F . x = lower_bound ((dist x) .: P) thus for x being Point of M holds F . x = lower_bound ((dist x) .: P) by A11; ::_thesis: verum end; uniqueness for b1, b2 being Function of (TopSpaceMetr M),R^1 st ( for x being Point of M holds b1 . x = lower_bound ((dist x) .: P) ) & ( for x being Point of M holds b2 . x = lower_bound ((dist x) .: P) ) holds b1 = b2 proof let F1, F2 be Function of (TopSpaceMetr M),R^1; ::_thesis: ( ( for x being Point of M holds F1 . x = lower_bound ((dist x) .: P) ) & ( for x being Point of M holds F2 . x = lower_bound ((dist x) .: P) ) implies F1 = F2 ) assume A12: for y being Point of M holds F1 . y = lower_bound ((dist y) .: P) ; ::_thesis: ( ex x being Point of M st not F2 . x = lower_bound ((dist x) .: P) or F1 = F2 ) assume A13: for y being Point of M holds F2 . y = lower_bound ((dist y) .: P) ; ::_thesis: F1 = F2 for y being set st y in the carrier of (TopSpaceMetr M) holds F1 . y = F2 . y proof let y be set ; ::_thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y ) A14: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; assume y in the carrier of (TopSpaceMetr M) ; ::_thesis: F1 . y = F2 . y then reconsider y = y as Point of M by A14; F1 . y = lower_bound ((dist y) .: P) by A12 .= F2 . y by A13 ; hence F1 . y = F2 . y ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def5 defines dist_max WEIERSTR:def_5_:_ for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) for b3 being Function of (TopSpaceMetr M),R^1 holds ( b3 = dist_max P iff for x being Point of M holds b3 . x = upper_bound ((dist x) .: P) ); :: deftheorem Def6 defines dist_min WEIERSTR:def_6_:_ for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) for b3 being Function of (TopSpaceMetr M),R^1 holds ( b3 = dist_min P iff for x being Point of M holds b3 . x = lower_bound ((dist x) .: P) ); theorem Th19: :: WEIERSTR:19 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) st P is compact holds for p1, p2 being Point of M st p1 in P holds ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) proof let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P is compact holds for p1, p2 being Point of M st p1 in P holds ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) let P be Subset of (TopSpaceMetr M); ::_thesis: ( P is compact implies for p1, p2 being Point of M st p1 in P holds ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) ) assume A1: P is compact ; ::_thesis: for p1, p2 being Point of M st p1 in P holds ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) let p1, p2 be Point of M; ::_thesis: ( p1 in P implies ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) ) dist p2 is continuous by Th16; then [#] ((dist p2) .: P) is real-bounded by A1, Th8, Th11; then A2: ( [#] ((dist p2) .: P) is bounded_above & [#] ((dist p2) .: P) is bounded_below ) by XXREAL_2:def_11; assume A3: p1 in P ; ::_thesis: ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) ( dist (p1,p2) = (dist p2) . p1 & dom (dist p2) = the carrier of (TopSpaceMetr M) ) by Def4, FUNCT_2:def_1; then dist (p1,p2) in [#] ((dist p2) .: P) by A3, FUNCT_1:def_6; hence ( dist (p1,p2) <= upper_bound ((dist p2) .: P) & lower_bound ((dist p2) .: P) <= dist (p1,p2) ) by A2, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum end; theorem Th20: :: WEIERSTR:20 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) proof let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) ) assume that A1: P <> {} and A2: P is compact ; ::_thesis: for p1, p2 being Point of M holds abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) let p1, p2 be Point of M; ::_thesis: abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) consider x1 being Point of (TopSpaceMetr M) such that A3: x1 in P and A4: (dist p1) . x1 = upper_bound ((dist p1) .: P) by A1, A2, Th14, Th16; A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider x1 = x1 as Point of M ; consider x2 being Point of (TopSpaceMetr M) such that A6: x2 in P and A7: (dist p2) . x2 = upper_bound ((dist p2) .: P) by A1, A2, Th14, Th16; reconsider x2 = x2 as Point of M by A5; A8: dist (x2,p2) = upper_bound ((dist p2) .: P) by A7, Def4; (dist p1) . x1 = dist (x1,p1) by Def4; then ( dist (x2,p2) <= (dist (x2,p1)) + (dist (p1,p2)) & dist (x2,p1) <= dist (x1,p1) ) by A2, A4, A6, Th19, METRIC_1:4; then (dist (x2,p2)) - (dist (x1,p1)) <= ((dist (x2,p1)) + (dist (p1,p2))) - (dist (x2,p1)) by XREAL_1:13; then A9: - (dist (p1,p2)) <= - ((dist (x2,p2)) - (dist (x1,p1))) by XREAL_1:24; (dist p2) . x2 = dist (x2,p2) by Def4; then ( dist (x1,p1) <= (dist (x1,p2)) + (dist (p2,p1)) & dist (x1,p2) <= dist (x2,p2) ) by A2, A3, A7, Th19, METRIC_1:4; then A10: (dist (x1,p1)) - (dist (x2,p2)) <= ((dist (x1,p2)) + (dist (p1,p2))) - (dist (x1,p2)) by XREAL_1:13; dist (x1,p1) = upper_bound ((dist p1) .: P) by A4, Def4; hence abs ((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))) <= dist (p1,p2) by A8, A10, A9, ABSVALUE:5; ::_thesis: verum end; theorem :: WEIERSTR:21 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds abs (x1 - x2) <= dist (p1,p2) proof let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds abs (x1 - x2) <= dist (p1,p2) let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds abs (x1 - x2) <= dist (p1,p2) ) assume A1: ( P <> {} & P is compact ) ; ::_thesis: for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds abs (x1 - x2) <= dist (p1,p2) let p1, p2 be Point of M; ::_thesis: for x1, x2 being Real st x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 holds abs (x1 - x2) <= dist (p1,p2) let x1, x2 be Real; ::_thesis: ( x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 implies abs (x1 - x2) <= dist (p1,p2) ) assume A2: ( x1 = (dist_max P) . p1 & x2 = (dist_max P) . p2 ) ; ::_thesis: abs (x1 - x2) <= dist (p1,p2) ( (dist_max P) . p1 = upper_bound ((dist p1) .: P) & (dist_max P) . p2 = upper_bound ((dist p2) .: P) ) by Def5; hence abs (x1 - x2) <= dist (p1,p2) by A1, A2, Th20; ::_thesis: verum end; theorem Th22: :: WEIERSTR:22 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) proof let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) ) assume that A1: P <> {} and A2: P is compact ; ::_thesis: for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) let p1, p2 be Point of M; ::_thesis: abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) consider x1 being Point of (TopSpaceMetr M) such that A3: x1 in P and A4: (dist p1) . x1 = lower_bound ((dist p1) .: P) by A1, A2, Th15, Th16; A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider x1 = x1 as Point of M ; consider x2 being Point of (TopSpaceMetr M) such that A6: x2 in P and A7: (dist p2) . x2 = lower_bound ((dist p2) .: P) by A1, A2, Th15, Th16; reconsider x2 = x2 as Point of M by A5; A8: dist (x2,p2) = lower_bound ((dist p2) .: P) by A7, Def4; (dist p2) . x2 = dist (x2,p2) by Def4; then ( dist (x1,p2) <= (dist (x1,p1)) + (dist (p1,p2)) & dist (x2,p2) <= dist (x1,p2) ) by A2, A3, A7, Th19, METRIC_1:4; then dist (x2,p2) <= (dist (x1,p1)) + (dist (p1,p2)) by XXREAL_0:2; then (dist (x2,p2)) - (dist (x1,p1)) <= dist (p1,p2) by XREAL_1:20; then A9: - (dist (p1,p2)) <= - ((dist (x2,p2)) - (dist (x1,p1))) by XREAL_1:24; (dist p1) . x1 = dist (x1,p1) by Def4; then ( dist (x2,p1) <= (dist (x2,p2)) + (dist (p2,p1)) & dist (x1,p1) <= dist (x2,p1) ) by A2, A4, A6, Th19, METRIC_1:4; then dist (x1,p1) <= (dist (x2,p2)) + (dist (p1,p2)) by XXREAL_0:2; then A10: (dist (x1,p1)) - (dist (x2,p2)) <= dist (p1,p2) by XREAL_1:20; dist (x1,p1) = lower_bound ((dist p1) .: P) by A4, Def4; hence abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist (p1,p2) by A8, A10, A9, ABSVALUE:5; ::_thesis: verum end; theorem :: WEIERSTR:23 for M being non empty MetrSpace for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds abs (x1 - x2) <= dist (p1,p2) proof let M be non empty MetrSpace; ::_thesis: for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds abs (x1 - x2) <= dist (p1,p2) let P be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact implies for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds abs (x1 - x2) <= dist (p1,p2) ) assume A1: ( P <> {} & P is compact ) ; ::_thesis: for p1, p2 being Point of M for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds abs (x1 - x2) <= dist (p1,p2) let p1, p2 be Point of M; ::_thesis: for x1, x2 being Real st x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 holds abs (x1 - x2) <= dist (p1,p2) let x1, x2 be Real; ::_thesis: ( x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 implies abs (x1 - x2) <= dist (p1,p2) ) assume A2: ( x1 = (dist_min P) . p1 & x2 = (dist_min P) . p2 ) ; ::_thesis: abs (x1 - x2) <= dist (p1,p2) ( (dist_min P) . p1 = lower_bound ((dist p1) .: P) & (dist_min P) . p2 = lower_bound ((dist p2) .: P) ) by Def6; hence abs (x1 - x2) <= dist (p1,p2) by A1, A2, Th22; ::_thesis: verum end; Lm2: [#] R^1 <> {} ; theorem Th24: :: WEIERSTR:24 for M being non empty MetrSpace for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds dist_max X is continuous proof let M be non empty MetrSpace; ::_thesis: for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds dist_max X is continuous let X be Subset of (TopSpaceMetr M); ::_thesis: ( X <> {} & X is compact implies dist_max X is continuous ) assume A1: ( X <> {} & X is compact ) ; ::_thesis: dist_max X is continuous for P being Subset of R^1 st P is open holds (dist_max X) " P is open proof let P be Subset of R^1; ::_thesis: ( P is open implies (dist_max X) " P is open ) assume A2: P is open ; ::_thesis: (dist_max X) " P is open for p being Point of M st p in (dist_max X) " P holds ex r being real number st ( r > 0 & Ball (p,r) c= (dist_max X) " P ) proof let p be Point of M; ::_thesis: ( p in (dist_max X) " P implies ex r being real number st ( r > 0 & Ball (p,r) c= (dist_max X) " P ) ) consider y being Point of RealSpace such that A3: y = upper_bound ((dist p) .: X) by METRIC_1:def_13; assume p in (dist_max X) " P ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (dist_max X) " P ) then A4: (dist_max X) . p in P by FUNCT_1:def_7; reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6; y in P by A4, A3, Def5; then consider r being real number such that A5: r > 0 and A6: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def_6; reconsider r = r as Real by XREAL_0:def_1; take r ; ::_thesis: ( r > 0 & Ball (p,r) c= (dist_max X) " P ) Ball (p,r) c= (dist_max X) " P proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball (p,r) or z in (dist_max X) " P ) assume A7: z in Ball (p,r) ; ::_thesis: z in (dist_max X) " P then reconsider z = z as Point of M ; consider q being Point of RealSpace such that A8: q = upper_bound ((dist z) .: X) by METRIC_1:def_13; dist (p,z) < r by A7, METRIC_1:11; then (abs ((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X)))) + (dist (p,z)) < r + (dist (p,z)) by A1, Th20, XREAL_1:8; then abs ((upper_bound ((dist p) .: X)) - (upper_bound ((dist z) .: X))) < r by XREAL_1:6; then dist (y,q) < r by A3, A8, TOPMETR:11; then A9: q in Ball (y,r) by METRIC_1:11; dom (dist_max X) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then A10: dom (dist_max X) = the carrier of M by TOPMETR:12; q = (dist_max X) . z by A8, Def5; hence z in (dist_max X) " P by A6, A9, A10, FUNCT_1:def_7; ::_thesis: verum end; hence ( r > 0 & Ball (p,r) c= (dist_max X) " P ) by A5; ::_thesis: verum end; hence (dist_max X) " P is open by TOPMETR:15; ::_thesis: verum end; hence dist_max X is continuous by Lm2, TOPS_2:43; ::_thesis: verum end; theorem :: WEIERSTR:25 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1 being Point of (TopSpaceMetr M) st ( x1 in Q & (dist_max P) . x1 = upper_bound ((dist_max P) .: Q) ) by Th14, Th24; theorem :: WEIERSTR:26 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x2 being Point of (TopSpaceMetr M) st ( x2 in Q & (dist_max P) . x2 = lower_bound ((dist_max P) .: Q) ) by Th15, Th24; theorem Th27: :: WEIERSTR:27 for M being non empty MetrSpace for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds dist_min X is continuous proof let M be non empty MetrSpace; ::_thesis: for X being Subset of (TopSpaceMetr M) st X <> {} & X is compact holds dist_min X is continuous let X be Subset of (TopSpaceMetr M); ::_thesis: ( X <> {} & X is compact implies dist_min X is continuous ) assume A1: ( X <> {} & X is compact ) ; ::_thesis: dist_min X is continuous for P being Subset of R^1 st P is open holds (dist_min X) " P is open proof let P be Subset of R^1; ::_thesis: ( P is open implies (dist_min X) " P is open ) assume A2: P is open ; ::_thesis: (dist_min X) " P is open for p being Point of M st p in (dist_min X) " P holds ex r being real number st ( r > 0 & Ball (p,r) c= (dist_min X) " P ) proof let p be Point of M; ::_thesis: ( p in (dist_min X) " P implies ex r being real number st ( r > 0 & Ball (p,r) c= (dist_min X) " P ) ) assume A3: p in (dist_min X) " P ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (dist_min X) " P ) ex r being Real st ( r > 0 & Ball (p,r) c= (dist_min X) " P ) proof A4: (dist_min X) . p in P by A3, FUNCT_1:def_7; reconsider P = P as Subset of (TopSpaceMetr RealSpace) by TOPMETR:def_6; consider y being Point of RealSpace such that A5: y = lower_bound ((dist p) .: X) by METRIC_1:def_13; y in P by A4, A5, Def6; then consider r being real number such that A6: r > 0 and A7: Ball (y,r) c= P by A2, TOPMETR:15, TOPMETR:def_6; reconsider r = r as Real by XREAL_0:def_1; take r ; ::_thesis: ( r > 0 & Ball (p,r) c= (dist_min X) " P ) Ball (p,r) c= (dist_min X) " P proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Ball (p,r) or z in (dist_min X) " P ) assume A8: z in Ball (p,r) ; ::_thesis: z in (dist_min X) " P then reconsider z = z as Point of M ; consider q being Point of RealSpace such that A9: q = lower_bound ((dist z) .: X) by METRIC_1:def_13; dist (p,z) < r by A8, METRIC_1:11; then (abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X)))) + (dist (p,z)) < r + (dist (p,z)) by A1, Th22, XREAL_1:8; then abs ((lower_bound ((dist p) .: X)) - (lower_bound ((dist z) .: X))) < r by XREAL_1:6; then dist (y,q) < r by A5, A9, TOPMETR:11; then A10: q in Ball (y,r) by METRIC_1:11; dom (dist_min X) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then A11: dom (dist_min X) = the carrier of M by TOPMETR:12; q = (dist_min X) . z by A9, Def6; hence z in (dist_min X) " P by A7, A10, A11, FUNCT_1:def_7; ::_thesis: verum end; hence ( r > 0 & Ball (p,r) c= (dist_min X) " P ) by A6; ::_thesis: verum end; hence ex r being real number st ( r > 0 & Ball (p,r) c= (dist_min X) " P ) ; ::_thesis: verum end; hence (dist_min X) " P is open by TOPMETR:15; ::_thesis: verum end; hence dist_min X is continuous by Lm2, TOPS_2:43; ::_thesis: verum end; theorem :: WEIERSTR:28 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1 being Point of (TopSpaceMetr M) st ( x1 in Q & (dist_min P) . x1 = upper_bound ((dist_min P) .: Q) ) by Th14, Th27; theorem :: WEIERSTR:29 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x2 being Point of (TopSpaceMetr M) st ( x2 in Q & (dist_min P) . x2 = lower_bound ((dist_min P) .: Q) ) by Th15, Th27; definition let M be non empty MetrSpace; let P, Q be Subset of (TopSpaceMetr M); func min_dist_min (P,Q) -> Real equals :: WEIERSTR:def 7 lower_bound ((dist_min P) .: Q); correctness coherence lower_bound ((dist_min P) .: Q) is Real; ; func max_dist_min (P,Q) -> Real equals :: WEIERSTR:def 8 upper_bound ((dist_min P) .: Q); correctness coherence upper_bound ((dist_min P) .: Q) is Real; ; func min_dist_max (P,Q) -> Real equals :: WEIERSTR:def 9 lower_bound ((dist_max P) .: Q); correctness coherence lower_bound ((dist_max P) .: Q) is Real; ; func max_dist_max (P,Q) -> Real equals :: WEIERSTR:def 10 upper_bound ((dist_max P) .: Q); correctness coherence upper_bound ((dist_max P) .: Q) is Real; ; end; :: deftheorem defines min_dist_min WEIERSTR:def_7_:_ for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) holds min_dist_min (P,Q) = lower_bound ((dist_min P) .: Q); :: deftheorem defines max_dist_min WEIERSTR:def_8_:_ for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) holds max_dist_min (P,Q) = upper_bound ((dist_min P) .: Q); :: deftheorem defines min_dist_max WEIERSTR:def_9_:_ for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) holds min_dist_max (P,Q) = lower_bound ((dist_max P) .: Q); :: deftheorem defines max_dist_max WEIERSTR:def_10_:_ for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) holds max_dist_max (P,Q) = upper_bound ((dist_max P) .: Q); theorem :: WEIERSTR:30 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) proof let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) ) assume that A1: ( P <> {} & P is compact ) and A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) consider x2 being Point of (TopSpaceMetr M) such that A3: x2 in Q and A4: (dist_min P) . x2 = lower_bound ((dist_min P) .: Q) by A1, A2, Th15, Th27; A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider x2 = x2 as Point of M ; consider x1 being Point of (TopSpaceMetr M) such that A6: x1 in P and A7: (dist x2) . x1 = lower_bound ((dist x2) .: P) by A1, Th15, Th16; reconsider x1 = x1 as Point of M by A5; take x1 ; ::_thesis: ex x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) take x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) dist (x1,x2) = (dist x2) . x1 by Def4 .= lower_bound ((dist_min P) .: Q) by A4, A7, Def6 ; hence ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_min (P,Q) ) by A3, A6; ::_thesis: verum end; theorem :: WEIERSTR:31 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) proof let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) ) assume that A1: ( P <> {} & P is compact ) and A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) consider x2 being Point of (TopSpaceMetr M) such that A3: x2 in Q and A4: (dist_max P) . x2 = lower_bound ((dist_max P) .: Q) by A1, A2, Th15, Th24; A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider x2 = x2 as Point of M ; consider x1 being Point of (TopSpaceMetr M) such that A6: x1 in P and A7: (dist x2) . x1 = upper_bound ((dist x2) .: P) by A1, Th14, Th16; reconsider x1 = x1 as Point of M by A5; take x1 ; ::_thesis: ex x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) take x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) dist (x1,x2) = (dist x2) . x1 by Def4 .= lower_bound ((dist_max P) .: Q) by A4, A7, Def5 ; hence ( x1 in P & x2 in Q & dist (x1,x2) = min_dist_max (P,Q) ) by A3, A6; ::_thesis: verum end; theorem :: WEIERSTR:32 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) proof let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) ) assume that A1: ( P <> {} & P is compact ) and A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) consider x2 being Point of (TopSpaceMetr M) such that A3: x2 in Q and A4: (dist_min P) . x2 = upper_bound ((dist_min P) .: Q) by A1, A2, Th14, Th27; A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider x2 = x2 as Point of M ; consider x1 being Point of (TopSpaceMetr M) such that A6: x1 in P and A7: (dist x2) . x1 = lower_bound ((dist x2) .: P) by A1, Th15, Th16; reconsider x1 = x1 as Point of M by A5; take x1 ; ::_thesis: ex x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) take x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) dist (x1,x2) = (dist x2) . x1 by Def4 .= upper_bound ((dist_min P) .: Q) by A4, A7, Def6 ; hence ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) ) by A3, A6; ::_thesis: verum end; theorem :: WEIERSTR:33 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) proof let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) ) assume that A1: ( P <> {} & P is compact ) and A2: ( Q <> {} & Q is compact ) ; ::_thesis: ex x1, x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) consider x2 being Point of (TopSpaceMetr M) such that A3: x2 in Q and A4: (dist_max P) . x2 = upper_bound ((dist_max P) .: Q) by A1, A2, Th14, Th24; A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5; then reconsider x2 = x2 as Point of M ; consider x1 being Point of (TopSpaceMetr M) such that A6: x1 in P and A7: (dist x2) . x1 = upper_bound ((dist x2) .: P) by A1, Th14, Th16; reconsider x1 = x1 as Point of M by A5; take x1 ; ::_thesis: ex x2 being Point of M st ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) take x2 ; ::_thesis: ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) dist (x1,x2) = (dist x2) . x1 by Def4 .= upper_bound ((dist_max P) .: Q) by A4, A7, Def5 ; hence ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) by A3, A6; ::_thesis: verum end; theorem :: WEIERSTR:34 for M being non empty MetrSpace for P, Q being Subset of (TopSpaceMetr M) st P is compact & Q is compact holds for x1, x2 being Point of M st x1 in P & x2 in Q holds ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) proof let M be non empty MetrSpace; ::_thesis: for P, Q being Subset of (TopSpaceMetr M) st P is compact & Q is compact holds for x1, x2 being Point of M st x1 in P & x2 in Q holds ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) let P, Q be Subset of (TopSpaceMetr M); ::_thesis: ( P is compact & Q is compact implies for x1, x2 being Point of M st x1 in P & x2 in Q holds ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) ) assume that A1: P is compact and A2: Q is compact ; ::_thesis: for x1, x2 being Point of M st x1 in P & x2 in Q holds ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) let x1, x2 be Point of M; ::_thesis: ( x1 in P & x2 in Q implies ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) ) assume that A3: x1 in P and A4: x2 in Q ; ::_thesis: ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) dist_max P is continuous by A1, A3, Th24; then [#] ((dist_max P) .: Q) is real-bounded by A2, Th8, Th11; then A5: [#] ((dist_max P) .: Q) is bounded_above by XXREAL_2:def_11; x2 in the carrier of M ; then x2 in the carrier of (TopSpaceMetr M) by TOPMETR:12; then (dist_min P) . x2 in the carrier of R^1 by FUNCT_2:5; then consider z being Real such that A6: z = (dist_min P) . x2 by TOPMETR:17; dist_min P is continuous by A1, A3, Th27; then [#] ((dist_min P) .: Q) is real-bounded by A2, Th8, Th11; then A7: [#] ((dist_min P) .: Q) is bounded_below by XXREAL_2:def_11; dom (dist_min P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then z in [#] ((dist_min P) .: Q) by A4, A6, FUNCT_1:def_6; then A8: lower_bound ((dist_min P) .: Q) <= z by A7, SEQ_4:def_2; x2 in the carrier of M ; then x2 in the carrier of (TopSpaceMetr M) by TOPMETR:12; then (dist_max P) . x2 in the carrier of R^1 by FUNCT_2:5; then consider y being Real such that A9: y = (dist_max P) . x2 by TOPMETR:17; dom (dist_max P) = the carrier of (TopSpaceMetr M) by FUNCT_2:def_1; then y in [#] ((dist_max P) .: Q) by A4, A9, FUNCT_1:def_6; then A10: y <= upper_bound ((dist_max P) .: Q) by A5, SEQ_4:def_1; A11: lower_bound ((dist x2) .: P) = z by A6, Def6; A12: upper_bound ((dist x2) .: P) = y by A9, Def5; ( dist (x1,x2) <= upper_bound ((dist x2) .: P) & lower_bound ((dist x2) .: P) <= dist (x1,x2) ) by A1, A3, Th19; hence ( min_dist_min (P,Q) <= dist (x1,x2) & dist (x1,x2) <= max_dist_max (P,Q) ) by A12, A10, A11, A8, XXREAL_0:2; ::_thesis: verum end;