:: TDLAT_3 semantic presentation

theorem Th1: :: TDLAT_3:1

canceled;

theorem Th2: :: TDLAT_3:2

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Cl b₂ = (Int (b₂ ` )) `

proof end;

theorem Th3: :: TDLAT_3:3

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Cl (b₂ ` ) = (Int b₂) `

proof end;

theorem Th4: :: TDLAT_3:4

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Int (b₂ ` ) = (Cl b₂) `

proof end;

theorem Th5: :: TDLAT_3:5

canceled;

theorem Th6: :: TDLAT_3:6

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ \/ b₃ = the carrier of b₁ holds
( ( b₂ is closed implies b₂ \/ (Int b₃) = the carrier of b₁ ) & ( b₃ is closed implies (Int b₂) \/ b₃ = the carrier of b₁ ) )

proof end;

theorem Th7: :: TDLAT_3:7

for b₁ being TopSpace
for b₂ being Subset of b₁ holds
( ( b₂ is open & b₂ is closed ) iff Cl b₂ = Int b₂ )

proof end;

theorem Th8: :: TDLAT_3:8

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is open & b₂ is closed holds
Int (Cl b₂) = Cl (Int b₂)

proof end;

theorem Th9: :: TDLAT_3:9

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed & Cl (Int b₂) c= Int (Cl b₂) holds
( b₂ is open_condensed & b₂ is closed_condensed )

proof end;

theorem Th10: :: TDLAT_3:10

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed & Cl (Int b₂) c= Int (Cl b₂) holds
( b₂ is open & b₂ is closed )

proof end;

theorem Th11: :: TDLAT_3:11

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed holds
( Int (Cl b₂) = Int b₂ & Cl b₂ = Cl (Int b₂) )

proof end;

definition

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

end;

:: deftheorem Def1 defines discrete TDLAT_3:def 1 :

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

theorem Th12: :: TDLAT_3:12

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

proof end;

theorem Th13: :: TDLAT_3:13

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

proof end;

registration

cluster non empty strict discrete anti-discrete TopStruct ;
existence

proof end;

end;

theorem Th14: :: TDLAT_3:14

for b₁ being discrete TopStruct
for b₂ being Subset of b₁ holds the carrier of b₁ \ b₂ in the topology of b₁

proof end;

theorem Th15: :: TDLAT_3:15

for b₁ being anti-discrete TopStruct
for b₂ being Subset of b₁ st b₂ in the topology of b₁ holds
the carrier of b₁ \ b₂ in the topology of b₁

proof end;

registration

cluster discrete -> TopSpace-like TopStruct ;
coherence

proof end;

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

proof end;

end;

theorem Th16: :: TDLAT_3:16

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

proof end;

definition

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

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 b₁ being TopSpace holds
( b₁ is discrete iff for b₂ being Subset of b₁ holds b₂ is open )

proof end;

theorem Th18: :: TDLAT_3:18

for b₁ being TopSpace holds
( b₁ is discrete iff for b₂ being Subset of b₁ holds b₂ is closed )

proof end;

theorem Th19: :: TDLAT_3:19

for b₁ being TopSpace st ( for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ = {b₃} holds
b₂ is open ) holds
b₁ is discrete

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th20: :: TDLAT_3:20

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

proof end;

theorem Th21: :: TDLAT_3:21

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

proof end;

theorem Th22: :: TDLAT_3:22

for b₁ being TopSpace st ( for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ = {b₃} holds
Cl b₂ = the carrier of b₁ ) holds
b₁ is anti-discrete

proof end;

registration

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

proof end;

end;

registration

let c₁ be non empty anti-discrete TopSpace;
cluster TopSpace-like anti-discrete almost_discrete SubSpace of a₁;
existence

proof end;

end;

theorem Th23: :: TDLAT_3:23

for b₁ being TopSpace holds
( b₁ is almost_discrete iff for b₂ being Subset of b₁ st b₂ is open holds
b₂ is closed )

proof end;

theorem Th24: :: TDLAT_3:24

for b₁ being TopSpace holds
( b₁ is almost_discrete iff for b₂ being Subset of b₁ st b₂ is closed holds
b₂ is open )

proof end;

theorem Th25: :: TDLAT_3:25

for b₁ being TopSpace holds
( b₁ is almost_discrete iff for b₂ being Subset of b₁ st b₂ is open holds
Cl b₂ = b₂ )

proof end;

theorem Th26: :: TDLAT_3:26

for b₁ being TopSpace holds
( b₁ is almost_discrete iff for b₂ being Subset of b₁ st b₂ is closed holds
Int b₂ = b₂ )

proof end;

registration

cluster strict almost_discrete TopStruct ;
existence

proof end;

end;

theorem Th27: :: TDLAT_3:27

for b₁ being TopSpace st ( for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ = {b₃} holds
Cl b₂ is open ) holds
b₁ is almost_discrete

proof end;

theorem Th28: :: TDLAT_3:28

for b₁ being TopSpace holds
( b₁ is discrete iff ( b₁ is almost_discrete & ( for b₂ being Subset of b₁
for b₃ being Point of b₁ st b₂ = {b₃} holds
b₂ 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 c₁ be non empty almost_discrete TopSpace;
cluster non empty -> non empty almost_discrete SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty almost_discrete TopSpace;
cluster open -> closed SubSpace of a₁;
coherence

proof end;

cluster closed -> open SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty almost_discrete TopSpace;
cluster non empty strict almost_discrete SubSpace of a₁;
existence

proof end;

end;

definition

let c₁ be non empty TopSpace;
attr a₁ is extremally_disconnected means :Def4: :: TDLAT_3:def 4
for b₁ being Subset of a₁ st b₁ is open holds
Cl b₁ 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 b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ st b₂ is closed holds
Int b₂ is closed )

proof end;

theorem Th30: :: TDLAT_3:30

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is open & b₂ misses b₃ holds
Cl b₂ misses Cl b₃ )

proof end;

theorem Th31: :: TDLAT_3:31

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂, b₃ being Subset of b₁ st b₂ is closed & b₃ is closed & b₂ \/ b₃ = the carrier of b₁ holds
(Int b₂) \/ (Int b₃) = the carrier of b₁ )

proof end;

theorem Th32: :: TDLAT_3:32

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ st b₂ is open holds
Cl b₂ = Int (Cl b₂) )

proof end;

theorem Th33: :: TDLAT_3:33

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ st b₂ is closed holds
Int b₂ = Cl (Int b₂) )

proof end;

theorem Th34: :: TDLAT_3:34

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ st b₂ is condensed holds
( b₂ is closed & b₂ is open ) )

proof end;

theorem Th35: :: TDLAT_3:35

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ st b₂ is condensed holds
( b₂ is closed_condensed & b₂ is open_condensed ) )

