let M be non empty TopSpace; ( M is 0 -locally_euclidean implies M is discrete )
assume A1:
M is 0 -locally_euclidean
; M is discrete
for X being Subset of M
for p being Point of M st X = {p} holds
X is open
proof
let X be
Subset of
M;
for p being Point of M st X = {p} holds
X is open let p be
Point of
M;
( X = {p} implies X is open )
assume A2:
X = {p}
;
X is open
consider U being
a_neighborhood of
p such that A3:
U,
[#] (TOP-REAL 0) are_homeomorphic
by A1, Th13;
A4:
Int U c= U
by TOPS_1:16;
p in Int U
by CONNSP_2:def 1;
then A5:
p in U
by A4;
M | U,
(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic
by A3, METRIZTS:def 1;
then consider f being
Function of
(M | U),
((TOP-REAL 0) | ([#] (TOP-REAL 0))) such that A6:
f is
being_homeomorphism
by T_0TOPSP:def 1;
consider V being
Subset of
M such that A7:
(
V is
open &
V c= U &
p in V )
by CONNSP_2:6;
for
x being
set holds
(
x in V iff
x = p )
proof
let x be
set ;
( x in V iff x = p )
hereby ( x = p implies x in V )
assume
x in V
;
x = pthen A8:
x in U
by A7;
A9:
f is
one-to-one
by A6, TOPS_2:def 5;
x in [#] (M | U)
by A8, PRE_TOPC:def 5;
then A10:
x in dom f
by A6, TOPS_2:def 5;
then A11:
f . x in rng f
by FUNCT_1:3;
p in [#] (M | U)
by A5, PRE_TOPC:def 5;
then A12:
p in dom f
by A6, TOPS_2:def 5;
then A13:
f . p in rng f
by FUNCT_1:3;
f . x =
0. (TOP-REAL 0)
by Lm2, A11
.=
f . p
by Lm2, A13
;
hence
x = p
by A9, A10, A12, FUNCT_1:def 4;
verum
end;
assume
x = p
;
x in V
hence
x in V
by A7;
verum
end;
hence
X is
open
by A2, A7, TARSKI:def 1;
verum
end;
hence
M is discrete
by TDLAT_3:17; verum