:: TDLAT_3 semantic presentation

theorem :: TDLAT_3:1

canceled;

theorem Th2: :: TDLAT_3:2

for X being TopSpace
for C being Subset of X holds Cl C = (Int (C ` )) `

proof end;

theorem Th3: :: TDLAT_3:3

for X being TopSpace
for C being Subset of X holds Cl (C ` ) = (Int C) `

proof end;

theorem Th4: :: TDLAT_3:4

for X being TopSpace
for C being Subset of X holds Int (C ` ) = (Cl C) `

proof end;

theorem :: TDLAT_3:5

canceled;

theorem :: TDLAT_3:6

for X being TopSpace
for A, B being Subset of X st A \/ B = the carrier of X holds
( ( A is closed implies A \/ (Int B) = the carrier of X ) & ( B is closed implies (Int A) \/ B = the carrier of X ) )

proof end;

theorem Th7: :: TDLAT_3:7

for X being TopSpace
for A being Subset of X holds
( ( A is open & A is closed ) iff Cl A = Int A )

proof end;

theorem :: TDLAT_3:8

for X being TopSpace
for A being Subset of X st A is open & A is closed holds
Int (Cl A) = Cl (Int A)

proof end;

theorem Th9: :: TDLAT_3:9

for X being TopSpace
for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds
( A is open_condensed & A is closed_condensed )

proof end;

theorem Th10: :: TDLAT_3:10

for X being TopSpace
for A being Subset of X st A is condensed & Cl (Int A) c= Int (Cl A) holds
( A is open & A is closed )

proof end;

theorem Th11: :: TDLAT_3:11

for X being TopSpace
for A being Subset of X st A is condensed holds
( Int (Cl A) = Int A & Cl A = Cl (Int A) )

proof end;

definition

let IT be TopStruct ;
attr IT is discrete means :Def1: :: TDLAT_3:def 1
the topology of IT = bool the carrier of IT;
attr IT is anti-discrete means :Def2: :: TDLAT_3:def 2
the topology of IT = {{} ,the carrier of IT};

end;

:: deftheorem Def1 defines discrete TDLAT_3:def 1 :

:: deftheorem Def2 defines anti-discrete TDLAT_3:def 2 :

theorem :: TDLAT_3:12

for Y being TopStruct st Y is discrete & Y is anti-discrete holds
bool the carrier of Y = {{} ,the carrier of Y}

proof end;

theorem Th13: :: TDLAT_3:13

for Y being TopStruct st {} in the topology of Y & the carrier of Y in the topology of Y & bool the carrier of Y = {{} ,the carrier of Y} holds
( Y is discrete & Y is anti-discrete )

proof end;

registration

cluster non empty strict discrete anti-discrete TopStruct ;
existence

proof end;

end;

theorem Th14: :: TDLAT_3:14

for Y being discrete TopStruct
for A being Subset of Y holds the carrier of Y \ A in the topology of Y

proof end;

theorem Th15: :: TDLAT_3:15

for Y being anti-discrete TopStruct
for A being Subset of Y st A in the topology of Y holds
the carrier of Y \ A in the topology of Y

proof end;

registration

cluster discrete -> TopSpace-like TopStruct ;
coherence

proof end;

cluster anti-discrete -> TopSpace-like TopStruct ;
coherence

proof end;

end;

theorem :: TDLAT_3:16

for Y being TopSpace-like TopStruct st bool the carrier of Y = {{} ,the carrier of Y} holds
( Y is discrete & Y is anti-discrete )

proof end;

definition

let IT be TopStruct ;
attr IT is almost_discrete means :Def3: :: TDLAT_3:def 3
for A being Subset of IT st A in the topology of IT holds
the carrier of IT \ A in the topology of IT;

end;

:: deftheorem Def3 defines almost_discrete TDLAT_3:def 3 :

registration

cluster discrete -> almost_discrete TopStruct ;
coherence

proof end;

cluster anti-discrete -> almost_discrete TopStruct ;
coherence

proof end;

end;

registration

cluster strict almost_discrete TopStruct ;
existence

proof end;

end;

registration

cluster non empty strict discrete anti-discrete almost_discrete TopStruct ;
existence

proof end;

end;

theorem Th17: :: TDLAT_3:17

for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is open )

proof end;

theorem Th18: :: TDLAT_3:18

for X being TopSpace holds
( X is discrete iff for A being Subset of X holds A is closed )

proof end;

theorem Th19: :: TDLAT_3:19

for X being TopSpace st ( for A being Subset of X
for x being Point of X st A = {x} holds
A is open ) holds
X is discrete

proof end;

registration

let X be non empty discrete TopSpace;
cluster -> TopSpace-like closed open discrete almost_discrete SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete SubSpace of X;
existence

proof end;

end;

theorem Th20: :: TDLAT_3:20

for X being TopSpace holds
( X is anti-discrete iff for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) )

proof end;

theorem Th21: :: TDLAT_3:21

for X being TopSpace holds
( X is anti-discrete iff for A being Subset of X holds
( not A is closed or A = {} or A = the carrier of X ) )

proof end;

theorem :: TDLAT_3:22

for X being TopSpace st ( for A being Subset of X
for x being Point of X st A = {x} holds
Cl A = the carrier of X ) holds
X is anti-discrete

proof end;

registration

let X be non empty anti-discrete TopSpace;
cluster -> TopSpace-like anti-discrete almost_discrete SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty anti-discrete TopSpace;
cluster TopSpace-like anti-discrete almost_discrete SubSpace of X;
existence

proof end;

end;

theorem Th23: :: TDLAT_3:23

for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is open holds
A is closed )

proof end;

theorem Th24: :: TDLAT_3:24

for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is closed holds
A is open )

