A14: [#] (() | ([#] ())) = {(0. ())} by ;
let M be non empty TopSpace; :: thesis: ( M is discrete implies M is 0 -locally_euclidean )
assume A15: M is discrete ; :: thesis:
for p being Point of M ex U being a_neighborhood of p st U, [#] () are_homeomorphic
proof
let p be Point of M; :: thesis: ex U being a_neighborhood of p st U, [#] () are_homeomorphic
reconsider U = {p} as Subset of M by ZFMISC_1:31;
A16: ( U is open & p in U ) by ;
then reconsider U = U as a_neighborhood of p by CONNSP_2:3;
take U ; :: thesis:
set f = {[p,(0. ())]};
A17: p in [#] (M | U) by ;
A19: dom {[p,(0. ())]} = U by RELAT_1:9;
then A20: dom {[p,(0. ())]} = [#] (M | U) by PRE_TOPC:def 5;
then reconsider f = {[p,(0. ())]} as Function of (M | U),(() | ([#] ())) by ;
A21: rng f = [#] (() | ([#] ())) by ;
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 ;
hence ( P is closed implies f .: P is closed ) by ; :: thesis: ( f .: P is closed implies P is closed )
thus ( f .: P is closed implies P is closed ) by ; :: thesis: verum
end;
end;
end;
then M | U,() | ([#] ()) are_homeomorphic by ;
hence U, [#] () are_homeomorphic by METRIZTS:def 1; :: thesis: verum
end;
hence M is 0 -locally_euclidean by Th13; :: thesis: verum