let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds
( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION {O},F) \ {{} } is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds
A misses B ) ) )
let F be Subset-Family of T; :: thesis: ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION {O},F) \ {{} } is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds
A misses B ) ) )
now let F be
Subset-Family of
T;
:: thesis: ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION {O},F) \ {{} } is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds
A misses B ) ) )
( ( for
p being
Point of
T ex
O being
open Subset of
T st
(
p in O &
(INTERSECTION {O},F) \ {{} } is
trivial ) ) & ( for
A,
B being
Subset of
T st
A in F &
B in F & not
A = B holds
A misses B ) implies
F is
discrete )
proof
assume A1:
( ( for
p being
Point of
T ex
O being
open Subset of
T st
(
p in O &
(INTERSECTION {O},F) \ {{} } is
trivial ) ) & ( for
A,
B being
Subset of
T st
A in F &
B in F & not
A = B holds
A misses B ) )
;
:: thesis: F is discrete
assume
not
F is
discrete
;
:: thesis: contradiction
then consider p being
Point of
T such that A2:
for
O being
open Subset of
T holds
( not
p in O or ex
A,
B being
Subset of
T st
(
A in F &
B in F &
O meets A &
O meets B & not
A = B ) )
by Def1;
consider O being
open Subset of
T such that A3:
(
p in O &
(INTERSECTION {O},F) \ {{} } is
trivial )
by A1;
set I =
INTERSECTION {O},
F;
consider A,
B being
Subset of
T such that A4:
(
A in F &
B in F &
O meets A &
O meets B &
A <> B )
by A2, A3;
A5:
(
O /\ A <> {} &
O /\ B <> {} )
by A4, XBOOLE_0:def 7;
O in {O}
by ZFMISC_1:37;
then
(
O /\ A in INTERSECTION {O},
F &
O /\ B in INTERSECTION {O},
F )
by A4, SETFAM_1:def 5;
then A6:
(
O /\ A in (INTERSECTION {O},F) \ {{} } &
O /\ B in (INTERSECTION {O},F) \ {{} } )
by A5, ZFMISC_1:64;
consider a being
set such that A7:
(
(INTERSECTION {O},F) \ {{} } = {} or
(INTERSECTION {O},F) \ {{} } = {a} )
by A3, REALSET1:def 4;
(
{(O /\ A)} c= {a} &
{(O /\ B)} c= {a} )
by A6, A7, ZFMISC_1:37;
then A8:
(
O /\ A = a &
O /\ B = a )
by ZFMISC_1:6;
consider f being
set such that A9:
f in O /\ A
by A5, XBOOLE_0:def 1;
(
f in A &
f in B )
by A8, A9, XBOOLE_0:def 4;
then
(
f in A /\ B &
A misses B )
by A1, A4, XBOOLE_0:def 4;
hence
contradiction
by XBOOLE_0:def 7;
:: thesis: verum
end; hence
(
F is
discrete iff ( ( for
p being
Point of
T ex
O being
open Subset of
T st
(
p in O &
(INTERSECTION {O},F) \ {{} } is
trivial ) ) & ( for
A,
B being
Subset of
T st
A in F &
B in F & not
A = B holds
A misses B ) ) )
by Th6, Th7;
:: thesis: verum end;
hence
( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION {O},F) \ {{} } is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds
A misses B ) ) )
; :: thesis: verum