let T be non empty TopSpace; 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; ( 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;
( 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 that A1:
for
p being
Point of
T ex
O being
open Subset of
T st
(
p in O &
(INTERSECTION ({O},F)) \ {{}} is
trivial )
and A2:
for
A,
B being
Subset of
T st
A in F &
B in F & not
A = B holds
A misses B
;
F is discrete
assume
not
F is
discrete
;
contradiction
then consider p being
Point of
T such that A3:
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 A4:
p in O
and A5:
(INTERSECTION ({O},F)) \ {{}} is
trivial
by A1;
consider A,
B being
Subset of
T such that A6:
A in F
and A7:
B in F
and A8:
O meets A
and A9:
O meets B
and A10:
A <> B
by A3, A4;
A11:
O /\ B <> {}
by A9, XBOOLE_0:def 7;
set I =
INTERSECTION (
{O},
F);
consider a being
set such that A12:
(
(INTERSECTION ({O},F)) \ {{}} = {} or
(INTERSECTION ({O},F)) \ {{}} = {a} )
by A5, ZFMISC_1:131;
A13:
O in {O}
by ZFMISC_1:31;
then
O /\ B in INTERSECTION (
{O},
F)
by A7, SETFAM_1:def 5;
then
O /\ B in (INTERSECTION ({O},F)) \ {{}}
by A11, ZFMISC_1:56;
then
{(O /\ B)} c= {a}
by A12, ZFMISC_1:31;
then A14:
O /\ B = a
by ZFMISC_1:3;
A15:
O /\ A <> {}
by A8, XBOOLE_0:def 7;
then consider f being
set such that A16:
f in O /\ A
by XBOOLE_0:def 1;
A17:
f in A
by A16, XBOOLE_0:def 4;
O /\ A in INTERSECTION (
{O},
F)
by A6, A13, SETFAM_1:def 5;
then
O /\ A in (INTERSECTION ({O},F)) \ {{}}
by A15, ZFMISC_1:56;
then
{(O /\ A)} c= {a}
by A12, ZFMISC_1:31;
then
O /\ A = a
by ZFMISC_1:3;
then
f in B
by A14, A16, XBOOLE_0:def 4;
then A18:
f in A /\ B
by A17, XBOOLE_0:def 4;
A misses B
by A2, A6, A7, A10;
hence
contradiction
by A18, XBOOLE_0:def 7;
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;
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 ) ) )
; verum