let X be non empty TopSpace; :: thesis: for A being Subset of X st ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) holds
A is discrete
let A be Subset of X; :: thesis: ( ( for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ) implies A is discrete )
assume A1: for x being Point of X st x in A holds
ex G being Subset of X st
( G is open & A /\ G = {x} ) ; :: thesis: A is discrete
hereby :: thesis: verum
per cases ( A is empty or not A is empty ) ;
suppose not A is empty ; :: thesis: A is discrete
then consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
A3: [#] X = the carrier of X ;
[#] X0 = the carrier of X0 ;
then A4: the carrier of X0 c= the carrier of X by A3, PRE_TOPC:def 4;
now :: thesis: for C being Subset of X0
for y being Point of X0 st C = {y} holds
C is open
let C be Subset of X0; :: thesis: for y being Point of X0 st C = {y} holds
C is open
let y be Point of X0; :: thesis: ( C = {y} implies C is open )
reconsider x = y as Point of X by A4, TARSKI:def 3;
consider G being Subset of X such that
A5: G is open and
A6: A /\ G = {x} by A1, A2;
assume A7: C = {y} ; :: thesis: C is open
( G in the topology of X & G /\ ([#] X0) = C ) by A2, A7, A6, A5;
then C in the topology of X0 by PRE_TOPC:def 4;
hence C is open ; :: thesis: verum
end;
then X0 is discrete by TDLAT_3:17;
hence A is discrete by A2, Th20; :: thesis: verum
end;
end;
end;