:: Completeness of the Lattices of Domains of a Topological Space :: by Zbigniew Karno and Toshihiko Watanabe :: :: Received July 16, 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, TOPS_1, TARSKI, RCOMP_1, XBOOLE_0, SETFAM_1, PCOMPS_1, ZFMISC_1, STRUCT_0, FINSET_1, FINSEQ_1, RELAT_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, FUNCT_1, TDLAT_1, LATTICES, EQREL_1, PBOOLE, LATTICE3, REWRITE1, TDLAT_2; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, SETFAM_1, STRUCT_0, FUNCT_1, ORDINAL1, NUMBERS, FINSET_1, FINSEQ_1, XCMPLX_0, NAT_1, PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, BINOP_1, LATTICES, LATTICE3, TDLAT_1, XXREAL_0; constructors SETFAM_1, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, TOPS_1, TOPS_2, PCOMPS_1, LATTICE3, TDLAT_1, BINOP_1; registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_1, XREAL_0, FINSEQ_1, RELAT_1, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: 1. Preliminary Theorems about Subsets of a Toplogical Space. reserve T for TopSpace; theorem :: TDLAT_2:1 for A being Subset of T holds Int Cl Int A c= Int Cl A & Int Cl Int A c= Cl Int A; theorem :: TDLAT_2:2 for A being Subset of T holds Cl Int A c= Cl Int Cl A & Int Cl A c= Cl Int Cl A; theorem :: TDLAT_2:3 for A, B being Subset of T st B is closed holds Cl(Int(A /\ B)) = A implies A c= B; theorem :: TDLAT_2:4 for A, B being Subset of T st A is open holds Int(Cl(A \/ B)) = B implies A c= B; theorem :: TDLAT_2:5 for A being Subset of T st A c= Cl Int A holds A \/ Int Cl A c= Cl Int(A \/ Int Cl A); theorem :: TDLAT_2:6 for A being Subset of T st Int Cl A c= A holds Int Cl(A /\ Cl Int A) c= A /\ Cl Int A; begin :: 2. The Closure and the Interior Operations for Families of Subsets of :: a Topological Space. ::(for the definition of clf see PCOMPS_1:def 3) notation let T; let F be Subset-Family of T; synonym Cl F for clf F; end; ::Properties of the Closure Operation Cl (see also PCOMPS_1). theorem :: TDLAT_2:7 for F being Subset-Family of T holds Cl F = {A where A is Subset of T : ex B being Subset of T st A = Cl B & B in F}; theorem :: TDLAT_2:8 for F being Subset-Family of T holds Cl F = Cl Cl F; theorem :: TDLAT_2:9 for F being Subset-Family of T holds F = {} iff Cl F = {}; theorem :: TDLAT_2:10 for F,G being Subset-Family of T holds Cl(F /\ G) c= (Cl F) /\ (Cl G); theorem :: TDLAT_2:11 for F,G being Subset-Family of T holds (Cl F) \ (Cl G) c= Cl(F \ G); theorem :: TDLAT_2:12 for F being Subset-Family of T, A being Subset of T st A in F holds meet(Cl F) c= Cl A & Cl A c= union(Cl F); ::for F being Subset-Family of T holds union F c= union(Cl F); ::(see PCOMPS_1:22) theorem :: TDLAT_2:13 for F being Subset-Family of T holds meet F c= meet(Cl F); theorem :: TDLAT_2:14 for F being Subset-Family of T holds Cl(meet F) c= meet(Cl F); theorem :: TDLAT_2:15 for F being Subset-Family of T holds union(Cl F) c= Cl(union F); definition let T; let F be Subset-Family of T; func Int F -> Subset-Family of T means :: TDLAT_2:def 1 for A being Subset of T holds A in it iff ex B being Subset of T st A = Int B & B in F; projectivity; end; ::Properties of the Interior Operation Int. theorem :: TDLAT_2:16 for F being Subset-Family of T holds Int F = {A where A is Subset of T : ex B being Subset of T st A = Int B & B in F}; ::$CT theorem :: TDLAT_2:18 for F being Subset-Family of T holds Int F is open; theorem :: TDLAT_2:19 for F being Subset-Family of T holds F = {} iff Int F = {}; theorem :: TDLAT_2:20 for A being Subset of T, F being Subset-Family of T st F = { A } holds Int F = { Int A }; theorem :: TDLAT_2:21 for F,G being Subset-Family of T holds F c= G implies Int F c= Int G; theorem :: TDLAT_2:22 for F,G being Subset-Family of T holds Int(F \/ G) = (Int F) \/ (Int G); theorem :: TDLAT_2:23 for F,G being Subset-Family of T holds Int(F /\ G) c= (Int F) /\ (Int G); theorem :: TDLAT_2:24 for F,G being Subset-Family of T holds (Int F) \ (Int G) c= Int(F \ G); theorem :: TDLAT_2:25 for F being Subset-Family of T, A being Subset of T holds A in F implies Int A c= union(Int F) & meet(Int F) c= Int A; theorem :: TDLAT_2:26 for F being Subset-Family of T holds union(Int F) c= union F; theorem :: TDLAT_2:27 for F being Subset-Family of T holds meet(Int F) c= meet F; theorem :: TDLAT_2:28 for F being Subset-Family of T holds union(Int F) c= Int(union F ); theorem :: TDLAT_2:29 for F being Subset-Family of T holds Int(meet F) c= meet(Int F); theorem :: TDLAT_2:30 for F being Subset-Family of T holds F is finite implies Int(meet F) = meet(Int F); ::Connections between the Operations Int and Cl. reserve T for non empty TopSpace; reserve F for Subset-Family of T; theorem :: TDLAT_2:31 Cl Int F = {A where A is Subset of T : ex B being Subset of T st A = Cl Int B & B in F}; theorem :: TDLAT_2:32 Int Cl F = {A where A is Subset of T : ex B being Subset of T st A = Int Cl B & B in F}; theorem :: TDLAT_2:33 Cl Int Cl F = {A where A is Subset of T : ex B being Subset of T st A = Cl Int Cl B & B in F}; theorem :: TDLAT_2:34 Int Cl Int F = {A where A is Subset of T : ex B being Subset of T st A = Int Cl Int B & B in F}; theorem :: TDLAT_2:35 Cl Int Cl Int F = Cl Int F; theorem :: TDLAT_2:36 Int Cl Int Cl F = Int Cl F; theorem :: TDLAT_2:37 union(Int Cl F) c= union(Cl Int Cl F); theorem :: TDLAT_2:38 meet(Int Cl F) c= meet(Cl Int Cl F); theorem :: TDLAT_2:39 union(Cl Int F) c= union(Cl Int Cl F); theorem :: TDLAT_2:40 meet(Cl Int F) c= meet(Cl Int Cl F); theorem :: TDLAT_2:41 union(Int Cl Int F) c= union(Int Cl F); theorem :: TDLAT_2:42 meet(Int Cl Int F) c= meet(Int Cl F); theorem :: TDLAT_2:43 union(Int Cl Int F) c= union(Cl Int F); theorem :: TDLAT_2:44 meet(Int Cl Int F) c= meet(Cl Int F); theorem :: TDLAT_2:45 union(Cl Int Cl F) c= union(Cl F); theorem :: TDLAT_2:46 meet(Cl Int Cl F) c= meet(Cl F); theorem :: TDLAT_2:47 union(Int F) c= union(Int Cl Int F); theorem :: TDLAT_2:48 meet(Int F) c= meet(Int Cl Int F); theorem :: TDLAT_2:49 union(Cl Int F) c= Cl Int(union F); theorem :: TDLAT_2:50 Cl Int(meet F) c= meet(Cl Int F); theorem :: TDLAT_2:51 union(Int Cl F) c= Int Cl(union F); theorem :: TDLAT_2:52 Int Cl(meet F) c= meet(Int Cl F); theorem :: TDLAT_2:53 union(Cl Int Cl F) c= Cl Int Cl(union F); theorem :: TDLAT_2:54 Cl Int Cl(meet F) c= meet(Cl Int Cl F); theorem :: TDLAT_2:55 union(Int Cl Int F) c= Int Cl Int(union F); theorem :: TDLAT_2:56 Int Cl Int(meet F) c= meet(Int Cl Int F); theorem :: TDLAT_2:57 for F being Subset-Family of T holds (for A being Subset of T st A in F holds A c= Cl Int A) implies union F c= Cl Int(union F) & Cl(union F) = Cl Int Cl(union F); theorem :: TDLAT_2:58 for F being Subset-Family of T holds (for A being Subset of T st A in F holds Int Cl A c= A) implies Int Cl(meet F) c= meet F & Int Cl Int(meet F) = Int(meet F); begin :: 3. Selected Properties of Domains of a Topological Space. reserve T for non empty TopSpace; theorem :: TDLAT_2:59 for A, B being Subset of T st B is condensed holds Int(Cl(A \/ B )) \/ (A \/ B) = B iff A c= B; theorem :: TDLAT_2:60 for A, B being Subset of T st A is condensed holds Cl(Int(A /\ B)) /\ (A /\ B) = A iff A c= B; theorem :: TDLAT_2:61 for A, B being Subset of T st A is closed_condensed & B is closed_condensed holds Int A c= Int B iff A c= B; theorem :: TDLAT_2:62 for A, B being Subset of T st A is open_condensed & B is open_condensed holds Cl A c= Cl B iff A c= B; theorem :: TDLAT_2:63 for A, B being Subset of T st A is closed_condensed holds A c= B implies Cl(Int(A /\ B)) = A; theorem :: TDLAT_2:64 for A, B being Subset of T st B is open_condensed holds A c= B implies Int(Cl(A \/ B)) = B; definition let T; let IT be Subset-Family of T; attr IT is domains-family means :: TDLAT_2:def 2 for A being Subset of T holds A in IT implies A is condensed; end; theorem :: TDLAT_2:65 for F being Subset-Family of T holds F c= Domains_of T iff F is domains-family; theorem :: TDLAT_2:66 for F being Subset-Family of T holds F is domains-family implies union F c= Cl Int(union F) & Cl(union F) = Cl Int Cl(union F); theorem :: TDLAT_2:67 for F being Subset-Family of T holds F is domains-family implies Int Cl(meet F) c= meet F & Int Cl Int(meet F) = Int(meet F); theorem :: TDLAT_2:68 for F being Subset-Family of T holds F is domains-family implies (union F) \/ (Int Cl(union F)) is condensed; theorem :: TDLAT_2:69 for F being Subset-Family of T holds (for B being Subset of T st B in F holds B c= (union F) \/ (Int Cl(union F))) & for A being Subset of T st A is condensed holds (for B being Subset of T st B in F holds B c= A) implies ( union F) \/ (Int Cl(union F)) c= A; theorem :: TDLAT_2:70 for F being Subset-Family of T holds F is domains-family implies (meet F) /\ (Cl Int(meet F)) is condensed; theorem :: TDLAT_2:71 for F being Subset-Family of T holds (for B being Subset of T st B in F holds (meet F) /\ (Cl Int(meet F)) c= B) & (F = {} or for A being Subset of T st A is condensed holds (for B being Subset of T st B in F holds A c= B) implies A c= (meet F) /\ (Cl Int(meet F))); definition let T; let IT be Subset-Family of T; attr IT is closed-domains-family means :: TDLAT_2:def 3 for A being Subset of T holds A in IT implies A is closed_condensed; end; theorem :: TDLAT_2:72 for F being Subset-Family of T holds F c= Closed_Domains_of T iff F is closed-domains-family; theorem :: TDLAT_2:73 for F being Subset-Family of T holds F is closed-domains-family implies F is domains-family; theorem :: TDLAT_2:74 for F being Subset-Family of T holds F is closed-domains-family implies F is closed; theorem :: TDLAT_2:75 for F being Subset-Family of T holds F is domains-family implies Cl F is closed-domains-family; theorem :: TDLAT_2:76 for F being Subset-Family of T holds F is closed-domains-family implies Cl(union F) is closed_condensed & Cl Int(meet F) is closed_condensed; theorem :: TDLAT_2:77 for F being Subset-Family of T holds (for B being Subset of T st B in F holds B c= Cl(union F)) & for A being Subset of T st A is closed_condensed holds (for B being Subset of T st B in F holds B c= A) implies Cl(union F) c= A; theorem :: TDLAT_2:78 for F being Subset-Family of T holds (F is closed implies for B being Subset of T st B in F holds Cl Int(meet F) c= B) & (F = {} or for A being Subset of T st A is closed_condensed holds (for B being Subset of T st B in F holds A c= B) implies A c= Cl Int(meet F)); definition let T; let IT be Subset-Family of T; attr IT is open-domains-family means :: TDLAT_2:def 4 for A being Subset of T holds A in IT implies A is open_condensed; end; theorem :: TDLAT_2:79 for F being Subset-Family of T holds F c= Open_Domains_of T iff F is open-domains-family; theorem :: TDLAT_2:80 for F being Subset-Family of T holds F is open-domains-family implies F is domains-family; theorem :: TDLAT_2:81 for F being Subset-Family of T holds F is open-domains-family implies F is open; theorem :: TDLAT_2:82 for F being Subset-Family of T holds F is domains-family implies Int F is open-domains-family; theorem :: TDLAT_2:83 for F being Subset-Family of T holds F is open-domains-family implies Int(meet F) is open_condensed & Int Cl(union F) is open_condensed; theorem :: TDLAT_2:84 for F being Subset-Family of T holds (F is open implies for B being Subset of T st B in F holds B c= Int Cl(union F)) & for A being Subset of T st A is open_condensed holds (for B being Subset of T st B in F holds B c= A) implies Int Cl(union F) c= A; theorem :: TDLAT_2:85 for F being Subset-Family of T holds (for B being Subset of T st B in F holds Int(meet F) c= B) & (F = {} or for A being Subset of T st A is open_condensed holds (for B being Subset of T st B in F holds A c= B) implies A c= Int(meet F)); begin :: 4. Completeness of the Lattice of Domains. reserve T for non empty TopSpace; theorem :: TDLAT_2:86 the carrier of Domains_Lattice T = Domains_of T; theorem :: TDLAT_2:87 for a, b being Element of Domains_Lattice T for A, B being Element of Domains_of T st a = A & b = B holds a "\/" b = Int(Cl(A \/ B)) \/ (A \/ B) & a "/\" b = Cl(Int(A /\ B)) /\ (A /\ B); theorem :: TDLAT_2:88 Bottom (Domains_Lattice T) = {}T & Top (Domains_Lattice T) = [#]T; theorem :: TDLAT_2:89 for a, b being Element of Domains_Lattice T for A, B being Element of Domains_of T st a = A & b = B holds a [= b iff A c= B; theorem :: TDLAT_2:90 for X being Subset of Domains_Lattice T ex a being Element of Domains_Lattice T st X is_less_than a & for b being Element of Domains_Lattice T st X is_less_than b holds a [= b; theorem :: TDLAT_2:91 Domains_Lattice T is complete; theorem :: TDLAT_2:92 for F being Subset-Family of T st F is domains-family for X being Subset of Domains_Lattice T st X = F holds "\/"(X,Domains_Lattice T) = ( union F) \/ (Int Cl(union F)); theorem :: TDLAT_2:93 for F being Subset-Family of T st F is domains-family for X being Subset of Domains_Lattice T st X = F holds (X <> {} implies "/\"(X, Domains_Lattice T) = (meet F) /\ (Cl Int(meet F))) & (X = {} implies "/\"(X, Domains_Lattice T) = [#]T); begin :: 5. Completeness of the Lattices of Closed Domains and Open Domains. reserve T for non empty TopSpace; ::The Lattice of Closed Domains. theorem :: TDLAT_2:94 the carrier of Closed_Domains_Lattice T = Closed_Domains_of T; theorem :: TDLAT_2:95 for a, b being Element of Closed_Domains_Lattice T for A, B being Element of Closed_Domains_of T st a = A & b = B holds a "\/" b = A \/ B & a "/\" b = Cl(Int(A /\ B)); theorem :: TDLAT_2:96 Bottom (Closed_Domains_Lattice T) = {}T & Top (Closed_Domains_Lattice T) = [#]T; theorem :: TDLAT_2:97 for a, b being Element of Closed_Domains_Lattice T for A, B being Element of Closed_Domains_of T st a = A & b = B holds a [= b iff A c= B ; theorem :: TDLAT_2:98 for X being Subset of Closed_Domains_Lattice T ex a being Element of Closed_Domains_Lattice T st X is_less_than a & for b being Element of Closed_Domains_Lattice T st X is_less_than b holds a [= b; theorem :: TDLAT_2:99 Closed_Domains_Lattice T is complete; theorem :: TDLAT_2:100 for F being Subset-Family of T st F is closed-domains-family for X being Subset of Closed_Domains_Lattice T st X = F holds "\/"(X, Closed_Domains_Lattice T) = Cl(union F); theorem :: TDLAT_2:101 for F being Subset-Family of T st F is closed-domains-family for X being Subset of Closed_Domains_Lattice T st X = F holds (X <> {} implies "/\"(X ,Closed_Domains_Lattice T) = Cl(Int(meet F))) & (X = {} implies "/\"(X, Closed_Domains_Lattice T) = [#]T); theorem :: TDLAT_2:102 for F being Subset-Family of T st F is closed-domains-family for X being Subset of Domains_Lattice T st X = F holds (X <> {} implies "/\"(X, Domains_Lattice T) = Cl(Int(meet F))) & (X = {} implies "/\"(X,Domains_Lattice T) = [#]T); ::The Lattice of Open Domains. theorem :: TDLAT_2:103 the carrier of Open_Domains_Lattice T = Open_Domains_of T; theorem :: TDLAT_2:104 for a, b being Element of Open_Domains_Lattice T for A, B being Element of Open_Domains_of T st a = A & b = B holds a "\/" b = Int(Cl(A \/ B)) & a "/\" b = A /\ B; theorem :: TDLAT_2:105 Bottom (Open_Domains_Lattice T) = {}T & Top (Open_Domains_Lattice T) = [#] T; theorem :: TDLAT_2:106 for a, b being Element of Open_Domains_Lattice T for A, B being Element of Open_Domains_of T st a = A & b = B holds a [= b iff A c= B; theorem :: TDLAT_2:107 for X being Subset of Open_Domains_Lattice T ex a being Element of Open_Domains_Lattice T st X is_less_than a & for b being Element of Open_Domains_Lattice T st X is_less_than b holds a [= b; theorem :: TDLAT_2:108 Open_Domains_Lattice T is complete; theorem :: TDLAT_2:109 for F being Subset-Family of T st F is open-domains-family for X being Subset of Open_Domains_Lattice T st X = F holds "\/"(X,Open_Domains_Lattice T) = Int Cl(union F); theorem :: TDLAT_2:110 for F being Subset-Family of T st F is open-domains-family for X being Subset of Open_Domains_Lattice T st X = F holds (X <> {} implies "/\"(X, Open_Domains_Lattice T) = Int(meet F)) & (X = {} implies "/\"(X, Open_Domains_Lattice T) = [#]T); theorem :: TDLAT_2:111 for F being Subset-Family of T st F is open-domains-family for X being Subset of Domains_Lattice T st X = F holds "\/"(X,Domains_Lattice T) = Int Cl( union F);