proof end;

theorem :: TDLAT_3:25

for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is open holds
Cl A = A )

proof end;

theorem :: TDLAT_3:26

for X being TopSpace holds
( X is almost_discrete iff for A being Subset of X st A is closed holds
Int A = A )

proof end;

registration

cluster strict almost_discrete TopStruct ;
existence

proof end;

end;

theorem :: TDLAT_3:27

for X being TopSpace st ( for A being Subset of X
for x being Point of X st A = {x} holds
Cl A is open ) holds
X is almost_discrete

proof end;

theorem :: TDLAT_3:28

for X being TopSpace holds
( X is discrete iff ( X is almost_discrete & ( for A being Subset of X
for x being Point of X st A = {x} holds
A is closed ) ) )

proof end;

registration

cluster discrete -> almost_discrete TopStruct ;
coherence

proof end;

cluster anti-discrete -> almost_discrete TopStruct ;
coherence

proof end;

end;

registration

let X be non empty almost_discrete TopSpace;
cluster non empty -> non empty almost_discrete SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty almost_discrete TopSpace;
cluster open -> closed SubSpace of X;
coherence

proof end;

cluster closed -> open SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty almost_discrete TopSpace;
cluster non empty strict almost_discrete SubSpace of X;
existence

proof end;

end;

definition

let IT be non empty TopSpace;
attr IT is extremally_disconnected means :Def4: :: TDLAT_3:def 4
for A being Subset of IT st A is open holds
Cl A is open;

end;

:: deftheorem Def4 defines extremally_disconnected TDLAT_3:def 4 :

registration

cluster non empty strict extremally_disconnected TopStruct ;
existence

proof end;

end;

theorem Th29: :: TDLAT_3:29

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is closed holds
Int A is closed )

proof end;

theorem Th30: :: TDLAT_3:30

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A, B being Subset of X st A is open & B is open & A misses B holds
Cl A misses Cl B )

proof end;

theorem :: TDLAT_3:31

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds
(Int A) \/ (Int B) = the carrier of X )

proof end;

theorem Th32: :: TDLAT_3:32

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is open holds
Cl A = Int (Cl A) )

proof end;

theorem :: TDLAT_3:33

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is closed holds
Int A = Cl (Int A) )

proof end;

theorem Th34: :: TDLAT_3:34

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
( A is closed & A is open ) )

proof end;

theorem Th35: :: TDLAT_3:35

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
( A is closed_condensed & A is open_condensed ) )

proof end;

theorem Th36: :: TDLAT_3:36

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
Int (Cl A) = Cl (Int A) )

proof end;

theorem :: TDLAT_3:37

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X st A is condensed holds
Int A = Cl A )

proof end;

theorem Th38: :: TDLAT_3:38

for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) )

proof end;

definition

let IT be non empty TopSpace;
attr IT is hereditarily_extremally_disconnected means :Def5: :: TDLAT_3:def 5
for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected;

