:: TDLAT_1 semantic presentation

theorem Th1: :: TDLAT_1:1

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂ \/ b₃ = [#] b₁ iff b₂ ` c= b₃ )

proof end;

theorem Th2: :: TDLAT_1:2

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds
( b₂ misses b₃ iff b₃ c= b₂ ` )

proof end;

theorem Th3: :: TDLAT_1:3

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

proof end;

theorem Th4: :: TDLAT_1:4

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

proof end;

theorem Th5: :: TDLAT_1:5

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

proof end;

theorem Th6: :: TDLAT_1:6

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st ( b₂ is closed or b₃ is closed ) holds
(Cl (Int b₂)) \/ (Cl (Int b₃)) = Cl (Int (b₂ \/ b₃))

proof end;

theorem Th7: :: TDLAT_1:7

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st ( b₂ is open or b₃ is open ) holds
(Int (Cl b₂)) /\ (Int (Cl b₃)) = Int (Cl (b₂ /\ b₃))

proof end;

theorem Th8: :: TDLAT_1:8

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Int (b₂ /\ (Cl (b₂ ` ))) = {} b₁

proof end;

theorem Th9: :: TDLAT_1:9

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Cl (b₂ \/ (Int (b₂ ` ))) = [#] b₁

proof end;

theorem Th10: :: TDLAT_1:10

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Int (Cl (b₂ \/ ((Int (Cl b₃)) \/ b₃)))) \/ (b₂ \/ ((Int (Cl b₃)) \/ b₃)) = (Int (Cl (b₂ \/ b₃))) \/ (b₂ \/ b₃)

proof end;

theorem Th11: :: TDLAT_1:11

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Int (Cl (((Int (Cl b₂)) \/ b₂) \/ b₃))) \/ (((Int (Cl b₂)) \/ b₂) \/ b₃) = (Int (Cl (b₂ \/ b₃))) \/ (b₂ \/ b₃) by Th10;

theorem Th12: :: TDLAT_1:12

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Cl (Int (b₂ /\ ((Cl (Int b₃)) /\ b₃)))) /\ (b₂ /\ ((Cl (Int b₃)) /\ b₃)) = (Cl (Int (b₂ /\ b₃))) /\ (b₂ /\ b₃)

proof end;

theorem Th13: :: TDLAT_1:13

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds (Cl (Int (((Cl (Int b₂)) /\ b₂) /\ b₃))) /\ (((Cl (Int b₂)) /\ b₂) /\ b₃) = (Cl (Int (b₂ /\ b₃))) /\ (b₂ /\ b₃) by Th12;

theorem Th14: :: TDLAT_1:14

for b₁ being TopSpace holds {} b₁ is condensed

proof end;

theorem Th15: :: TDLAT_1:15

for b₁ being TopSpace holds [#] b₁ is condensed

proof end;

theorem Th16: :: TDLAT_1:16

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed holds
b₂ ` is condensed

proof end;

theorem Th17: :: TDLAT_1:17

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is condensed & b₃ is condensed holds
( (Int (Cl (b₂ \/ b₃))) \/ (b₂ \/ b₃) is condensed & (Cl (Int (b₂ /\ b₃))) /\ (b₂ /\ b₃) is condensed )

proof end;

theorem Th18: :: TDLAT_1:18

for b₁ being TopSpace holds {} b₁ is closed_condensed

proof end;

theorem Th19: :: TDLAT_1:19

for b₁ being TopSpace holds [#] b₁ is closed_condensed

proof end;

theorem Th20: :: TDLAT_1:20

for b₁ being TopSpace holds {} b₁ is open_condensed

proof end;

theorem Th21: :: TDLAT_1:21

for b₁ being TopSpace holds [#] b₁ is open_condensed

proof end;

theorem Th22: :: TDLAT_1:22

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Cl (Int b₂) is closed_condensed

proof end;

theorem Th23: :: TDLAT_1:23

for b₁ being TopSpace
for b₂ being Subset of b₁ holds Int (Cl b₂) is open_condensed

proof end;

theorem Th24: :: TDLAT_1:24

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed holds
Cl b₂ is closed_condensed

proof end;

theorem Th25: :: TDLAT_1:25

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed holds
Int b₂ is open_condensed

proof end;

theorem Th26: :: TDLAT_1:26

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed holds
Cl (b₂ ` ) is closed_condensed

proof end;

theorem Th27: :: TDLAT_1:27

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₂ is condensed holds
Int (b₂ ` ) is open_condensed

proof end;

theorem Th28: :: TDLAT_1:28

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is closed_condensed & b₃ is closed_condensed & b₄ is closed_condensed holds
Cl (Int (b₂ /\ (Cl (Int (b₃ /\ b₄))))) = Cl (Int ((Cl (Int (b₂ /\ b₃))) /\ b₄))

proof end;

theorem Th29: :: TDLAT_1:29

for b₁ being TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is open_condensed & b₃ is open_condensed & b₄ is open_condensed holds
Int (Cl (b₂ \/ (Int (Cl (b₃ \/ b₄))))) = Int (Cl ((Int (Cl (b₂ \/ b₃))) \/ b₄))

proof end;

definition

let c₁ be TopStruct ;
func Domains_of c₁ -> Subset-Family of a₁ equals :: TDLAT_1:def 1
{ b₁ where B is Subset of a₁ : b₁ is condensed } ;
coherence

proof end;

end;

:: deftheorem Def1 defines Domains_of TDLAT_1:def 1 :

registration

let c₁ be TopSpace;
cluster Domains_of a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be TopSpace;
func Domains_Union c₁ -> BinOp of Domains_of a₁ means :Def2: :: TDLAT_1:def 2
for b₁, b₂ being Element of Domains_of a₁ holds a₂ . b₁,b₂ = (Int (Cl (b₁ \/ b₂))) \/ (b₁ \/ b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Domains_Union TDLAT_1:def 2 :

notation

let c₁ be TopSpace;
synonym D-Union c₁ for Domains_Union c₁;

end;

definition

let c₁ be TopSpace;
func Domains_Meet c₁ -> BinOp of Domains_of a₁ means :Def3: :: TDLAT_1:def 3
for b₁, b₂ being Element of Domains_of a₁ holds a₂ . b₁,b₂ = (Cl (Int (b₁ /\ b₂))) /\ (b₁ /\ b₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Domains_Meet TDLAT_1:def 3 :

notation

let c₁ be TopSpace;
synonym D-Meet c₁ for Domains_Meet c₁;

end;

theorem Th30: :: TDLAT_1:30

for b₁ being TopSpace holds LattStr(# (Domains_of b₁),(D-Union b₁),(D-Meet b₁) #) is C_Lattice

proof end;

definition

let c₁ be TopSpace;
func Domains_Lattice c₁ -> C_Lattice equals :: TDLAT_1:def 4
LattStr(# (Domains_of a₁),(Domains_Union a₁),(Domains_Meet a₁) #);
coherence by Th30;

end;

:: deftheorem Def4 defines Domains_Lattice TDLAT_1:def 4 :

definition

let c₁ be TopStruct ;
func Closed_Domains_of c₁ -> Subset-Family of a₁ equals :: TDLAT_1:def 5
{ b₁ where B is Subset of a₁ : b₁ is closed_condensed } ;
coherence

proof end;

end;

:: deftheorem Def5 defines Closed_Domains_of TDLAT_1:def 5 :

registration

let c₁ be TopSpace;
cluster Closed_Domains_of a₁ -> non empty ;
coherence

proof end;

end;

theorem Th31: :: TDLAT_1:31

for b₁ being TopSpace holds Closed_Domains_of b₁ c= Domains_of b₁ ;

definition

let c₁ be TopSpace;
func Closed_Domains_Union c₁ -> BinOp of Closed_Domains_of a₁ means :Def6: :: TDLAT_1:def 6
for b₁, b₂ being Element of Closed_Domains_of a₁ holds a₂ . b₁,b₂ = b₁ \/ b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Closed_Domains_Union TDLAT_1:def 6 :

notation

let c₁ be TopSpace;
synonym CLD-Union c₁ for Closed_Domains_Union c₁;

end;

theorem Th32: :: TDLAT_1:32

for b₁ being TopSpace
for b₂, b₃ being Element of Closed_Domains_of b₁ holds (CLD-Union b₁) . b₂,b₃ = (D-Union b₁) . b₂,b₃

proof end;

definition

let c₁ be TopSpace;
func Closed_Domains_Meet c₁ -> BinOp of Closed_Domains_of a₁ means :Def7: :: TDLAT_1:def 7
for b₁, b₂ being Element of Closed_Domains_of a₁ holds a₂ . b₁,b₂ = Cl (Int (b₁ /\ b₂));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def 7 :

notation

let c₁ be TopSpace;
synonym CLD-Meet c₁ for Closed_Domains_Meet c₁;

end;

theorem Th33: :: TDLAT_1:33

for b₁ being TopSpace
for b₂, b₃ being Element of Closed_Domains_of b₁ holds (CLD-Meet b₁) . b₂,b₃ = (D-Meet b₁) . b₂,b₃

proof end;

theorem Th34: :: TDLAT_1:34

for b₁ being TopSpace holds LattStr(# (Closed_Domains_of b₁),(CLD-Union b₁),(CLD-Meet b₁) #) is B_Lattice

proof end;

definition

let c₁ be TopSpace;
func Closed_Domains_Lattice c₁ -> B_Lattice equals :: TDLAT_1:def 8
LattStr(# (Closed_Domains_of a₁),(Closed_Domains_Union a₁),(Closed_Domains_Meet a₁) #);
coherence by Th34;

end;

:: deftheorem Def8 defines Closed_Domains_Lattice TDLAT_1:def 8 :

definition

let c₁ be TopStruct ;
func Open_Domains_of c₁ -> Subset-Family of a₁ equals :: TDLAT_1:def 9
{ b₁ where B is Subset of a₁ : b₁ is open_condensed } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Open_Domains_of TDLAT_1:def 9 :

registration

let c₁ be TopSpace;
cluster Open_Domains_of a₁ -> non empty ;
coherence

proof end;

end;

theorem Th35: :: TDLAT_1:35

for b₁ being TopSpace holds Open_Domains_of b₁ c= Domains_of b₁ ;

definition

let c₁ be TopSpace;
func Open_Domains_Union c₁ -> BinOp of Open_Domains_of a₁ means :Def10: :: TDLAT_1:def 10
for b₁, b₂ being Element of Open_Domains_of a₁ holds a₂ . b₁,b₂ = Int (Cl (b₁ \/ b₂));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def 10 :

notation

let c₁ be TopSpace;
synonym OPD-Union c₁ for Open_Domains_Union c₁;

end;

theorem Th36: :: TDLAT_1:36

for b₁ being TopSpace
for b₂, b₃ being Element of Open_Domains_of b₁ holds (OPD-Union b₁) . b₂,b₃ = (D-Union b₁) . b₂,b₃

proof end;

definition

let c₁ be TopSpace;
func Open_Domains_Meet c₁ -> BinOp of Open_Domains_of a₁ means :Def11: :: TDLAT_1:def 11
for b₁, b₂ being Element of Open_Domains_of a₁ holds a₂ . b₁,b₂ = b₁ /\ b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Open_Domains_Meet TDLAT_1:def 11 :

notation

let c₁ be TopSpace;
synonym OPD-Meet c₁ for Open_Domains_Meet c₁;

end;

theorem Th37: :: TDLAT_1:37

for b₁ being TopSpace
for b₂, b₃ being Element of Open_Domains_of b₁ holds (OPD-Meet b₁) . b₂,b₃ = (D-Meet b₁) . b₂,b₃

proof end;

theorem Th38: :: TDLAT_1:38

for b₁ being TopSpace holds LattStr(# (Open_Domains_of b₁),(OPD-Union b₁),(OPD-Meet b₁) #) is B_Lattice

proof end;

definition

let c₁ be TopSpace;
func Open_Domains_Lattice c₁ -> B_Lattice equals :: TDLAT_1:def 12
LattStr(# (Open_Domains_of a₁),(Open_Domains_Union a₁),(Open_Domains_Meet a₁) #);
coherence by Th38;

end;

:: deftheorem Def12 defines Open_Domains_Lattice TDLAT_1:def 12 :

theorem Th39: :: TDLAT_1:39

for b₁ being TopSpace holds CLD-Union b₁ = (D-Union b₁) || (Closed_Domains_of b₁)

proof end;

theorem Th40: :: TDLAT_1:40

for b₁ being TopSpace holds CLD-Meet b₁ = (D-Meet b₁) || (Closed_Domains_of b₁)

proof end;

theorem Th41: :: TDLAT_1:41

for b₁ being TopSpace holds Closed_Domains_Lattice b₁ is SubLattice of Domains_Lattice b₁

proof end;

theorem Th42: :: TDLAT_1:42

for b₁ being TopSpace holds OPD-Union b₁ = (D-Union b₁) || (Open_Domains_of b₁)

proof end;

theorem Th43: :: TDLAT_1:43

for b₁ being TopSpace holds OPD-Meet b₁ = (D-Meet b₁) || (Open_Domains_of b₁)

proof end;

theorem Th44: :: TDLAT_1:44

for b₁ being TopSpace holds Open_Domains_Lattice b₁ is SubLattice of Domains_Lattice b₁

proof end;