A14: [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) = {(0. (TOP-REAL 0))} by Lm2, EUCLID:22, EUCLID:77;
let M be non empty TopSpace; :: thesis: ( M is discrete implies M is 0 -locally_euclidean )
assume A15: M is discrete ; :: thesis: M is 0 -locally_euclidean
for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic
proof
let p be Point of M; :: thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic
reconsider U = {p} as Subset of M by ZFMISC_1:31;
A16: ( U is open & p in U ) by A15, TARSKI:def 1, TDLAT_3:15;
then reconsider U = U as a_neighborhood of p by CONNSP_2:3;
take U ; :: thesis: U, [#] (TOP-REAL 0) are_homeomorphic
set f = {[p,(0. (TOP-REAL 0))]};
A17: p in [#] (M | U) by A16, PRE_TOPC:def 5;
A19: dom {[p,(0. (TOP-REAL 0))]} = U by RELAT_1:9;
then A20: dom {[p,(0. (TOP-REAL 0))]} = [#] (M | U) by PRE_TOPC:def 5;
then reconsider f = {[p,(0. (TOP-REAL 0))]} as Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A17, Lm2, ZFMISC_1:87, FUNCT_2:def 1, ZFMISC_1:31;
A21: rng f = [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A14, RELAT_1:9;
for P being Subset of (M | U) holds
( P is closed iff f .: P is closed )
proof
let P be Subset of (M | U); :: thesis: ( P is closed iff f .: P is closed )
per cases ( P is empty or not P is empty ) ;
suppose A22: P is empty ; :: thesis: ( P is closed iff f .: P is closed )
thus ( P is closed iff f .: P is closed ) by A22; :: thesis: verum
end;
suppose A23: not P is empty ; :: thesis: ( P is closed iff f .: P is closed )
then P = [#] (M | U) by A20, A19, ZFMISC_1:33;
hence ( P is closed implies f .: P is closed ) by A21, A20, RELAT_1:113; :: thesis: ( f .: P is closed implies P is closed )
thus ( f .: P is closed implies P is closed ) by A23, A20, A19, ZFMISC_1:33; :: thesis: verum
end;
end;
end;
then M | U,(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic by T_0TOPSP:def 1, A20, A21, TOPS_2:58;
hence U, [#] (TOP-REAL 0) are_homeomorphic by METRIZTS:def 1; :: thesis: verum
end;
hence M is 0 -locally_euclidean by Th13; :: thesis: verum