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