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


begin

theorem Th1: :: TDLAT_1:1
for T being 1-sorted
for A, B being Subset of T holds
( A \/ B = [#] T iff A ` c= B )
proofend;

theorem Th2: :: TDLAT_1:2
for T being 1-sorted
for A, B being Subset of T holds
( A misses B iff B c= A ` ) by SUBSET_1:23;

theorem Th3: :: TDLAT_1:3
for T being TopSpace
for A being Subset of T holds Cl (Int (Cl A)) c= Cl A
proofend;

theorem Th4: :: TDLAT_1:4
for T being TopSpace
for A being Subset of T holds Int A c= Int (Cl (Int A))
proofend;

theorem Th5: :: TDLAT_1:5
for T being TopSpace
for A being Subset of T holds Int (Cl A) = Int (Cl (Int (Cl A)))
proofend;

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))
proofend;

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))
proofend;

theorem Th8: :: TDLAT_1:8
for T being TopSpace
for A being Subset of T holds Int (A /\ (Cl (A `))) = {} T
proofend;

theorem Th9: :: TDLAT_1:9
for T being TopSpace
for A being Subset of T holds Cl (A \/ (Int (A `))) = [#] T
proofend;

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)
proofend;

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)
proofend;

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

:: 2. Properties of Domains_of of Topological Spaces.
theorem Th14: :: TDLAT_1:14
for T being TopSpace holds {} T is condensed
proofend;

theorem Th15: :: TDLAT_1:15
for T being TopSpace holds [#] T is condensed
proofend;

theorem Th16: :: TDLAT_1:16
for T being TopSpace
for A being Subset of T st A is condensed holds
A ` is condensed
proofend;

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 )
proofend;

theorem Th18: :: TDLAT_1:18
for T being TopSpace holds {} T is closed_condensed
proofend;

theorem Th19: :: TDLAT_1:19
for T being TopSpace holds [#] T is closed_condensed
proofend;

theorem Th20: :: TDLAT_1:20
for T being TopSpace holds {} T is open_condensed
proofend;

theorem Th21: :: TDLAT_1:21
for T being TopSpace holds [#] T is open_condensed
proofend;

theorem Th22: :: TDLAT_1:22
for T being TopSpace
for A being Subset of T holds Cl (Int A) is closed_condensed
proofend;

theorem Th23: :: TDLAT_1:23
for T being TopSpace
for A being Subset of T holds Int (Cl A) is open_condensed
proofend;

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
proofend;

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
proofend;

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))
proofend;

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))
proofend;

begin

:: 3. The Lattice of Domains.
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
proofend;
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
proofend;
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 b1 being BinOp of (Domains_of T) st
for A, B being Element of Domains_of T holds b1 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B)
proofend;
uniqueness
 for b1, b2 being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b1 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) & ( for A, B being Element of Domains_of T holds b2 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Domains_Union TDLAT_1:def_2_:_
 for T being TopSpace
for b2 being BinOp of (Domains_of T) holds
( b2 = Domains_Union T iff for A, B being Element of Domains_of T holds b2 . (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 b1 being BinOp of (Domains_of T) st
for A, B being Element of Domains_of T holds b1 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B)
proofend;
uniqueness
 for b1, b2 being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b1 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) & ( for A, B being Element of Domains_of T holds b2 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Domains_Meet TDLAT_1:def_3_:_
 for T being TopSpace
for b2 being BinOp of (Domains_of T) holds
( b2 = Domains_Meet T iff for A, B being Element of Domains_of T holds b2 . (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
proofend;

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

:: 4. The Lattice of Closed Domains.
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
proofend;
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
proofend;
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 b1 being BinOp of (Closed_Domains_of T) st
for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = A \/ B
proofend;
uniqueness
 for b1, b2 being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = A \/ B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines Closed_Domains_Union TDLAT_1:def_6_:_
 for T being TopSpace
for b2 being BinOp of (Closed_Domains_of T) holds
( b2 = Closed_Domains_Union T iff for A, B being Element of Closed_Domains_of T holds b2 . (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)
proofend;

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 b1 being BinOp of (Closed_Domains_of T) st
for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = Cl (Int (A /\ B))
proofend;
uniqueness
 for b1, b2 being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = Cl (Int (A /\ B)) ) & ( for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = Cl (Int (A /\ B)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def_7_:_
 for T being TopSpace
for b2 being BinOp of (Closed_Domains_of T) holds
( b2 = Closed_Domains_Meet T iff for A, B being Element of Closed_Domains_of T holds b2 . (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)
proofend;

theorem Th34: :: TDLAT_1:34
for T being TopSpace holds LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice
proofend;

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

:: 5. The Lattice of Open Domains.
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
proofend;
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
proofend;
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 b1 being BinOp of (Open_Domains_of T) st
for A, B being Element of Open_Domains_of T holds b1 . (A,B) = Int (Cl (A \/ B))
proofend;
uniqueness
 for b1, b2 being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b1 . (A,B) = Int (Cl (A \/ B)) ) & ( for A, B being Element of Open_Domains_of T holds b2 . (A,B) = Int (Cl (A \/ B)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def_10_:_
 for T being TopSpace
for b2 being BinOp of (Open_Domains_of T) holds
( b2 = Open_Domains_Union T iff for A, B being Element of Open_Domains_of T holds b2 . (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)
proofend;

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 b1 being BinOp of (Open_Domains_of T) st
for A, B being Element of Open_Domains_of T holds b1 . (A,B) = A /\ B
proofend;
uniqueness
 for b1, b2 being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of Open_Domains_of T holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines Open_Domains_Meet TDLAT_1:def_11_:_
 for T being TopSpace
for b2 being BinOp of (Open_Domains_of T) holds
( b2 = Open_Domains_Meet T iff for A, B being Element of Open_Domains_of T holds b2 . (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)
proofend;

theorem Th38: :: TDLAT_1:38
for T being TopSpace holds LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice
proofend;

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

:: 6. Connections between Lattices of Domains.
theorem Th39: :: TDLAT_1:39
for T being TopSpace holds CLD-Union T = (D-Union T) || (Closed_Domains_of T)
proofend;

theorem Th40: :: TDLAT_1:40
for T being TopSpace holds CLD-Meet T = (D-Meet T) || (Closed_Domains_of T)
proofend;

theorem :: TDLAT_1:41
for T being TopSpace holds Closed_Domains_Lattice T is SubLattice of Domains_Lattice T
proofend;

theorem Th42: :: TDLAT_1:42
for T being TopSpace holds OPD-Union T = (D-Union T) || (Open_Domains_of T)
proofend;

theorem Th43: :: TDLAT_1:43
for T being TopSpace holds OPD-Meet T = (D-Meet T) || (Open_Domains_of T)
proofend;

theorem :: TDLAT_1:44
for T being TopSpace holds Open_Domains_Lattice T is SubLattice of Domains_Lattice T
proofend;