:: 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 b₁ being Real_Sequence st
for n being Nat holds b₁ . n = k to_power (seq . n)

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = k to_power (seq . n) ) & ( for n being 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 Nat
for b₃ being Real_Sequence holds
( b₃ = k to_power seq iff for n being Nat holds b₃ . 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;

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