let M be non empty TopSpace; :: thesis: ( M is 0 -locally_euclidean implies M is discrete )

assume A1: M is 0 -locally_euclidean ; :: thesis: M is discrete

for X being Subset of M

for p being Point of M st X = {p} holds

X is open

assume A1: M is 0 -locally_euclidean ; :: thesis: M is discrete

for X being Subset of M

for p being Point of M st X = {p} holds

X is open

proof

hence
M is discrete
by TDLAT_3:17; :: thesis: verum
let X be Subset of M; :: thesis: for p being Point of M st X = {p} holds

X is open

let p be Point of M; :: thesis: ( X = {p} implies X is open )

assume A2: X = {p} ; :: thesis: 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;

A5: p in U by A4, CONNSP_2:def 1;

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, A3, METRIZTS: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 object holds

( x in V iff x = p )

end;X is open

let p be Point of M; :: thesis: ( X = {p} implies X is open )

assume A2: X = {p} ; :: thesis: 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;

A5: p in U by A4, CONNSP_2:def 1;

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, A3, METRIZTS: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 object holds

( x in V iff x = p )

proof

hence
X is open
by A2, A7, TARSKI:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in V iff x = p )

hence x in V by A7; :: thesis: verum

end;hereby :: thesis: ( x = p implies x in V )

assume
x = p
; :: thesis: x in Vassume
x in V
; :: thesis: x = p

then 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; :: thesis: verum

end;then 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; :: thesis: verum

hence x in V by A7; :: thesis: verum