:: Complete Spaces :: by Karol P\c{a}k :: :: Received October 12, 2007 :: Copyright (c) 2007-2021 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, ORDINAL1, REAL_1, XBOOLE_0, METRIC_1, PROB_1, XXREAL_2, FUNCT_1, RELAT_1, STRUCT_0, PRE_TOPC, SUBSET_1, FUNCOP_1, XXREAL_0, MEASURE5, SEQ_1, CARD_1, ARYTM_1, ARYTM_3, VALUED_0, TARSKI, ORDINAL2, NAT_1, BHSP_3, COMPLEX1, RELAT_2, RCOMP_1, PCOMPS_1, ZFMISC_1, REWRITE1, SETFAM_1, SEQ_2, METRIC_6, FRECHET, FINSET_1, VALUED_1, CARD_3, TOPGEN_1, WELLORD1, ORDERS_2, PARTFUN1, WELLFND1, TBSP_1, WAYBEL23, RLVECT_3, COMPL_SP; notations METRIC_6, RELAT_2, BINOP_1, TOPMETR, CARD_1, FUNCOP_1, CANTOR_1, WELLORD1, XCMPLX_0, COMPLEX1, FINSET_1, SEQ_2, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, ZFMISC_1, XXREAL_0, XREAL_0, REAL_1, SETFAM_1, DOMAIN_1, TOPS_2, FUNCT_1, VALUED_1, NAT_1, VALUED_0, STRUCT_0, PRE_TOPC, COMPTS_1, SEQ_1, TBSP_1, RELSET_1, PARTFUN1, FUNCT_2, METRIC_1, PCOMPS_1, CARD_3, PROB_1, FRECHET, KURATO_0, KURATO_2, WELLFND1, WAYBEL23, ORDERS_2, TOPGEN_1; constructors REAL_1, TBSP_1, FRECHET, COMPLEX1, SEQ_2, TOPS_2, WELLORD1, CANTOR_1, URYSOHN3, METRIC_6, WELLFND1, TOPGEN_4, WAYBEL23, TOPGEN_1, COMPTS_1, BINOP_2, KURATO_0, COMSEQ_2, BINOP_1; registrations TOPMETR, PRE_TOPC, PCOMPS_1, NAT_1, TBSP_1, XREAL_0, RELSET_1, SUBSET_1, STRUCT_0, TOPS_1, METRIC_1, HAUSDORF, MEMBERED, YELLOW13, CARD_1, XBOOLE_0, VALUED_1, FUNCT_2, NUMBERS, FINSET_1, SEQ_4, WELLFND1, VALUED_0, ORDINAL1; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; begin :: Preliminaries reserve i,n,m for Nat, x,y,X,Y for set, r,s for Real; definition let M be non empty MetrStruct; let S be SetSequence of M; attr S is pointwise_bounded means :: COMPL_SP:def 1 for i holds S.i is bounded; end; registration let M be non empty Reflexive MetrStruct; cluster pointwise_bounded non-empty for SetSequence of M; end; definition let M be Reflexive non empty MetrStruct; let S be SetSequence of M; func diameter S -> Real_Sequence means :: COMPL_SP:def 2 for i holds it.i = diameter S. i; end; theorem :: COMPL_SP:1 for M be Reflexive non empty MetrStruct for S be pointwise_bounded SetSequence of M holds diameter S is bounded_below; registration let M be Reflexive non empty MetrStruct, S be SetSequence of M; cluster diameter S -> real-valued; end; theorem :: COMPL_SP:2 for M be Reflexive non empty MetrStruct for S be pointwise_bounded SetSequence of M st S is non-ascending holds diameter S is bounded_above & diameter S is non-increasing; theorem :: COMPL_SP:3 for M be Reflexive non empty MetrStruct for S be pointwise_bounded SetSequence of M st S is non-descending holds diameter S is non-decreasing; theorem :: COMPL_SP:4 for M be non empty Reflexive MetrStruct for S be pointwise_bounded SetSequence of M st S is non-ascending & lim diameter S = 0 for F be sequence of M st for i holds F.i in S.i holds F is Cauchy; theorem :: COMPL_SP:5 for M be Reflexive symmetric triangle non empty MetrStruct for p be Point of M holds 0 <= r implies diameter cl_Ball(p,r) <= 2*r; definition let M be MetrStruct; let U be Subset of M; attr U is open means :: COMPL_SP:def 3 U in Family_open_set M; end; definition let M be MetrStruct; let A be Subset of M; attr A is closed means :: COMPL_SP:def 4 A` is open; end; registration let M be MetrStruct; cluster empty -> open for Subset of M; cluster empty -> closed for Subset of M; end; registration let M be non empty MetrStruct; cluster open non empty for Subset of M; cluster closed non empty for Subset of M; end; theorem :: COMPL_SP:6 for M be MetrStruct for A be Subset of M, A9 be Subset of TopSpaceMetr M st A9 = A holds ( A is open iff A9 is open ) & ( A is closed iff A9 is closed ); definition let T be TopStruct; let S be SetSequence of T; attr S is open means :: COMPL_SP:def 5 for i holds S.i is open; attr S is closed means :: COMPL_SP:def 6 for i holds S.i is closed; end; registration let T be TopSpace; cluster open for SetSequence of T; cluster closed for SetSequence of T; end; registration let T be non empty TopSpace; cluster open non-empty for SetSequence of T; cluster closed non-empty for SetSequence of T; end; definition let M be MetrStruct; let S be SetSequence of M; attr S is open means :: COMPL_SP:def 7 for i holds S.i is open; attr S is closed means :: COMPL_SP:def 8 for i holds S.i is closed; end; registration let M be non empty MetrSpace; cluster non-empty pointwise_bounded open for SetSequence of M; cluster non-empty pointwise_bounded closed for SetSequence of M; end; theorem :: COMPL_SP:7 for M be MetrStruct for S be SetSequence of M, S9 be SetSequence of TopSpaceMetr M st S9 = S holds ( S is open iff S9 is open ) & ( S is closed iff S9 is closed ); theorem :: COMPL_SP:8 for M be Reflexive symmetric triangle non empty MetrStruct for S, CL be Subset of M st S is bounded for S9 be Subset of TopSpaceMetr M st S = S9 & CL = Cl S9 holds CL is bounded & diameter S = diameter CL; begin :: Cantor's theorem on complete spaces theorem :: COMPL_SP:9 for M be non empty MetrSpace for C be sequence of M ex S be non-empty closed SetSequence of M st S is non-ascending & ( C is Cauchy implies S is pointwise_bounded & lim diameter S = 0 ) & for i ex U be Subset of TopSpaceMetr M st U = { C.j where j is Nat: j >= i } & S.i = Cl U; theorem :: COMPL_SP:10 for M be non empty MetrSpace holds M is complete iff for S be non-empty pointwise_bounded closed SetSequence of M st S is non-ascending & lim diameter S = 0 holds meet S is non empty; theorem :: COMPL_SP:11 for T be non empty TopSpace for S be non-empty SetSequence of T st S is non-ascending for F be Subset-Family of T st F = rng S holds F is centered; theorem :: COMPL_SP:12 for M be non empty MetrStruct for S be SetSequence of M for F be Subset-Family of TopSpaceMetr M st F = rng S holds ( S is open implies F is open ) & ( S is closed implies F is closed ); theorem :: COMPL_SP:13 for T be non empty TopSpace for F be Subset-Family of T for S be SetSequence of T st rng S c= F ex R be SetSequence of T st R is non-ascending & ( F is centered implies R is non-empty ) & ( F is open implies R is open ) & ( F is closed implies R is closed ) & for i holds R.i = meet {S.j where j is Element of NAT: j <= i}; theorem :: COMPL_SP:14 for M be non empty MetrSpace holds M is complete iff for F be Subset-Family of TopSpaceMetr M st F is closed & F is centered & for r be Real st r > 0 ex A be Subset of M st A in F & A is bounded & diameter A < r holds meet F is non empty; theorem :: COMPL_SP:15 for M be non empty MetrSpace,A be non empty Subset of M for B be Subset of M, B9 be Subset of M|A st B = B9 holds B9 is bounded iff B is bounded ; theorem :: COMPL_SP:16 for M be non empty MetrSpace,A be non empty Subset of M for B be Subset of M, B9 be Subset of M|A st B = B9 & B is bounded holds diameter B9 <= diameter B; theorem :: COMPL_SP:17 for M be non empty MetrSpace, A be non empty Subset of M for S be sequence of (M|A) holds S is sequence of M; theorem :: COMPL_SP:18 for M be non empty MetrSpace, A be non empty Subset of M for S be sequence of (M|A),S9 be sequence of M st S = S9 holds S9 is Cauchy iff S is Cauchy; theorem :: COMPL_SP:19 for M be non empty MetrSpace st M is complete for A be non empty Subset of M, A9 be Subset of TopSpaceMetr M st A = A9 holds M|A is complete iff A9 is closed; begin :: Countable compact spaces definition let T be TopStruct; attr T is countably_compact means :: COMPL_SP:def 9 for F being Subset-Family of T st F is Cover of T & F is open & F is countable ex G being Subset-Family of T st G c= F & G is Cover of T & G is finite; end; theorem :: COMPL_SP:20 for T be TopStruct st T is compact holds T is countably_compact; theorem :: COMPL_SP:21 for T being non empty TopSpace holds T is countably_compact iff for F being Subset-Family of T st F is centered & F is closed & F is countable holds meet F <> {}; theorem :: COMPL_SP:22 for T being non empty TopSpace holds T is countably_compact iff for S be non-empty closed SetSequence of T st S is non-ascending holds meet S <> {}; theorem :: COMPL_SP:23 for T being non empty TopSpace for F be Subset-Family of T for S be SetSequence of T st rng S c= F & S is non-empty ex R be non-empty closed SetSequence of T st R is non-ascending & ( F is locally_finite & S is one-to-one implies meet R = {} ) & for i ex Si be Subset-Family of T st R.i = Cl union Si & Si = {S.j where j is Element of NAT: j >= i}; ::$CT theorem :: COMPL_SP:25 for X be non empty set, F be SetSequence of X st F is non-ascending for S be sequence of X st for n holds S.n in F.n holds rng S is finite implies meet F is non empty; theorem :: COMPL_SP:26 for T be non empty TopSpace holds T is countably_compact iff for F be Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds F is finite; theorem :: COMPL_SP:27 for T be non empty TopSpace holds T is countably_compact iff for F be Subset-Family of T st F is locally_finite & for A be Subset of T st A in F holds card A = 1 holds F is finite; theorem :: COMPL_SP:28 for T be T_1 non empty TopSpace holds T is countably_compact iff for A be Subset of T st A is infinite holds Der A is non empty; theorem :: COMPL_SP:29 for T be T_1 non empty TopSpace holds T is countably_compact iff for A be Subset of T st A is infinite countable holds Der A is non empty; scheme :: COMPL_SP:sch 1 Th39{X()->non empty set,P[set,set]}: ex A be Subset of X() st ( for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y] ) & for x be Element of X() ex y be Element of X() st y in A & not P[x,y] provided for x,y be Element of X() holds P[x,y] iff P[y,x] and for x be Element of X() holds not P[x,x]; scheme :: COMPL_SP:sch 2 Th39{X()->non empty set,P[set,set]}: ex A be Subset of X() st ( for x,y be Element of X() st x in A & y in A & x <> y holds P[x,y] ) & for x be Element of X() ex y be Element of X() st y in A & not P[x,y] provided for x,y be Element of X() holds P[x,y] iff P[y,x] and for x be Element of X() holds not P[x,x]; theorem :: COMPL_SP:30 for M be Reflexive symmetric non empty MetrStruct for r be Real st r > 0 ex A be Subset of M st (for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r) & for p be Point of M ex q be Point of M st q in A & p in Ball(q,r); theorem :: COMPL_SP:31 for M be Reflexive symmetric triangle non empty MetrStruct holds M is totally_bounded iff for r be Real,A be Subset of M st r>0 & for p,q be Point of M st p <> q & p in A & q in A holds dist(p,q) >= r holds A is finite ; theorem :: COMPL_SP:32 for M be Reflexive symmetric triangle non empty MetrStruct st TopSpaceMetr M is countably_compact holds M is totally_bounded; theorem :: COMPL_SP:33 for M be non empty MetrSpace st M is totally_bounded holds TopSpaceMetr M is second-countable; theorem :: COMPL_SP:34 for T be non empty TopSpace holds T is second-countable implies for F being Subset-Family of T st F is Cover of T & F is open ex G being Subset-Family of T st G c= F & G is Cover of T & G is countable; begin :: The main theorem theorem :: COMPL_SP:35 for M be non empty MetrSpace holds TopSpaceMetr M is compact iff TopSpaceMetr M is countably_compact; theorem :: COMPL_SP:36 for X be set, F be Subset-Family of X st F is finite for A be Subset of X st A is infinite & A c= union F ex Y be Subset of X st Y in F & Y /\ A is infinite; theorem :: COMPL_SP:37 for M be non empty MetrSpace holds TopSpaceMetr M is compact iff M is totally_bounded & M is complete; begin :: Well spaces theorem :: COMPL_SP:38 for M be MetrStruct, a be Point of M,x holds x in [:X,(the carrier of M)\{a}:]\/{[X,a]} iff ex y be set,b be Point of M st x=[y,b] & (y in X & b<>a or y = X & b = a); definition let M be MetrStruct; let a be Point of M; let X be set; func well_dist(a,X) -> Function of [:[:X,(the carrier of M)\{a}:]\/{[X,a]}, [:X,(the carrier of M)\{a}:]\/{[X,a]}:],REAL means :: COMPL_SP:def 10 for x,y be Element of [:X,(the carrier of M)\{a}:]\/{[X,a]} for x1,y1 be object,x2,y2 be Point of M st x = [x1,x2] & y = [y1,y2] holds (x1 = y1 implies it.(x,y) = dist(x2,y2) ) & (x1 <> y1 implies it.(x,y) = dist(x2,a)+dist(a,y2) ); end; theorem :: COMPL_SP:39 for M be MetrStruct,a be Point of M for X be non empty set holds ( well_dist(a,X) is Reflexive implies M is Reflexive ) & ( well_dist(a,X) is symmetric implies M is symmetric ) & ( well_dist(a,X) is triangle Reflexive implies M is triangle ) & (well_dist(a,X) is discerning Reflexive implies M is discerning ); definition let M be MetrStruct; let a be Point of M; let X be set; func WellSpace(a,X) -> strict MetrStruct equals :: COMPL_SP:def 11 MetrStruct (#[:X,(the carrier of M)\{a}:]\/{[X,a]},well_dist(a,X)#); end; registration let M be MetrStruct; let a be Point of M; let X be set; cluster WellSpace(a,X) -> non empty; end; registration let M be Reflexive MetrStruct; let a be Point of M; let X be set; cluster WellSpace(a,X) -> Reflexive; end; registration let M be symmetric MetrStruct; let a be Point of M; let X be set; cluster WellSpace(a,X) -> symmetric; end; registration let M be symmetric triangle Reflexive MetrStruct; let a be Point of M; let X be set; cluster WellSpace(a,X) -> triangle; end; registration let M be MetrSpace; let a be Point of M; let X be set; cluster WellSpace(a,X) -> discerning; end; theorem :: COMPL_SP:40 for M be triangle Reflexive non empty MetrStruct for a be Point of M for X be non empty set holds WellSpace(a,X) is complete implies M is complete ; theorem :: COMPL_SP:41 for M be symmetric triangle Reflexive non empty MetrStruct for a be Point of M for S be sequence of WellSpace(a,X) st S is Cauchy holds (for Xa be Point of WellSpace(a,X) st Xa=[X,a] for r st r > 0 ex n st for m st m >= n holds dist(S.m,Xa) < r) or ex n,Y st for m st m >= n ex p be Point of M st S.m = [Y,p]; theorem :: COMPL_SP:42 for M be symmetric triangle Reflexive non empty MetrStruct for a be Point of M holds M is complete implies WellSpace(a,X) is complete; theorem :: COMPL_SP:43 for M be symmetric triangle Reflexive non empty MetrStruct st M is complete for a be Point of M st ex b be Point of M st dist(a,b)<>0 for X be infinite set holds WellSpace(a,X) is complete & ex S be non-empty pointwise_bounded SetSequence of WellSpace(a,X) st S is closed & S is non-ascending & meet S is empty; theorem :: COMPL_SP:44 ex M be non empty MetrSpace st M is complete & ex S be non-empty pointwise_bounded SetSequence of M st S is closed & S is non-ascending & meet S is empty;