:: The Lattice of Domains of a Topological Space :: by Toshihiko Watanabe :: :: Received June 12, 1992 :: Copyright (c) 1992-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies PRE_TOPC, SUBSET_1, XBOOLE_0, TARSKI, TOPS_1, RCOMP_1, SETFAM_1, ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, MCART_1, LATTICES, EQREL_1, REALSET1, NAT_LAT, TDLAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, STRUCT_0, PRE_TOPC, LATTICES, BINOP_1, TOPS_1, FUNCT_1, DOMAIN_1, FUNCT_2, NAT_LAT; constructors PARTFUN1, BINOP_1, REALSET1, TOPS_1, NAT_LAT; registrations SUBSET_1, REALSET1, LATTICES, TOPS_1, RELAT_1, PRE_TOPC; requirements BOOLE, SUBSET; begin :: 1. Preliminary Theorems on Subsets of Topological Spaces. reserve T for 1-sorted; theorem :: TDLAT_1:1 for A,B being Subset of T holds A \/ B = [#] T iff A` c= B; theorem :: TDLAT_1:2 for A,B being Subset of T holds A misses B iff B c= A`; reserve T for TopSpace; theorem :: TDLAT_1:3 for A being Subset of T holds Cl Int Cl A c= Cl A; theorem :: TDLAT_1:4 for A being Subset of T holds Int A c= Int Cl Int A; theorem :: TDLAT_1:5 for A being Subset of T holds Int Cl A = Int Cl Int Cl A; theorem :: TDLAT_1:6 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); theorem :: TDLAT_1:7 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); theorem :: TDLAT_1:8 for A being Subset of T holds Int(A /\ Cl A`) = {} T; theorem :: TDLAT_1:9 for A being Subset of T holds Cl(A \/ Int A`) = [#] T; theorem :: TDLAT_1:10 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); theorem :: TDLAT_1:11 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); theorem :: TDLAT_1:12 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); theorem :: TDLAT_1:13 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); begin :: 2. Properties of Domains_of of Topological Spaces. theorem :: TDLAT_1:14 {}T is condensed; theorem :: TDLAT_1:15 [#] T is condensed; theorem :: TDLAT_1:16 for A being Subset of T st A is condensed holds A` is condensed; theorem :: TDLAT_1:17 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; theorem :: TDLAT_1:18 {} T is closed_condensed; theorem :: TDLAT_1:19 [#] T is closed_condensed; theorem :: TDLAT_1:20 {} T is open_condensed; theorem :: TDLAT_1:21 [#] T is open_condensed; theorem :: TDLAT_1:22 for A being Subset of T holds Cl(Int A) is closed_condensed; theorem :: TDLAT_1:23 for A being Subset of T holds Int(Cl A) is open_condensed; theorem :: TDLAT_1:24 for A being Subset of T st A is condensed holds Cl A is closed_condensed; theorem :: TDLAT_1:25 for A being Subset of T st A is condensed holds Int A is open_condensed; theorem :: TDLAT_1:26 for A being Subset of T st A is condensed holds Cl A` is closed_condensed; theorem :: TDLAT_1:27 for A being Subset of T st A is condensed holds Int A` is open_condensed; theorem :: TDLAT_1:28 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))); theorem :: TDLAT_1:29 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))); 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 }; end; registration let T be TopSpace; cluster Domains_of T -> non empty; end; definition let T be TopSpace; func Domains_Union T -> BinOp of Domains_of T means :: TDLAT_1:def 2 for A,B being Element of Domains_of T holds it.(A,B) = Int(Cl(A \/ B)) \/ (A \/ B); end; 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 :: TDLAT_1:def 3 for A,B being Element of Domains_of T holds it.(A,B) = Cl(Int(A /\ B)) /\ (A /\ B); end; notation let T be TopSpace; synonym D-Meet T for Domains_Meet T; end; theorem :: TDLAT_1:30 for T being TopSpace holds LattStr(#Domains_of T,D-Union T, D-Meet T#) is C_Lattice; 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#); end; 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 }; end; registration let T be TopSpace; cluster Closed_Domains_of T -> non empty; 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 :: TDLAT_1:def 6 for A,B being Element of Closed_Domains_of T holds it.(A,B) = A \/ B; end; notation let T be TopSpace; synonym CLD-Union T for Closed_Domains_Union T; end; theorem :: TDLAT_1:32 for A,B being Element of Closed_Domains_of T holds (CLD-Union T) .(A,B) = (D-Union T).(A,B); definition let T be TopSpace; func Closed_Domains_Meet T -> BinOp of Closed_Domains_of T means :: TDLAT_1:def 7 for A,B being Element of Closed_Domains_of T holds it.(A,B) = Cl(Int(A /\ B)); end; notation let T be TopSpace; synonym CLD-Meet T for Closed_Domains_Meet T; end; theorem :: TDLAT_1:33 for A,B being Element of Closed_Domains_of T holds (CLD-Meet T). (A,B) = (D-Meet T).(A,B); theorem :: TDLAT_1:34 for T being TopSpace holds LattStr(#Closed_Domains_of T, CLD-Union T,CLD-Meet T#) is B_Lattice; 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 #); end; 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 }; end; registration let T be TopSpace; cluster Open_Domains_of T -> non empty; 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 :: TDLAT_1:def 10 for A, B being Element of Open_Domains_of T holds it.(A,B) = Int(Cl(A \/ B)); end; notation let T be TopSpace; synonym OPD-Union T for Open_Domains_Union T; end; theorem :: TDLAT_1:36 for A,B being Element of Open_Domains_of T holds (OPD-Union T).( A,B) = (D-Union T).(A,B); definition let T be TopSpace; func Open_Domains_Meet T -> BinOp of Open_Domains_of T means :: TDLAT_1:def 11 for A,B being Element of Open_Domains_of T holds it.(A,B) = A /\ B; end; notation let T be TopSpace; synonym OPD-Meet T for Open_Domains_Meet T; end; theorem :: TDLAT_1:37 for A,B being Element of Open_Domains_of T holds (OPD-Meet T).(A ,B) = (D-Meet T).(A,B); theorem :: TDLAT_1:38 for T being TopSpace holds LattStr(#Open_Domains_of T,OPD-Union T,OPD-Meet T#) is B_Lattice; 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#); end; begin :: 6. Connections between Lattices of Domains. theorem :: TDLAT_1:39 CLD-Union T = (D-Union T)||Closed_Domains_of T; theorem :: TDLAT_1:40 CLD-Meet T = (D-Meet T)||Closed_Domains_of T; theorem :: TDLAT_1:41 Closed_Domains_Lattice T is SubLattice of Domains_Lattice T; theorem :: TDLAT_1:42 OPD-Union T = (D-Union T)||Open_Domains_of T; theorem :: TDLAT_1:43 OPD-Meet T = (D-Meet T)||Open_Domains_of T; theorem :: TDLAT_1:44 Open_Domains_Lattice T is SubLattice of Domains_Lattice T;