let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is discrete iff for D being Subset of X st D c= A holds
A /\ (Cl D) = D )
let A be Subset of X; :: thesis: ( A is discrete iff for D being Subset of X st D c= A holds
A /\ (Cl D) = D )
thus ( A is discrete implies for D being Subset of X st D c= A holds
A /\ (Cl D) = D ) :: thesis: ( ( for D being Subset of X st D c= A holds
A /\ (Cl D) = D ) implies A is discrete )
proof
assume A1: A is discrete ; :: thesis: for D being Subset of X st D c= A holds
A /\ (Cl D) = D
let D be Subset of X; :: thesis: ( D c= A implies A /\ (Cl D) = D )
assume A2: D c= A ; :: thesis: A /\ (Cl D) = D
then consider F being Subset of X such that
A3: F is closed and
A4: A /\ F = D by A1;
Cl D c= F by A3, A4, TOPS_1:5, XBOOLE_1:17;
then A5: A /\ (Cl D) c= D by A4, XBOOLE_1:26;
D c= Cl D by PRE_TOPC:18;
then D c= A /\ (Cl D) by A2, XBOOLE_1:19;
hence A /\ (Cl D) = D by A5; :: thesis: verum
end;
assume A6: for D being Subset of X st D c= A holds
A /\ (Cl D) = D ; :: thesis: A is discrete
now :: thesis: for D being Subset of X st D c= A holds
ex F being Subset of X st
( F is closed & A /\ F = D )
let D be Subset of X; :: thesis: ( D c= A implies ex F being Subset of X st
( F is closed & A /\ F = D ) )
assume A7: D c= A ; :: thesis: ex F being Subset of X st
( F is closed & A /\ F = D )
now :: thesis: ex F being Element of bool the carrier of X st
( F is closed & A /\ F = D )
take F = Cl D; :: thesis: ( F is closed & A /\ F = D )
thus F is closed ; :: thesis: A /\ F = D
thus A /\ F = D by A6, A7; :: thesis: verum
end;
hence ex F being Subset of X st
( F is closed & A /\ F = D ) ; :: thesis: verum
end;
hence A is discrete ; :: thesis: verum