:: The Theorem of Weierstrass :: by J\'ozef Bia\las and Yatsuka Nakamura :: :: Received July 10, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, METRIC_1, PRE_TOPC, REAL_1, XBOOLE_0, TARSKI, COMPLEX1, ARYTM_3, XXREAL_0, CARD_1, ARYTM_1, NAT_1, SETFAM_1, FINSEQ_1, TOPMETR, RELAT_1, FINSET_1, FUNCT_1, ORDINAL2, RCOMP_1, SUBSET_1, ZFMISC_1, EUCLID, XXREAL_2, STRUCT_0, PCOMPS_1, XREAL_0, ORDINAL1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, WEIERSTR; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, SETFAM_1, ORDINAL1, NUMBERS, XREAL_0, COMPLEX1, REAL_1, NAT_1, TOPMETR, METRIC_1, COMPTS_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, FINSEQ_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_2, RCOMP_1, EUCLID, PCOMPS_1, XXREAL_0, XXREAL_2; constructors REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, TOPS_2, COMPTS_1, EUCLID, TOPMETR, SEQ_1, BINOP_2, PCOMPS_1, COMSEQ_2; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, FINSEQ_1; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; definitions STRUCT_0, TARSKI, XXREAL_2; theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, FINSEQ_1, ZFMISC_1, SEQ_2, SEQ_4, ABSVALUE, COMPTS_1, RELAT_1, TOPS_2, RCOMP_1, TOPMETR, PCOMPS_1, METRIC_1, METRIC_6, XBOOLE_0, XBOOLE_1, XREAL_0, SUBSET_1, XREAL_1, COMPLEX1, XXREAL_0, SETFAM_1, XXREAL_2; schemes NAT_1, SUBSET_1, FUNCT_2; begin theorem Th1: for M being MetrSpace, x1,x2 being Point of M, r1,r2 being Real ex x being Point of M, r being Real st Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x,r) proof let M be MetrSpace; let x1,x2 be Point of M; let r1,r2 be Real; reconsider x = x1 as Point of M; reconsider r = abs(r1) + abs(r2) + dist(x1,x2) as Real; take x; take r; for a being set holds a in Ball(x1,r1) \/ Ball(x2,r2) implies a in Ball( x,r) proof let a be set; assume A1: a in (Ball(x1,r1) \/ Ball(x2,r2)); then reconsider a as Point of M; now per cases by A1,XBOOLE_0:def 3; case A2: a in Ball(x1,r1); 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; M is non empty by A2; hence thesis by A5,METRIC_1:11; end; case A6: a in Ball(x2,r2); 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; M is non empty by A6; hence thesis by A7,METRIC_1:11; end; end; hence thesis; end; hence thesis by TARSKI:def 3; end; theorem Th2: for M being MetrSpace, n being Nat, F being Subset-Family of M, 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 st ex r being Real st union F c= union G \/ Ball(x,r) ) proof let M be MetrSpace; let n be Nat; let F be Subset-Family of M; let p be FinSequence; assume that A1: F is being_ball-family and A2: rng p = F and A3: dom p = Seg(n+1); 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 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 st ex r being Real st union F c= union G \/ Ball( x,r) proof take x; take r; union F c= union G \/ Ball(x,r) proof let t be set; assume t in union F; 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 per cases by A8,A12,XBOOLE_0:def 3; case s in dom q; then q.s in G & q.s = A by A13,FUNCT_1:47,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 thesis by A14; end; case s in {n+1}; then p.s = Ball(x,r) by A5,TARSKI:def 1; hence thesis by A10,A13,XBOOLE_0:def 3; end; end; hence thesis; end; hence thesis; end; take G; for x being set holds x in G implies ex y being Point of M st ex r being Real st x = Ball(y,r) by A1,A2,A6,TOPMETR:def 4; hence thesis by A7,A9,TOPMETR:def 4; end; theorem Th3: for M being MetrSpace, F being Subset-Family of M st F is finite & F is being_ball-family holds ex x being Point of M, r being Real st union F c= Ball(x,r) proof let M be MetrSpace; let F be Subset-Family of M; assume that A1: F is finite and A2: F is being_ball-family; 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 holds for p being FinSequence st rng p = F & dom p = Seg n holds ex x being Point of M, r being Real st union F c= Ball(x,r) proof defpred P[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 st ex r being Real st union F c= Ball(x,r)); A5: for k being Nat st P[k] holds P[k + 1] proof let k be Nat; assume A6: P[k]; let F be Subset-Family of M; assume that F is finite and A7: F is being_ball-family; let n be Nat; assume A8: n = k+1; let p be FinSequence; assume rng p = F & dom p = Seg(n); 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 st 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; consider r being Real such that A16: Ball(x1,r1) \/ Ball(x2,r2) c= Ball(x,r) by A15; take 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 thesis by A16,XBOOLE_1:1; end; A17: P[0] proof let F be Subset-Family of M; assume that F is finite and F is being_ball-family; let n be Nat; assume n = 0; then A18: Seg n = {}; for p being FinSequence st rng p = F & dom p = Seg(n) holds ex x being Point of M st ex r being Real st union F c= Ball(x,r) proof set x = the Point of M; let p be FinSequence; assume A19: rng p = F & dom p = Seg(n); take x, 0; union F = {} by A19,A18,RELAT_1:42,ZFMISC_1:2; hence thesis by XBOOLE_1:2; end; hence thesis; end; for n being Nat holds P[n] from NAT_1:sch 2(A17,A5); hence thesis; end; ex n being Nat st dom p = Seg n by FINSEQ_1:def 2; hence thesis by A2,A4,A3; end; theorem Th4: for T,S being non empty TopSpace, f being Function of T,S, 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; let f be Function of T,S; let B be Subset-Family of S; assume that A1: f is continuous and A2: B is open; for P being Subset of T holds P in f"B implies P is open proof let P be Subset of T; assume A3: P in f"(B); thus P is open 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 as Subset of S; [#]S <> {} & C is open by A2,A4,TOPS_2:def 1; hence thesis by A1,A5,TOPS_2:43; end; end; hence thesis by TOPS_2:def 1; end; theorem for T,S being non empty TopSpace holds for f being Function of T,S holds for Q being Subset-Family of S holds Q is finite implies f"Q is finite proof let T,S be non empty TopSpace; let f be Function of T,S; let Q be Subset-Family of S; defpred EF[Subset of [#](S),Subset of [#](T)] means for s,t being set holds ($1 = s & $2 = t implies t = f"s); assume 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 EF[x,y] proof let x be Subset of [#](S); reconsider x as set; set y = f"x; reconsider y as Subset of [#](T); take y; thus thesis; end; consider F being Function of bool [#](S),bool [#](T) such that A3: for x being Subset of [#](S) holds EF[x,F.x qua Subset of [#](T)] 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; A4: dom F = bool [#](S) by FUNCT_2:def 1; thus x in F.:Q implies x in f"Q proof assume 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 as Subset of S by A5; F.y = f"y by A3; hence thesis by A6,FUNCT_2:def 9; end; assume A7: x in f"Q; then reconsider 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 thesis by A8,A4,FUNCT_1:def 6; end; then A10: F.:Q = f"Q by TARSKI:1; ex q being FinSequence st rng q = f"Q proof take q; thus thesis by A1,A10,RELAT_1:127; end; hence thesis; end; theorem for T,S being non empty TopSpace holds for f being Function of T,S holds for P being Subset-Family of T holds P is finite implies f.:P is finite proof let T,S be non empty TopSpace; let f be Function of T,S; let P be Subset-Family of T; defpred EF[Subset of [#](T),Subset of [#](S)] means for s,t being set holds ($1 = s & $2 = t implies t = f.:s); assume 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 EF[x,y] proof let x be Subset of [#](T); reconsider x as set; set y = f.:x; reconsider y as Subset of [#](S); take y; thus thesis; end; consider F being Function of bool [#](T),bool [#](S) such that A3: for x being Subset of [#](T) holds EF[x,F.x qua Subset of [#](S)] 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; thus x in F.:P implies x in f.:P proof assume 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 as Subset of T by A4; F.y = f.:y by A3; hence thesis by A5,FUNCT_2:def 10; end; thus x in f.:P implies x in F.:P proof assume A6: x in f.:P; then reconsider 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 thesis by A7,A9,FUNCT_1:def 6; end; end; then A10: F.:P = f.:P by TARSKI:1; ex q being FinSequence st rng q = f.:P proof take q; thus thesis by A1,A10,RELAT_1:127; end; hence thesis; end; theorem Th7: for T,S being non empty TopSpace holds for f being Function of T ,S holds for P being Subset of T holds for F being Subset-Family of S holds (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 proof let T,S be non empty TopSpace; let f be Function of T,S; let P be Subset of T; let F be Subset-Family of S; 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; A4: P c= union B by A2,SETFAM_1:def 11; now per cases; case A5: P <> {}; thus 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 P0[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 P0[x,y] proof let x be Element of D; A9: x in B by A7; then reconsider 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 as Subset of [#](S); take y; thus thesis by A10; end; consider F0 being Function of D,bool [#](S) such that A11: for x being Element of D holds P0[x,F0.x qua Subset of [#](S) ] 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 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: G c= F proof let x be set; assume x in G; 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,12; hence thesis by A7,A12; end; then reconsider G as Subset-Family of S by XBOOLE_1:1; reconsider G as Subset-Family of S; take G; for x being set holds x in f.:P implies x in union G proof let x be set; assume A16: x in f.:P; 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 A; f.:(f"(F0.C)) c= F0.C & G = rng F0 by A6,A13,FUNCT_1:75,RELAT_1:28 ; hence thesis by A21,A22,FUNCT_2:4; end; hence thesis by TARSKI:def 4; end; then f.:P c= union G by TARSKI:def 3; hence thesis by A14,SETFAM_1:def 11; end; hence thesis; end; case A23: P = {}; 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 as Subset-Family of S; take G; f.:P = {} proof assume f.:P <> {}; 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; end; hence thesis by SETFAM_1:def 11,XBOOLE_1:2,ZFMISC_1:2; end; hence thesis; end; end; hence thesis; end; begin :: :: The Weierstrass` theorem :: theorem Th8: for T,S being non empty TopSpace holds for f being Function of T ,S holds for P being Subset of T holds P is compact & f is continuous implies f .:P is compact proof let T,S be non empty TopSpace; let f be Function of T,S; let P be Subset of T; assume that A1: P is compact and A2: f is continuous; 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 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; assume that A4: F0 is Cover of f.:P and A5: F0 is open; set B0 = f"F0; A6: f.:P c= union F0 by A4,SETFAM_1:def 11; P c= union B0 proof let x be set; thus x in P implies x in union B0 proof A7: f"(union F0) c= union(f"F0) proof let y be set; assume A8: y in f"(union F0); thus y in union(f"F0) 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 Z; thus thesis by A10,A9,FUNCT_1:def 7,FUNCT_2:def 9; end; hence thesis by TARSKI:def 4; end; end; assume A11: x in P; then A12: f.x in f.:P by A3,FUNCT_1:def 6; reconsider 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; assume A15: y in f"{f.x}; 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 thesis by A16,FUNCT_1:def 7; 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 thesis by A7; end; end; then A17: B0 is Cover of P by SETFAM_1:def 11; B0 is open by A2,A5,Th4; then ex B being Subset-Family of T st B c= B0 & 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; thus thesis by A18; end; hence thesis by COMPTS_1:def 4; end; theorem for T being non empty TopSpace holds for f being Function of T,R^1 holds for P being Subset of T holds P is compact & f is continuous implies f.:P is compact by Th8; theorem for f being Function of TOP-REAL 2,R^1 holds for P being Subset of TOP-REAL 2 holds P is compact & f is continuous implies f.:P is compact by Th8 ; definition let P be Subset of R^1; func [#](P) -> Subset of REAL equals P; correctness by TOPMETR:17; end; theorem Th11: for P being Subset of R^1 holds P is compact implies [#](P) is real-bounded proof let P be Subset of R^1; assume A1: P is compact; thus [#](P) is real-bounded proof now per cases; case [#](P) <> {}; set r0 = 1; defpred P[Subset of R^1] means ex x being Point of RealSpace st x in [#](P) & $1 = Ball(x,r0); consider R being Subset-Family of R^1 such that A2: for A being Subset of R^1 holds A in R iff P[A] from SUBSET_1: sch 3; for x being set holds x in [#](P) implies x in union R proof let x be set; assume A3: x in [#](P); then reconsider x as Point of RealSpace by METRIC_1:def 13; consider A being Subset of RealSpace such that A4: A = Ball(x,r0); R^1 = TopStruct (#the carrier of RealSpace, Family_open_set( RealSpace)#) by PCOMPS_1:def 5,TOPMETR:def 6; then reconsider A as Subset of R^1; ex A being set st x in A & A in R proof take A; dist(x,x) = 0 by METRIC_1:1; hence thesis by A2,A3,A4,METRIC_1:11; end; hence thesis by TARSKI:def 4; 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 holds A in R implies A is open proof let A be Subset of R^1; assume A in R; then ex x being Point of RealSpace st x in [#](P) & A = Ball(x,r0) by A2; hence thesis by TOPMETR:14,def 6; 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 holds A in R0 implies ex x being Point of RealSpace,r being Real st A = Ball(x,r) proof let A be set; assume A11: A in R0; then reconsider A as Subset of R^1; consider x being Point of RealSpace such that x in [#](P) and A12: A = Ball(x,r0) by A2,A6,A11; take x; take r0; thus thesis by A12; end; R^1 = TopStruct (#the carrier of RealSpace, Family_open_set( RealSpace)#) by PCOMPS_1:def 5,TOPMETR:def 6; then reconsider 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 as Real by METRIC_1:def 13; A16: for p being Real holds p in [#](P) implies x1 - r1 <= p & p <= x1 + r1 proof let p be Real; reconsider a=x1,b=p as Element of RealSpace by METRIC_1:def 13; assume p in [#](P); 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 thesis by A18,XREAL_1:20; end; x1 - r1 is LowerBound of [#]P proof let r be ext-real number; thus thesis by A16; 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; thus thesis by A16; end; then [#](P) is bounded_above by XXREAL_2:def 10; hence thesis by A19,XXREAL_2:def 11; end; case A20: [#](P) = {}; 0 is LowerBound of [#]P proof let r be ext-real number; thus thesis by A20; end; then A21: [#](P) is bounded_below by XXREAL_2:def 9; 0 is UpperBound of [#]P proof let r be ext-real number; thus thesis by A20; end; then [#](P) is bounded_above by XXREAL_2:def 10; hence thesis by A21,XXREAL_2:def 11; end; end; hence thesis; end; end; theorem Th12: for P being Subset of R^1 holds P is compact implies [#](P) is closed proof let P be Subset of R^1; assume A1: P is compact; now per cases; case A2: [#](P) <> {}; 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; assume that A4: (rng s1) c= [#](P) and A5: s1 is convergent; set x = lim s1; reconsider x as Point of R^1 by TOPMETR:17; thus lim s1 in [#](P) proof assume not lim s1 in [#](P); 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 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,def 6; reconsider r as Real by XREAL_0:def 1; A12: Ball(x,r) = {q where q is Element of RealSpace :dist(x,q) {}; [#](P) is real-bounded by A1,Th11; hence thesis by A1,Th12,RCOMP_1:11; end; case A2: [#](P) = {}; assume not [#](P) is compact; then A3: ex s1 being Real_Sequence st (rng s1) c= [#](P) & not(ex s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent & (lim s2) in [#](P )) by RCOMP_1:def 3; ex x being set st x in NAT by XBOOLE_0:def 1; hence thesis by A2,A3,FUNCT_2:4; end; end; hence thesis; end; Lm1: for T being non empty TopSpace holds for f being Function of T,R^1 holds for P being Subset of T holds 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) proof let T be non empty TopSpace; let f be Function of T,R^1; let P be Subset of T; assume that A1: P <> {} and A2: P is compact & f is continuous; 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 thesis; 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,x2 as Point of T by A8,A10; take x1; take x2; thus thesis by A5,A6,A9,A11; end; definition let P be Subset of R^1; func upper_bound(P) -> Real equals upper_bound([#](P)); correctness; func lower_bound(P) -> Real equals lower_bound([#](P)); correctness; end; theorem Th14: for T being non empty TopSpace holds for f being Function of T, R^1 holds for P being Subset of T holds P <> {} & P is compact & f is continuous implies ex x1 being Point of T st x1 in P & f.x1 = upper_bound(f.:P) proof let T be non empty TopSpace; let f be Function of T,R^1; let P be Subset of T; assume P <> {} & P is compact & f is continuous; 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; thus thesis by A1,A2; end; ::$N Weierstrass Theorem theorem Th15: for T being non empty TopSpace holds for f being Function of T, R^1 holds for P being Subset of T holds P <> {} & P is compact & f is continuous implies ex x2 being Point of T st x2 in P & f.x2 = lower_bound(f.:P) proof let T be non empty TopSpace; let f be Function of T,R^1; let P be Subset of T; assume P <> {} & P is compact & f is continuous; 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; thus thesis by A1,A2; end; begin :: :: The measure of the distance between compact sets :: definition let M be non empty MetrSpace; let x be Point of M; func dist(x) -> Function of TopSpaceMetr(M),R^1 means :Def4: for y being Point of M holds it.y = dist(y,x); existence proof defpred EF[Element of M,Element of R^1] means for s being Element of M holds for t being Element of R^1 holds ($1 = s & $2 = t implies t = dist(s,x)); A1: for s being Element of M ex t being Element of R^1 st EF[s,t] proof let s be Element of M; consider t being Real such that A2: t = dist(s,x); reconsider t as Element of R^1 by TOPMETR:17; take t; thus thesis by A2; 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 EF[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 as Function of TopSpaceMetr(M),R^1; take F; thus thesis by A4; end; uniqueness proof let F1,F2 be Function of TopSpaceMetr(M),R^1; assume A5: for y being Point of M holds F1.y = dist(y,x); assume A6: for y being Point of M holds F2.y = dist(y,x); for y being set st y in the carrier of TopSpaceMetr(M) holds F1.y = F2 .y proof let y be set; 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); then reconsider y as Point of M by A7; F1.y = dist(y,x) by A5 .= F2.y by A6; hence thesis; end; hence thesis by FUNCT_2:12; end; end; theorem Th16: for M being non empty MetrSpace holds for x being Point of M holds dist(x) is continuous proof let M be non empty MetrSpace; let x be Point of M; 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; assume A2: P is open; for p being Point of M st p in (dist(x))"P ex r being real number st r >0 & Ball(p,r) c= (dist(x))"P proof let p be Point of M; consider y being Point of RealSpace such that A3: y = dist(p,x) by METRIC_1:def 13; assume p in (dist(x))"P; then A4: (dist(x)).p in P by FUNCT_1:def 7; reconsider 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,def 6; reconsider r as Real by XREAL_0:def 1; take r; Ball(p,r) c= (dist(x))"P proof let z be set; assume A7: z in Ball(p,r); then reconsider 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 thesis by A9,FUNCT_1:def 7; end; hence thesis by A5; end; hence (dist(x))"P is open by TOPMETR:15; end; [#]R^1 <> {}; hence thesis by A1,TOPS_2:43; end; theorem for M being non empty MetrSpace holds for x being Point of M holds for P being Subset of TopSpaceMetr(M) holds P <> {} & P is compact implies ex x1 being Point of TopSpaceMetr(M) st x1 in P & (dist(x)).x1 = upper_bound((dist(x) ).:P) by Th14,Th16; theorem for M being non empty MetrSpace holds for x being Point of M holds for P being Subset of TopSpaceMetr(M) holds P <> {} & P is compact implies 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: for x being Point of M holds it.x = upper_bound((dist(x)).:P); existence proof defpred EF[Element of M,Element of R^1] means for s being Element of M holds for t being Element of R^1 holds ($1 = s & $2 = t implies t = upper_bound ((dist(s)).:P)); A1: for s being Element of M ex t being Element of R^1 st EF[s,t] proof let s be Element of M; consider t being Real such that A2: t = upper_bound((dist(s)).:P); reconsider t as Element of R^1 by TOPMETR:17; take t; thus thesis by A2; 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 EF[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 as Function of TopSpaceMetr(M),R^1; take F; thus thesis by A4; end; uniqueness proof let F1,F2 be Function of TopSpaceMetr(M),R^1; assume A5: for y being Point of M holds F1.y = upper_bound((dist(y)).:P); assume A6: for y being Point of M holds F2.y = upper_bound((dist(y)).:P); for y being set st y in the carrier of TopSpaceMetr(M) holds F1.y = F2 .y proof let y be set; 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); then reconsider y as Point of M by A7; F1.y = upper_bound((dist(y)).:P) by A5 .= F2.y by A6; hence thesis; end; hence thesis by FUNCT_2:12; end; func dist_min(P) -> Function of TopSpaceMetr(M),R^1 means :Def6: for x being Point of M holds it.x = lower_bound((dist(x)).:P); existence proof defpred EF[Element of M,Element of R^1] means for s being Element of M holds for t being Element of R^1 holds ($1 = s & $2 = t implies t = lower_bound ((dist(s)).:P)); A8: for s being Element of M ex t being Element of R^1 st EF[s,t] proof let s be Element of M; consider t being Real such that A9: t = lower_bound((dist(s)).:P); reconsider t as Element of R^1 by TOPMETR:17; take t; thus thesis by A9; 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 EF[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 as Function of TopSpaceMetr(M),R^1; take F; thus thesis by A11; end; uniqueness proof let F1,F2 be Function of TopSpaceMetr(M),R^1; assume A12: for y being Point of M holds F1.y = lower_bound((dist(y)).:P); assume A13: for y being Point of M holds F2.y = lower_bound((dist(y)).:P); for y being set st y in the carrier of TopSpaceMetr(M) holds F1.y = F2.y proof let y be set; 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); then reconsider y as Point of M by A14; F1.y = lower_bound((dist(y)).:P) by A12 .= F2.y by A13; hence thesis; end; hence thesis by FUNCT_2:12; end; end; theorem Th19: for M being non empty MetrSpace holds for P being Subset of TopSpaceMetr(M) st P is compact for p1,p2 being Point of M holds p1 in P implies dist(p1,p2) <= upper_bound((dist(p2)).:P) & lower_bound((dist(p2)).:P) <= dist(p1,p2) proof let M be non empty MetrSpace; let P be Subset of TopSpaceMetr(M); assume A1: P is compact; let p1,p2 be Point of M; 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; 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 thesis by A2,SEQ_4:def 1,def 2; end; theorem Th20: for M being non empty MetrSpace holds 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; let P be Subset of TopSpaceMetr(M); assume that A1: P <> {} and A2: P is compact; let p1,p2 be Point of M; 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 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 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 thesis by A8,A10,A9,ABSVALUE:5; end; theorem for M being non empty MetrSpace holds for P being Subset of TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M holds for x1,x2 being Real holds x1 = (dist_max(P)).p1 & x2 = (dist_max(P)).p2 implies abs(x1 - x2) <= dist(p1,p2) proof let M be non empty MetrSpace; let P be Subset of TopSpaceMetr(M); assume A1: P <> {} & P is compact; let p1,p2 be Point of M; let x1,x2 be Real; assume A2: x1 = (dist_max(P)).p1 & x2 = (dist_max(P)).p2; (dist_max(P)).p1 = upper_bound((dist(p1)).:P) & (dist_max(P)).p2 = upper_bound((dist(p2)).:P) by Def5; hence thesis by A1,A2,Th20; end; theorem Th22: for M being non empty MetrSpace holds 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; let P be Subset of TopSpaceMetr(M); assume that A1: P <> {} and A2: P is compact; let p1,p2 be Point of M; 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 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 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 thesis by A8,A10,A9,ABSVALUE:5; end; theorem for M being non empty MetrSpace holds for P being Subset of TopSpaceMetr(M) st P <> {} & P is compact holds for p1,p2 being Point of M holds for x1,x2 being Real holds x1 = (dist_min(P)).p1 & x2 = (dist_min(P)).p2 implies abs(x1 - x2) <= dist(p1,p2) proof let M be non empty MetrSpace; let P be Subset of TopSpaceMetr(M); assume A1: P <> {} & P is compact; let p1,p2 be Point of M; let x1,x2 be Real; assume A2: x1 = (dist_min(P)).p1 & x2 = (dist_min(P)).p2; (dist_min(P)).p1 = lower_bound((dist(p1)).:P) & (dist_min(P)).p2 = lower_bound((dist(p2)).:P) by Def6; hence thesis by A1,A2,Th22; end; Lm2: [#]R^1 <> {}; theorem Th24: for M being non empty MetrSpace holds 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; let X be Subset of TopSpaceMetr(M); assume A1: X <> {} & X is compact; 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; assume A2: P is open; for p being Point of M st p in (dist_max(X))"P ex r being real number st r>0 & Ball(p,r) c= (dist_max(X))"P proof let p be Point of M; 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; then A4: (dist_max(X)).p in P by FUNCT_1:def 7; reconsider 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,def 6; reconsider r as Real by XREAL_0:def 1; take r; Ball(p,r) c= (dist_max(X))"P proof let z be set; assume A7: z in Ball(p,r); then reconsider 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 thesis by A6,A9,A10,FUNCT_1:def 7; end; hence thesis by A5; end; hence thesis by TOPMETR:15; end; hence thesis by Lm2,TOPS_2:43; end; theorem for M being non empty MetrSpace holds for P,Q being Subset of TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies 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 for M being non empty MetrSpace holds for P,Q being Subset of TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies 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: for M being non empty MetrSpace holds 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; let X be Subset of TopSpaceMetr(M); assume A1: X <> {} & X is compact; 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; assume A2: P is open; for p being Point of M st p in (dist_min(X))"P ex r being real number st r>0 & Ball(p,r) c= (dist_min(X))"P proof let p be Point of M; assume A3: p in (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 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,def 6; reconsider r as Real by XREAL_0:def 1; take r; Ball(p,r) c= (dist_min(X))"P proof let z be set; assume A8: z in Ball(p,r); then reconsider 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 thesis by A7,A10,A11,FUNCT_1:def 7; end; hence thesis by A6; end; hence thesis; end; hence (dist_min(X))"P is open by TOPMETR:15; end; hence thesis by Lm2,TOPS_2:43; end; theorem for M being non empty MetrSpace holds for P,Q being Subset of TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies 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 for M being non empty MetrSpace holds for P,Q being Subset of TopSpaceMetr(M) holds P <> {} & P is compact & Q <> {} & Q is compact implies 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 lower_bound((dist_min(P)).:Q); correctness; func max_dist_min(P,Q) -> Real equals upper_bound((dist_min(P)).:Q); correctness; func min_dist_max(P,Q) -> Real equals lower_bound((dist_max(P)).:Q); correctness; func max_dist_max(P,Q) -> Real equals upper_bound((dist_max(P)).:Q); correctness; end; theorem for M being non empty MetrSpace holds 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; let P,Q be Subset of TopSpaceMetr(M); assume that A1: P <> {} & P is compact and A2: Q <> {} & Q is compact; 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 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 as Point of M by A5; take x1; take x2; dist(x1,x2) = (dist(x2)).x1 by Def4 .= lower_bound((dist_min(P)).:Q) by A4,A7,Def6; hence thesis by A3,A6; end; theorem for M being non empty MetrSpace holds 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; let P,Q be Subset of TopSpaceMetr(M); assume that A1: P <> {} & P is compact and A2: Q <> {} & Q is compact; 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 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 as Point of M by A5; take x1; take x2; dist(x1,x2) = (dist(x2)).x1 by Def4 .= lower_bound((dist_max(P)).:Q) by A4,A7,Def5; hence thesis by A3,A6; end; theorem for M being non empty MetrSpace holds 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; let P,Q be Subset of TopSpaceMetr(M); assume that A1: P <> {} & P is compact and A2: Q <> {} & Q is compact; 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 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 as Point of M by A5; take x1; take x2; dist(x1,x2) = (dist(x2)).x1 by Def4 .= upper_bound((dist_min(P)).:Q) by A4,A7,Def6; hence thesis by A3,A6; end; theorem for M being non empty MetrSpace holds 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; let P,Q be Subset of TopSpaceMetr(M); assume that A1: P <> {} & P is compact and A2: Q <> {} & Q is compact; 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 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 as Point of M by A5; take x1; take x2; dist(x1,x2) = (dist(x2)).x1 by Def4 .= upper_bound((dist_max(P)).:Q) by A4,A7,Def5; hence thesis by A3,A6; end; theorem for M being non empty MetrSpace holds 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; let P,Q be Subset of TopSpaceMetr(M); assume that A1: P is compact and A2: Q is compact; let x1,x2 be Point of M; assume that A3: x1 in P and A4: x2 in 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 thesis by A12,A10,A11,A8,XXREAL_0:2; end; :: B i b l i o g r a p h y :: J.Dieudonne, "Foundations of Modern Analysis",Academic Press, 1960. :: J.L.Kelley, "General Topology", von Nostnend, 1955. :: K.Yosida, "Functional Analysis", Springer Verlag, 1968.