let T be non empty TopSpace; :: thesis: ( T is first-countable implies T is Frechet )
assume A1:
T is first-countable
; :: thesis: T is Frechet
let A be Subset of T; :: according to FRECHET:def 5 :: thesis: for x being Point of T st x in Cl A holds
ex S being sequence of T st
( rng S c= A & x in Lim S )
let x be Point of T; :: thesis: ( x in Cl A implies ex S being sequence of T st
( rng S c= A & x in Lim S ) )
assume A2:
x in Cl A
; :: thesis: ex S being sequence of T st
( rng S c= A & x in Lim S )
consider B being Basis of x such that
A3:
B is countable
by A1, Def1;
consider f being Function of NAT ,B such that
A4:
rng f = B
by A3, CARD_3:146;
defpred S1[ set , set ] means $2 in A /\ (meet (f .: (succ $1)));
A5:
for n being set st n in NAT holds
ex y being set st
( y in the carrier of T & S1[n,y] )
proof
let n be
set ;
:: thesis: ( n in NAT implies ex y being set st
( y in the carrier of T & S1[n,y] ) )
assume
n in NAT
;
:: thesis: ex y being set st
( y in the carrier of T & S1[n,y] )
then reconsider n =
n as
Element of
NAT ;
defpred S2[
Element of
NAT ]
means ex
H being
Subset of
T st
(
H = meet (f .: (succ $1)) &
H is
open );
for
n being
Element of
NAT holds
S2[
n]
proof
A6:
S2[
0 ]
A8:
for
n being
Element of
NAT st
S2[
n] holds
S2[
n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S2[n] implies S2[n + 1] )
given G being
Subset of
T such that A9:
G = meet (f .: (succ n))
and A10:
G is
open
;
:: thesis: S2[n + 1]
n + 1
in NAT
;
then A11:
n + 1
in dom f
by FUNCT_2:def 1;
f . (n + 1) in B
;
then consider H1 being
Subset of
T such that A12:
H1 = f . (n + 1)
;
reconsider H1 =
H1 as
Subset of
T ;
A13:
H1 is
open
by A12, YELLOW_8:21;
(
n in succ n &
dom f = NAT )
by FUNCT_2:def 1, ORDINAL1:10;
then A14:
f . n in f .: (succ n)
by FUNCT_1:def 12;
consider H being
Subset of
T such that A15:
H = H1 /\ G
;
reconsider H =
H as
Subset of
T ;
take
H
;
:: thesis: ( H = meet (f .: (succ (n + 1))) & H is open )
meet (f .: (succ (n + 1))) =
meet (f .: ({(n + 1)} \/ (n + 1)))
by ORDINAL1:def 1
.=
meet (f .: ({(n + 1)} \/ (succ n)))
by NAT_1:39
.=
meet ((Im f,(n + 1)) \/ (f .: (succ n)))
by RELAT_1:153
.=
meet ({(f . (n + 1))} \/ (f .: (succ n)))
by A11, FUNCT_1:117
.=
(meet {(f . (n + 1))}) /\ (meet (f .: (succ n)))
by A14, SETFAM_1:10
.=
H
by A9, A12, A15, SETFAM_1:11
;
hence
(
H = meet (f .: (succ (n + 1))) &
H is
open )
by A10, A13, A15, TOPS_1:38;
:: thesis: verum
end;
thus
for
n being
Element of
NAT holds
S2[
n]
from NAT_1:sch 1(A6, A8); :: thesis: verum
end;
then consider H being
Subset of
T such that A16:
(
H = meet (f .: (succ n)) &
H is
open )
;
(
n in succ n &
dom f = NAT )
by FUNCT_2:def 1, ORDINAL1:10;
then A17:
f . n in f .: (succ n)
by FUNCT_1:def 12;
for
G being
set st
G in f .: (succ n) holds
x in G
then
x in meet (f .: (succ n))
by A17, SETFAM_1:def 1;
then
A meets meet (f .: (succ n))
by A2, A16, PRE_TOPC:def 13;
then consider y being
set such that A20:
y in A /\ (meet (f .: (succ n)))
by XBOOLE_0:4;
take
y
;
:: thesis: ( y in the carrier of T & S1[n,y] )
thus
(
y in the
carrier of
T &
S1[
n,
y] )
by A20;
:: thesis: verum
end;
consider S being Function such that
A21:
( dom S = NAT & rng S c= the carrier of T & ( for n being set st n in NAT holds
S1[n,S . n] ) )
from WELLORD2:sch 1(A5);
A22:
for m, n being Element of NAT st n <= m holds
A /\ (meet (f .: (succ m))) c= A /\ (meet (f .: (succ n)))
A25:
rng S c= A
reconsider S = S as sequence of T by A21, FUNCT_2:def 1, RELSET_1:11;
S is_convergent_to x
then
x in Lim S
by Def4;
hence
ex S being sequence of T st
( rng S c= A & x in Lim S )
by A25; :: thesis: verum