end;

:: deftheorem Def5 defines hereditarily_extremally_disconnected TDLAT_3:def 5 :

registration

cluster non empty strict hereditarily_extremally_disconnected TopStruct ;
existence

proof end;

end;

registration

cluster non empty hereditarily_extremally_disconnected -> non empty extremally_disconnected TopStruct ;
coherence

proof end;

cluster non empty almost_discrete -> non empty hereditarily_extremally_disconnected TopStruct ;
coherence

proof end;

end;

theorem Th39: :: TDLAT_3:39

for X being non empty extremally_disconnected TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of X0 & A is dense holds
X0 is extremally_disconnected

proof end;

registration

let X be non empty extremally_disconnected TopSpace;
cluster non empty open -> non empty extremally_disconnected SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty extremally_disconnected TopSpace;
cluster non empty strict extremally_disconnected SubSpace of X;
existence

proof end;

end;

registration

let X be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty -> non empty extremally_disconnected hereditarily_extremally_disconnected SubSpace of X;
coherence

proof end;

end;

registration

let X be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty strict extremally_disconnected hereditarily_extremally_disconnected SubSpace of X;
existence

proof end;

end;

theorem :: TDLAT_3:40

for X being non empty TopSpace st ( for X0 being non empty closed SubSpace of X holds X0 is extremally_disconnected ) holds
X is hereditarily_extremally_disconnected

proof end;

theorem Th41: :: TDLAT_3:41

for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Closed_Domains_of Y

proof end;

theorem Th42: :: TDLAT_3:42

for Y being non empty extremally_disconnected TopSpace holds
( D-Union Y = CLD-Union Y & D-Meet Y = CLD-Meet Y )

proof end;

theorem Th43: :: TDLAT_3:43

for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Closed_Domains_Lattice Y

proof end;

theorem Th44: :: TDLAT_3:44

for Y being non empty extremally_disconnected TopSpace holds Domains_of Y = Open_Domains_of Y

proof end;

theorem Th45: :: TDLAT_3:45

for Y being non empty extremally_disconnected TopSpace holds
( D-Union Y = OPD-Union Y & D-Meet Y = OPD-Meet Y )

proof end;

theorem Th46: :: TDLAT_3:46

for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Open_Domains_Lattice Y

proof end;

theorem Th47: :: TDLAT_3:47

for Y being non empty extremally_disconnected TopSpace
for A, B being Element of Domains_of Y holds
( (D-Union Y) . A,B = A \/ B & (D-Meet Y) . A,B = A /\ B )

proof end;

theorem :: TDLAT_3:48

for Y being non empty extremally_disconnected TopSpace
for a, b being Element of (Domains_Lattice Y)
for A, B being Element of Domains_of Y st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = A /\ B )

proof end;

theorem :: TDLAT_3:49

for Y being non empty extremally_disconnected TopSpace
for F being Subset-Family of Y st F is domains-family holds
for S being Subset of (Domains_Lattice Y) st S = F holds
"\/" S,(Domains_Lattice Y) = Cl (union F)

proof end;

theorem :: TDLAT_3:50

for Y being non empty extremally_disconnected TopSpace
for F being Subset-Family of Y st F is domains-family holds
for S being Subset of (Domains_Lattice Y) st S = F holds
( ( S <> {} implies "/\" S,(Domains_Lattice Y) = Int (meet F) ) & ( S = {} implies "/\" S,(Domains_Lattice Y) = [#] Y ) )

proof end;

theorem Th51: :: TDLAT_3:51

for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is M_Lattice )

proof end;

theorem :: TDLAT_3:52

for X being non empty TopSpace st Domains_Lattice X = Closed_Domains_Lattice X holds
X is extremally_disconnected by Th51;

theorem :: TDLAT_3:53

for X being non empty TopSpace st Domains_Lattice X = Open_Domains_Lattice X holds
X is extremally_disconnected by Th51;

theorem :: TDLAT_3:54

for X being non empty TopSpace st Closed_Domains_Lattice X = Open_Domains_Lattice X holds
X is extremally_disconnected

proof end;

theorem :: TDLAT_3:55

for X being non empty TopSpace holds
( X is extremally_disconnected iff Domains_Lattice X is B_Lattice )

proof end;