:: Heine--Borel's Covering Theorem
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991-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, REAL_1, PRE_TOPC, METRIC_1, COMPLEX1, ARYTM_1,
FUNCT_1, SEQ_1, ORDINAL2, RELAT_1, TARSKI, XXREAL_0, ARYTM_3, CARD_1,
POWER, LIMFUNC1, NEWTON, TOPMETR, RCOMP_1, XXREAL_1, STRUCT_0, PCOMPS_1,
SETFAM_1, FINSET_1, XBOOLE_0, VALUED_0, SEQ_2, NAT_1, ZFMISC_1, XXREAL_2,
VALUED_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, METRIC_1,
FINSET_1, BINOP_1, STRUCT_0, PRE_TOPC, COMPTS_1, PCOMPS_1, VALUED_0,
VALUED_1, SEQ_1, SEQ_2, LIMFUNC1, POWER, RCOMP_1, NEWTON, TOPMETR,
XXREAL_0, RECDEF_1;
constructors SETFAM_1, REAL_1, NAT_1, SEQ_2, SEQM_3, SEQ_4, RCOMP_1, LIMFUNC1,
NEWTON, POWER, COMPTS_1, TOPMETR, VALUED_1, RECDEF_1, PCOMPS_1, COMSEQ_2,
BINOP_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS,
XREAL_0, MEMBERED, PRE_TOPC, METRIC_1, VALUED_1, FUNCT_2, VALUED_0,
NAT_1, ZFMISC_1, NEWTON, POWER;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_2, SEQ_2, LIMFUNC1;
equalities XCMPLX_0;
expansions TARSKI, LIMFUNC1;
theorems ABSVALUE, FUNCT_1, FUNCT_2, TOPMETR, LIMFUNC1, METRIC_1, NAT_1,
NEWTON, POWER, PCOMPS_1, RCOMP_1, SEQ_1, SEQ_2, SEQ_4, SEQM_3, TARSKI,
ZFMISC_1, XREAL_0, XBOOLE_1, XCMPLX_1, XREAL_1, COMPLEX1, COMPTS_1,
XXREAL_0, XXREAL_1, VALUED_0, VALUED_1, SETFAM_1, RELSET_1, ORDINAL1,
NUMBERS;
schemes RECDEF_1, NAT_1, SEQ_1;
begin
reserve a,b,x,y for Real,
i,k,n,m for Nat;
reserve p,w for Real;
theorem Th1:
for A being SubSpace of RealSpace, p,q being Point of A st x = p
& y = q holds dist(p,q) = |.x-y.|
proof
let A be SubSpace of RealSpace, p,q be Point of A;
assume
A1: x = p & y = q;
thus dist(p,q) = (the distance of A).(p,q) by METRIC_1:def 1
.= (real_dist).(x, y) by A1,METRIC_1:def 13,TOPMETR:def 1
.= |.x-y.| by METRIC_1:def 12;
end;
reserve seq for Real_Sequence;
theorem Th2:
seq is increasing & rng seq c= NAT implies n <= seq.n
proof
defpred P[Nat] means $1 <= seq.$1;
assume that
A1: seq is increasing and
A2: rng seq c= NAT;
A3: for k st P[k] holds P[k+1]
proof
let k such that
A4: k <= seq.k;
k+1 in NAT;
then k+1 in dom seq by FUNCT_2:def 1;
then seq.(k+1) in rng seq by FUNCT_1:def 3;
then reconsider k9 = seq.(k+1) as Element of NAT by A2;
seq.k < seq.(k+1) by A1,SEQM_3:def 6;
then k < k9 by A4,XXREAL_0:2;
hence thesis by NAT_1:13;
end;
0 in NAT;
then 0 in dom seq by FUNCT_2:def 1;
then seq.0 in rng seq by FUNCT_1:def 3;
then
A5: P[0] by A2;
for n holds P[n] from NAT_1:sch 2(A5,A3);
hence thesis;
end;
definition
let seq,k;
func k to_power seq -> Real_Sequence means
:Def1:
for n holds it.n = k to_power (seq.n);
existence
proof
deffunc F(Nat) = k to_power (seq.$1);
thus ex s being Real_Sequence st
for n holds s.n = F(n) from SEQ_1:sch 1;
end;
uniqueness
proof
let s1,s2 be Real_Sequence;
assume that
A1: for n holds s1.n = k to_power (seq.n) and
A2: for n holds s2.n = k to_power (seq.n);
let n be Element of NAT;
thus s1.n = k to_power (seq.n) by A1
.= s2.n by A2;
end;
end;
theorem Th3:
seq is divergent_to+infty implies 2 to_power seq is divergent_to+infty
proof
assume
A1: seq is divergent_to+infty;
let r be Real;
consider p being Nat such that
A2: p > r by SEQ_4:3;
consider n such that
A3: for m st n <= m holds p < seq.m by A1;
take n;
let m;
assume m >= n;
then p < seq.m by A3;
then
A4: 2 to_power p < 2 to_power (seq.m) by POWER:39;
p < 2 to_power p by NEWTON:86;
then p < 2 to_power (seq.m) by A4,XXREAL_0:2;
then r < 2 to_power (seq.m) by A2,XXREAL_0:2;
hence thesis by Def1;
end;
::$N Heine-Borel Theorem for intervals
::$L https://en.wikipedia.org/wiki/Heine-Borel_theorem Heine-Borel Theorem for intervals
theorem
a <= b implies Closed-Interval-TSpace(a,b) is compact
proof
set M = Closed-Interval-MSpace(a,b);
assume
A1: a <= b;
reconsider a, b as Real;
set r = b-a qua Real;
now
per cases by A1,XREAL_1:48;
suppose
r = 0;
then
[. a,b .] = {a} & the carrier of Closed-Interval-TSpace(a,b) = [. a,
b .] by TOPMETR:18,XXREAL_1:17;
hence Closed-Interval-TSpace(a,b) is compact by COMPTS_1:18;
end;
suppose
A2: r > 0;
A3: TopSpaceMetr M = Closed-Interval-TSpace(a,b) by TOPMETR:def 7;
assume not Closed-Interval-TSpace(a,b) is compact;
then not M is compact by A3,TOPMETR:def 5;
then consider F being Subset-Family of M such that
A4: F is being_ball-family and
A5: F is Cover of M and
A6: not ex G being Subset-Family of M st (G c= F & G is Cover of M
& G is finite) by TOPMETR:16;
defpred P[Nat, Element of REAL, Element of REAL] means ((not
ex G being Subset-Family of M st G c= F & [. $2-(r/2|^($1+1)), $2 .] c= union G
& G is finite) implies $3 = $2 - r/2|^($1+2)) & (not (not ex G being
Subset-Family of M st G c= F & [. $2-r/2|^($1+1), $2 .] c= union G & G is
finite) implies $3 = $2 + r/2|^($1+2));
A7: for n being Nat for p being Element of REAL
ex w being Element of REAL st P[n,p,w]
proof
let n be Nat; let p be Element of REAL;
now
per cases;
suppose
A8: not ex G being Subset-Family of M st G c= F & [. p-(r/2|^
(n+1)), p .] c= union G & G is finite;
reconsider y = p - r/2|^(n+2) as Element of REAL by XREAL_0:def 1;
take y;
thus P[n,p,y] by A8;
end;
suppose
A9: ex G being Subset-Family of M st G c= F & [. p-(r/2|^(n+1
)), p .] c= union G & G is finite;
reconsider y = p + r/2|^(n+2) as Element of REAL by XREAL_0:def 1;
take y;
thus P[n,p,y] by A9;
end;
end;
hence thesis;
end;
consider f being sequence of REAL such that
A10: f.0 = In((a+b)/2,REAL) and
A11: for n being Nat holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A7);
defpred R[Nat] means
not ex G being Subset-Family of M st (G
c= F & [. f.$1 - r/2|^($1+1), f.$1 + r/2|^($1+1) .] c= union G & G is finite);
A12: f.0 + r/2|^(0+1) = (a+b)/2 + r/2 by A10
.= b;
defpred Q[Nat] means
a <= f.$1 - r/2|^($1+1) & f.$1 + r/2|^(
$1+1) <= b;
A13: for n holds f.(n+1) = f.n + r/2|^(n+2) or f.(n+1) = f.n - r/2|^(n+2 )
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n,f.n,f.(n+1)] by A11;
hence thesis;
end;
A14: for k st Q[k] holds Q[k+1]
proof
let k;
A15: r/(2*(2|^(k+1))) + r/(2*(2|^(k+1))) = r/2|^(k+1) by XCMPLX_1:118;
A16: r/2|^(k+1) - r/2|^(k+(1+1)) = r/2|^(k+1) - r/2|^((k+1)+1)
.= r/2|^(k+1) - r/(2*2|^(k+1)) by NEWTON:6
.= r/2|^(k+1+1) by A15,NEWTON:6
.= r/2|^(k+(1+1));
assume
A17: Q[k];
then
A18: b - f.k >= r/2|^(k+1) by XREAL_1:19;
A19: f.k - a >= r/2|^(k+1) by A17,XREAL_1:11;
now
per cases by A13;
suppose
A20: f.(k+1) = f.k + r/2|^(k+2);
2|^(k+1) > 0 & r >= 0 by A1,NEWTON:83,XREAL_1:48;
then
A21: r/2|^(k+1) >= 0;
f.(k+1) - a = f.k - a + r/2|^(k+2) by A20;
then f.(k+1) - a >= r/2|^(k+2) by A19,A21,XREAL_1:31;
hence a <= f.(k+1) - r/2|^(k+1+1) by XREAL_1:11;
b - f.(k+1) = b - f.k - r/2|^(k+2) by A20;
then b - f.(k+1) >= r/2|^(k+2) by A18,A16,XREAL_1:9;
hence f.(k+1) + r/2|^(k+1+1) <= b by XREAL_1:19;
end;
suppose
A22: f.(k+1) = f.k - r/2|^(k+2);
then f.(k+1) - a = f.k - a - r/2|^(k+2);
then f.(k+1) - a >= r/2|^(k+2) by A19,A16,XREAL_1:9;
hence a <= f.(k+1) - r/2|^(k+1+1) by XREAL_1:11;
2|^(k+1) > 0 & r >= 0 by A1,NEWTON:83,XREAL_1:48;
then
A23: r/2|^(k+1) >= 0;
b - f.(k+1) = b - f.k + r/2|^(k+2) by A22;
then b - f.(k+1) >= r/2|^(k+2) by A18,A23,XREAL_1:31;
hence f.(k+1) + r/2|^(k+1+1) <= b by XREAL_1:19;
end;
end;
hence thesis;
end;
A24: f.0 - r/2|^(0+1) = (a+b)/2 - r/2 by A10
.= a;
then
A25: Q[0] by A12;
A26: for k holds Q[k] from NAT_1:sch 2(A25,A14);
A27: rng f c= [. a,b .]
proof
let y be object;
assume y in rng f;
then consider x being object such that
A28: x in dom f and
A29: y = f.x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A28,FUNCT_2:def 1;
A30: 2|^(n+1) > 0 & r >= 0 by A1,NEWTON:83,XREAL_1:48;
f.n + r/2|^(n+1) <= b by A26;
then
A31: f.n <= b by A30,XREAL_1:40;
a <= f.n - r/2|^(n+1) by A26;
then a <= f.n by A30,XREAL_1:51;
then y in { y1 where y1 is Real: a <= y1 <= b} by A29,A31;
hence thesis by RCOMP_1:def 1;
end;
A32: for k st R[k] holds R[k+1]
proof
let k such that
A33: R[k];
given G being Subset-Family of M such that
A34: G c= F and
A35: [. f.(k+1) - r/2|^(k+1+1), f.(k+1) + r/2|^(k+1+1) .] c= union G and
A36: G is finite;
A37: r/2|^(k+(1+1)) = r/2|^(k+1+1) .= r/((2|^(k+1))*2) by NEWTON:6
.= r/(2|^(k+1))/2 by XCMPLX_1:78;
now
per cases;
suppose
A38: ex G being Subset-Family of M st G c= F & [. f.k - r/2|^(
k+1), f.k .] c= union G & G is finite;
2|^(k+1) > 0 & r >= 0 by A1,NEWTON:83,XREAL_1:48;
then f.k - r/2|^(k+1) <= f.k & f.k <= f.k + r/2|^(k+1) by
XREAL_1:31,43;
then
A39: [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] = [. f.k - r/2|^(k+1)
, f.k .] \/ [. f.k, f.k + r/2|^(k+1).] by XXREAL_1:165;
A40: f.(k+1) - r/2|^(k+1+1) = f.k + r/2|^(k+2) - r/2|^(k+(1+1))
by A11,A38
.= f.k;
consider G1 being Subset-Family of M such that
A41: G1 c= F and
A42: [. f.k - r/2|^(k+1), f.k .] c= union G1 and
A43: G1 is finite by A38;
reconsider G3 = G1 \/ G as Subset-Family of M;
f.(k+1) + r/2|^(k+1+1) = f.k + r/2|^(k+2) + r/2|^(k+(1+1))
by A11,A38
.= f.k + r/(2|^(k+1))/2 + r/(2|^(k+1))/2 by A37
.= f.k + r/2|^(k+1);
then [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] c= union G1 \/ union
G by A35,A42,A40,A39,XBOOLE_1:13;
then [. f.k - r/2|^(k+1), f.k + r/2|^(k+1).] c= union G3 by
ZFMISC_1:78;
hence contradiction by A33,A34,A36,A41,A43,XBOOLE_1:8;
end;
suppose
A44: not (ex G being Subset-Family of M st G c= F & [. f.k - r
/2|^(k+1), f.k .] c= union G & G is finite);
then
A45: f.(k+1) + r/2|^(k+1+1) = f.k - r/2|^(k+2) + r/2|^(k+(1+1))
by A11
.= f.k;
f.(k+1) - r/2|^(k+1+1) = f.k - r/2|^(k+2) - r/2|^( k+(1+1))
by A11,A44
.= f.k - r/(2|^(k+1))/2 - r/(2|^(k+1))/2 by A37
.= f.k - r/2|^(k+1);
hence contradiction by A34,A35,A36,A44,A45;
end;
end;
hence thesis;
end;
A46: the carrier of M = [. a,b .] by A1,TOPMETR:10;
A47: R[0]
proof
given G being Subset-Family of M such that
A48: G c= F and
A49: [. f.0 - r/2|^(0+1), f.0 + r/2|^(0+1) .] c= union G and
A50: G is finite;
the carrier of M c= union G by A1,A24,A12,A49,TOPMETR:10;
then G is Cover of M by SETFAM_1:def 11;
hence contradiction by A6,A48,A50;
end;
reconsider f as Real_Sequence;
[. a,b .] is compact by RCOMP_1:6;
then consider s being Real_Sequence such that
A51: s is subsequence of f and
A52: s is convergent and
A53: lim s in [. a,b .] by A27,RCOMP_1:def 3;
reconsider ls = lim s as Point of M by A1,A53,TOPMETR:10;
consider Nseq being increasing sequence of NAT such that
A54: s = f*Nseq by A51,VALUED_0:def 17;
the carrier of M c= union F by A5,SETFAM_1:def 11;
then consider Z being set such that
A55: lim s in Z and
A56: Z in F by A53,A46,TARSKI:def 4;
consider p being Point of M, r0 being Real such that
A57: Z = Ball(p,r0) by A4,A56,TOPMETR:def 4;
set G = {Ball(p,r0)};
G c= bool the carrier of M
proof
let a be object;
assume a in G;
then a = Ball(p,r0) by TARSKI:def 1;
hence thesis;
end;
then reconsider G as Subset-Family of M;
A58: G c= F by A56,A57,ZFMISC_1:31;
reconsider Ns = Nseq as Real_Sequence by RELSET_1:7, NUMBERS:19;
not Ns is bounded_above
proof
let r be Real;
consider n being Nat such that
A59: n > r by SEQ_4:3;
rng Nseq c= NAT by VALUED_0:def 6;
then n <= Ns.n by Th2;
hence thesis by A59,XXREAL_0:2;
end;
then
A60: 2 to_power Ns is divergent_to+infty by Th3,LIMFUNC1:31;
then
A61: (2 to_power Ns)" is convergent by LIMFUNC1:34;
consider r1 being Real such that
A62: r1 > 0 and
A63: Ball(ls,r1) c= Ball(p,r0) by A55,A57,PCOMPS_1:27;
A64: r1/2 > 0 by A62,XREAL_1:139;
then consider n being Nat such that
A65: for m being Nat st m >= n holds |.s.m - lim s.| <
r1/2 by A52,SEQ_2:def 7;
A66: for m being Element of NAT for q being Point of M st s.m = q & m >=
n holds dist(ls, q) < r1/2
proof
let m be Element of NAT, q be Point of M;
assume that
A67: s.m = q and
A68: m >= n;
|.s.m - lim s.| < r1/2 by A65,A68;
then
A69: |.-(s.m - lim s).| < r1/2 by COMPLEX1:52;
dist(ls, q) = (the distance of M).(lim s, s.m) by A67,METRIC_1:def 1
.= (the distance of RealSpace).(ls, q) by A67,TOPMETR:def 1
.= |.lim s - s.m.| by A67,METRIC_1:def 12,def 13;
hence thesis by A69;
end;
A70: for m being Element of NAT st m >= n holds (f*Nseq).m in Ball(ls, r1/2)
proof
let m be Element of NAT such that
A71: m >= n;
dom f = NAT & s.m = f.(Nseq.m) by A54,FUNCT_2:15,def 1;
then s.m in rng f by FUNCT_1:def 3;
then reconsider q = s.m as Point of M by A1,A27,TOPMETR:10;
dist(ls, q) < r1/2 by A66,A71;
hence thesis by A54,METRIC_1:11;
end;
lim (2 to_power Ns)" = 0 by A60,LIMFUNC1:34;
then
A72: lim (r(#)((2 to_power Ns)")) = r*0 by A61,SEQ_2:8
.= 0;
r(#)((2 to_power Ns)") is convergent by A61,SEQ_2:7;
then consider i such that
A73: for m st i <= m holds |.(r(#)((2 to_power Ns)")).m - 0.| <
r1/2 by A64,A72,SEQ_2:def 7;
reconsider l = i + 1 + n as Element of NAT by ORDINAL1:def 12;
A74: l = n + 1 + i;
[. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .] c= Ball( ls,r1)
proof
|.(r(#)(2 to_power Ns)").l - 0.| < r1/2 by A73,A74,NAT_1:11;
then |.r*((2 to_power Ns)").l.| < r1/2 by SEQ_1:9;
then |.r*((2 to_power Ns).l)".| < r1/2 by VALUED_1:10;
then |.r*(2 to_power (Ns.l))".| < r1/2 by Def1;
then
A75: |.r*(2|^(Nseq.l))".| < r1/2 by POWER:41;
2|^(Nseq.l+1) = 2*2|^Nseq.l & 2|^Nseq.l > 0 by NEWTON:6,83;
then 1/(2|^(Nseq.l+1)) < (2|^Nseq.l)" by XREAL_1:88,155;
then
A76: r*(2|^(Nseq.l+1))" < r*(2|^Nseq.l)" by A2,XREAL_1:68;
2|^(Nseq.l+1) > 0 & r >= 0 by A1,NEWTON:83,XREAL_1:48;
then |.r*(2|^(Nseq.l+1))".| = r*(2|^(Nseq.l+1))" by ABSVALUE:def 1;
then |.r*(2|^(Nseq.l+1))".| < |.r*(2|^Nseq.l)".| by A76,
ABSVALUE:5;
then
A77: |.r*(2|^(Nseq.l+1))".| < r1/2 by A75,XXREAL_0:2;
2|^(Nseq.l+1) > 0 & r >= 0 by A1,NEWTON:83,XREAL_1:48;
then
A78: r*(2|^(Nseq.l+1))" < r1/2 by A77,ABSVALUE:def 1;
A79: s.l in Ball(ls, r1/2) by A54,A70,NAT_1:11;
then reconsider sl = s.l as Point of M;
dist(ls,sl) < r1/2 by A79,METRIC_1:11;
then
A80: |.lim s - s.l.| < r1/2 by Th1;
let z be object;
A81: the carrier of M = [. a,b .] by A1,TOPMETR:10;
assume z in [. s.l - r*(2|^(Nseq.l+1))", s.l + r*(2|^(Nseq.l+1))" .];
then z in {m where m is Real:
s.l - r*(2|^(Nseq.l+1))" <= m & m <= s.
l + r*(2|^(Nseq.l+1))" } by RCOMP_1:def 1;
then consider x be Real such that
A82: x = z and
A83: s.l - r*(2|^(Nseq.l+1))" <= x and
A84: x <= s.l + r*(2|^(Nseq.l+1))";
f.(Nseq.l) - r/(2|^(Nseq.l+1)) >= a by A26;
then s.l - r*(2|^(Nseq.l+1))" >= a by A54,FUNCT_2:15;
then
A85: x >= a by A83,XXREAL_0:2;
f.(Nseq.l) + r/(2|^(Nseq.l+1)) <= b by A26;
then s.l + r*(2|^(Nseq.l+1))" <= b by A54,FUNCT_2:15;
then x <= b by A84,XXREAL_0:2;
then x in {m where m is Real: a <= m & m <= b} by A85;
then reconsider x9 = x as Point of M by A81,RCOMP_1:def 1;
|.lim s - x.| = |.(lim s - s.l) + (s.l - x).|;
then
A86: |.lim s - x.| <= |.lim s - s.l.| + |.s.l - x.| by COMPLEX1:56;
x - s.l <= r*(2|^(Nseq.l+1))" by A84,XREAL_1:20;
then
A87: -(x - s.l)>=-r*(2|^(Nseq.l+1))" by XREAL_1:24;
s.l <= r*(2|^(Nseq.l+1))" + x by A83,XREAL_1:20;
then s.l - x <= r*(2|^(Nseq.l+1))" by XREAL_1:20;
then |.s.l - x.| <= r*(2|^(Nseq.l+1))" by A87,ABSVALUE:5;
then |.s.l - x.| < r1/2 by A78,XXREAL_0:2;
then |.lim s - s.l.| + |.s.l - x.| < r1/2 + r1/2 by A80,XREAL_1:8;
then |.lim s - x.| < r1/2 + r1/2 by A86,XXREAL_0:2;
then dist(ls,x9) < r1 by Th1;
hence thesis by A82,METRIC_1:11;
end;
then [. s.l - r/2|^(Nseq.l+1), s.l + r*(2|^(Nseq.l+1))" .] c= Ball(p,r0
) by A63;
then [. f.(Nseq.l) - r/(2|^(Nseq.l+1)), s.l + r/2|^(Nseq.l+1) .] c=
Ball(p,r0) by A54,FUNCT_2:15;
then
A88: [. f.(Nseq.l) - r/2|^(Nseq.l+1), f.(Nseq.l) + r/2|^(Nseq.l+1) .]
c= union {Ball(p,r0)} by A54,FUNCT_2:15;
for k holds R[k] from NAT_1:sch 2(A47,A32);
hence contradiction by A58,A88;
end;
end;
hence thesis;
end;