The abstract of the Mizar article:

Heine--Borel's Covering Theorem

by

Agata Darmochwal, and

Yatsuka Nakamura

Received November 21, 1991

MML identifier: HEINE

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, PRE_TOPC, METRIC_1, ABSVALUE, ARYTM_1, FUNCT_1, RCOMP_1,
      BOOLE, GROUP_1, SEQ_1, ORDINAL2, RELAT_1, POWER, LIMFUNC1, FINSET_1,
      COMPTS_1, SETFAM_1, TOPMETR, PCOMPS_1, ARYTM_3, TARSKI, SEQM_3, SEQ_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      ORDINAL2, REAL_1, NAT_1, RELAT_1, FUNCT_2, METRIC_1, FINSET_1, BINOP_1,
      STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, PCOMPS_1, ABSVALUE, SEQ_1, SEQ_2,
      SEQM_3, LIMFUNC1, POWER, RCOMP_1, NEWTON, TOPMETR;
 constructors REAL_1, NAT_1, TOPS_2, COMPTS_1, ABSVALUE, SEQ_2, SEQM_3,
      LIMFUNC1, POWER, RCOMP_1, NEWTON, TOPMETR, PARTFUN1, SEQ_4, MEMBERED,
      XBOOLE_0;
 clusters PRE_TOPC, FINSET_1, XREAL_0, METRIC_1, RELSET_1, SEQ_1, SEQM_3,
      ARYTM_3, NEWTON, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve a,b,x,y,z for real number, i,k,n,m for Nat;
reserve p,q,w for Real;

theorem :: HEINE:1
for A being SubSpace of RealSpace, p,q being Point of A
 st x = p & y = q holds dist(p,q) = abs( x - y );

theorem :: HEINE:2
x <= y & y <= z implies [. x,y .] \/ [. y,z .] = [. x,z .];

theorem :: HEINE:3
x >= 0 & a + x <= b implies a <= b;

theorem :: HEINE:4
x >= 0 & a - x >= b implies a >= b;

theorem :: HEINE:5
x > 0 implies x|^k > 0;

reserve seq for Real_Sequence;

theorem :: HEINE:6
 seq is increasing & rng seq c= NAT implies n <= seq.n;

definition let seq,k;
 func k to_power seq -> Real_Sequence means
:: HEINE:def 1
   for n holds it.n = k to_power (seq.n);
end;

theorem :: HEINE:7
  2|^n >= n + 1;

theorem :: HEINE:8
  2|^n > n;

theorem :: HEINE:9
 seq is divergent_to+infty implies 2 to_power seq is divergent_to+infty;

theorem :: HEINE:10
 for T being TopSpace st the carrier of T is finite holds T is compact;

:: HEINE - BOREL THEOREM

theorem :: HEINE:11
   a <= b implies Closed-Interval-TSpace(a,b) is compact;