Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### Maximal Anti-Discrete Subspaces of Topological Spaces

**by****Zbigniew Karno**- Received July 26, 1994
- MML identifier: TEX_4

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, BOOLE, COLLSP, SUBSET_1, REALSET1, SETFAM_1, TOPS_1, TARSKI, TDLAT_3, RELAT_1, TEX_2, TEX_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, REALSET1, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TEX_2; constructors REALSET1, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TEX_2, MEMBERED; clusters SUBSET_1, PRE_TOPC, BORSUK_1, TSEP_1, TEX_1, TEX_2, STRUCT_0, TOPS_1, SETFAM_1, MEMBERED, ZFMISC_1; requirements BOOLE, SUBSET; begin :: 1. Properties of the Closure and the Interior Operations. definition let X be non empty TopSpace, A be non empty Subset of X; cluster Cl A -> non empty; end; definition let X be non empty TopSpace, A be empty Subset of X; cluster Cl A -> empty; end; definition let X be non empty TopSpace, A be non proper Subset of X; cluster Cl A -> non proper; end; definition let X be non trivial non empty TopSpace, A be non trivial (non empty 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}; theorem :: TEX_4:3 for A, B being Subset of X holds B c= Cl A implies Cl B c= Cl A; definition let X be non empty TopSpace, A be non proper Subset of X; cluster Int A -> non proper; end; definition let X be non empty TopSpace, A be proper Subset of X; cluster Int A -> proper; end; definition let X be non empty TopSpace, A be empty Subset of X; cluster Int A -> empty; end; theorem :: TEX_4:4 for A being Subset of X holds Int A = union {G where G is Subset of X : G is open & G c= A}; theorem :: TEX_4:5 for A, B being Subset of X holds Int A c= B implies Int A c= Int B; 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:6 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:7 for A, B being Subset of Y st B c= A holds A is anti-discrete implies B is anti-discrete; theorem :: TEX_4:8 for x being Point of Y holds {x} is anti-discrete; theorem :: TEX_4:9 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:10 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:11 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; definition 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:12 MaxADSF(x) is anti-discrete-set-family; theorem :: TEX_4:13 {x} = meet MaxADSF(x); theorem :: TEX_4:14 {x} c= union MaxADSF(x); theorem :: TEX_4:15 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:16 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:17 for A being empty Subset of Y holds A is not maximal_anti-discrete; theorem :: TEX_4:18 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:19 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; definition let Y be non empty TopStruct, x be Point of Y; cluster MaxADSet(x) -> non empty; end; theorem :: TEX_4:20 for x being Point of Y holds {x} c= MaxADSet(x); theorem :: TEX_4:21 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:22 for x being Point of Y holds MaxADSet(x) is maximal_anti-discrete; theorem :: TEX_4:23 for x, y being Point of Y holds y in MaxADSet(x) iff MaxADSet(y) = MaxADSet(x); theorem :: TEX_4:24 for x, y being Point of Y holds MaxADSet(x) misses MaxADSet(y) or MaxADSet(x) = MaxADSet(y); theorem :: TEX_4:25 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:26 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:27 for x being Point of Y holds {F where F is Subset of Y : F is closed & x in F} <> {} implies MaxADSet(x) c= meet {F where F is Subset of Y : F is closed & x in F}; theorem :: TEX_4:28 for x being Point of Y holds {G where G is Subset of Y : G is open & x in G} <> {} implies 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:29 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:30 for x being Point of Y holds MaxADSet(x) = MaxADSet({x}); theorem :: TEX_4:31 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:32 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:33 for A, B being Subset of Y holds A c= B implies MaxADSet(A) c= MaxADSet(B); theorem :: TEX_4:34 for A being Subset of Y holds A c= MaxADSet(A); theorem :: TEX_4:35 for A being Subset of Y holds MaxADSet(A) = MaxADSet(MaxADSet(A)); theorem :: TEX_4:36 for A, B being Subset of Y holds A c= MaxADSet(B) implies MaxADSet(A) c= MaxADSet(B); theorem :: TEX_4:37 for A, B being Subset of Y holds B c= MaxADSet(A) & A c= MaxADSet(B) iff MaxADSet(A) = MaxADSet(B); theorem :: TEX_4:38 for A, B being Subset of Y holds MaxADSet(A \/ B) = MaxADSet(A) \/ MaxADSet(B); theorem :: TEX_4:39 for A, B being Subset of Y holds MaxADSet(A /\ B) c= MaxADSet(A) /\ MaxADSet(B); definition let Y be non empty TopStruct, A be non empty Subset of Y; cluster MaxADSet(A) -> non empty; end; definition let Y be non empty TopStruct, A be empty Subset of Y; cluster MaxADSet(A) -> empty; end; definition let Y be non empty TopStruct, A be non proper Subset of Y; cluster MaxADSet(A) -> non proper; end; definition let Y be non trivial non empty TopStruct, A be non trivial (non empty Subset of Y); cluster MaxADSet(A) -> non trivial; end; theorem :: TEX_4:40 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:41 for A being Subset of Y holds {G where G is Subset of Y : G is open & A c= G} <> {} implies MaxADSet(A) c= meet {G where G is Subset of Y : G is open & A c= G}; theorem :: TEX_4:42 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:43 for A being Subset of Y holds {F where F is Subset of Y : F is closed & A c= F} <> {} implies 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:44 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:45 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:46 for A being Subset of X holds A is anti-discrete & A is not open implies A is boundary; theorem :: TEX_4:47 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:48 MaxADSet(x) c= meet {G where G is Subset of X : G is open & x in G}; theorem :: TEX_4:49 MaxADSet(x) c= meet {F where F is Subset of X : F is closed & x in F}; theorem :: TEX_4:50 MaxADSet(x) c= Cl {x}; theorem :: TEX_4:51 MaxADSet(x) = MaxADSet(y) iff Cl {x} = Cl {y}; theorem :: TEX_4:52 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:53 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:54 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:55 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:56 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:57 MaxADSet(A) c= meet {G where G is Subset of X : G is open & A c= G}; theorem :: TEX_4:58 P is open implies MaxADSet(P) = P; theorem :: TEX_4:59 MaxADSet(Int A) = Int A; theorem :: TEX_4:60 MaxADSet(A) c= meet {F where F is Subset of X : F is closed & A c= F}; theorem :: TEX_4:61 MaxADSet(A) c= Cl A; theorem :: TEX_4:62 P is closed implies MaxADSet(P) = P; theorem :: TEX_4:63 MaxADSet(Cl A) = Cl A; theorem :: TEX_4:64 Cl MaxADSet(A) = Cl A; theorem :: TEX_4:65 MaxADSet(A) = MaxADSet(B) implies Cl A = Cl B; theorem :: TEX_4:66 P is closed or Q is closed implies MaxADSet(P /\ Q) = MaxADSet(P) /\ MaxADSet(Q); theorem :: TEX_4:67 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:68 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:69 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:70 (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:71 (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:72 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:73 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; definition let Y be non empty TopStruct; cluster maximal_anti-discrete -> anti-discrete SubSpace of Y; cluster non anti-discrete -> non maximal_anti-discrete SubSpace of Y; end; theorem :: TEX_4:74 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; definition let X be non empty TopSpace; cluster open anti-discrete -> maximal_anti-discrete (non empty SubSpace of X); cluster open non maximal_anti-discrete -> non anti-discrete (non empty SubSpace of X); cluster anti-discrete non maximal_anti-discrete -> non open (non empty SubSpace of X); cluster closed anti-discrete -> maximal_anti-discrete (non empty SubSpace of X); cluster closed non maximal_anti-discrete -> non anti-discrete (non empty SubSpace of X); cluster anti-discrete non maximal_anti-discrete -> non closed (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; definition let Y be non empty TopStruct, x be Point of Y; cluster MaxADSspace(x) -> non empty; end; theorem :: TEX_4:75 for x being Point of Y holds Sspace(x) is SubSpace of MaxADSspace(x); theorem :: TEX_4:76 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:77 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); definition let X be non empty TopSpace; cluster maximal_anti-discrete strict SubSpace of X; end; definition let X be non empty TopSpace, x be Point of X; cluster MaxADSspace(x) -> maximal_anti-discrete; end; theorem :: TEX_4:78 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:79 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:80 for x being Point of X st Cl {x} = {x} holds Sspace(x) is maximal_anti-discrete; definition let Y be TopStruct, A be Subset of Y; func Sspace(A) -> strict SubSpace of Y means :: TEX_4:def 18 the carrier of it = A; end; definition let Y be non empty TopStruct, A be non empty Subset of Y; cluster Sspace(A) -> non empty; end; theorem :: TEX_4:81 for A being non empty Subset of Y holds A is Subset of Sspace(A); theorem :: TEX_4:82 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; definition let Y be non trivial non empty TopStruct; cluster non proper strict SubSpace of Y; end; definition let Y be non trivial non empty TopStruct, A be non trivial (non empty Subset of Y); cluster Sspace(A) -> non trivial; end; definition let Y be non empty TopStruct, A be non proper non empty 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 19 the carrier of it = MaxADSet(A); end; definition let Y be non empty TopStruct, A be non empty Subset of Y; cluster MaxADSspace(A) -> non empty; end; theorem :: TEX_4:83 for A being non empty Subset of Y holds A is Subset of MaxADSspace(A); theorem :: TEX_4:84 for A being non empty Subset of Y holds Sspace(A) is SubSpace of MaxADSspace(A); theorem :: TEX_4:85 for x being Point of Y holds the TopStruct of MaxADSspace(x) = the TopStruct of MaxADSspace({x}); theorem :: TEX_4:86 for A, B being non empty Subset of Y holds A c= B implies MaxADSspace(A) is SubSpace of MaxADSspace(B); theorem :: TEX_4:87 for A being non empty Subset of Y holds the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(MaxADSet(A)); theorem :: TEX_4:88 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:89 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); definition let Y be non trivial non empty TopStruct, A be non trivial (non empty Subset of Y); cluster MaxADSspace(A) -> non trivial; end; definition let Y be non empty TopStruct, A be non proper non empty Subset of Y; cluster MaxADSspace(A) -> non proper; end; theorem :: TEX_4:90 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:91 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;

Back to top