:: The Lattice of Domains_of of a Topological Space
:: by Toshihiko Watanabe
::
:: Received June 12, 1992
:: Copyright (c) 1992 Association of Mizar Users

begin

theorem Th1: :: TDLAT_1:1

for T being TopSpace
for A, B being Subset of T holds
( A \/ B = [#] T iff A ` c= B )

proof end;

theorem Th2: :: TDLAT_1:2

for T being TopSpace
for A, B being Subset of T holds
( A misses B iff B c= A ` )

proof end;

theorem Th3: :: TDLAT_1:3

for T being TopSpace
for A being Subset of T holds Cl (Int (Cl A)) c= Cl A

proof end;

theorem Th4: :: TDLAT_1:4

for T being TopSpace
for A being Subset of T holds Int A c= Int (Cl (Int A))

proof end;

theorem Th5: :: TDLAT_1:5

for T being TopSpace
for A being Subset of T holds Int (Cl A) = Int (Cl (Int (Cl A)))

proof end;

theorem Th6: :: TDLAT_1:6

for T being TopSpace
for A, B being Subset of T st ( A is closed or B is closed ) holds
(Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B))

proof end;

theorem Th7: :: TDLAT_1:7

for T being TopSpace
for A, B being Subset of T st ( A is open or B is open ) holds
(Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B))

proof end;

theorem Th8: :: TDLAT_1:8

for T being TopSpace
for A being Subset of T holds Int (A /\ (Cl (A `))) = {} T

proof end;

theorem Th9: :: TDLAT_1:9

for T being TopSpace
for A being Subset of T holds Cl (A \/ (Int (A `))) = [#] T

proof end;

theorem Th10: :: TDLAT_1:10

for T being TopSpace
for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B)

proof end;

theorem :: TDLAT_1:11

for T being TopSpace
for A, C being Subset of T holds (Int (Cl (((Int (Cl A)) \/ A) \/ C))) \/ (((Int (Cl A)) \/ A) \/ C) = (Int (Cl (A \/ C))) \/ (A \/ C) by Th10;

theorem Th12: :: TDLAT_1:12

for T being TopSpace
for A, B being Subset of T holds (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B)

proof end;

theorem :: TDLAT_1:13

for T being TopSpace
for A, C being Subset of T holds (Cl (Int (((Cl (Int A)) /\ A) /\ C))) /\ (((Cl (Int A)) /\ A) /\ C) = (Cl (Int (A /\ C))) /\ (A /\ C) by Th12;

begin

theorem Th14: :: TDLAT_1:14

for T being TopSpace holds {} T is condensed

proof end;

theorem Th15: :: TDLAT_1:15

for T being TopSpace holds [#] T is condensed

proof end;

theorem Th16: :: TDLAT_1:16

for T being TopSpace
for A being Subset of T st A is condensed holds
A ` is condensed

proof end;

theorem Th17: :: TDLAT_1:17

for T being TopSpace
for A, B being Subset of T st A is condensed & B is condensed holds
( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed )

proof end;

theorem Th18: :: TDLAT_1:18

for T being TopSpace holds {} T is closed_condensed

proof end;

theorem Th19: :: TDLAT_1:19

for T being TopSpace holds [#] T is closed_condensed

proof end;

theorem Th20: :: TDLAT_1:20

for T being TopSpace holds {} T is open_condensed

proof end;

theorem Th21: :: TDLAT_1:21

for T being TopSpace holds [#] T is open_condensed

proof end;

theorem Th22: :: TDLAT_1:22

for T being TopSpace
for A being Subset of T holds Cl (Int A) is closed_condensed

proof end;

theorem Th23: :: TDLAT_1:23

for T being TopSpace
for A being Subset of T holds Int (Cl A) is open_condensed

proof end;

theorem Th24: :: TDLAT_1:24

for T being TopSpace
for A being Subset of T st A is condensed holds
Cl A is closed_condensed

proof end;

theorem Th25: :: TDLAT_1:25

for T being TopSpace
for A being Subset of T st A is condensed holds
Int A is open_condensed

proof end;

theorem :: TDLAT_1:26

for T being TopSpace
for A being Subset of T st A is condensed holds
Cl (A `) is closed_condensed by Th16, Th24;

theorem :: TDLAT_1:27

for T being TopSpace
for A being Subset of T st A is condensed holds
Int (A `) is open_condensed by Th16, Th25;

theorem Th28: :: TDLAT_1:28

for T being TopSpace
for A, B, C being Subset of T st A is closed_condensed & B is closed_condensed & C is closed_condensed holds
Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C))

proof end;

theorem Th29: :: TDLAT_1:29

for T being TopSpace
for A, B, C being Subset of T st A is open_condensed & B is open_condensed & C is open_condensed holds
Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C))

proof end;

begin

definition

let T be TopStruct ;
func Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 1
{ A where A is Subset of T : A is condensed } ;
coherence
{ A where A is Subset of T : A is condensed } is Subset-Family of T

proof end;

end;

:: deftheorem defines Domains_of TDLAT_1:def 1 :
for T being TopStruct holds Domains_of T = { A where A is Subset of T : A is condensed } ;

registration

let T be TopSpace;
cluster Domains_of T -> non empty ;
coherence
not Domains_of T is empty

proof end;

end;

definition

let T be TopSpace;
func Domains_Union T -> BinOp of (Domains_of T) means :Def2: :: TDLAT_1:def 2
for A, B being Element of Domains_of T holds it . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B);
existence
ex b₁ being BinOp of (Domains_of T) st
for A, B being Element of Domains_of T holds b₁ . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b₁ . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) & ( for A, B being Element of Domains_of T holds b₂ . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Domains_Union TDLAT_1:def 2 :
for T being TopSpace
for b₂ being BinOp of (Domains_of T) holds
( b₂ = Domains_Union T iff for A, B being Element of Domains_of T holds b₂ . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) );

