Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### The Lattice of Domains of a Topological Space

**by****Toshihiko Watanabe**- Received June 12, 1992
- MML identifier: TDLAT_1

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, BOOLE, SUBSET_1, TOPS_1, SETFAM_1, BINOP_1, FUNCT_1, MCART_1, LATTICES, RELAT_1, NAT_LAT, TDLAT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, PRE_TOPC, LATTICES, BINOP_1, TOPS_1, RELAT_1, FUNCT_1, DOMAIN_1, FUNCT_2, NAT_LAT; constructors BINOP_1, TOPS_1, DOMAIN_1, NAT_LAT, PARTFUN1, MEMBERED; clusters PRE_TOPC, FUNCT_1, RLSUB_2, RELSET_1, SUBSET_1, TOPS_1, LATTICES, MEMBERED, ZFMISC_1; requirements BOOLE, SUBSET; begin :: 1. Preliminary Theorems on Subsets of Topological Spaces. reserve T for non empty TopSpace; 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`; 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. reserve T for non empty TopSpace; 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; definition let T be non empty TopSpace; cluster Domains_of T -> non empty; end; definition let T be non empty 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); synonym D-Union T; end; definition let T be non empty 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); synonym D-Meet T; end; theorem :: TDLAT_1:30 for T being non empty TopSpace holds LattStr(#Domains_of T,D-Union T,D-Meet T#) is C_Lattice; definition let T be non empty 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; definition let T be non empty TopSpace; cluster Closed_Domains_of T -> non empty; end; theorem :: TDLAT_1:31 for T being non empty TopSpace holds Closed_Domains_of T c= Domains_of T; definition let T be non empty 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; synonym CLD-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 non empty 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)); synonym CLD-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 non empty TopSpace holds LattStr(#Closed_Domains_of T,CLD-Union T,CLD-Meet T#) is B_Lattice; definition let T be non empty 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; definition let T be non empty TopSpace; cluster Open_Domains_of T -> non empty; end; theorem :: TDLAT_1:35 for T being non empty TopSpace holds Open_Domains_of T c= Domains_of T; definition let T be non empty 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)); synonym OPD-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 non empty 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; synonym OPD-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 non empty TopSpace holds LattStr(#Open_Domains_of T,OPD-Union T,OPD-Meet T#) is B_Lattice; definition let T be non empty 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. reserve T for non empty TopSpace; theorem :: TDLAT_1:39 CLD-Union T = (D-Union T)|[:Closed_Domains_of T,Closed_Domains_of T:]; theorem :: TDLAT_1:40 CLD-Meet T = (D-Meet T)|[:Closed_Domains_of 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,Open_Domains_of T:]; theorem :: TDLAT_1:43 OPD-Meet T = (D-Meet T)|[:Open_Domains_of T,Open_Domains_of T:]; theorem :: TDLAT_1:44 Open_Domains_Lattice T is SubLattice of Domains_Lattice T;

Back to top