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


begin

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

theorem Th2: :: HEINE:2
for n being Element of NAT
for seq being Real_Sequence st seq is V40() & rng seq c= NAT holds
n <= seq . n
proofend;

definition
let seq be Real_Sequence;
let k be Element of NAT ;
funck to_power seq ->  Real_Sequence means :Def1: :: HEINE:def 1
 for n being Element of NAT holds it . n = k to_power (seq . n);
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = k to_power (seq . n)
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = k to_power (seq . n) ) &amp; ( for n being Element of NAT holds b2 . n = k to_power (seq . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines to_power HEINE:def_1_:_
 for seq being Real_Sequence
for k being Element of NAT
for b3 being Real_Sequence holds
( b3 = k to_power seq iff for n being Element of NAT holds b3 . n = k to_power (seq . n) );

theorem Th3: :: HEINE:3
for seq being Real_Sequence st seq is divergent_to+infty holds
2 to_power seq is divergent_to+infty
proofend;

:: [WP: ] Heine-Borel_Theorem_for_intervals
theorem :: HEINE:4
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is compact
proofend;