:: 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)
proof end;

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
proof end;

definition
let seq be Real_Sequence;
let k be Element of NAT ;
func k 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)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = k to_power (seq . n) ) & ( for n being Element of NAT holds b2 . n = k to_power (seq . n) ) holds
b1 = b2
proof end;
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
proof end;

:: 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
proof end;