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


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
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = k to_power (seq . n)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = k to_power (seq . n) ) & ( for n being 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 Nat
for b3 being Real_Sequence holds
( b3 = k to_power seq iff for n being 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 st a <= b holds
Closed-Interval-TSpace (a,b) is compact
proof end;