let T be non empty TopSpace; for F being Subset-Family of T st F is discrete holds
Cl (union F) = union (clf F)
let F be Subset-Family of T; ( F is discrete implies Cl (union F) = union (clf F) )
assume A1:
F is discrete
; Cl (union F) = union (clf F)
A2:
Cl (union F) c= union (clf F)
proof
let x be
object ;
TARSKI:def 3 ( not x in Cl (union F) or x in union (clf F) )
assume A3:
x in Cl (union F)
;
x in union (clf F)
then consider O being
open Subset of
T such that A4:
x in O
and A5:
for
A,
B being
Subset of
T st
A in F &
B in F &
O meets A &
O meets B holds
A = B
by A1;
not
O misses union F
by A3, A4, PRE_TOPC:def 7;
then consider f being
object such that A6:
f in O
and A7:
f in union F
by XBOOLE_0:3;
consider AF being
set such that A8:
f in AF
and A9:
AF in F
by A7, TARSKI:def 4;
reconsider AF =
AF as
Subset of
T by A9;
A10:
O meets AF
by A6, A8, XBOOLE_0:3;
for
D being
Subset of
T st
D is
open &
x in D holds
not
D misses AF
proof
assume
ex
D being
Subset of
T st
(
D is
open &
x in D &
D misses AF )
;
contradiction
then consider D being
Subset of
T such that A11:
D is
open
and A12:
x in D
and A13:
D misses AF
;
x in D /\ O
by A4, A12, XBOOLE_0:def 4;
then
D /\ O meets union F
by A3, A11, PRE_TOPC:def 7;
then consider y being
object such that A14:
y in D /\ O
and A15:
y in union F
by XBOOLE_0:3;
consider BF being
set such that A16:
y in BF
and A17:
BF in F
by A15, TARSKI:def 4;
y in D
by A14, XBOOLE_0:def 4;
then
y in D /\ BF
by A16, XBOOLE_0:def 4;
then A18:
D meets BF
by XBOOLE_0:def 7;
y in O
by A14, XBOOLE_0:def 4;
then
y in O /\ BF
by A16, XBOOLE_0:def 4;
then
O meets BF
by XBOOLE_0:def 7;
hence
contradiction
by A5, A9, A10, A13, A17, A18;
verum
end;
then A19:
x in Cl AF
by A3, PRE_TOPC:def 7;
Cl AF in clf F
by A9, PCOMPS_1:def 2;
hence
x in union (clf F)
by A19, TARSKI:def 4;
verum
end;
union (clf F) c= Cl (union F)
hence
Cl (union F) = union (clf F)
by A2, XBOOLE_0:def 10; verum