:: Heine--Borel's Covering Theorem
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Received November 21, 1991
:: Copyright (c) 1991-2011 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 :: HEINE:2

canceled;

theorem :: HEINE:3

canceled;

theorem :: HEINE:4

canceled;

theorem :: HEINE:5

canceled;

theorem Th6: :: HEINE:6

for n being Element of NAT
for seq being Real_Sequence st seq is increasing & 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 b₁ being Real_Sequence st
for n being Element of NAT holds b₁ . n = k to_power (seq . n)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Element of NAT holds b₁ . n = k to_power (seq . n) ) & ( for n being Element of NAT holds b₂ . n = k to_power (seq . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines to_power HEINE:def 1 :
for seq being Real_Sequence
for k being Element of NAT
for b₃ being Real_Sequence holds
( b₃ = k to_power seq iff for n being Element of NAT holds b₃ . n = k to_power (seq . n) );

theorem :: HEINE:7

canceled;

theorem :: HEINE:8

canceled;

theorem Th9: :: HEINE:9

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

proof end;

theorem :: HEINE:10

canceled;

theorem :: HEINE:11

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

proof end;