let M be non empty TopSpace; ( M is n -locally_euclidean implies M is first-countable )
assume A1:
M is n -locally_euclidean
; M is first-countable
for p being Point of M ex B being Basis of p st B is countable
proof
let p be
Point of
M;
ex B being Basis of p st B is countable
consider U being
a_neighborhood of
p such that A2:
U,
[#] (TOP-REAL n) are_homeomorphic
by A1, Th13;
M | U,
(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic
by A2, METRIZTS:def 1;
then
M | U,
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
are_homeomorphic
by TSEP_1:93;
then consider f being
Function of
(M | U),
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
such that A3:
f is
being_homeomorphism
by T_0TOPSP:def 1;
A4:
(
dom f = [#] (M | U) &
rng f = [#] TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #) &
f is
one-to-one &
f is
continuous &
f " is
continuous )
by A3, TOPS_2:def 5;
then A5:
dom f = U
by PRE_TOPC:def 5;
B2:
f is
onto
by A4, FUNCT_2:def 3;
A6:
Int U c= U
by TOPS_1:16;
A7:
p in Int U
by CONNSP_2:def 1;
A8:
p in dom f
by A7, A6, A5;
f . p in rng f
by A7, A6, A5, FUNCT_1:3;
then reconsider q =
f . p as
Point of
(TOP-REAL n) ;
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
TOP-REAL n1 is
first-countable
;
then consider B1 being
Basis of
q such that A9:
B1 is
countable
by FRECHET:def 2;
reconsider A =
bool the
carrier of
(TOP-REAL n) as non
empty set ;
deffunc H1(
set )
-> Element of
bool the
carrier of
M =
((f ") .: n) /\ (Int U);
set B =
{ H1(X) where X is Element of A : X in B1 } ;
A10:
card B1 c= omega
by A9, CARD_3:def 14;
card { H1(X) where X is Element of A : X in B1 } c= card B1
from TREES_2:sch 2();
then A11:
card { H1(X) where X is Element of A : X in B1 } c= omega
by A10, XBOOLE_1:1;
for
x being
set st
x in { H1(X) where X is Element of A : X in B1 } holds
x in bool the
carrier of
M
then reconsider B =
{ H1(X) where X is Element of A : X in B1 } as
Subset-Family of
M by TARSKI:def 3;
A13:
for
P being
Subset of
M st
P in B holds
P is
open
proof
let P be
Subset of
M;
( P in B implies P is open )
assume
P in B
;
P is open
then consider X1 being
Element of
A such that A14:
(
P = H1(
X1) &
X1 in B1 )
;
reconsider X1 =
X1 as
Subset of
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #) ;
reconsider X2 =
X1 as
Subset of
(TOP-REAL n) ;
X2 is
open
by A14, YELLOW_8:12;
then
X2 in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2;
then A15:
X1 is
open
by PRE_TOPC:def 2;
reconsider U1 =
M | U as non
empty TopStruct by A7, A6;
reconsider g =
f " as
Function of
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #),
U1 ;
A16:
g is
being_homeomorphism
by A3, TOPS_2:56;
A17:
g .: X1 is
open
by A15, A16, TOPGRP_1:25;
g .: X1 in the
topology of
(M | U)
by A17, PRE_TOPC:def 2;
then consider Q being
Subset of
M such that A18:
(
Q in the
topology of
M &
g .: X1 = Q /\ ([#] (M | U)) )
by PRE_TOPC:def 4;
[#] (M | U) = U
by PRE_TOPC:def 5;
then A19:
P =
Q /\ (U /\ (Int U))
by A18, A14, XBOOLE_1:16
.=
Q /\ (Int U)
by TOPS_1:16, XBOOLE_1:28
;
Q is
open
by A18, PRE_TOPC:def 2;
hence
P is
open
by A19;
verum
end;
for
Y being
set st
Y in B holds
p in Y
proof
let Y be
set ;
( Y in B implies p in Y )
assume
Y in B
;
p in Y
then consider X1 being
Element of
A such that A20:
(
Y = H1(
X1) &
X1 in B1 )
;
reconsider g =
f as
Function ;
[p,(g . p)] in g
by A7, A6, A5, FUNCT_1:def 2;
then
[q,p] in g ~
by RELAT_1:def 7;
then
[q,p] in g "
by A4, FUNCT_1:def 5;
then A21:
[q,p] in f "
by B2, A4, TOPS_2:def 4;
q in X1
by A20, YELLOW_8:12;
then
p in (f ") .: X1
by A21, RELAT_1:def 13;
hence
p in Y
by A20, A7, XBOOLE_0:def 4;
verum
end;
then A22:
p in Intersect B
by SETFAM_1:43;
for
S being
Subset of
M st
S is
open &
p in S holds
ex
V being
Subset of
M st
(
V in B &
V c= S )
proof
let S be
Subset of
M;
( S is open & p in S implies ex V being Subset of M st
( V in B & V c= S ) )
assume A23:
(
S is
open &
p in S )
;
ex V being Subset of M st
( V in B & V c= S )
set S1 =
S /\ ([#] (M | U));
S in the
topology of
M
by A23, PRE_TOPC:def 2;
then A24:
S /\ ([#] (M | U)) in the
topology of
(M | U)
by PRE_TOPC:def 4;
reconsider U1 =
M | U as non
empty TopStruct by A7, A6;
reconsider S1 =
S /\ ([#] (M | U)) as
Subset of
U1 ;
S1 is
open
by A24, PRE_TOPC:def 2;
then A25:
f .: S1 is
open
by A3, TOPGRP_1:25;
reconsider S2 =
f .: S1 as
Subset of
(TOP-REAL n) ;
f .: S1 in the
topology of
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
by A25, PRE_TOPC:def 2;
then A26:
S2 is
open
by PRE_TOPC:def 2;
reconsider g1 =
f as
Function ;
A27:
[p,q] in f
by A7, A6, A5, FUNCT_1:def 2;
p in S1
by A8, A23, XBOOLE_0:def 4;
then A28:
q in S2
by A27, RELAT_1:def 13;
consider W being
Subset of
(TOP-REAL n) such that A29:
(
W in B1 &
W c= S2 )
by A28, A26, YELLOW_8:13;
reconsider W =
W as
Element of
A ;
set V =
((f ") .: W) /\ (Int U);
reconsider V =
((f ") .: W) /\ (Int U) as
Subset of
M ;
take
V
;
( V in B & V c= S )
thus
V in B
by A29;
V c= S
A30:
g1 " = f "
by B2, A4, TOPS_2:def 4;
A31:
(f ") .: (f .: S1) = S1
by A30, A4, FUNCT_1:107;
A32:
((f ") .: W) /\ (Int U) c= (f ") .: W
by XBOOLE_1:17;
A33:
S1 c= S
by XBOOLE_1:17;
(f ") .: W c= (f ") .: (f .: S1)
by A29, RELAT_1:123;
then
(f ") .: W c= S
by A31, A33, XBOOLE_1:1;
hence
V c= S
by A32, XBOOLE_1:1;
verum
end;
then reconsider B =
B as
Basis of
p by A13, A22, TOPS_2:def 1, YELLOW_8:def 1;
take
B
;
B is countable
thus
B is
countable
by A11, CARD_3:def 14;
verum
end;
hence
M is first-countable
by FRECHET:def 2; verum