HEINE: Heine--Borel's Covering Theorem

:: Heine--Borel's Covering Theorem
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, FUNCT_2, SEQ_2, 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;
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, XCMPLX_0, NEWTON, POWER;
constructors HIDDEN, 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;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XCMPLX_0;
expansions TARSKI, LIMFUNC1;

theorem Th1: :: HEINE:1

for x, y being Real
for A being SubSpace of RealSpace
for p, q being Point of A st x = p & y = q holds
dist (p,q) = |.(x - y).|

proof end;

theorem Th2: :: HEINE:2

for n being Nat
for seq being Real_Sequence st seq is V46() & rng seq c= NAT holds
n <= seq . n

proof end;

definition

let seq be Real_Sequence;
let k be Nat;

func k to_power seq -> Real_Sequence means :Def1: :: HEINE:def 1
for n being Nat holds it . n = k to_power (seq . n);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines to_power HEINE:def 1 :

theorem Th3: :: HEINE:3

for seq being Real_Sequence st seq is divergent_to+infty holds
2 to_power seq is divergent_to+infty

proof end;

Heine-Borel Theorem for intervals

theorem :: HEINE:4

for a, b being Real st a <= b holds
Closed-Interval-TSpace (a,b) is compact

proof end;