notation

let T be TopSpace;
synonym D-Union T for Domains_Union T;

end;

definition

let T be TopSpace;
func Domains_Meet T -> BinOp of (Domains_of T) means :Def3: :: TDLAT_1:def 3
for A, B being Element of Domains_of T holds it . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B);
existence
ex b₁ being BinOp of (Domains_of T) st
for A, B being Element of Domains_of T holds b₁ . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b₁ . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) & ( for A, B being Element of Domains_of T holds b₂ . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Domains_Meet TDLAT_1:def 3 :
for T being TopSpace
for b₂ being BinOp of (Domains_of T) holds
( b₂ = Domains_Meet T iff for A, B being Element of Domains_of T holds b₂ . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) );

notation

let T be TopSpace;
synonym D-Meet T for Domains_Meet T;

end;

theorem Th30: :: TDLAT_1:30

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

proof end;

definition

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

end;

:: deftheorem defines Domains_Lattice TDLAT_1:def 4 :
for T being TopSpace holds Domains_Lattice T = LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #);

begin

definition

let T be TopStruct ;
func Closed_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 5
{ A where A is Subset of T : A is closed_condensed } ;
coherence
{ A where A is Subset of T : A is closed_condensed } is Subset-Family of T

proof end;

end;

:: deftheorem defines Closed_Domains_of TDLAT_1:def 5 :
for T being TopStruct holds Closed_Domains_of T = { A where A is Subset of T : A is closed_condensed } ;

registration

let T be TopSpace;
cluster Closed_Domains_of T -> non empty ;
coherence
not Closed_Domains_of T is empty

proof end;

end;

theorem :: TDLAT_1:31

for T being TopSpace holds Closed_Domains_of T c= Domains_of T ;

definition

let T be TopSpace;
func Closed_Domains_Union T -> BinOp of (Closed_Domains_of T) means :Def6: :: TDLAT_1:def 6
for A, B being Element of Closed_Domains_of T holds it . (A,B) = A \/ B;
existence
ex b₁ being BinOp of (Closed_Domains_of T) st
for A, B being Element of Closed_Domains_of T holds b₁ . (A,B) = A \/ B

proof end;

uniqueness
for b₁, b₂ being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b₁ . (A,B) = A \/ B ) & ( for A, B being Element of Closed_Domains_of T holds b₂ . (A,B) = A \/ B ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Closed_Domains_Union TDLAT_1:def 6 :
for T being TopSpace
for b₂ being BinOp of (Closed_Domains_of T) holds
( b₂ = Closed_Domains_Union T iff for A, B being Element of Closed_Domains_of T holds b₂ . (A,B) = A \/ B );

notation

let T be TopSpace;
synonym CLD-Union T for Closed_Domains_Union T;

end;

theorem Th32: :: TDLAT_1:32

for T being TopSpace
for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B)

proof end;

definition

let T be TopSpace;
func Closed_Domains_Meet T -> BinOp of (Closed_Domains_of T) means :Def7: :: TDLAT_1:def 7
for A, B being Element of Closed_Domains_of T holds it . (A,B) = Cl (Int (A /\ B));
existence
ex b₁ being BinOp of (Closed_Domains_of T) st
for A, B being Element of Closed_Domains_of T holds b₁ . (A,B) = Cl (Int (A /\ B))

proof end;

