:: HEINE semantic presentation

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 x, y, z being real number st x <= y & y <= z holds
[.x,y.] \/ [.y,z.] = [.x,z.]

proof end;

Lm1: for x, a, b being real number st x >= 0 & a + x <= b holds
a <= b
by XREAL_1:42;

Lm2: for x, a, b being real number st x >= 0 & a - x >= b holds
a >= b
by XREAL_1:53;

theorem :: HEINE:3

canceled;

theorem :: HEINE:4

canceled;

theorem Th5: :: HEINE:5

for x being real number
for k being Nat st x > 0 holds
x |^ k > 0

proof end;

theorem Th6: :: HEINE:6

for n being 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines to_power HEINE:def 1 :

defpred S₁[ Nat] means 2 |^ $1 >= $1 + 1;

Lm3: S₁[0]
by NEWTON:9;

Lm4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof end;

theorem Th7: :: HEINE:7

for n being Nat holds 2 |^ n >= n + 1

proof end;

theorem Th8: :: HEINE:8

for n being Nat holds 2 |^ n > n

proof end;

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 Th10: :: HEINE:10

for T being TopSpace st the carrier of T is finite holds
T is compact

proof end;

theorem :: HEINE:11

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

proof end;