let A be Subset of REAL? ; :: according to FRECHET:def 5 :: thesis: for x being Point of REAL? st x in Cl A holds
ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
let x be Point of REAL? ; :: thesis: ( x in Cl A implies ex S being sequence of REAL? st
( rng S c= A & x in Lim S ) )
assume A1:
x in Cl A
; :: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )
x in the carrier of REAL?
;
then
x in (REAL \ NAT ) \/ {REAL }
by Def7;
then A2:
( x in REAL \ NAT or x in {REAL } )
by XBOOLE_0:def 3;
per cases
( x in REAL \ NAT or ( x = REAL & x in A ) or ( x = REAL & not x in A ) )
by A2, TARSKI:def 1;
suppose A28:
(
x = REAL & not
x in A )
;
:: thesis: ex S being sequence of REAL? st
( rng S c= A & x in Lim S )then reconsider A' =
A as
Subset of
R^1 by Th32;
ex
k being
Point of
R^1 st
(
k in NAT & ex
S' being
sequence of
R^1 st
(
rng S' c= A' &
S' is_convergent_to k ) )
proof
assume A29:
for
k being
Point of
R^1 holds
( not
k in NAT or for
S' being
sequence of
R^1 holds
( not
rng S' c= A' or not
S' is_convergent_to k ) )
;
:: thesis: contradiction
defpred S1[
set ,
set ]
means ( $1
in $2 & $2
in the
topology of
R^1 & $2
/\ A' = {} );
A30:
for
k being
set st
k in NAT holds
ex
U1 being
set st
S1[
k,
U1]
proof
given k being
set such that A31:
k in NAT
and A32:
for
U1 being
set st
k in U1 &
U1 in the
topology of
R^1 holds
not
U1 /\ A' = {}
;
:: thesis: contradiction
reconsider k =
k as
Point of
R^1 by A31, TOPMETR:24;
reconsider k'' =
k as
Point of
(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
reconsider k' =
k'' as
Point of
RealSpace by TOPMETR:16;
consider Bs being
Basis of
k'' such that A33:
Bs = { (Ball k',(1 / n)) where n is Element of NAT : n <> 0 }
and
Bs is
countable
and A34:
ex
f being
Function of
NAT ,
Bs st
for
n being
set st
n in NAT holds
ex
n' being
Element of
NAT st
(
n = n' &
f . n = Ball k',
(1 / (n' + 1)) )
by Th11;
consider h being
Function of
NAT ,
Bs such that A35:
for
n being
set st
n in NAT holds
ex
n' being
Element of
NAT st
(
n = n' &
h . n = Ball k',
(1 / (n' + 1)) )
by A34;
defpred S2[
set ,
set ]
means $2
in (h . $1) /\ A';
A36:
for
n being
set st
n in NAT holds
ex
z being
set st
(
z in the
carrier of
R^1 &
S2[
n,
z] )
proof
let n be
set ;
:: thesis: ( n in NAT implies ex z being set st
( z in the carrier of R^1 & S2[n,z] ) )
assume
n in NAT
;
:: thesis: ex z being set st
( z in the carrier of R^1 & S2[n,z] )
then consider n' being
Element of
NAT such that
n = n'
and A37:
h . n = Ball k',
(1 / (n' + 1))
by A35;
A38:
h . n in Bs
by A33, A37;
A39:
Bs c= the
topology of
(TopSpaceMetr RealSpace )
by YELLOW_8:def 2;
reconsider H =
h . n as
Subset of
(TopSpaceMetr RealSpace ) by A38;
reconsider H =
H as
Subset of
(TopSpaceMetr RealSpace ) ;
k in H
by A38, YELLOW_8:21;
then A40:
H /\ A' <> {}
by A32, A38, A39, TOPMETR:def 7;
consider z being
Element of
H /\ A';
A41:
z in H
by A40, XBOOLE_0:def 4;
take
z
;
:: thesis: ( z in the carrier of R^1 & S2[n,z] )
thus
(
z in the
carrier of
R^1 &
S2[
n,
z] )
by A40, A41, TOPMETR:def 7;
:: thesis: verum
end;
consider S' being
Function such that A42:
(
dom S' = NAT &
rng S' c= the
carrier of
R^1 )
and A43:
for
n being
set st
n in NAT holds
S2[
n,
S' . n]
from WELLORD2:sch 1(A36);
reconsider S' =
S' as
Function of
NAT ,the
carrier of
R^1 by A42, FUNCT_2:4;
A44:
rng S' c= A'
S' is_convergent_to k
proof
let U1 be
Subset of
R^1 ;
:: according to FRECHET:def 2 :: thesis: ( U1 is open & k in U1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S' . m in U1 )
assume A47:
(
U1 is
open &
k in U1 )
;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
S' . m in U1
reconsider U2 =
U1 as
Subset of
(TopSpaceMetr RealSpace ) by TOPMETR:def 7;
consider r being
real number such that A48:
r > 0
and A49:
Ball k',
r c= U2
by A47, TOPMETR:22, TOPMETR:def 7;
reconsider r =
r as
Real by XREAL_0:def 1;
consider n being
Element of
NAT such that A50:
1
/ n < r
and A51:
n > 0
by A48, Lm2;
take
n
;
:: thesis: for m being Element of NAT st n <= m holds
S' . m in U1
thus
for
m being
Element of
NAT st
n <= m holds
S' . m in U1
:: thesis: verumproof
let m be
Element of
NAT ;
:: thesis: ( n <= m implies S' . m in U1 )
assume
n <= m
;
:: thesis: S' . m in U1
then
n < m + 1
by NAT_1:13;
then
1
/ (m + 1) < 1
/ n
by A51, XREAL_1:90;
then
Ball k',
(1 / (m + 1)) c= Ball k',
r
by A50, PCOMPS_1:1, XXREAL_0:2;
then A52:
Ball k',
(1 / (m + 1)) c= U2
by A49, XBOOLE_1:1;
consider m' being
Element of
NAT such that A53:
m = m'
and A54:
h . m = Ball k',
(1 / (m' + 1))
by A35;
S' . m in (h . m) /\ A'
by A43;
then
S' . m in h . m
by XBOOLE_0:def 4;
hence
S' . m in U1
by A52, A53, A54;
:: thesis: verum
end;
end;
hence
contradiction
by A29, A31, A44;
:: thesis: verum
end;
consider g being
Function such that A55:
dom g = NAT
and A56:
for
k being
set st
k in NAT holds
S1[
k,
g . k]
from CLASSES1:sch 1(A30);
rng g c= bool the
carrier of
R^1
then reconsider F =
rng g as
Subset-Family of
R^1 ;
F is
open
then A61:
union F is
open
by TOPS_2:26;
A62:
NAT c= union F
(union F) \ NAT c= REAL \ NAT
by TOPMETR:24, XBOOLE_1:33;
then
((union F) \ NAT ) \/ {REAL } c= (REAL \ NAT ) \/ {REAL }
by XBOOLE_1:9;
then reconsider B =
((union F) \ NAT ) \/ {REAL } as
Subset of
REAL? by Def7;
reconsider B =
B as
Subset of
REAL? ;
(
B is
open &
REAL in B )
by A61, A62, Th31;
then A65:
A meets B
by A1, A28, PRE_TOPC:def 13;
B /\ A = {}
hence
contradiction
by A65, XBOOLE_0:def 7;
:: thesis: verum
end; then consider k being
Point of
R^1 such that A72:
k in NAT
and A73:
ex
S' being
sequence of
R^1 st
(
rng S' c= A' &
S' is_convergent_to k )
;
consider S' being
sequence of
R^1 such that A74:
rng S' c= A'
and A75:
S' is_convergent_to k
by A73;
reconsider S =
S' as
sequence of
REAL? by A74, Th2, XBOOLE_1:1;
take
S
;
:: thesis: ( rng S c= A & x in Lim S )thus
rng S c= A
by A74;
:: thesis: x in Lim S
S is_convergent_to x
hence
x in Lim S
by Def4;
:: thesis: verum end;