:: HEINE semantic presentation

theorem Th1: :: HEINE:1

for b₁, b₂ being real number
for b₃ being SubSpace of RealSpace
for b₄, b₅ being Point of b₃ st b₁ = b₄ & b₂ = b₅ holds
dist b₄,b₅ = abs (b₁ - b₂)

proof end;

theorem Th2: :: HEINE:2

for b₁, b₂, b₃ being real number st b₁ <= b₂ & b₂ <= b₃ holds
[.b₁,b₂.] \/ [.b₂,b₃.] = [.b₁,b₃.]

proof end;

Lemma3: for b₁, b₂, b₃ being real number st b₁ >= 0 & b₂ + b₁ <= b₃ holds
b₂ <= b₃
by XREAL_1:42;

Lemma4: for b₁, b₂, b₃ being real number st b₁ >= 0 & b₂ - b₁ >= b₃ holds
b₂ >= b₃
by XREAL_1:53;

theorem Th3: :: HEINE:3

canceled;

theorem Th4: :: HEINE:4

canceled;

theorem Th5: :: HEINE:5

for b₁ being real number
for b₂ being Nat st b₁ > 0 holds
b₁ |^ b₂ > 0

proof end;

theorem Th6: :: HEINE:6

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is increasing & rng b₂ c= NAT holds
b₁ <= b₂ . b₁

proof end;

definition

let c₁ be Real_Sequence;
let c₂ be Nat;
func c₂ to_power c₁ -> Real_Sequence means :Def1: :: HEINE:def 1
for b₁ being Nat holds a₃ . b₁ = a₂ to_power (a₁ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines to_power HEINE:def 1 :

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

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

Lemma9: for b₁ being Nat st S₁[b₁] holds
S₁[b₁ + 1]

proof end;

theorem Th7: :: HEINE:7

for b₁ being Nat holds 2 |^ b₁ >= b₁ + 1

proof end;

theorem Th8: :: HEINE:8

for b₁ being Nat holds 2 |^ b₁ > b₁

proof end;

theorem Th9: :: HEINE:9

for b₁ being Real_Sequence st b₁ is divergent_to+infty holds
2 to_power b₁ is divergent_to+infty

proof end;

theorem Th10: :: HEINE:10

for b₁ being TopSpace st the carrier of b₁ is finite holds
b₁ is compact

proof end;

theorem Th11: :: HEINE:11

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

proof end;