:: Compactness in Metric Spaces
:: by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama
::
:: Received June 30, 2016
:: Copyright (c) 2016-2026 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, SUBSET_1, FUNCT_1, NAT_1, RELAT_1, XBOOLE_0, XXREAL_2,
XXREAL_0, CARD_1, REAL_1, ARYTM_3, ARYTM_1, SEQ_1, SEQ_2, ORDINAL2,
COMPLEX1, STRUCT_0, TARSKI, TOPMETR, FINSET_1, PRE_TOPC, TOPMETR4,
MEMBERED, RCOMP_1, BHSP_3, COMPL_SP, NORMSP_1, NORMSP_2, VALUED_0,
SETFAM_1, METRIC_1, TBSP_1, PCOMPS_1, REWRITE1, ZFMISC_1, TOPGEN_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FINSET_1, NUMBERS, XCMPLX_0, MEMBERED, XXREAL_0,
XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, SEQ_1, SEQ_2, RCOMP_1,
STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, METRIC_1, NORMSP_1, NFCONT_1,
NORMSP_2, PCOMPS_1, TBSP_1, TOPMETR, TOPGEN_1, COMPL_SP;
constructors SEQ_4, NAT_D, INTEGRA2, SEQ_2, TOPGEN_1, TOPMETR, COMSEQ_2,
C0SP2, TOPS_2, COMPL_SP, TBSP_1, PCOMPS_1, NFCONT_1, NORMSP_2;
registrations XREAL_0, FUNCT_2, NAT_1, MEMBERED, XXREAL_0, ORDINAL1, VALUED_0,
RELSET_1, PSCOMP_1, TOPMETR, COMPTS_1, CARD_1, INT_1, PRE_TOPC, PCOMPS_1,
STRUCT_0, XXREAL_2, FINSET_1, ZFMISC_1, XCMPLX_0, METRIC_1, TBSP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TBSP_1;
equalities XBOOLE_0, TOPMETR, XCMPLX_0, NORMSP_2, PCOMPS_1, STRUCT_0,
METRIC_1;
expansions XBOOLE_0, TOPMETR, TBSP_1, VALUED_1, NFCONT_1, TOPS_2, COMPTS_1,
PRE_TOPC;
theorems XBOOLE_0, XBOOLE_1, XREAL_0, XXREAL_2, XXREAL_0, RELAT_1, ORDINAL1,
XREAL_1, SEQ_4, SEQ_2, FUNCT_1, FUNCT_2, PRE_TOPC, COMPTS_1, TOPMETR,
TOPMETR3, PCOMPS_1, TARSKI, GOBOARD6, JGRAPH_2, BORSUK_5, METRIC_1,
TOPGEN_1, COMPL_SP, DICKSON, NORMSP_2, TBSP_1, FINSET_1, ZFMISC_1,
VALUED_0, NAT_1, SEQM_3, JORDAN5A, HAUSDORF;
schemes FUNCT_2, FRAENKEL, RECDEF_2, NAT_1, RECDEF_1;
begin :: 1. Topological properties of metric spaces
theorem LM1:
for M be non empty set,
x be sequence of M st rng x is finite
ex z be Element of M st x"{z} c= NAT & x"{z} is infinite
proof
let M be non empty set,
x be sequence of M;
assume
A1: rng x is finite;
assume
A2: not (ex z be Element of M st x"{z} c= NAT & x"{z} is infinite);
deffunc X(object) = x"{$1};
set K = {X(w) where w is Element of M: w in rng x};
A3: K is finite from FRAENKEL:sch 21(A1);
for Y be set st Y in K holds Y is finite
proof
let Y be set;
assume Y in K; then
consider w be Element of M such that
A4: Y = x"{w} & w in rng x;
thus Y is finite by A2,A4;
end; then
A5: union K is finite by A3,FINSET_1:7;
dom x c= union K
proof
let s be object;
assume
A6: s in dom x; then
reconsider sn = s as Element of NAT;
reconsider w = x.sn as Element of M;
w in rng x by A6,FUNCT_1:3; then
A7: x"{w} in K;
w in {w} by TARSKI:def 1; then
s in x"{w} by A6,FUNCT_1:def 7;
hence s in union K by A7,TARSKI:def 4;
end;
hence contradiction by A5,FUNCT_2:def 1;
end;
theorem LM2:
for X be Subset of NAT st X is infinite
ex N be increasing sequence of NAT st rng N c= X
proof
let X be Subset of NAT;
assume
A1: X is infinite;
reconsider BX = bool X as non empty set by ZFMISC_1:def 1;
reconsider N0 = min*(X) as Element of NAT;
reconsider Y0 = X as Element of BX by ZFMISC_1:def 1;
defpred P[object,object,set,object,set] means
$5= $3 \ {$2} & $4= min*($5);
A2: for n be Nat, x be Element of NAT, y be Element of BX
ex x1 be Element of NAT, y1 be Element of BX st P[n,x,y,x1,y1]
proof
let n be Nat, x be Element of NAT,
y be Element of BX;
reconsider y1 = y \ {x} as Element of BX by XBOOLE_1:1;
set x1 = min*(y1);
take x1,y1;
thus thesis;
end;
consider N be sequence of NAT, Y be sequence of BX such that
A3: N.0 = N0 & Y.0 = Y0
& for n be Nat holds P[n,N.n,Y.n,N.(n+1),Y.(n+1)]
from RECDEF_2:sch 3(A2);
defpred Q[Nat] means
N.$1= min*(Y.$1) & N.$1 in Y.$1 & Y.$1 is infinite & Y.$1 c= NAT;
A4: Q[0] by A1,A3,NAT_1:def 1;
A5: for i be Nat st Q[i] holds Q[i+1]
proof
let i be Nat;
assume
A6: Q[i];
A7: Y.(i+1) = (Y.i) \ {N.i} & N.(i+1) = min*(Y.(i+1)) by A3;
A8: Y.(i+1) is infinite
proof
assume Y.(i+1) is finite; then
Y.(i+1) \/ {N.i} is finite;
hence contradiction by A6,A7,XBOOLE_1:45,ZFMISC_1:31;
end;
Y.(i+1) c= NAT by XBOOLE_1:1;
hence thesis by A7,A8,NAT_1:def 1;
end;
A9: for i be Nat holds Q[i] from NAT_1:sch 2(A4,A5);
A11:rng N c= X
proof
let y be object;
assume y in rng N; then
consider i be object such that
A10: i in NAT & N.i = y by FUNCT_2:11;
reconsider i as Nat by A10;
N.i = min*(Y.i) & N.i in Y.i & Y.i is infinite & Y.i c= NAT by A9;
hence y in X by A10;
end;
for i be Nat holds N.i < N.(i+1)
proof
let i be Nat;
A12: N.i= min*(Y.i) & N.i in Y.i & Y.i is infinite & Y.i c= NAT by A9;
Y.(i+1) = (Y.i) \ {N.i} & N.(i+1) = min*(Y.(i+1)) by A3; then
A13: N.(i+1) in (Y.i) \ {N.i} by A9; then
N.(i+1) in (Y.i) & not N.(i+1) in {N.i} by XBOOLE_0:def 5; then
A14: N.(i+1) <> N.i by TARSKI:def 1;
N.i <= N.(i+1) by A12,A13,NAT_1:def 1;
hence N.i < N.(i+1) by A14,XXREAL_0:1;
end; then
N is increasing;
hence thesis by A11;
end;
theorem
for M be non empty MetrSpace,
V be Subset of TopSpaceMetr M st V is open holds
ex F be Subset-Family of M
st F = {Ball(x,r) where x is Element of M, r is Real:
r > 0 & Ball(x,r) c= V}
& V = union F
proof
let M be non empty MetrSpace,
V be Subset of TopSpaceMetr M;
assume
A1: V is open;
set F = {Ball(x,r) where x is Element of M, r is Real:
r > 0 & Ball(x,r) c= V};
for z be object st z in F holds z in Family_open_set M
proof
let z be object;
assume z in F; then
ex x be Element of M, r be Real
st z = Ball(x,r) & r > 0 & Ball(x,r) c= V;
hence z in Family_open_set M by PCOMPS_1:29;
end; then
F c= Family_open_set M by TARSKI:def 3; then
reconsider F as Subset-Family of M by XBOOLE_1:1;
take F;
thus F = {Ball(x,r) where x is Element of M, r is Real:
r > 0 & Ball(x,r) c= V};
reconsider Q = union F as Subset of TopSpaceMetr M;
for z be object holds z in V iff z in Q
proof
let z be object;
hereby
assume
A2: z in V; then
reconsider x = z as Element of M;
consider r be Real such that
A3: r > 0 & Ball(x,r) c= V by A1,A2,TOPMETR:15;
dist(x,x) = 0 by METRIC_1:1; then
A4: x in Ball(x,r) by A3,METRIC_1:11;
Ball(x,r) in F by A3;
hence z in Q by A4,TARSKI:def 4;
end;
assume z in Q; then
consider B be set such that
A5: z in B & B in F by TARSKI:def 4;
consider x be Element of M, r be Real such that
A6: B = Ball(x,r) & r > 0 & Ball(x,r) c= V by A5;
thus z in V by A5,A6;
end;
hence thesis by TARSKI:2;
end;
theorem
for M be non empty MetrSpace,
X be Subset of TopSpaceMetr M,
p be Element of M holds
(p in Cl(X) iff for r be Real st 0 < r holds X meets Ball(p,r))
proof
let M be non empty MetrSpace,
X be Subset of TopSpaceMetr M,
p be Element of M;
hereby
assume
A1: p in Cl(X);
let r be Real;
assume
A2: 0 < r;
reconsider G = Ball(p,r) as Subset of TopSpaceMetr M;
dist(p,p) = 0 by METRIC_1:1; then
G is open & p in G by A2,METRIC_1:11,TOPMETR:14;
hence X meets Ball(p,r) by A1,PRE_TOPC:def 7;
end;
assume
A3: for r be Real st 0 < r holds X meets Ball(p,r);
now
let G be Subset of TopSpaceMetr M;
assume G is open & p in G; then
consider r be Real such that
A4: 0 < r & Ball(p,r) c= G by PCOMPS_1:def 4;
X meets Ball(p,r) by A3,A4;
hence X meets G by A4,XBOOLE_1:63;
end;
hence p in Cl(X) by PRE_TOPC:def 7;
end;
theorem Th3:
for M be non empty MetrSpace,
X be Subset of TopSpaceMetr M holds
for x be object holds
x in Cl X
iff
ex S be sequence of M
st (for n be Nat holds S.n in X)
& S is convergent & lim S = x
proof
let M be non empty MetrSpace,
X be Subset of TopSpaceMetr M;
let x be object;
hereby
assume
A1: x in Cl X;
reconsider x0 = x as Element of M by A1;
defpred P[Element of NAT, object] means
$2 in X & $2 in Ball(x0, 1/($1+1));
A2: for n be Element of NAT ex p be Element of M st P[n,p]
proof
let n be Element of NAT;
set r = 1/(n+1);
reconsider G = Ball(x0,r) as Subset of TopSpaceMetr M;
dist(x0,x0) = 0 by METRIC_1:1; then
G is open & x0 in G by METRIC_1:11,TOPMETR:14; then
X meets Ball(x0,r) by A1,PRE_TOPC:def 7; then
consider p be object such that
A3: p in X /\ Ball(x0,r) by XBOOLE_0:def 1;
reconsider p as Element of M by A3;
take p;
thus thesis by A3,XBOOLE_0:def 4;
end;
consider S be sequence of M such that
A4: for n be Element of NAT holds P[n,S.n] from FUNCT_2:sch 3(A2);
A5: now
let n be Nat;
n in NAT by ORDINAL1:def 12; then
S.n in X & S.n in Ball(x0,1/(n+1)) by A4;
hence S.n in X & dist(S.n,x0) < 1/(n+1) by METRIC_1:11;
end;
A6: now
let s be Real;
assume
A7: 0 < s;
consider n be Nat such that
A8: s"<n by SEQ_4:3;
take k=n;
let m be Nat;
assume k<=m; then
k+1<=m+1 by XREAL_1:6; then
A9: 1/(m+1)<=1/(k+1) by XREAL_1:118;
s"+0 <n+1 by A8,XREAL_1:8; then
1/(n+1)<1/s" by A7,XREAL_1:76; then
1/(m+1)<s by A9,XXREAL_0:2;
hence dist(S.m,x0) < s by A5,XXREAL_0:2;
end; then
A10: S is convergent; then
lim S = x by A6,TBSP_1:def 3;
hence ex S be sequence of M
st (for n be Nat holds S.n in X)
& S is convergent & lim S = x by A5,A10;
end;
given S be sequence of M such that
A11: for n be Nat holds S.n in X and
A12: S is convergent and
A13: lim S = x;
X c= Cl X by PRE_TOPC:18; then
A14: for n be Nat holds S.n in Cl X by A11,TARSKI:def 3;
Cl (Cl X) = Cl X;
hence x in Cl X by A12,A13,A14,PRE_TOPC:22,TOPMETR3:1;
end;
theorem Th4:
for M be non empty MetrSpace,
X be Subset of TopSpaceMetr M holds
X is closed
iff
for S be sequence of M
st (for n be Nat holds S.n in X)
& S is convergent
holds lim S in X
proof
let M be non empty MetrSpace,
X be Subset of TopSpaceMetr M;
thus X is closed implies
for S be sequence of M
st (for n be Nat holds S . n in X) & S is convergent
holds lim S in X by TOPMETR3:1;
assume
A1: for S be sequence of M
st (for n be Nat holds S.n in X)
& S is convergent holds lim S in X;
for x be object st x in Cl X holds x in X
proof
let x be object;
assume x in Cl X; then
consider S be sequence of M such that
A2: (for n be Nat holds S.n in X) & S is convergent & lim S = x by Th3;
thus x in X by A1,A2;
end; then
Cl X = X by PRE_TOPC:18,TARSKI:def 3;
hence X is closed by PRE_TOPC:22;
end;
theorem
for X, Y be non empty MetrSpace
for f be Function of TopSpaceMetr X, TopSpaceMetr Y holds
f is continuous
iff
for S be sequence of X, T be sequence of Y
st S is convergent & T = f * S
holds T is convergent & lim T = f.(lim S)
proof
let X, Y be non empty MetrSpace;
let f be Function of TopSpaceMetr X, TopSpaceMetr Y;
hereby
assume
A1: f is continuous;
let S be sequence of X, T be sequence of Y;
assume that
A2: S is convergent and
A3: T = f*S;
set z0 = lim S;
reconsider p = z0 as Point of TopSpaceMetr(X);
A4: dom f = the carrier of X by FUNCT_2:def 1; then
f.(lim S) in rng f by FUNCT_1:3; then
reconsider x0 = f.(lim S) as Element of Y;
A5: for r be Real st r>0
ex n be Nat st for m be Nat st n<=m holds dist(T.m,x0)<r
proof
let r be Real;
reconsider V = Ball(x0,r) as Subset of TopSpaceMetr(Y);
assume r > 0; then
V is open & x0 in V by GOBOARD6:1,TOPMETR:14; then
consider W be Subset of TopSpaceMetr(X) such that
A6: p in W & W is open and
A7: f.:W c= V by A1,JGRAPH_2:10;
consider r0 be Real such that
A8: r0 > 0 and
A9: Ball(z0,r0) c= W by A6,TOPMETR:15;
reconsider r00 = r0 as Real;
consider n0 be Nat such that
A10: for m be Nat st n0<=m holds dist(S.m,z0)<r00
by A2,A8,TBSP_1:def 3;
for m be Nat st n0<=m holds dist(T.m,x0)<r
proof
let m be Nat;
assume n0 <= m; then
dist(S.m,z0) < r0 by A10; then
S.m in Ball(z0,r0) by METRIC_1:11; then
A11: f.(S.m) in f.:W by A4,A9,FUNCT_1:def 6;
dom T = NAT by FUNCT_2:def 1; then
T.m in f.:W by A3,A11,FUNCT_1:12,ORDINAL1:def 12;
hence thesis by A7,METRIC_1:11;
end;
hence thesis;
end;
hence T is convergent;
hence lim T = f.(lim S) by A5,TBSP_1:def 3;
end;
assume
A12: for S be sequence of X, T be sequence of Y
st S is convergent & T = f * S
holds T is convergent & lim T = f.(lim S);
for B be Subset of TopSpaceMetr Y st B is closed
holds f " B is closed
proof
let B be Subset of TopSpaceMetr Y;
reconsider A = f " B as Subset of TopSpaceMetr X;
assume
A13: B is closed;
for S be sequence of X
st (for n be Nat holds S . n in f " B) & S is convergent
holds lim S in f " B
proof
let S be sequence of X;
assume that
A14: for n be Nat holds S . n in f " B and
A15: S is convergent;
reconsider T = f * S as sequence of Y;
for n be Nat holds T.n in B
proof
let n be Nat;
S.n in f " B by A14; then
f.(S.n) in B by FUNCT_1:def 7;
hence T.n in B by FUNCT_2:15,ORDINAL1:def 12;
end; then
lim T in B by A12,A13,A15,Th4; then
A16: f.(lim S) in B by A12,A15;
dom f= the carrier of X by FUNCT_2:def 1;
hence lim S in f " B by A16,FUNCT_1:def 7;
end;
hence f " B is closed by Th4;
end;
hence f is continuous;
end;
begin :: 2. Compactness in metric spaces
definition
let M be non empty MetrSpace;
let X be Subset of M;
attr X is sequentially_compact means :Def1:
for S1 be sequence of M st rng S1 c= X
ex S2 be sequence of M
st (ex N be increasing sequence of NAT st S2 = S1 * N)
& S2 is convergent & lim S2 in X;
end;
Th6:
for M be non empty MetrSpace,
X be Subset of M st X = {} holds X is sequentially_compact
proof
let M be non empty MetrSpace;
let X be Subset of M;
assume
A1: X = {};
let S1 be sequence of M;
assume
A2: rng S1 c= X;
S1.0 in rng S1 by FUNCT_2:4;
hence ex S2 be sequence of M
st (ex N be increasing sequence of NAT st S2 = S1 * N)
& S2 is convergent & lim S2 in X by A1,A2;
end;
registration let M be non empty MetrSpace;
cluster empty -> sequentially_compact for Subset of M;
coherence by Th6;
end;
definition
let M be non empty MetrSpace;
attr M is sequentially_compact means
[#]M is sequentially_compact;
end;
theorem Th7:
for M be non empty MetrSpace,
X be Subset of M,
Y be Subset of TopSpaceMetr M,
x be Element of M,
y be Element of TopSpaceMetr M
st X=Y & x=y holds
y is_an_accumulation_point_of Y
iff
for r be Real st 0 < r holds Ball(x,r) meets X \ {x}
proof
let M be non empty MetrSpace,
X be Subset of M,
Y be Subset of TopSpaceMetr M,
x be Element of M,
y be Element of TopSpaceMetr M;
assume
A1: X=Y & x=y;
hereby
assume y is_an_accumulation_point_of Y; then
A2: y in Der Y by TOPGEN_1:16;
let r be Real;
assume
A3: 0 < r;
reconsider U = Ball(x,r) as Subset of TopSpaceMetr M;
A4: U is open by TOPMETR:14;
dist(x,x) = 0 by METRIC_1:1; then
consider z be Point of TopSpaceMetr M such that
A5: z in Y /\ U & y <> z by A1,A2,A3,A4,METRIC_1:11,TOPGEN_1:17;
z in Y & z in U & not z in {y} by A5,TARSKI:def 1,XBOOLE_0:def 4; then
z in (Y \ {y}) & z in U by XBOOLE_0:def 5;
hence Ball(x,r) meets X \{x} by A1,XBOOLE_0:def 4;
end;
assume
A6: for r be Real st 0 < r holds Ball(x,r) meets X \ {x};
for U be open Subset of TopSpaceMetr M st y in U
ex z be Point of TopSpaceMetr M st z in Y /\ U & y <> z
proof
let U be open Subset of TopSpaceMetr M;
assume
A7: y in U;
U is open; then
consider r be Real such that
A8: 0 < r & Ball(x,r) c= U by A1,A7,PCOMPS_1:def 4;
Ball(x,r) meets X \ {x} by A6,A8; then
consider z be object such that
A9: z in Ball(x,r) /\ (X \ {x}) by XBOOLE_0:def 1;
z in Ball(x,r) & z in X \ {x} by A9,XBOOLE_0:def 4; then
A10: z in U & z in Y & not z in {x} by A1,A8,XBOOLE_0:def 5;
reconsider z as Point of TopSpaceMetr M by A9;
take z;
thus z in Y /\ U & y <> z by A1,A10,TARSKI:def 1,XBOOLE_0:def 4;
end; then
y in Der Y by TOPGEN_1:17;
hence y is_an_accumulation_point_of Y by TOPGEN_1:16;
end;
LM3:
for M be non empty MetrSpace,
X be Subset of M,
x be Element of M st
(for r be Real st 0 < r holds Ball(x,r) meets X \ {x}) holds
for r be Real st 0 < r
holds Ball(x,r) /\ (X \ {x}) is infinite
proof
let M be non empty MetrSpace,
X be Subset of M,
x be Element of M;
assume
A1: for r be Real st 0 < r holds Ball(x,r) meets (X \{x});
assume not (for r be Real st 0 < r holds
Ball(x,r) /\ (X \{x}) is infinite); then
consider r be Real such that
A2: 0 < r & Ball(x,r) /\ (X \{x}) is finite;
A3: Ball(x,r) /\ (X \{x}) is finite by A2;
A4: Ball(x,r) meets (X \{x}) by A1,A2;
deffunc F(Point of M) = dist(x,$1);
set D = {F(y) where y is Element of the carrier of M:
y in Ball(x,r) /\ (X \{x})};
A5: D is finite from FRAENKEL:sch 21(A3);
A7: D c= REAL
proof
let z be object;
assume z in D; then
consider y be Point of M such that
A6: z = dist(x,y) & y in Ball(x,r) /\ (X \{x});
thus z in REAL by A6,XREAL_0:def 1;
end;
consider w be object such that
A8: w in Ball(x,r) /\ (X \{x}) by A4,XBOOLE_0:def 1;
reconsider w as Point of M by A8;
dist(x,w) in D by A8; then
reconsider D as non empty real-membered set by A7;
reconsider D as left_end real-membered set by A5;
set r0 = min D;
A9: r0 in D
& for s be Real st s in D holds r0 <= s by XXREAL_2:def 7;
consider y be Point of M such that
A10: r0 = dist(x,y) & y in Ball(x,r) /\ (X \{x}) by A9;
A11: y in Ball(x,r) by A10,XBOOLE_0:def 4;
y in X \ {x} by A10,XBOOLE_0:def 4; then
not y in {x} by XBOOLE_0:def 5; then
A12: y <> x by TARSKI:def 1; then
0 < r0 by A10,METRIC_1:7; then
Ball(x,r0/2) meets X \{x} by A1; then
consider z be object such that
A13: z in Ball(x,r0/2) /\ (X \{x}) by XBOOLE_0:def 1;
A14: z in Ball(x,r0/2) & z in X \{x} by A13,XBOOLE_0:def 4;
reconsider z as Point of M by A13;
r0/2 < r0 by A10,A12,METRIC_1:7,XREAL_1:216; then
A15: dist(x,z) < r0 by A14,METRIC_1:11,XXREAL_0:2; then
dist(x,z) < r by A10,A11,METRIC_1:11,XXREAL_0:2; then
z in Ball(x,r) by METRIC_1:11; then
z in Ball(x,r) /\ (X \{x}) by A14,XBOOLE_0:def 4; then
dist(x,z) in D;
hence thesis by A15,XXREAL_2:def 7;
end;
theorem Th8:
for M be non empty MetrSpace
st TopSpaceMetr M is countably_compact holds
M is sequentially_compact
proof
let M be non empty MetrSpace;
assume
A1: TopSpaceMetr M is countably_compact;
A2: TopSpaceMetr M is T_2 by PCOMPS_1:34;
A3: for X be Subset of M st X is infinite
ex x be Element of M
st for r be Real st 0 < r holds Ball(x,r) meets X \ {x}
proof
let X be Subset of M;
assume
A4: X is infinite;
reconsider A = X as Subset of TopSpaceMetr M;
Der A is non empty by A1,A2,A4,COMPL_SP:28; then
consider z be object such that
A5: z in Der A;
A6: z is_an_accumulation_point_of A by A5,TOPGEN_1:16;
reconsider z as Point of TopSpaceMetr M by A5;
reconsider x=z as Element of M;
take x;
thus for r be Real st 0 < r
holds Ball(x,r) meets X \{x} by A6,Th7;
end;
for x be sequence of M st rng x c= [#]M
ex xN be sequence of M
st (ex N be increasing sequence of NAT st xN = x * N)
& xN is convergent & lim xN in [#]M
proof
let x be sequence of M such that
rng x c= [#]M;
per cases;
suppose
rng x is finite; then
consider z be Element of the carrier of M such that
A7: x"{z} c= NAT & x"{z} is infinite by LM1;
consider N be increasing sequence of NAT such that
A8: rng N c=x"{z} by A7,LM2;
set xN = x * N;
take xN;
A9: for n be Nat holds xN.n = z
proof
let n be Nat;
N.n in rng N by FUNCT_2:4,ORDINAL1:def 12; then
x.(N.n) in {z} by A8,FUNCT_2:38; then
x.(N.n) = z by TARSKI:def 1;
hence xN.n = z by FUNCT_2:15,ORDINAL1:def 12;
end;
now
let r be Real;
assume
A10: 0 < r;
reconsider n = 0 as Nat;
take n;
thus for m be Nat st n <= m holds dist(xN.m,z) < r
proof
let m be Nat;
assume n <= m;
dist(xN.m,z) = dist(z,z) by A9
.= 0 by METRIC_1:1;
hence dist(xN.m,z) < r by A10;
end;
end;
hence thesis;
end;
suppose rng x is infinite; then
consider z be Element of M such that
A12: for r be Real st 0 < r
holds Ball(z,r) meets (rng x) \ {z} by A3;
Ball(z,1) meets (rng x) \ {z} by A12; then
consider w be object such that
A13: w in Ball(z,1) /\ ((rng x) \ {z}) by XBOOLE_0:def 1;
reconsider w as Point of M by A13;
w in (rng x) \ {z} by A13,XBOOLE_0:def 4; then
w in rng x by XBOOLE_0:def 5; then
consider N0 be Element of NAT such that
A14: w = x.N0 by FUNCT_2:113;
defpred P[Nat,Nat,Nat] means
$2 < $3 & x.$3 in Ball(z,1/(2+$1));
A15: for n be Nat for ix be Element of NAT
ex iy be Element of NAT st P[n,ix,iy]
proof
let n be Nat,ix be Element of NAT;
assume
A16: not ex iy be Element of NAT st P[n,ix,iy];
A17: Ball(z,1/(2+n)) /\ ((rng x) \ {z})
c= Ball(z,1/(2+n)) by XBOOLE_1:17;
for g be object st g in Ball(z,1/(2+n)) /\ ((rng x) \{z})
holds g in x.:(Segm (ix+1))
proof
let g be object;
assume
A18: g in Ball(z,1/(2+n)) /\ ((rng x) \{z}); then
g in Ball(z,1/(2+n)) & g in ((rng x) \{z})
by XBOOLE_0:def 4; then
g in rng x by XBOOLE_0:def 5; then
consider iy be Element of NAT such that
A19: g = x.iy by FUNCT_2:113;
iy <= ix by A16,A17,A18,A19; then
iy < ix +1 by NAT_1:13; then
iy in Segm(ix+1) by NAT_1:44;
hence g in x.:Segm(ix+1) by A19,FUNCT_2:35;
end; then
Ball(z,1/(2+n)) /\ ((rng x) \{z})
c= x.:(Segm (ix+1)) by TARSKI:def 3;
hence contradiction by A12,LM3;
end;
consider N be sequence of NAT such that
A20: N.0 = N0 & for n be Nat holds P[n,N.n,N.(n+1)]
from RECDEF_1:sch 2(A15);
N is increasing by A20; then
reconsider N as increasing sequence of NAT;
defpred Q[Nat] means x.(N.$1) in Ball(z,1/(1+$1));
A21: Q[0] by A13,A14,A20,XBOOLE_0:def 4;
A22: for k be Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume Q[k];
N.k < N.(k+1) & x.(N.(k+1)) in Ball(z,1/(2+k)) by A20;
hence thesis;
end;
A23: for i be Nat holds Q[i] from NAT_1:sch 2(A21,A22);
now
let r be Real;
assume
A24: 0 < r;
consider n be Nat such that
A25: r " < n by SEQ_4:3;
A26: 1 / n < 1 / (r ") by A24,A25,XREAL_1:76;
A27: 0 < n by A24,A25;
take n;
thus for m be Nat st n <= m holds dist((x*N).m,z) < r
proof
let m be Nat;
assume n <= m; then
n+0 < m+1 by XREAL_1:8; then
A28: 1/(1+m) <= 1/n by A27,XREAL_1:118;
x.(N.m) in Ball(z,1/(1+m)) by A23; then
A29: dist(x.(N.m),z) < 1/n by A28,METRIC_1:11,XXREAL_0:2;
x.(N.m) = (x*N).m by FUNCT_2:15,ORDINAL1:def 12;
hence dist((x*N).m,z) < r by A26,A29,XXREAL_0:2;
end;
end; then
A30: (x*N) is convergent;
lim (x*N) in [#]M;
hence thesis by A30;
end;
end; then
[#]M is sequentially_compact;
hence M is sequentially_compact;
end;
theorem
for M be non empty MetrSpace st M is sequentially_compact holds
TopSpaceMetr M is countably_compact
proof
let M be non empty MetrSpace;
assume
A1: M is sequentially_compact;
A2: for X be Subset of M st X is infinite
ex x be Element of M
st for r be Real st 0 < r
holds Ball(x,r) meets X \ {x}
proof
let X be Subset of M;
assume
A3: X is infinite; then
consider S1 be sequence of X such that
A4: S1 is one-to-one by DICKSON:3;
A5: rng S1 c= X;
rng S1 c= [#]M by XBOOLE_1:1; then
S1 is Function of dom S1,[#]M by FUNCT_2:2; then
reconsider S1 as sequence of [#]M by A3,FUNCT_2:def 1;
rng S1 c= [#]M; then
consider S2 be sequence of M such that
A6: (ex N be increasing sequence of NAT st S2 = S1 * N)
& S2 is convergent & lim S2 in [#]M by A1,Def1;
set x = lim S2;
rng S2 c= rng S1 by A6,RELAT_1:26; then
A7: rng S2 c= X by A5,XBOOLE_1:1;
take x;
thus
for r be Real st 0 < r holds Ball(x,r) meets X \ {x}
proof
let r be Real;
assume 0 < r; then
consider n be Nat such that
A8: for m be Nat st m>=n holds dist(S2.m,x)<r by A6,TBSP_1:def 3;
per cases;
suppose
S2.n <> x; then
A9: not S2.n in {x} by TARSKI:def 1;
n in NAT by ORDINAL1:def 12; then
S2.n in rng S2 by FUNCT_2:112; then
A10: S2.n in X \ {x} by A7,A9,XBOOLE_0:def 5;
dist(S2.n,x) < r by A8; then
S2.n in Ball(x,r) by METRIC_1:11;
hence Ball(x,r) meets X \{x} by A10,XBOOLE_0:def 4;
end;
suppose
A11: S2.n = x;
consider N be increasing sequence of NAT such that
A12: S2 = S1 * N by A6;
for x1,x2 be object st x1 in NAT & x2 in NAT & N.x1 = N.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A13: x1 in NAT & x2 in NAT; then
reconsider n=x1,m=x2 as Nat;
assume
A14: N.x1 = N.x2;
assume x1 <> x2; then
A15: n < m or m < n by XXREAL_0:1;
dom N = NAT by FUNCT_2:def 1;
hence contradiction by A13,A14,A15,SEQM_3:def 1;
end; then
N is one-to-one by FUNCT_2:19; then
A16: S2 is one-to-one by A4,A12,FUNCT_1:24;
A17: n < n+1 by NAT_1:16;
n in NAT & n+1 in NAT by ORDINAL1:def 12; then
S2.(n+1) <> x by A11,A16,A17,FUNCT_2:19; then
A18: not S2.(n+1) in {x} by TARSKI:def 1;
S2.(n+1) in rng S2 by FUNCT_2:112; then
A19: S2.(n+1) in X \{x} by A7,A18,XBOOLE_0:def 5;
dist(S2.(n+1),x)<r by A8,A17; then
S2.(n+1) in Ball(x,r) by METRIC_1:11;
hence Ball(x,r) meets X \{x} by A19,XBOOLE_0:def 4;
end;
end;
end;
A20: for A be Subset of TopSpaceMetr M st A is infinite
holds Der A is non empty
proof
let A be Subset of TopSpaceMetr M;
assume
A21: A is infinite;
reconsider X = A as Subset of M;
consider x be Element of M such that
A22: for r be Real st 0 < r holds Ball(x,r) meets X \{x} by A2,A21;
reconsider y = x as Point of TopSpaceMetr M;
y is_an_accumulation_point_of A by A22,Th7;
hence Der A is non empty by TOPGEN_1:16;
end;
TopSpaceMetr M is T_2 by PCOMPS_1:34;
hence TopSpaceMetr M is countably_compact by A20,COMPL_SP:28;
end;
Th10:
for M be non empty MetrSpace
st M is sequentially_compact holds
M is totally_bounded complete
proof
let M be non empty MetrSpace;
assume M is sequentially_compact; then
A1: [#]M is sequentially_compact;
thus M is totally_bounded
proof
assume not M is totally_bounded; then
consider r be Real such that
A2: r > 0 & not (ex G be Subset-Family of M
st G is finite
& the carrier of M = union G
& for C be Subset of M st C in G
ex w be Element of M st C = Ball(w,r));
set S0 = the Element of M;
set G0 = {};
set ABL = {GX where GX is Subset-Family of M : GX is finite
& for C be Subset of M st C in GX
holds ex w be Element of M st C = Ball(w,r)};
A3: G0 is Subset of bool [#]M by XBOOLE_1:2;
for C be Subset of M st C in G0
holds ex w be Element of M st C = Ball(w,r); then
A4: G0 in ABL by A3; then
reconsider ABL as non empty set;
reconsider G0 as Element of ABL by A4;
defpred P[Nat,Element of M,set,Element of M,set] means
$5 = $3 \/ {Ball($2,r)} & not $4 in union $5;
A5: for n be Nat, x be Element of M, y be Element of ABL
ex x1 be Element of M, y1 be Element of ABL st P[n,x,y,x1,y1]
proof
let n be Nat, x be Element of M, y be Element of ABL;
y in ABL; then
consider GX be Subset-Family of M such that
A6: y = GX & GX is finite
& for C be Subset of M st C in GX
holds ex w be Element of M st C = Ball(w,r);
set y1 = y \/ {Ball(x,r)};
Ball(x,r) in (bool [#]M) by ZFMISC_1:def 1; then
{Ball(x,r)} c= (bool [#]M) by ZFMISC_1:31; then
reconsider y1 as Subset-Family of M by A6,XBOOLE_1:8;
A7: for C be Subset of M st C in y1
holds ex w be Element of M st C = Ball(w,r)
proof
let C be Subset of M;
assume C in y1; then
per cases by XBOOLE_0:def 3;
suppose
C in y;
hence ex w be Element of M st C = Ball(w,r) by A6;
end;
suppose
C in {Ball(x,r)}; then
C = Ball(x,r) by TARSKI:def 1;
hence ex w be Element of M st C = Ball(w,r);
end;
end; then
A8: y1 in ABL by A6;
not the carrier of M = union y1 by A2,A6,A7; then
consider x1 be object such that
A9: x1 in the carrier of M & not x1 in union y1 by TARSKI:def 3;
reconsider x1 as Element of M by A9;
reconsider y1 as Element of ABL by A8;
take x1,y1;
thus thesis by A9;
end;
consider S1 be sequence of M, Y be sequence of ABL such that
A10: S1.0 = S0 & Y.0 = G0
& for n be Nat holds P[n,S1.n,Y.n,S1.(n+1),Y.(n+1)]
from RECDEF_2:sch 3(A5);
rng S1 c= [#]M; then
consider S2 be sequence of M such that
A11: (ex N be increasing sequence of NAT st S2 = S1 * N)
& S2 is convergent & lim S2 in [#]M by A1;
defpred Q[Nat] means
for k be Nat st k<=$1 holds Ball(S1.k,r) c= union (Y.($1+1));
A12: Q[0]
proof
let k be Nat;
assume
A13: k<=0;
Y.(0+1) = {} \/ {Ball(S1.0,r)} by A10
.= {Ball(S1.0,r)};
hence thesis by A13;
end;
A14: for n be Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
assume
A15: Q[n];
A16: Y.((n+1)+1) = Y.(n+1) \/ {Ball(S1.(n+1),r)} by A10; then
A17: union (Y.(n+1)) c= union (Y.((n+1)+1)) by XBOOLE_1:7,ZFMISC_1:77;
Ball(S1.(n+1),r) in {Ball(S1.(n+1),r)} by TARSKI:def 1; then
A18: Ball(S1.(n+1),r) in Y.((n+1)+1) by A16,TARSKI:def 3,XBOOLE_1:7;
let k be Nat;
assume k <= n+1; then
per cases by NAT_1:8;
suppose
k <= n; then
Ball(S1.k,r) c= union (Y.(n+1)) by A15;
hence Ball(S1.k,r) c= union (Y.((n+1)+1)) by A17,XBOOLE_1:1;
end;
suppose
k = n+1;
hence Ball(S1.k,r) c= union (Y.((n+1)+1)) by A18,ZFMISC_1:74;
end;
end;
A19: for n be Nat holds Q[n] from NAT_1:sch 2(A12,A14);
A20: for n,k be Nat st k<=n holds r <= dist(S1.(n+1),S1.k)
proof
let n,k be Nat;
assume k <= n; then
Ball(S1.k,r) c= union (Y.(n+1)) by A19; then
not S1.(n+1) in Ball(S1.k,r) by A10;
hence thesis by METRIC_1:11;
end;
A21: for n,k be Nat st k < n holds r <= dist(S1.n,S1.k)
proof
let n,k be Nat;
assume
A22: k < n; then
k+1 <= n by NAT_1:13; then
A23: k + 1 -1 <= n-1 by XREAL_1:9;
reconsider n1=n-1 as Nat by A22;
r <= dist(S1.(n1+1),S1.k) by A20,A23;
hence r <= dist(S1.n,S1.k);
end;
not S2 is convergent
proof
assume S2 is convergent; then
S2 is Cauchy; then
consider p be Nat such that
A24: for n,m be Nat st p<=n & p<=m holds dist(S2.n,S2.m)<r by A2;
consider N be increasing sequence of NAT such that
A25: S2 = S1 * N by A11;
set q=p+1;
A26: p < q by NAT_1:16;
A27: S2.p = S1.(N.p) & S2.q = S1.(N.q) by A25,FUNCT_2:15,ORDINAL1:def 12;
p in NAT & q in NAT by ORDINAL1:def 12; then
p in dom N & q in dom N by FUNCT_2:def 1; then
N.p < N.q by NAT_1:16,SEQM_3:def 1; then
r <= dist(S1.(N.q),S1.(N.p)) by A21;
hence contradiction by A24,A26,A27;
end;
hence contradiction by A11;
end;
now
let S be sequence of M such that
A28: S is Cauchy;
thus S is convergent
proof
reconsider S1 = S as sequence of [#]M;
rng S1 c= [#]M; then
consider S2 be sequence of M such that
A29: (ex N be increasing sequence of NAT st S2 = S1 * N)
& S2 is convergent & lim S2 in [#]M by A1;
consider N be increasing sequence of NAT such that
A30: S2 = S1 * N by A29;
take x = lim S2;
let r be Real;
assume
A31: 0<r; then
consider p be Nat such that
A32: for n,m be Nat st p<=n & p<=m holds dist(S.n,S.m)<r/2 by A28;
consider q be Nat such that
A33: for m be Nat st m>=q holds dist(S2.m,lim S2)< r/2
by A29,A31,TBSP_1:def 3;
reconsider l = max(p,q) as Nat by XXREAL_0:16;
take l;
let m be Nat;
assume
A34: l<=m;
p <= l by XXREAL_0:25; then
A35: p <= m by A34,XXREAL_0:2;
m <= N.m by SEQM_3:14; then
p <= N.m by A35,XXREAL_0:2; then
dist(S.m,S.(N.m))<r/2 by A32,A35; then
A36: dist(S.m,S2.m)<r/2 by A30,FUNCT_2:15,ORDINAL1:def 12;
q <= l by XXREAL_0:25; then
q <= m by A34,XXREAL_0:2; then
dist(S2.m,lim S2)<r/2 by A33; then
A37: dist(S.m,S2.m)+dist(S2.m,lim S2)<r/2+r/2 by A36,XREAL_1:8;
dist(S.m,x)<=dist(S.m,S2.m)+dist(S2.m,x) by METRIC_1:4;
hence thesis by A37,XXREAL_0:2;
end;
end;
hence M is complete;
end;
theorem Th11:
for M be non empty MetrSpace holds
TopSpaceMetr M is compact iff M is sequentially_compact
proof
let M be non empty MetrSpace;
thus TopSpaceMetr M is compact implies M is sequentially_compact
by Th8,COMPL_SP:35;
assume M is sequentially_compact; then
M is totally_bounded complete by Th10;
hence TopSpaceMetr M is compact by COMPL_SP:37;
end;
theorem Th12:
for M be non empty MetrSpace holds
M is totally_bounded complete iff M is sequentially_compact
proof
let M be non empty MetrSpace;
M is totally_bounded complete
iff TopSpaceMetr M is compact by COMPL_SP:37;
hence thesis by Th11;
end;
theorem Th14:
for M be non empty MetrSpace,
S be non empty Subset of M holds
S is sequentially_compact
iff
(M|S) is sequentially_compact
proof
let M be non empty MetrSpace,
S be non empty Subset of M;
A1: the carrier of (M|S) = S by TOPMETR:def 2;
set X = [#](M|S);
hereby
assume
A2: S is sequentially_compact;
for S1 be sequence of (M|S) st rng S1 c= X
ex S2 be sequence of (M|S)
st (ex N be increasing sequence of NAT st S2 = S1 * N )
& S2 is convergent & lim S2 in X
proof
let S1 be sequence of (M|S);
assume rng S1 c= X;
A3: rng S1 c= S by A1;
rng S1 c= [#]M by A1,XBOOLE_1:1; then
reconsider SS1=S1 as sequence of M by FUNCT_2:6;
consider SS2 be sequence of M such that
A4: (ex N be increasing sequence of NAT st SS2 = SS1 * N)
& SS2 is convergent & lim SS2 in S by A2,A3;
consider N be increasing sequence of NAT such that
A5: SS2 = SS1 * N by A4;
rng SS2 c= rng SS1 by A5,RELAT_1:26; then
rng SS2 c= [#](M|S) by A3,XBOOLE_1:1; then
reconsider S2=SS2 as sequence of (M|S) by FUNCT_2:6;
take S2;
thus ex N be increasing sequence of NAT st S2 = S1 * N by A5;
reconsider x = lim SS2 as Element of (M|S) by A4,TOPMETR:def 2;
now
let r be Real;
assume 0 < r; then
consider n be Nat such that
A6: for m be Nat st n<=m holds dist(SS2.m,lim SS2) < r
by A4,TBSP_1:def 3;
take n;
thus for m be Nat st n<=m holds dist(S2.m,x) < r
proof
let m be Nat;
assume n<=m; then
dist(SS2.m,lim SS2) < r by A6;
hence dist(S2.m,x) < r by TOPMETR:def 1;
end;
end;
hence S2 is convergent;
thus lim S2 in X;
end; then
X is sequentially_compact;
hence (M|S) is sequentially_compact;
end;
assume
A7: (M|S) is sequentially_compact;
for S1 be sequence of M st rng S1 c= S
ex S2 be sequence of M
st (ex N be increasing sequence of NAT st S2 = S1 * N)
& S2 is convergent & lim S2 in S
proof
let S1 be sequence of M;
assume rng S1 c= S; then
A8: rng S1 c= [#] (M|S) by TOPMETR:def 2; then
reconsider SS1=S1 as sequence of (M|S) by FUNCT_2:6;
consider SS2 be sequence of (M|S) such that
A9: (ex N be increasing sequence of NAT st SS2 = SS1 * N)
& SS2 is convergent & lim SS2 in X by A7,A8,Def1;
consider N be increasing sequence of NAT such that
A10: SS2 = SS1 * N by A9;
rng SS2 c= [#]M by A1,XBOOLE_1:1; then
reconsider S2=SS2 as sequence of M by FUNCT_2:6;
take S2;
thus ex N be increasing sequence of NAT st S2 = S1 * N by A10;
reconsider x = lim SS2 as Element of M by A1,A9;
A11: now
let r be Real;
assume 0 < r; then
consider n be Nat such that
A12: for m be Nat st n<=m holds dist(SS2.m,lim SS2) < r
by A9,TBSP_1:def 3;
take n;
thus for m be Nat st n<=m holds dist(S2.m,x) < r
proof
let m be Nat;
assume n<=m; then
dist(SS2.m,lim SS2) < r by A12;
hence dist(S2.m,x) < r by TOPMETR:def 1;
end;
end;
hence S2 is convergent; then
lim S2 = x by A11,TBSP_1:def 3;
hence lim S2 in S by A1;
end;
hence S is sequentially_compact;
end;
theorem
for M be non empty MetrSpace,
S be non empty Subset of M holds
S is sequentially_compact
iff
(M|S) is compact
proof
let M be non empty MetrSpace,
S be non empty Subset of M;
(M|S) is sequentially_compact iff (M|S) is compact by Th11;
hence thesis by Th14;
end;
theorem Th16:
for M be non empty MetrSpace,
S be Subset of M,
T be Subset of TopSpaceMetr M
st T = S holds
T is compact iff S is sequentially_compact
proof
let M be non empty MetrSpace,
S0 be Subset of M,
T0 be Subset of TopSpaceMetr M;
assume
A1: T0 = S0;
per cases;
suppose
T0 = {};
hence thesis by A1;
end;
suppose
A2: T0 <> {}; then
reconsider T = T0 as non empty Subset of TopSpaceMetr M;
reconsider S = T0 as non empty Subset of M by A2;
hereby
assume T0 is compact; then
(TopSpaceMetr M) | T is compact; then
TopSpaceMetr (M|S) is compact by HAUSDORF:16; then
(M|S) is sequentially_compact by Th11;
hence S0 is sequentially_compact by A1,Th14;
end;
assume S0 is sequentially_compact; then
(M|S) is sequentially_compact by A1,Th14; then
TopSpaceMetr (M|S) is compact by Th11; then
(TopSpaceMetr M) | T is compact by HAUSDORF:16;
hence T0 is compact by COMPTS_1:3;
end;
end;
theorem
for M be non empty MetrSpace,
S be non empty Subset of M,
T be non empty Subset of TopSpaceMetr M
st T = S holds
(TopSpaceMetr M) | T is countably_compact
iff S is sequentially_compact
proof
let M be non empty MetrSpace,
S be non empty Subset of M,
T be non empty Subset of TopSpaceMetr M;
assume
A1: T = S;
hereby
assume (TopSpaceMetr M) | T is countably_compact; then
TopSpaceMetr (M|S) is countably_compact by A1,HAUSDORF:16; then
(M|S) is sequentially_compact by Th11,COMPL_SP:35;
hence S is sequentially_compact by Th14;
end;
assume S is sequentially_compact; then
(M|S) is sequentially_compact by Th14; then
TopSpaceMetr (M|S) is countably_compact by Th11,COMPL_SP:35;
hence (TopSpaceMetr M) |T is countably_compact by A1,HAUSDORF:16;
end;
theorem
for M be non empty MetrSpace,
S be non empty Subset of M holds
(M|S is totally_bounded complete)
iff S is sequentially_compact
proof
let M be non empty MetrSpace,
S be non empty Subset of M;
hereby
assume M|S is totally_bounded complete; then
(M|S) is sequentially_compact by Th12;
hence S is sequentially_compact by Th14;
end;
assume S is sequentially_compact; then
(M|S) is sequentially_compact by Th14;
hence M|S is totally_bounded complete by Th12;
end;
begin :: 3. Compactness in norm spaces
theorem Th19:
for NrSp be RealNormSpace,
S be Subset of NrSp,
T be Subset of MetricSpaceNorm NrSp
st S = T
holds S is compact iff T is sequentially_compact
proof
let NrSp be RealNormSpace,
S be Subset of NrSp,
T be Subset of MetricSpaceNorm NrSp;
assume
A1: S = T;
hereby
assume
A2: S is compact;
now
let S1 be sequence of MetricSpaceNorm NrSp;
assume
A3: rng S1 c= T;
reconsider s1 = S1 as sequence of NrSp;
consider s2 be sequence of NrSp such that
A4: s2 is subsequence of s1 & s2 is convergent
& lim s2 in S by A1,A2,A3;
consider N be increasing sequence of NAT such that
A5: s2 = s1 * N by A4,VALUED_0:def 17;
reconsider S2 = s2 as sequence of MetricSpaceNorm NrSp;
take S2;
thus ex N be increasing sequence of NAT st S2 = S1 * N by A5;
thus S2 is convergent by A4,NORMSP_2:5;
hence lim S2 in T by A1,A4,NORMSP_2:6;
end;
hence T is sequentially_compact;
end;
assume
A6: T is sequentially_compact;
now
let s1 be sequence of NrSp;
assume
A7: rng s1 c= S;
reconsider S1 = s1 as sequence of MetricSpaceNorm NrSp;
consider S2 be sequence of MetricSpaceNorm NrSp such that
A8: (ex N be increasing sequence of NAT st S2 = S1 * N)
& S2 is convergent & lim S2 in T by A1,A6,A7;
consider N be increasing sequence of NAT such that
A9: S2 = S1 * N by A8;
reconsider s2 = S2 as sequence of NrSp;
take s2;
thus s2 is subsequence of s1 by A9;
thus s2 is convergent by A8,NORMSP_2:5;
thus lim s2 in S by A1,A8,NORMSP_2:6;
end;
hence S is compact;
end;
theorem
for NrSp be RealNormSpace,
S be Subset of NrSp,
T be Subset of TopSpaceNorm NrSp
st S = T
holds S is compact iff T is compact
proof
let NrSp be RealNormSpace,
S be Subset of NrSp,
T be Subset of TopSpaceNorm NrSp;
assume
A1: S = T;
reconsider W = S as Subset of MetricSpaceNorm NrSp;
W is sequentially_compact iff T is compact by A1,Th16;
hence thesis by Th19;
end;
begin :: 4. Topological properties of the real line
theorem Th23:
for S1 be sequence of RealSpace, seq be Real_Sequence,
g be Real, g1 be Element of RealSpace st S1 = seq & g = g1 holds
(for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds |.seq.m - g.| < p)
iff
(for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds dist(S1.m,g1) < p)
proof
let S1 be sequence of RealSpace, seq be Real_Sequence,
g be Real, g1 be Element of RealSpace;
assume
A1: S1 = seq & g = g1;
hereby
assume
A2: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds |.seq.m - g.| < p;
thus for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds dist(S1.m,g1) < p
proof
let p be Real;
assume 0 < p; then
consider n be Nat such that
A3: for m be Nat st n <= m holds |.seq.m - g.| < p by A2;
A4: for m be Nat st n <= m holds dist(S1.m,g1) < p
proof
let m be Nat;
assume C5: n <= m;
set s = seq.m;
set s1 = S1.m;
dist(s1,g1) = |.s - g.| by A1,TOPMETR:11;
hence thesis by A3,C5;
end;
take n;
thus thesis by A4;
end;
end;
assume
A5: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds dist(S1.m,g1) < p;
thus for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds |.seq.m - g.| < p
proof
let p be Real;
assume 0 < p; then
consider n be Nat such that
A6: for m be Nat st n <= m holds dist(S1.m,g1) < p by A5;
A7: for m be Nat st n <= m holds |.seq.m - g.| < p
proof
let m be Nat;
assume
A8: n <= m;
set s = seq.m;
set s1 = S1.m;
dist(s1,g1) = |.s - g.| by A1,TOPMETR:11;
hence thesis by A6,A8;
end;
take n;
thus thesis by A7;
end;
end;
theorem
for S1 be sequence of RealSpace, seq be Real_Sequence,
g be Real, g1 be Element of RealSpace st S1 = seq & g = g1
holds
(seq is convergent & lim seq = g)
iff
(S1 is convergent & lim S1 = g1)
proof
let S1 be sequence of RealSpace, seq be Real_Sequence,
g be Real, g1 be Element of RealSpace;
assume AS: S1=seq & g=g1;
hereby
assume seq is convergent & lim seq = g; then
for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds |.seq.m - g.| < p
by SEQ_2:def 7; then
A1: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds dist(S1.m,g1) < p
by AS,Th23;
hence S1 is convergent;
hence lim S1 = g1 by A1,TBSP_1:def 3;
end;
assume S1 is convergent & lim S1 = g1; then
for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds dist(S1.m,g1) < p
by TBSP_1:def 3; then
A2: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds |.seq.m - g.| < p
by AS,Th23;
hence seq is convergent by SEQ_2:def 6;
hence lim seq = g by A2,SEQ_2:def 7;
end;
theorem
for S1 be sequence of RealSpace, seq be Real_Sequence
st S1 = seq & seq is convergent
holds S1 is convergent & lim S1 = lim seq
proof
let S1 be sequence of RealSpace, seq be Real_Sequence;
assume
A1: S1 = seq & seq is convergent;
reconsider g1 = lim seq as Point of RealSpace by XREAL_0:def 1;
for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds |.seq.m - lim seq.| < p
by A1,SEQ_2:def 7; then
A2: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds dist(S1.m,g1) < p
by A1,Th23;
hence S1 is convergent;
hence lim S1 = lim seq by A2,TBSP_1:def 3;
end;
begin :: 5. Compactness in the real line
:: The equivalence of the notions of compactness in R^1 and REAL was shown
:: in JORDAN5A
theorem Th27:
for N be Subset of REAL, M be Subset of R^1 st N = M holds
(for F be Subset-Family of REAL
st F is Cover of N
& (for P be Subset of REAL st P in F holds P is open)
holds
ex G be Subset-Family of REAL
st G c= F & G is Cover of N & G is finite)
iff
(for F1 be Subset-Family of R^1 st F1 is Cover of M & F1 is open
holds
ex G1 be Subset-Family of R^1
st G1 c= F1 & G1 is Cover of M & G1 is finite)
proof
let N be Subset of REAL, M be Subset of R^1;
assume
A1: N = M;
hereby
assume
A2: for F be Subset-Family of REAL
st F is Cover of N
& (for P be Subset of REAL st P in F holds P is open)
holds
ex G be Subset-Family of REAL
st G c= F & G is Cover of N & G is finite;
thus for F1 be Subset-Family of R^1
st F1 is Cover of M & F1 is open holds
ex G1 be Subset-Family of R^1
st G1 c= F1 & G1 is Cover of M & G1 is finite
proof
let F1 be Subset-Family of R^1;
assume
A3: F1 is Cover of M & F1 is open;
reconsider F = F1 as Subset-Family of REAL;
for P be Subset of REAL st P in F holds P is open
proof
let P be Subset of REAL;
assume
A4: P in F;
reconsider P1 = P as Subset of R^1;
P1 is open by A3,A4;
hence P is open by BORSUK_5:39;
end; then
consider G be Subset-Family of REAL such that
A5: G c= F & G is Cover of N & G is finite by A1,A2,A3;
reconsider G1 = G as Subset-Family of R^1;
take G1;
thus thesis by A1,A5;
end;
end;
assume
A6: for F1 be Subset-Family of R^1
st F1 is Cover of M & F1 is open holds
ex G1 be Subset-Family of R^1
st G1 c= F1 & G1 is Cover of M & G1 is finite;
let F be Subset-Family of REAL;
assume that
A7: F is Cover of N and
A8: for P be Subset of REAL st P in F holds P is open;
reconsider F1 = F as Subset-Family of R^1;
for P1 be Subset of R^1 st P1 in F1 holds P1 is open
proof
let P1 be Subset of R^1;
assume
A9: P1 in F1;
reconsider P = P1 as Subset of REAL;
P is open by A8,A9;
hence P1 is open by BORSUK_5:39;
end; then
F1 is open; then
consider G1 be Subset-Family of R^1 such that
A10: G1 c= F1 & G1 is Cover of M & G1 is finite by A1,A6,A7;
reconsider G = G1 as Subset-Family of REAL;
take G;
thus thesis by A1,A10;
end;
theorem
for N be Subset of REAL holds
N is compact
iff
(for F be Subset-Family of REAL
st F is Cover of N
& (for P be Subset of REAL st P in F holds P is open) holds
ex G be Subset-Family of REAL
st G c= F & G is Cover of N & G is finite)
proof
let N be Subset of REAL;
reconsider M = N as Subset of R^1;
M is compact iff
(for F be Subset-Family of REAL
st F is Cover of N
& for P be Subset of REAL st P in F holds P is open holds
ex G be Subset-Family of REAL
st G c= F & G is Cover of N & G is finite) by Th27;
hence thesis by JORDAN5A:25;
end;