let M be non empty TopSpace; ( M is without_boundary & M is locally_euclidean implies M is first-countable )
assume A1:
( M is without_boundary & M is 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,
n being
Nat such that A2:
M | U,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A1, MFOLD_0:6;
set TR =
TOP-REAL n;
p in Int U
by CONNSP_2:def 1;
then K1:
ex
W being
Subset of
M st
(
W is
open &
W c= U &
p in W )
by TOPS_1:22;
( not
Ball (
(0. (TOP-REAL n)),1) is
empty &
Ball (
(0. (TOP-REAL n)),1) is
ball )
;
then
Tball (
(0. (TOP-REAL n)),1),
(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic
by Th10, METRIZTS:def 1;
then
M | U,
(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic
by A2, K1, BORSUK_3:3;
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;
A6:
f is
onto
by A4, FUNCT_2:def 3;
A7:
Int U c= U
by TOPS_1:16;
A8:
p in Int U
by CONNSP_2:def 1;
A9:
p in dom f
by CONNSP_2:def 1, A7, A5;
f . p in rng f
by A8, A7, 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;
consider B1 being
Basis of
q such that A10:
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 ") .: c1) /\ (Int U);
set B =
{ H1(X) where X is Element of A : X in B1 } ;
A11:
card B1 c= omega
by A10, 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 A12:
card { H1(X) where X is Element of A : X in B1 } c= omega
by A11;
for
x being
object 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;
A14:
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 A15:
(
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 in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2, A15, YELLOW_8:12;
then A16:
X1 is
open
by PRE_TOPC:def 2;
reconsider U1 =
M | U as non
empty TopStruct by A8, A7;
reconsider g =
f " as
Function of
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #),
U1 ;
A17:
g is
being_homeomorphism
by A3, TOPS_2:56;
A18:
g .: X1 is
open
by A16, A17, TOPGRP_1:25;
g .: X1 in the
topology of
(M | U)
by A18, PRE_TOPC:def 2;
then consider Q being
Subset of
M such that A19:
(
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 A20:
P =
Q /\ (U /\ (Int U))
by A19, A15, XBOOLE_1:16
.=
Q /\ (Int U)
by TOPS_1:16, XBOOLE_1:28
;
Q is
open
by A19, PRE_TOPC:def 2;
hence
P is
open
by A20;
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 A21:
(
Y = H1(
X1) &
X1 in B1 )
;
reconsider g =
f as
Function ;
[p,(g . p)] in g
by A8, A7, 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 A22:
[q,p] in f "
by A6, A4, TOPS_2:def 4;
q in X1
by A21, YELLOW_8:12;
then
p in (f ") .: X1
by A22, RELAT_1:def 13;
hence
p in Y
by A21, A8, XBOOLE_0:def 4;
verum
end;
then A23:
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 A24:
(
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 A24, PRE_TOPC:def 2;
then A25:
S /\ ([#] (M | U)) in the
topology of
(M | U)
by PRE_TOPC:def 4;
reconsider U1 =
M | U as non
empty TopStruct by A8, A7;
reconsider S1 =
S /\ ([#] (M | U)) as
Subset of
U1 ;
S1 is
open
by A25, PRE_TOPC:def 2;
then A26:
f .: S1 is
open
by A3, TOPGRP_1:25;
reconsider S2 =
f .: S1 as
Subset of
(TOP-REAL n) ;
K:
f .: S1 in the
topology of
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
by A26, PRE_TOPC:def 2;
reconsider g1 =
f as
Function ;
A28:
[p,q] in f
by A8, A7, A5, FUNCT_1:def 2;
p in S1
by A9, A24, XBOOLE_0:def 4;
then A29:
q in S2
by A28, RELAT_1:def 13;
consider W being
Subset of
(TOP-REAL n) such that A30:
(
W in B1 &
W c= S2 )
by A29, K, PRE_TOPC:def 2, 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 A30;
V c= S
A31:
g1 " = f "
by A6, A4, TOPS_2:def 4;
A32:
(f ") .: (f .: S1) = S1
by A31, A4, FUNCT_1:107;
A33:
((f ") .: W) /\ (Int U) c= (f ") .: W
by XBOOLE_1:17;
A34:
S1 c= S
by XBOOLE_1:17;
(f ") .: W c= (f ") .: (f .: S1)
by A30, RELAT_1:123;
hence
V c= S
by A33, A32, A34;
verum
end;
then reconsider B =
B as
Basis of
p by A14, A23, TOPS_2:def 1, YELLOW_8:def 1;
take
B
;
B is countable
thus
B is
countable
by A12, CARD_3:def 14;
verum
end;
hence
M is first-countable
by FRECHET:def 2; verum