uniqueness
for b₁, b₂ being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b₁ . (A,B) = Cl (Int (A /\ B)) ) & ( for A, B being Element of Closed_Domains_of T holds b₂ . (A,B) = Cl (Int (A /\ B)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def 7 :
for T being TopSpace
for b₂ being BinOp of (Closed_Domains_of T) holds
( b₂ = Closed_Domains_Meet T iff for A, B being Element of Closed_Domains_of T holds b₂ . (A,B) = Cl (Int (A /\ B)) );

notation

let T be TopSpace;
synonym CLD-Meet T for Closed_Domains_Meet T;

end;

theorem Th33: :: TDLAT_1:33

for T being TopSpace
for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B)

proof end;

theorem Th34: :: TDLAT_1:34

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

proof end;

definition

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

end;

:: deftheorem defines Closed_Domains_Lattice TDLAT_1:def 8 :
for T being TopSpace holds Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #);

begin

definition

let T be TopStruct ;
func Open_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 9
{ A where A is Subset of T : A is open_condensed } ;
coherence
{ A where A is Subset of T : A is open_condensed } is Subset-Family of T

proof end;

end;

:: deftheorem defines Open_Domains_of TDLAT_1:def 9 :
for T being TopStruct holds Open_Domains_of T = { A where A is Subset of T : A is open_condensed } ;

registration

let T be TopSpace;
cluster Open_Domains_of T -> non empty ;
coherence
not Open_Domains_of T is empty

proof end;

end;

theorem :: TDLAT_1:35

for T being TopSpace holds Open_Domains_of T c= Domains_of T ;

definition

let T be TopSpace;
func Open_Domains_Union T -> BinOp of (Open_Domains_of T) means :Def10: :: TDLAT_1:def 10
for A, B being Element of Open_Domains_of T holds it . (A,B) = Int (Cl (A \/ B));
existence
ex b₁ being BinOp of (Open_Domains_of T) st
for A, B being Element of Open_Domains_of T holds b₁ . (A,B) = Int (Cl (A \/ B))

proof end;

uniqueness
for b₁, b₂ being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b₁ . (A,B) = Int (Cl (A \/ B)) ) & ( for A, B being Element of Open_Domains_of T holds b₂ . (A,B) = Int (Cl (A \/ B)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def 10 :
for T being TopSpace
for b₂ being BinOp of (Open_Domains_of T) holds
( b₂ = Open_Domains_Union T iff for A, B being Element of Open_Domains_of T holds b₂ . (A,B) = Int (Cl (A \/ B)) );

notation

let T be TopSpace;
synonym OPD-Union T for Open_Domains_Union T;

end;

theorem Th36: :: TDLAT_1:36

for T being TopSpace
for A, B being Element of Open_Domains_of T holds (OPD-Union T) . (A,B) = (D-Union T) . (A,B)

proof end;

definition

let T be TopSpace;
func Open_Domains_Meet T -> BinOp of (Open_Domains_of T) means :Def11: :: TDLAT_1:def 11
for A, B being Element of Open_Domains_of T holds it . (A,B) = A /\ B;
existence
ex b₁ being BinOp of (Open_Domains_of T) st
for A, B being Element of Open_Domains_of T holds b₁ . (A,B) = A /\ B

proof end;

uniqueness
for b₁, b₂ being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b₁ . (A,B) = A /\ B ) & ( for A, B being Element of Open_Domains_of T holds b₂ . (A,B) = A /\ B ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines Open_Domains_Meet TDLAT_1:def 11 :
for T being TopSpace
for b₂ being BinOp of (Open_Domains_of T) holds
( b₂ = Open_Domains_Meet T iff for A, B being Element of Open_Domains_of T holds b₂ . (A,B) = A /\ B );

notation

let T be TopSpace;
synonym OPD-Meet T for Open_Domains_Meet T;

end;

theorem Th37: :: TDLAT_1:37

for T being TopSpace
for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B)

proof end;

theorem Th38: :: TDLAT_1:38

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

proof end;

definition

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

end;

:: deftheorem defines Open_Domains_Lattice TDLAT_1:def 12 :
for T being TopSpace holds Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);

begin

theorem Th39: :: TDLAT_1:39

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

proof end;

theorem Th40: :: TDLAT_1:40

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

proof end;

theorem :: TDLAT_1:41

for T being TopSpace holds Closed_Domains_Lattice T is SubLattice of Domains_Lattice T

proof end;

theorem Th42: :: TDLAT_1:42

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

proof end;

theorem Th43: :: TDLAT_1:43

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

proof end;

theorem :: TDLAT_1:44

for T being TopSpace holds Open_Domains_Lattice T is SubLattice of Domains_Lattice T

proof end;