Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Maximal Anti-Discrete Subspaces of Topological Spaces

by
Zbigniew Karno

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;
end;

reserve x for Point of Y;

theorem :: TEX_4:12

theorem :: TEX_4:13

theorem :: TEX_4:14

theorem :: TEX_4:15

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
end;

definition let Y be non empty TopStruct, x be Point of Y;
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

theorem :: TEX_4:23
for x, y being Point of Y holds

theorem :: TEX_4:24
for x, y being Point of Y holds

theorem :: TEX_4:25
for F being Subset of Y, x being Point of Y st F is closed & x in F holds

theorem :: TEX_4:26
for G being Subset of Y, x being Point of Y st G is open & x in G holds

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

theorem :: TEX_4:31
for A being Subset of Y, x being Point of Y holds

theorem :: TEX_4:32
for A being Subset of Y, x being Point of Y holds

theorem :: TEX_4:33
for A, B being Subset of Y holds A c= 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

theorem :: TEX_4:36
for A, B being Subset of Y holds

theorem :: TEX_4:37
for A, B being Subset of Y holds

theorem :: TEX_4:38
for A, B being Subset of Y

theorem :: TEX_4:39
for A, B being Subset of Y

definition let Y be non empty TopStruct,
A be non empty Subset of Y;
end;

definition let Y be non empty TopStruct, A be empty Subset of Y;
end;

definition let Y be non empty TopStruct,
A be non proper Subset of Y;
end;

definition let Y be non trivial non empty TopStruct,
A be non trivial (non empty Subset of Y);
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

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

theorem :: TEX_4:51

theorem :: TEX_4:52

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
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
(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

theorem :: TEX_4:56
for x, y being Point of X holds
(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

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

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

theorem :: TEX_4:62
P is closed implies MaxADSet(P) = P;

theorem :: TEX_4:63

theorem :: TEX_4:64

theorem :: TEX_4:65

theorem :: TEX_4:66
P is closed or Q is closed implies

theorem :: TEX_4:67
P is open or Q is open implies

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;
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

theorem :: TEX_4:77
for x, y being Point of Y holds

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;
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;
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

theorem :: TEX_4:85
for x being Point of Y holds

theorem :: TEX_4:86
for A, B being non empty Subset of Y holds

theorem :: TEX_4:87
for A being non empty Subset of Y holds

theorem :: TEX_4:88
for A, B being non empty Subset of Y holds
A is Subset of MaxADSspace(B) implies

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

definition let Y be non trivial non empty TopStruct,
A be non trivial (non empty Subset of Y);
end;

definition let Y be non empty TopStruct,
A be non proper non empty Subset of Y;
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;
```