let P be Subset of R^1 ; :: thesis: ( P is compact implies [#] P is closed )
assume A1:
P is compact
; :: thesis: [#] P is closed
now per cases
( [#] P <> {} or [#] P = {} )
;
case A2:
[#] P <> {}
;
:: thesis: [#] P is closed A3:
R^1 is
T_2
by PCOMPS_1:38, TOPMETR:def 7;
for
s1 being
Real_Sequence st
rng s1 c= [#] P &
s1 is
convergent holds
lim s1 in [#] P
proof
let s1 be
Real_Sequence;
:: thesis: ( rng s1 c= [#] P & s1 is convergent implies lim s1 in [#] P )
assume A4:
(
rng s1 c= [#] P &
s1 is
convergent )
;
:: thesis: lim s1 in [#] P
set x =
lim s1;
reconsider x =
lim s1 as
Point of
R^1 by TOPMETR:24;
thus
lim s1 in [#] P
:: thesis: verumproof
assume
not
lim s1 in [#] P
;
:: thesis: contradiction
then
x in P `
by SUBSET_1:50;
then consider Otx,
OtP being
Subset of
R^1 such that A5:
(
Otx is
open &
OtP is
open &
x in Otx &
P c= OtP &
Otx misses OtP )
by A1, A2, A3, COMPTS_1:15;
A6:
rng s1 misses Otx
by A4, A5, XBOOLE_1:1, XBOOLE_1:63;
A7:
R^1 = TopStruct(# the
carrier of
RealSpace ,
(Family_open_set RealSpace ) #)
by PCOMPS_1:def 6, TOPMETR:def 7;
then reconsider x =
x as
Point of
RealSpace ;
consider r being
real number such that A8:
(
r > 0 &
Ball x,
r c= Otx )
by A5, TOPMETR:22, TOPMETR:def 7;
reconsider r =
r as
Real by XREAL_0:def 1;
A9:
Ball x,
r misses rng s1
by A6, A8, XBOOLE_1:63;
A10:
Ball x,
r = { q where q is Element of RealSpace : dist x,q < r }
by METRIC_1:18;
for
n being
Element of
NAT ex
m being
Element of
NAT st
(
n <= m & not
abs ((s1 . m) - (lim s1)) < r )
proof
given n being
Element of
NAT such that A11:
for
m being
Element of
NAT st
n <= m holds
abs ((s1 . m) - (lim s1)) < r
;
:: thesis: contradiction
set m =
n + 1;
abs ((s1 . (n + 1)) - (lim s1)) < r
by A11, NAT_1:11;
then
real_dist . (s1 . (n + 1)),
(lim s1) < r
by METRIC_1:def 13;
then A12:
real_dist . (lim s1),
(s1 . (n + 1)) < r
by METRIC_1:10;
reconsider y =
s1 . (n + 1) as
Element of
RealSpace by A7, TOPMETR:24;
dist x,
y = the
distance of
RealSpace . x,
y
by METRIC_1:def 1;
then A13:
y in Ball x,
r
by A10, A12, METRIC_1:def 14;
s1 . (n + 1) in rng s1
by FUNCT_2:6;
then
y in (Ball x,r) /\ (rng s1)
by A13, XBOOLE_0:def 4;
hence
contradiction
by A9, XBOOLE_0:def 7;
:: thesis: verum
end;
hence
contradiction
by A4, A8, SEQ_2:def 7;
:: thesis: verum
end;
end; hence
[#] P is
closed
by RCOMP_1:def 4;
:: thesis: verum end;
hence
[#] P is closed
; :: thesis: verum