let n be Nat; for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds
A is compact
defpred S1[ Nat] means for A being Subset of (TOP-REAL $1) st A is closed & A is bounded holds
A is compact ;
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
per cases
( n = 0 or n <> 0 )
;
suppose A3:
n <> 0
;
S1[n + 1]set n1 =
n + 1;
set TR1 =
TOP-REAL 1;
set TRn =
TOP-REAL n;
set TRn1 =
TOP-REAL (n + 1);
let A be
Subset of
(TOP-REAL (n + 1));
( A is closed & A is bounded implies A is compact )assume that A4:
A is
closed
and A5:
A is
bounded
;
A is compact consider p being
Point of
(Euclid (n + 1)),
r being
Real such that A6:
A c= OpenHypercube (
p,
r)
by A5, Th21;
n in NAT
by ORDINAL1:def 12;
then consider f being
Function of
[:(TOP-REAL n),(TOP-REAL 1):],
(TOP-REAL (n + 1)) such that A7:
f is
being_homeomorphism
and A8:
for
fi being
Element of
(TOP-REAL n) for
fj being
Element of
(TOP-REAL 1) holds
f . (
fi,
fj)
= fi ^ fj
by Th19;
A9:
(
f is
one-to-one &
dom f = [#] [:(TOP-REAL n),(TOP-REAL 1):] )
by A7, TOPGRP_1:24;
len p = n + 1
by CARD_1:def 7;
then consider q1,
q2 being
FinSequence such that A10:
len q1 = n
and A11:
len q2 = 1
and A12:
p = q1 ^ q2
by FINSEQ_2:22;
rng p c= REAL
;
then A13:
p is
FinSequence of
REAL
by FINSEQ_1:def 4;
then A14:
q1 is
FinSequence of
REAL
by A12, FINSEQ_1:36;
A15:
q2 is
FinSequence of
REAL
by A12, A13, FINSEQ_1:36;
reconsider q1 =
q1 as
Element of
(Euclid n) by A10, A14, TOPREAL3:45;
reconsider q2 =
q2 as
Element of
(Euclid 1) by A11, A15, TOPREAL3:45;
A16:
f is
continuous
by A7, TOPS_2:def 5;
reconsider Bn =
cl_Ball (
q1,
(r * (sqrt n))) as
Subset of
(TOP-REAL n) by TOPREAL3:8;
reconsider B1 =
cl_Ball (
q2,
(r * (sqrt 1))) as
Subset of
(TOP-REAL 1) by TOPREAL3:8;
(
Ball (
q2,
(r * (sqrt 1)))
c= B1 &
OpenHypercube (
q2,
r)
c= Ball (
q2,
(r * (sqrt 1))) )
by EUCLID_9:18, METRIC_1:14;
then A17:
OpenHypercube (
q2,
r)
c= B1
;
(
Ball (
q1,
(r * (sqrt n)))
c= Bn &
OpenHypercube (
q1,
r)
c= Ball (
q1,
(r * (sqrt n))) )
by A3, EUCLID_9:18, METRIC_1:14;
then
OpenHypercube (
q1,
r)
c= Bn
;
then A18:
[:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] c= [:Bn,B1:]
by A17, ZFMISC_1:96;
cl_Ball (
q2,
(r * (sqrt 1))) is
bounded
by TOPREAL6:59;
then
B1 is
bounded
by JORDAN2C:11;
then A19:
B1 is
compact
by Lm4, TOPREAL6:58;
cl_Ball (
q1,
(r * (sqrt n))) is
bounded
by TOPREAL6:59;
then
Bn is
bounded
by JORDAN2C:11;
then
Bn is
compact
by A2, TOPREAL6:58;
then A20:
[:Bn,B1:] is
compact Subset of
[:(TOP-REAL n),(TOP-REAL 1):]
by A19, BORSUK_3:23;
rng f = [#] (TOP-REAL (n + 1))
by A7, TOPGRP_1:24;
then A21:
f .: (f " A) = A
by FUNCT_1:77;
f .: [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] = OpenHypercube (
p,
r)
by A8, A10, A12, Th20;
then A22:
f " A c= [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):]
by A6, A9, A21, FUNCT_1:87;
f " A is
closed
by A4, A7, TOPGRP_1:24;
then
f " A is
compact
by A18, A20, A22, COMPTS_1:9, XBOOLE_1:1;
hence
A is
compact
by A16, A21, WEIERSTR:8;
verum end;
end;
A23:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A23, A1);
hence
for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds
A is compact
; verum