let M be non empty TopSpace; ( M is 0 -locally_euclidean implies M is discrete )
assume A3:
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 A4:
X = {p}
;
X is open
consider U being
a_neighborhood of
p such that A5:
U,
[#] (TOP-REAL 0) are_homeomorphic
by A3, Th15;
A6:
Int U c= U
by TOPS_1:44;
p in Int U
by CONNSP_2:def 1;
then A7:
p in U
by A6;
M | U,
(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic
by A5, METRIZTS:def 1;
then consider f being
Function of
(M | U),
((TOP-REAL 0) | ([#] (TOP-REAL 0))) such that A8:
f is
being_homeomorphism
by T_0TOPSP:def 1;
consider V being
Subset of
M such that A9:
(
V is
open &
V c= U &
p in V )
by CONNSP_2:8;
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 A10:
x in U
by A9;
A11:
f is
one-to-one
by A8, TOPS_2:def 5;
x in [#] (M | U)
by A10, PRE_TOPC:def 10;
then A12:
x in dom f
by A8, TOPS_2:def 5;
then A13:
f . x in rng f
by FUNCT_1:12;
p in [#] (M | U)
by A7, PRE_TOPC:def 10;
then A14:
p in dom f
by A8, TOPS_2:def 5;
then A15:
f . p in rng f
by FUNCT_1:12;
f . x =
0. (TOP-REAL 0)
by A1, A13
.=
f . p
by A1, A15
;
hence
x = p
by A11, A12, A14, FUNCT_1:def 8;
verum
end;
assume
x = p
;
x in V
hence
x in V
by A9;
verum
end;
hence
X is
open
by A4, A9, TARSKI:def 1;
verum
end;
hence
M is discrete
by TDLAT_3:19; verum