:: The Theorem of Weierstrass :: by J\'ozef Bia\las and Yatsuka Nakamura :: :: Received July 10, 1995 :: Copyright (c) 1995-2018 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, SEQ_1, SEQ_2, VALUED_0, SEQ_4, WEIERSTR; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, 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, BINOP_2, PCOMPS_1, COMSEQ_2, BINOP_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, FINSEQ_1, NAT_1; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; begin theorem :: WEIERSTR:1 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); theorem :: WEIERSTR:2 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) ); theorem :: WEIERSTR:3 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); theorem :: WEIERSTR:4 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; theorem :: WEIERSTR:5 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; theorem :: WEIERSTR:6 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 ; theorem :: WEIERSTR:7 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; begin :: :: The Weierstrass` theorem :: theorem :: WEIERSTR:8 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; theorem :: WEIERSTR:9 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; theorem :: WEIERSTR:10 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; definition let P be Subset of R^1; func [#](P) -> Subset of REAL equals :: WEIERSTR:def 1 P; end; theorem :: WEIERSTR:11 for P being Subset of R^1 holds P is compact implies [#](P) is real-bounded; theorem :: WEIERSTR:12 for P being Subset of R^1 holds P is compact implies [#](P) is closed; theorem :: WEIERSTR:13 for P being Subset of R^1 holds P is compact implies [#](P) is compact; definition let P be Subset of R^1; func upper_bound(P) -> Real equals :: WEIERSTR:def 2 upper_bound([#](P)); func lower_bound(P) -> Real equals :: WEIERSTR:def 3 lower_bound([#](P)); end; ::\$N Extreme value theorem#Generalization to arbitrary topological spaces theorem :: WEIERSTR:14 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) ; ::\$N Extreme value theorem#Generalization to arbitrary topological spaces theorem :: WEIERSTR:15 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) ; 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 :: WEIERSTR:def 4 for y being Point of M holds it.y = dist(y,x); end; theorem :: WEIERSTR:16 for M being non empty MetrSpace holds for x being Point of M holds dist(x) is continuous; theorem :: WEIERSTR:17 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); theorem :: WEIERSTR:18 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); 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 :: WEIERSTR:def 5 for x being Point of M holds it.x = upper_bound((dist(x)).:P); func dist_min(P) -> Function of TopSpaceMetr(M),R^1 means :: WEIERSTR:def 6 for x being Point of M holds it.x = lower_bound((dist(x)).:P); end; theorem :: WEIERSTR:19 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); theorem :: WEIERSTR:20 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 |.upper_bound((dist(p1)).:P) - upper_bound((dist(p2)).:P).| <= dist(p1, p2); theorem :: WEIERSTR:21 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 |.x1 - x2.| <= dist(p1,p2); theorem :: WEIERSTR:22 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 |.lower_bound((dist(p1)).:P) - lower_bound((dist(p2)).:P).| <= dist(p1, p2); theorem :: WEIERSTR:23 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 |.x1 - x2.| <= dist(p1,p2); theorem :: WEIERSTR:24 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; theorem :: WEIERSTR:25 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); theorem :: WEIERSTR:26 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); theorem :: WEIERSTR:27 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; theorem :: WEIERSTR:28 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); theorem :: WEIERSTR:29 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); 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); func max_dist_min(P,Q) -> Real equals :: WEIERSTR:def 8 upper_bound((dist_min(P)).:Q); func min_dist_max(P,Q) -> Real equals :: WEIERSTR:def 9 lower_bound((dist_max(P)).:Q); func max_dist_max(P,Q) -> Real equals :: WEIERSTR:def 10 upper_bound((dist_max(P)).:Q); end; theorem :: WEIERSTR:30 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); theorem :: WEIERSTR:31 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); theorem :: WEIERSTR:32 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); theorem :: WEIERSTR:33 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); theorem :: WEIERSTR:34 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); :: 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.