Loading [MathJax]/extensions/tex2jax.js
begin
begin
begin
Lm1:
0 in REAL
by XREAL_0:def 1;
Lm2:
for n being Nat holds [#] (TOP-REAL n) = [#] (Euclid n)
begin
Lm3:
for x being set holds {x} is c=-linear
Lm4:
for n being Nat holds [#] (TOP-REAL n) = [#] (TopSpaceMetr (Euclid n))
Lm5:
for A being Subset of (TOP-REAL 1) st A is closed & A is bounded holds
A is compact
Lm6:
for n being Nat
for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds
A is compact
begin