proof end;

theorem Th36: :: TDLAT_3:36

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ st b₂ is condensed holds
Int (Cl b₂) = Cl (Int b₂) )

proof end;

theorem Th37: :: TDLAT_3:37

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ st b₂ is condensed holds
Int b₂ = Cl b₂ )

proof end;

theorem Th38: :: TDLAT_3:38

for b₁ being non empty TopSpace holds
( b₁ is extremally_disconnected iff for b₂ being Subset of b₁ holds
( ( b₂ is open_condensed implies b₂ is closed_condensed ) & ( b₂ is closed_condensed implies b₂ is open_condensed ) ) )

proof end;

definition

let c₁ be non empty TopSpace;
attr a₁ is hereditarily_extremally_disconnected means :Def5: :: TDLAT_3:def 5
for b₁ being non empty SubSpace of a₁ holds b₁ 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 b₁ being non empty extremally_disconnected TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ & b₃ is dense holds
b₂ is extremally_disconnected

proof end;

registration

let c₁ be non empty extremally_disconnected TopSpace;
cluster non empty open -> non empty extremally_disconnected SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty extremally_disconnected TopSpace;
cluster non empty strict extremally_disconnected SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty -> non empty extremally_disconnected hereditarily_extremally_disconnected SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty hereditarily_extremally_disconnected TopSpace;
cluster non empty strict extremally_disconnected hereditarily_extremally_disconnected SubSpace of a₁;
existence

proof end;

end;

theorem Th40: :: TDLAT_3:40

for b₁ being non empty TopSpace st ( for b₂ being non empty closed SubSpace of b₁ holds b₂ is extremally_disconnected ) holds
b₁ is hereditarily_extremally_disconnected

proof end;

theorem Th41: :: TDLAT_3:41

for b₁ being non empty extremally_disconnected TopSpace holds Domains_of b₁ = Closed_Domains_of b₁

proof end;

theorem Th42: :: TDLAT_3:42

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

proof end;

theorem Th43: :: TDLAT_3:43

for b₁ being non empty extremally_disconnected TopSpace holds Domains_Lattice b₁ = Closed_Domains_Lattice b₁

proof end;

theorem Th44: :: TDLAT_3:44

for b₁ being non empty extremally_disconnected TopSpace holds Domains_of b₁ = Open_Domains_of b₁

proof end;

theorem Th45: :: TDLAT_3:45

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

proof end;

theorem Th46: :: TDLAT_3:46

for b₁ being non empty extremally_disconnected TopSpace holds Domains_Lattice b₁ = Open_Domains_Lattice b₁

proof end;

theorem Th47: :: TDLAT_3:47

for b₁ being non empty extremally_disconnected TopSpace
for b₂, b₃ being Element of Domains_of b₁ holds
( (D-Union b₁) . b₂,b₃ = b₂ \/ b₃ & (D-Meet b₁) . b₂,b₃ = b₂ /\ b₃ )

proof end;

theorem Th48: :: TDLAT_3:48

for b₁ being non empty extremally_disconnected TopSpace
for b₂, b₃ being Element of (Domains_Lattice b₁)
for b₄, b₅ being Element of Domains_of b₁ st b₂ = b₄ & b₃ = b₅ holds
( b₂ "\/" b₃ = b₄ \/ b₅ & b₂ "/\" b₃ = b₄ /\ b₅ )

proof end;

theorem Th49: :: TDLAT_3:49

for b₁ being non empty extremally_disconnected TopSpace
for b₂ being Subset-Family of b₁ st b₂ is domains-family holds
for b₃ being Subset of (Domains_Lattice b₁) st b₃ = b₂ holds
"\/" b₃,(Domains_Lattice b₁) = Cl (union b₂)

proof end;

theorem Th50: :: TDLAT_3:50

proof end;

theorem Th51: :: TDLAT_3:51

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

proof end;

theorem Th52: :: TDLAT_3:52

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

theorem Th53: :: TDLAT_3:53

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

theorem Th54: :: TDLAT_3:54

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

proof end;

theorem Th55: :: TDLAT_3:55

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

proof end;