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