:: Maximal Anti-Discrete Subspaces of Topological Spaces :: by Zbigniew Karno :: :: Received July 26, 1994 :: Copyright (c) 1994-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 XBOOLE_0, PRE_TOPC, SUBSET_1, ZFMISC_1, SETFAM_1, RCOMP_1, TARSKI, STRUCT_0, TOPS_1, TDLAT_3, RELAT_1, TEX_2, TEX_4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TEX_2; constructors SETFAM_1, TOPS_1, TOPS_2, REALSET2, BORSUK_1, TSEP_1, TDLAT_3, TEX_1, TEX_2, COMPTS_1; registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_1, TEX_2; requirements BOOLE, SUBSET; begin :: 1. Properties of the Closure and the Interior Operations. registration let X be non empty TopSpace, A be non empty Subset of X; cluster Cl A -> non empty; end; registration let X be TopSpace, A be empty Subset of X; cluster Cl A -> empty; end; registration let X be non empty TopSpace, A be non proper Subset of X; cluster Cl A -> non proper; end; registration let X be non trivial TopSpace, A be non trivial Subset of X; cluster Cl A -> non trivial; end; reserve X for non empty TopSpace; theorem :: TEX_4:1 for A being Subset of X holds Cl A = meet {F where F is Subset of X: F is closed & A c= F}; theorem :: TEX_4:2 for x being Point of X holds Cl {x} = meet {F where F is Subset of X : F is closed & x in F}; registration let X be non empty TopSpace, A be non proper Subset of X; cluster Int A -> non proper; end; registration let X be non empty TopSpace, A be proper Subset of X; cluster Int A -> proper; end; registration let X be non empty TopSpace, A be empty Subset of X; cluster Int A -> empty; end; theorem :: TEX_4:3 for A being Subset of X holds Int A = union {G where G is Subset of X : G is open & G c= A}; begin :: 2. Anti-discrete Subsets of Topological Structures. definition let Y be TopStruct; let IT be Subset of Y; attr IT is anti-discrete means :: TEX_4:def 1 for x being Point of Y, G being Subset of Y st G is open & x in G holds x in IT implies IT c= G; end; definition let Y be non empty TopStruct; let A be Subset of Y; redefine attr A is anti-discrete means :: TEX_4:def 2 for x being Point of Y, F being Subset of Y st F is closed & x in F holds x in A implies A c= F; end; definition let Y be TopStruct; let A be Subset of Y; redefine attr A is anti-discrete means :: TEX_4:def 3 for G being Subset of Y st G is open holds A misses G or A c= G; end; definition let Y be TopStruct; let A be Subset of Y; redefine attr A is anti-discrete means :: TEX_4:def 4 for F being Subset of Y st F is closed holds A misses F or A c= F; end; theorem :: TEX_4:4 for Y0, Y1 being TopStruct, D0 being Subset of Y0, D1 being Subset of Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is anti-discrete implies D1 is anti-discrete; reserve Y for non empty TopStruct; theorem :: TEX_4:5 for A, B being Subset of Y st B c= A holds A is anti-discrete implies B is anti-discrete; theorem :: TEX_4:6 for x being Point of Y holds {x} is anti-discrete; theorem :: TEX_4:7 for A being empty Subset of Y holds A is anti-discrete; definition let Y be TopStruct; let IT be Subset-Family of Y; attr IT is anti-discrete-set-family means :: TEX_4:def 5 for A being Subset of Y st A in IT holds A is anti-discrete; end; theorem :: TEX_4:8 for F being Subset-Family of Y st F is anti-discrete-set-family holds meet F <> {} implies union F is anti-discrete; theorem :: TEX_4:9 for F being Subset-Family of Y st F is anti-discrete-set-family holds meet F is anti-discrete; definition let Y be TopStruct, x be Point of Y; func MaxADSF(x) -> Subset-Family of Y equals :: TEX_4:def 6 {A where A is Subset of Y : A is anti-discrete & x in A}; end; registration let Y be non empty TopStruct, x be Point of Y; cluster MaxADSF(x) -> non empty; end; reserve x for Point of Y; theorem :: TEX_4:10 MaxADSF(x) is anti-discrete-set-family; theorem :: TEX_4:11 {x} = meet MaxADSF(x); theorem :: TEX_4:12 {x} c= union MaxADSF(x); theorem :: TEX_4:13 union MaxADSF(x) is anti-discrete; begin :: 3. Maximal Anti-discrete Subsets of Topological Structures. definition let Y be TopStruct; let IT be Subset of Y; attr IT is maximal_anti-discrete means :: TEX_4:def 7 IT is anti-discrete & for D being Subset of Y st D is anti-discrete & IT c= D holds IT = D; end; theorem :: TEX_4:14 for Y0, Y1 being TopStruct, D0 being Subset of Y0, D1 being Subset of Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is maximal_anti-discrete implies D1 is maximal_anti-discrete; reserve Y for non empty TopStruct; theorem :: TEX_4:15 for A being empty Subset of Y holds A is not maximal_anti-discrete; theorem :: TEX_4:16 for A being non empty Subset of Y holds A is anti-discrete & A is open implies A is maximal_anti-discrete; theorem :: TEX_4:17 for A being non empty Subset of Y holds A is anti-discrete & A is closed implies A is maximal_anti-discrete; definition let Y be TopStruct, x be Point of Y; func MaxADSet(x) -> Subset of Y equals :: TEX_4:def 8 union MaxADSF(x); end; registration let Y be non empty TopStruct, x be Point of Y; cluster MaxADSet(x) -> non empty; end; theorem :: TEX_4:18 for x being Point of Y holds {x} c= MaxADSet(x); theorem :: TEX_4:19 for D being Subset of Y, x being Point of Y st D is anti-discrete & x in D holds D c= MaxADSet(x); theorem :: TEX_4:20 for x being Point of Y holds MaxADSet(x) is maximal_anti-discrete; theorem :: TEX_4:21 for x, y being Point of Y holds y in MaxADSet(x) iff MaxADSet(y) = MaxADSet(x); theorem :: TEX_4:22 for x, y being Point of Y holds MaxADSet(x) misses MaxADSet(y) or MaxADSet(x) = MaxADSet(y); theorem :: TEX_4:23 for F being Subset of Y, x being Point of Y st F is closed & x in F holds MaxADSet(x) c= F; theorem :: TEX_4:24 for G being Subset of Y, x being Point of Y st G is open & x in G holds MaxADSet(x) c= G; theorem :: TEX_4:25 for Y being non empty TopSpace, x being Point of Y holds MaxADSet(x) c= meet {F where F is Subset of Y : F is closed & x in F}; theorem :: TEX_4:26 for Y being non empty TopSpace, x being Point of Y holds MaxADSet(x) c= meet {G where G is Subset of Y : G is open & x in G}; definition let Y be non empty TopStruct; let A be Subset of Y; redefine attr A is maximal_anti-discrete means :: TEX_4:def 9 ex x being Point of Y st x in A & A = MaxADSet(x); end; theorem :: TEX_4:27 for A being Subset of Y, x being Point of Y st x in A holds A is maximal_anti-discrete implies A = MaxADSet(x); definition let Y be non empty TopStruct; let A be non empty Subset of Y; redefine attr A is maximal_anti-discrete means :: TEX_4:def 10 for x being Point of Y st x in A holds A = MaxADSet(x); end; definition let Y be non empty TopStruct, A be Subset of Y; func MaxADSet(A) -> Subset of Y equals :: TEX_4:def 11 union {MaxADSet(a) where a is Point of Y : a in A}; end; theorem :: TEX_4:28 for x being Point of Y holds MaxADSet(x) = MaxADSet({x}); theorem :: TEX_4:29 for A being Subset of Y, x being Point of Y holds MaxADSet(x) meets MaxADSet(A) implies MaxADSet(x) meets A; theorem :: TEX_4:30 for A being Subset of Y, x being Point of Y holds MaxADSet(x) meets MaxADSet(A) implies MaxADSet(x) c= MaxADSet(A); theorem :: TEX_4:31 for A, B being Subset of Y holds A c= B implies MaxADSet(A) c= MaxADSet(B); theorem :: TEX_4:32 for A being Subset of Y holds A c= MaxADSet(A); theorem :: TEX_4:33 for A being Subset of Y holds MaxADSet(A) = MaxADSet(MaxADSet(A) ); theorem :: TEX_4:34 for A, B being Subset of Y holds A c= MaxADSet(B) implies MaxADSet(A) c= MaxADSet(B); theorem :: TEX_4:35 for A, B being Subset of Y st B c= MaxADSet(A) & A c= MaxADSet(B) holds MaxADSet(A) = MaxADSet(B); theorem :: TEX_4:36 for A, B being Subset of Y holds MaxADSet(A \/ B) = MaxADSet(A) \/ MaxADSet(B); theorem :: TEX_4:37 for A, B being Subset of Y holds MaxADSet(A /\ B) c= MaxADSet(A) /\ MaxADSet(B); registration let Y be non empty TopStruct, A be non empty Subset of Y; cluster MaxADSet(A) -> non empty; end; registration let Y be non empty TopStruct, A be empty Subset of Y; cluster MaxADSet(A) -> empty; end; registration let Y be non empty TopStruct, A be non proper Subset of Y; cluster MaxADSet(A) -> non proper; end; registration let Y be non trivial TopStruct, A be non trivial Subset of Y; cluster MaxADSet(A) -> non trivial; end; theorem :: TEX_4:38 for G being Subset of Y, A being Subset of Y st G is open & A c= G holds MaxADSet(A) c= G; theorem :: TEX_4:39 for Y being non empty TopSpace, A being Subset of Y holds MaxADSet(A) c= meet {G where G is Subset of Y : G is open & A c= G}; theorem :: TEX_4:40 for F being Subset of Y, A being Subset of Y st F is closed & A c= F holds MaxADSet(A) c= F; theorem :: TEX_4:41 for Y being non empty TopSpace, A being Subset of Y holds MaxADSet(A) c= meet {F where F is Subset of Y : F is closed & A c= F}; begin :: 4. Anti-discrete and Maximal Anti-discrete Subsets of Topological Spaces. definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is anti-discrete means :: TEX_4:def 12 for x being Point of X st x in A holds A c= Cl {x}; end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is anti-discrete means :: TEX_4:def 13 for x being Point of X st x in A holds Cl A = Cl {x}; end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is anti-discrete means :: TEX_4:def 14 for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y}; end; reserve X for non empty TopSpace; theorem :: TEX_4:42 for x being Point of X, D being Subset of X st D is anti-discrete & Cl {x} c= D holds D = Cl {x}; theorem :: TEX_4:43 for A being Subset of X holds A is anti-discrete & A is closed iff for x being Point of X st x in A holds A = Cl {x}; theorem :: TEX_4:44 for A being Subset of X holds A is anti-discrete & A is not open implies A is boundary; theorem :: TEX_4:45 for x being Point of X st Cl {x} = {x} holds {x} is maximal_anti-discrete; reserve x,y for Point of X; theorem :: TEX_4:46 MaxADSet(x) c= meet {G where G is Subset of X : G is open & x in G}; theorem :: TEX_4:47 MaxADSet(x) c= meet {F where F is Subset of X : F is closed & x in F}; theorem :: TEX_4:48 MaxADSet(x) c= Cl {x}; theorem :: TEX_4:49 MaxADSet(x) = MaxADSet(y) iff Cl {x} = Cl {y}; theorem :: TEX_4:50 MaxADSet(x) misses MaxADSet(y) iff Cl {x} <> Cl {y}; definition let X be non empty TopSpace, x be Point of X; redefine func MaxADSet(x) -> non empty Subset of X equals :: TEX_4:def 15 (Cl {x}) /\ meet { G where G is Subset of X : G is open & x in G}; end; theorem :: TEX_4:51 for x, y being Point of X holds Cl {x} c= Cl {y} iff meet {G where G is Subset of X : G is open & y in G} c= meet {G where G is Subset of X : G is open & x in G}; theorem :: TEX_4:52 for x, y being Point of X holds Cl {x} c= Cl {y} iff MaxADSet(y) c= meet {G where G is Subset of X : G is open & x in G}; theorem :: TEX_4:53 for x, y being Point of X holds MaxADSet(x) misses MaxADSet(y) iff (ex V being Subset of X st V is open & MaxADSet(x) c= V & V misses MaxADSet (y)) or ex W being Subset of X st W is open & W misses MaxADSet(x) & MaxADSet(y ) c= W; theorem :: TEX_4:54 for x, y being Point of X holds MaxADSet(x) misses MaxADSet(y) iff (ex E being Subset of X st E is closed & MaxADSet(x) c= E & E misses MaxADSet(y)) or ex F being Subset of X st F is closed & F misses MaxADSet(x) & MaxADSet(y) c= F; reserve A, B for Subset of X; reserve P, Q for Subset of X; theorem :: TEX_4:55 MaxADSet(A) c= meet {G where G is Subset of X : G is open & A c= G}; theorem :: TEX_4:56 P is open implies MaxADSet(P) = P; theorem :: TEX_4:57 MaxADSet(Int A) = Int A; theorem :: TEX_4:58 MaxADSet(A) c= meet {F where F is Subset of X : F is closed & A c= F}; theorem :: TEX_4:59 MaxADSet(A) c= Cl A; theorem :: TEX_4:60 P is closed implies MaxADSet(P) = P; theorem :: TEX_4:61 MaxADSet(Cl A) = Cl A; theorem :: TEX_4:62 Cl MaxADSet(A) = Cl A; theorem :: TEX_4:63 MaxADSet(A) = MaxADSet(B) implies Cl A = Cl B; theorem :: TEX_4:64 P is closed or Q is closed implies MaxADSet(P /\ Q) = MaxADSet(P) /\ MaxADSet(Q); theorem :: TEX_4:65 P is open or Q is open implies MaxADSet(P /\ Q) = MaxADSet(P) /\ MaxADSet(Q); begin :: 5. Maximal Anti-discrete Subspaces. reserve Y for non empty TopStruct; theorem :: TEX_4:66 for Y0 being SubSpace of Y, A being Subset of Y st A = the carrier of Y0 holds Y0 is anti-discrete implies A is anti-discrete; theorem :: TEX_4:67 for Y0 being SubSpace of Y st Y0 is TopSpace-like for A being Subset of Y st A = the carrier of Y0 holds A is anti-discrete implies Y0 is anti-discrete; reserve X for non empty TopSpace, Y0 for non empty SubSpace of X; theorem :: TEX_4:68 (for X0 being open SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0) implies Y0 is anti-discrete; theorem :: TEX_4:69 (for X0 being closed SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0) implies Y0 is anti-discrete; theorem :: TEX_4:70 for Y0 being anti-discrete SubSpace of X for X0 being open SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0; theorem :: TEX_4:71 for Y0 being anti-discrete SubSpace of X for X0 being closed SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0; definition let Y be non empty TopStruct; let IT be SubSpace of Y; attr IT is maximal_anti-discrete means :: TEX_4:def 16 IT is anti-discrete & for Y0 being SubSpace of Y st Y0 is anti-discrete holds the carrier of IT c= the carrier of Y0 implies the carrier of IT = the carrier of Y0; end; registration let Y be non empty TopStruct; cluster maximal_anti-discrete -> anti-discrete for SubSpace of Y; cluster non anti-discrete -> non maximal_anti-discrete for SubSpace of Y; end; theorem :: TEX_4:72 for Y0 being non empty SubSpace of X, A being Subset of X st A = the carrier of Y0 holds Y0 is maximal_anti-discrete iff A is maximal_anti-discrete; registration let X be non empty TopSpace; cluster open anti-discrete -> maximal_anti-discrete for non empty SubSpace of X; cluster open non maximal_anti-discrete -> non anti-discrete for non empty SubSpace of X; cluster anti-discrete non maximal_anti-discrete -> non open for non empty SubSpace of X; cluster closed anti-discrete -> maximal_anti-discrete for non empty SubSpace of X; cluster closed non maximal_anti-discrete -> non anti-discrete for non empty SubSpace of X; cluster anti-discrete non maximal_anti-discrete -> non closed for non empty SubSpace of X; end; definition let Y be TopStruct, x be Point of Y; func MaxADSspace(x) -> strict SubSpace of Y means :: TEX_4:def 17 the carrier of it = MaxADSet(x); end; registration let Y be non empty TopStruct, x be Point of Y; cluster MaxADSspace(x) -> non empty; end; theorem :: TEX_4:73 for x being Point of Y holds Sspace(x) is SubSpace of MaxADSspace(x); theorem :: TEX_4:74 for x, y being Point of Y holds y is Point of MaxADSspace(x) iff the TopStruct of MaxADSspace(y) = the TopStruct of MaxADSspace(x); theorem :: TEX_4:75 for x, y being Point of Y holds the carrier of MaxADSspace(x) misses the carrier of MaxADSspace(y) or the TopStruct of MaxADSspace(x) = the TopStruct of MaxADSspace(y); registration let X be non empty TopSpace; cluster maximal_anti-discrete strict for SubSpace of X; end; registration let X be non empty TopSpace, x be Point of X; cluster MaxADSspace(x) -> maximal_anti-discrete; end; theorem :: TEX_4:76 for X0 being closed non empty SubSpace of X, x being Point of X holds x is Point of X0 implies MaxADSspace(x) is SubSpace of X0; theorem :: TEX_4:77 for X0 being open non empty SubSpace of X, x being Point of X holds x is Point of X0 implies MaxADSspace(x) is SubSpace of X0; theorem :: TEX_4:78 for x being Point of X st Cl {x} = {x} holds Sspace(x) is maximal_anti-discrete; notation let Y be TopStruct, A be Subset of Y; synonym Sspace(A) for Y|A; end; theorem :: TEX_4:79 for A being non empty Subset of Y holds A is Subset of Sspace(A); theorem :: TEX_4:80 for Y0 being SubSpace of Y, A being non empty Subset of Y holds A is Subset of Y0 implies Sspace(A) is SubSpace of Y0; registration let Y be non trivial TopStruct; cluster non proper strict for SubSpace of Y; end; registration let Y be non trivial TopStruct, A be non trivial Subset of Y; cluster Sspace(A) -> non trivial; end; registration let Y be non empty TopStruct, A be non proper Subset of Y; cluster Sspace(A) -> non proper; end; definition let Y be non empty TopStruct, A be Subset of Y; func MaxADSspace(A) -> strict SubSpace of Y means :: TEX_4:def 18 the carrier of it = MaxADSet(A); end; registration let Y be non empty TopStruct, A be non empty Subset of Y; cluster MaxADSspace(A) -> non empty; end; theorem :: TEX_4:81 for A being non empty Subset of Y holds A is Subset of MaxADSspace(A); theorem :: TEX_4:82 for A being non empty Subset of Y holds Sspace(A) is SubSpace of MaxADSspace(A); theorem :: TEX_4:83 for x being Point of Y holds the TopStruct of MaxADSspace(x) = the TopStruct of MaxADSspace({x}); theorem :: TEX_4:84 for A, B being non empty Subset of Y holds A c= B implies MaxADSspace( A) is SubSpace of MaxADSspace(B); theorem :: TEX_4:85 for A being non empty Subset of Y holds the TopStruct of MaxADSspace(A ) = the TopStruct of MaxADSspace(MaxADSet(A)); theorem :: TEX_4:86 for A, B being non empty Subset of Y holds A is Subset of MaxADSspace( B) implies MaxADSspace(A) is SubSpace of MaxADSspace(B); theorem :: TEX_4:87 for A, B being non empty Subset of Y holds B is Subset of MaxADSspace( A) & A is Subset of MaxADSspace(B) iff the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(B); registration let Y be non trivial TopStruct, A be non trivial Subset of Y; cluster MaxADSspace(A) -> non trivial; end; registration let Y be non empty TopStruct, A be non proper Subset of Y; cluster MaxADSspace(A) -> non proper; end; theorem :: TEX_4:88 for X0 being open SubSpace of X, A being non empty Subset of X holds A is Subset of X0 implies MaxADSspace(A) is SubSpace of X0; theorem :: TEX_4:89 for X0 being closed SubSpace of X, A being non empty Subset of X holds A is Subset of X0 implies MaxADSspace(A) is SubSpace of X0;