:: Maximal Discrete Subspaces of Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received November 5, 1993
:: Copyright (c) 1993-2016 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, ZFMISC_1, SUBSET_1, TARSKI, STRUCT_0, PRE_TOPC,
RELAT_1, NATTRA_1, TDLAT_3, RCOMP_1, TOPS_3, TOPS_1, SETFAM_1, FUNCT_1,
ORDINAL2, COMPTS_1, TEX_1, BORSUK_1, TEX_2, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1,
TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, COMPTS_1, TEX_1;
constructors SETFAM_1, TOPS_1, TOPS_2, COMPTS_1, REALSET2, BORSUK_1, TSEP_1,
TDLAT_3, TOPS_3, TEX_1;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, STRUCT_0,
PRE_TOPC, TOPS_1, BORSUK_1, TDLAT_3, TEX_1, CARD_1;
requirements BOOLE, SUBSET, NUMERALS;
begin
:: 1. Proper Subsets of 1-sorted Structures.
theorem :: TEX_2:1
for A being non empty set, B being 1-element set st A c=
B holds A = B;
theorem :: TEX_2:2
for A being 1-element set, B being set st A /\ B is non empty
holds A c= B;
registration
let S be 1-element set;
cluster proper -> empty for Subset of S;
cluster non empty -> non proper for Subset of S;
end;
theorem :: TEX_2:3
for S being non empty set, y being Element of S holds {y} is proper
implies S is non trivial;
theorem :: TEX_2:4
for S being non trivial set, y being Element of S holds {y}
is proper;
registration
let S be 1-element set;
cluster non proper -> trivial for non empty Subset of S;
end;
registration
let S be non trivial set;
cluster trivial -> proper for non empty Subset of S;
cluster non proper -> non trivial for non empty Subset of S;
end;
registration
let S be non trivial set;
cluster trivial proper for non empty Subset of S;
cluster non trivial non proper for non empty Subset of S;
end;
theorem :: TEX_2:5
for Y being non empty 1-sorted, y being Element of Y holds {y} is
proper implies Y is non trivial;
theorem :: TEX_2:6
for Y being non trivial 1-sorted, y being Element of Y holds
{y} is proper;
registration
let Y be 1-element 1-sorted;
cluster -> non proper for non empty Subset of Y;
cluster non proper -> trivial for non empty Subset of Y;
end;
registration
let Y be non trivial 1-sorted;
cluster trivial -> proper for non empty Subset of Y;
cluster non proper -> non trivial for non empty Subset of Y;
end;
registration
let Y be non trivial 1-sorted;
cluster trivial proper for non empty Subset of Y;
cluster non trivial non proper for non empty Subset of Y;
end;
registration
let Y be non trivial 1-sorted;
cluster non empty trivial proper for Subset of Y;
end;
registration
let X be non empty set;
let A be proper Subset of X;
cluster A` -> non empty;
end;
begin
:: 2. Proper Subspaces of Topological Spaces.
theorem :: TEX_2:7
for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of
Y1 holds Y0 is TopSpace-like implies Y1 is TopSpace-like;
definition
let Y be TopStruct;
let IT be SubSpace of Y;
attr IT is proper means
:: TEX_2:def 1
for A being Subset of Y st A = the carrier of IT holds A is proper;
end;
reserve Y for TopStruct;
theorem :: TEX_2:8
for Y0 being SubSpace of Y, A being Subset of Y st A = the
carrier of Y0 holds A is proper iff Y0 is proper;
theorem :: TEX_2:9
for Y0, Y1 being SubSpace of Y st the TopStruct of Y0 = the TopStruct
of Y1 holds Y0 is proper implies Y1 is proper;
theorem :: TEX_2:10
for Y0 being SubSpace of Y holds the carrier of Y0 = the carrier
of Y implies Y0 is non proper;
registration
let Y be 1-element TopStruct;
cluster -> non proper for non empty SubSpace of Y;
cluster non proper -> trivial for non empty SubSpace of Y;
end;
registration
let Y be non trivial TopStruct;
cluster trivial -> proper for non empty SubSpace of Y;
cluster non proper -> non trivial for non empty SubSpace of Y;
end;
registration
let Y be non empty TopStruct;
cluster non proper strict non empty for SubSpace of Y;
end;
theorem :: TEX_2:11
for Y being non empty TopStruct, Y0 being non proper SubSpace of Y
holds the TopStruct of Y0 = the TopStruct of Y;
registration
let Y be non empty TopStruct;
cluster discrete -> TopSpace-like for SubSpace of Y;
cluster anti-discrete -> TopSpace-like for SubSpace of Y;
cluster non TopSpace-like -> non discrete for SubSpace of Y;
cluster non TopSpace-like -> non anti-discrete for SubSpace of Y;
end;
theorem :: TEX_2:12
for Y0, Y1 being TopStruct st the TopStruct of Y0 = the
TopStruct of Y1 holds Y0 is discrete implies Y1 is discrete;
theorem :: TEX_2:13
for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of
Y1 holds Y0 is anti-discrete implies Y1 is anti-discrete;
registration
let Y be non empty TopStruct;
cluster discrete -> almost_discrete for SubSpace of Y;
cluster non almost_discrete -> non discrete for SubSpace of Y;
cluster anti-discrete -> almost_discrete for SubSpace of Y;
cluster non almost_discrete -> non anti-discrete for SubSpace of Y;
end;
theorem :: TEX_2:14
for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of
Y1 holds Y0 is almost_discrete implies Y1 is almost_discrete;
registration
let Y be non empty TopStruct;
cluster discrete anti-discrete -> trivial for non empty SubSpace of Y;
cluster anti-discrete non trivial -> non discrete for
non empty SubSpace of Y;
cluster discrete non trivial -> non anti-discrete for
non empty SubSpace of Y;
end;
definition
let Y be non empty TopStruct, y be Point of Y;
func Sspace(y) -> strict non empty SubSpace of Y means
:: TEX_2:def 2
the carrier of it = {y};
end;
registration
let Y be non empty TopStruct;
cluster strict 1-element for SubSpace of Y;
end;
registration
let Y be non empty TopStruct, y be Point of Y;
cluster Sspace(y) -> 1-element;
end;
theorem :: TEX_2:15
for Y being non empty TopStruct, y being Point of Y holds Sspace(y) is
proper iff {y} is proper;
theorem :: TEX_2:16
for Y being non empty TopStruct, y being Point of Y holds Sspace(y) is
proper implies Y is non trivial;
registration
let Y be non trivial TopStruct;
cluster proper trivial strict for non empty SubSpace of Y;
end;
registration let Y be non empty TopStruct;
cluster 1-element for SubSpace of Y;
end;
theorem :: TEX_2:17
for Y being non empty TopStruct, Y0 be 1-element SubSpace of Y
holds ex y being Point of Y st the TopStruct of Y0 = the TopStruct of Sspace(y)
;
theorem :: TEX_2:18
for Y being non empty TopStruct, y being Point of Y holds Sspace(y) is
TopSpace-like implies Sspace(y) is discrete anti-discrete;
registration
let Y be non empty TopStruct;
cluster trivial TopSpace-like -> discrete anti-discrete for
non empty SubSpace
of Y;
end;
registration
let X be non empty TopSpace;
cluster trivial strict TopSpace-like non empty for SubSpace of X;
end;
registration
let X be non empty TopSpace, x be Point of X;
cluster Sspace(x) -> TopSpace-like;
end;
registration
let X be non empty TopSpace;
cluster discrete anti-discrete strict non empty for SubSpace of X;
end;
registration
let X be non empty TopSpace, x be Point of X;
cluster Sspace(x) -> discrete anti-discrete;
end;
registration
let X be non empty TopSpace;
cluster non proper -> open closed for SubSpace of X;
cluster non open -> proper for SubSpace of X;
cluster non closed -> proper for SubSpace of X;
end;
registration
let X be non empty TopSpace;
cluster open closed strict for SubSpace of X;
end;
registration
let X be discrete non empty TopSpace;
cluster anti-discrete -> trivial for non empty SubSpace of X;
cluster non trivial -> non anti-discrete for non empty SubSpace of X;
end;
registration
let X be discrete non trivial TopSpace;
cluster discrete open closed proper strict for SubSpace of X;
end;
registration
let X be anti-discrete non empty TopSpace;
cluster discrete -> trivial for non empty SubSpace of X;
cluster non trivial -> non discrete for non empty SubSpace of X;
end;
registration
let X be anti-discrete non trivial TopSpace;
cluster -> non open non closed for proper non empty SubSpace of X;
cluster -> trivial proper for discrete non empty SubSpace of X;
end;
registration
let X be anti-discrete non trivial TopSpace;
cluster anti-discrete non open non closed proper strict for SubSpace of X;
end;
registration
let X be almost_discrete non trivial TopSpace;
cluster almost_discrete proper strict non empty for SubSpace of X;
end;
begin
:: 3. Maximal Discrete Subsets and Subspaces.
definition
let Y be TopStruct, IT be Subset of Y;
attr IT is discrete means
:: TEX_2:def 3
for D being Subset of Y st D c= IT ex G
being Subset of Y st G is open & IT /\ G = D;
end;
definition
let Y be TopStruct;
let A be Subset of Y;
redefine attr A is discrete means
:: TEX_2:def 4
for D being Subset of Y st D c= A
ex F being Subset of Y st F is closed & A /\ F = D;
end;
theorem :: TEX_2:19
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
discrete implies D1 is discrete;
theorem :: TEX_2:20
for Y being non empty TopStruct, Y0 being non empty SubSpace of
Y, A being Subset of Y st A = the carrier of Y0 holds A is discrete iff Y0 is
discrete;
theorem :: TEX_2:21
for Y being non empty TopStruct, A being Subset of Y st A = the
carrier of Y holds A is discrete iff Y is discrete;
theorem :: TEX_2:22
for A, B being Subset of Y st B c= A holds A is discrete implies
B is discrete;
theorem :: TEX_2:23
for A, B being Subset of Y holds A is discrete or B is discrete
implies A /\ B is discrete;
theorem :: TEX_2:24
(for P, Q being Subset of Y st P is open & Q is open holds P /\
Q is open & P \/ Q is open) implies for A, B being Subset of Y st A is open & B
is open holds A is discrete & B is discrete implies A \/ B is discrete;
theorem :: TEX_2:25
(for P, Q being Subset of Y st P is closed & Q is closed holds P
/\ Q is closed & P \/ Q is closed) implies for A, B being Subset of Y st A is
closed & B is closed holds A is discrete & B is discrete implies A \/ B is
discrete;
theorem :: TEX_2:26
for A being Subset of Y holds A is discrete implies for x being
Point of Y st x in A ex G being Subset of Y st G is open & A /\ G = {x};
theorem :: TEX_2:27
for A being Subset of Y holds A is discrete implies for x being Point
of Y st x in A ex F being Subset of Y st F is closed & A /\ F = {x};
reserve X for non empty TopSpace;
theorem :: TEX_2:28
for A0 being non empty Subset of X st A0 is discrete ex X0 being
discrete strict non empty SubSpace of X st A0 = the carrier of X0;
theorem :: TEX_2:29
for A being empty Subset of X holds A is discrete;
theorem :: TEX_2:30
for x being Point of X holds {x} is discrete;
theorem :: TEX_2:31
for A being Subset of X holds (for x being Point of X st x in A
ex G being Subset of X st G is open & A /\ G = {x}) implies A is discrete;
theorem :: TEX_2:32
for A, B being Subset of X st A is open & B is open holds A is
discrete & B is discrete implies A \/ B is discrete;
theorem :: TEX_2:33
for A, B being Subset of X st A is closed & B is closed holds A is
discrete & B is discrete implies A \/ B is discrete;
theorem :: TEX_2:34
for A being Subset of X st A is everywhere_dense holds A is discrete
implies A is open;
theorem :: TEX_2:35
for A being Subset of X holds A is discrete iff for D being
Subset of X st D c= A holds A /\ Cl D = D;
theorem :: TEX_2:36
for A being Subset of X holds A is discrete implies for x being
Point of X st x in A holds A /\ Cl {x} = {x};
theorem :: TEX_2:37
for X being discrete non empty TopSpace, A being Subset of X holds A
is discrete;
theorem :: TEX_2:38
for X being anti-discrete non empty TopSpace, A being non empty
Subset of X holds A is discrete iff A is trivial;
definition
let Y be TopStruct, IT be Subset of Y;
attr IT is maximal_discrete means
:: TEX_2:def 5
IT is discrete & for D being Subset
of Y st D is discrete & IT c= D holds IT = D;
end;
theorem :: TEX_2:39
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_discrete implies D1 is maximal_discrete;
theorem :: TEX_2:40
for A being empty Subset of X holds A is not maximal_discrete;
theorem :: TEX_2:41
for A being Subset of X st A is open holds A is maximal_discrete
implies A is dense;
theorem :: TEX_2:42
for A being Subset of X st A is dense holds A is discrete implies A is
maximal_discrete;
theorem :: TEX_2:43
for X being discrete non empty TopSpace, A being Subset of X
holds A is maximal_discrete iff A is non proper;
theorem :: TEX_2:44
for X being anti-discrete non empty TopSpace, A being non empty
Subset of X holds A is maximal_discrete iff A is trivial;
definition
let Y be non empty TopStruct;
let IT be SubSpace of Y;
attr IT is maximal_discrete means
:: TEX_2:def 6
for A being Subset of Y st A = the carrier of IT holds A is maximal_discrete;
end;
theorem :: TEX_2:45
for Y being non empty TopStruct, Y0 being SubSpace of Y, A being
Subset of Y st A = the carrier of Y0 holds A is maximal_discrete iff Y0 is
maximal_discrete;
registration
let Y be non empty TopStruct;
cluster maximal_discrete -> discrete for non empty SubSpace of Y;
cluster non discrete -> non maximal_discrete for non empty SubSpace of Y;
end;
theorem :: TEX_2:46
for X0 being non empty SubSpace of X holds X0 is maximal_discrete iff
X0 is discrete & for Y0 being discrete non empty SubSpace of X st X0 is
SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0;
theorem :: TEX_2:47
for A0 being non empty Subset of X st A0 is maximal_discrete ex
X0 being strict non empty SubSpace of X st X0 is maximal_discrete & A0 = the
carrier of X0;
registration
let X be discrete non empty TopSpace;
cluster maximal_discrete -> non proper for SubSpace of X;
cluster proper -> non maximal_discrete for SubSpace of X;
cluster non proper -> maximal_discrete for SubSpace of X;
cluster non maximal_discrete -> proper for SubSpace of X;
end;
registration
let X be anti-discrete non empty TopSpace;
cluster maximal_discrete -> trivial for non empty SubSpace of X;
cluster non trivial -> non maximal_discrete for non empty SubSpace of X;
cluster trivial -> maximal_discrete for non empty SubSpace of X;
cluster non maximal_discrete -> non trivial for non empty SubSpace of X;
end;
begin
:: 4. Maximal Discrete Subspaces of Almost Discrete Spaces.
scheme :: TEX_2:sch 1
ExChoiceFCol{X()->non empty TopStruct,F()->Subset-Family of X(),
P[object,object]}:
ex f being Function of F(),the carrier of X() st for S being Subset of X() st S
in F() holds P[S,f.S]
provided
for S being Subset of X() st S in F() ex x being Point of X() st P[S ,x];
reserve X for almost_discrete non empty TopSpace;
theorem :: TEX_2:48
for A being Subset of X holds Cl A = union {Cl {a} where a is
Point of X : a in A};
theorem :: TEX_2:49
for a, b being Point of X holds a in Cl {b} implies Cl {a} = Cl {b};
theorem :: TEX_2:50
for a, b being Point of X holds Cl {a} misses Cl {b} or Cl {a} = Cl {b};
theorem :: TEX_2:51
for A being Subset of X holds (for x being Point of X st x in A
ex F being Subset of X st F is closed & A /\ F = {x}) implies A is discrete;
theorem :: TEX_2:52
for A being Subset of X holds (for x being Point of X st x in A
holds A /\ Cl {x} = {x}) implies A is discrete;
theorem :: TEX_2:53
for A being Subset of X holds A is discrete iff for a, b being Point
of X st a in A & b in A holds a <> b implies Cl {a} misses Cl {b};
theorem :: TEX_2:54
for A being Subset of X holds A is discrete iff for x being
Point of X st x in Cl A ex a being Point of X st a in A & A /\ Cl {x} = {a};
theorem :: TEX_2:55
for A being Subset of X st A is open or A is closed holds A is
maximal_discrete implies A is not proper;
theorem :: TEX_2:56
for A being Subset of X holds A is maximal_discrete implies A is dense;
theorem :: TEX_2:57
for A being Subset of X st A is maximal_discrete holds union {Cl
{a} where a is Point of X : a in A} = the carrier of X;
theorem :: TEX_2:58
for A being Subset of X holds A is maximal_discrete iff for x
being Point of X ex a being Point of X st a in A & A /\ Cl {x} = {a};
theorem :: TEX_2:59
for A being Subset of X holds A is discrete implies ex M being
Subset of X st A c= M & M is maximal_discrete;
theorem :: TEX_2:60
ex M being Subset of X st M is maximal_discrete;
theorem :: TEX_2:61
for Y0 being discrete non empty SubSpace of X ex X0 being strict
non empty SubSpace of X st Y0 is SubSpace of X0 & X0 is maximal_discrete;
registration
let X be almost_discrete non discrete non empty TopSpace;
cluster maximal_discrete -> proper for non empty SubSpace of X;
cluster non proper -> non maximal_discrete for non empty SubSpace of X;
end;
registration
let X be almost_discrete non anti-discrete non empty TopSpace;
cluster maximal_discrete -> non trivial for non empty SubSpace of X;
cluster trivial -> non maximal_discrete for non empty SubSpace of X;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster maximal_discrete strict non empty non empty for SubSpace of X;
end;
begin
:: 5. Continuous Mappings and Almost Discrete Spaces.
reserve X,Y for non empty TopSpace;
theorem :: TEX_2:62
for X being discrete TopSpace, Y being TopSpace, f being
Function of X,Y holds f is continuous;
theorem :: TEX_2:63
(for Y being non empty TopSpace, f being Function of X,Y holds f is
continuous) implies X is discrete;
theorem :: TEX_2:64
for Y being anti-discrete non empty TopSpace, f being Function of X,Y
holds f is continuous;
theorem :: TEX_2:65
(for X being non empty TopSpace, f being Function of X,Y holds f is
continuous ) implies Y is anti-discrete;
reserve X for discrete non empty TopSpace,
X0 for non empty SubSpace of X;
theorem :: TEX_2:66
ex r being continuous Function of X,X0 st r is being_a_retraction;
theorem :: TEX_2:67
X0 is_a_retract_of X;
reserve X for almost_discrete non empty TopSpace,
X0 for maximal_discrete non empty SubSpace of X;
theorem :: TEX_2:68
ex r being continuous Function of X,X0 st r is being_a_retraction;
theorem :: TEX_2:69
X0 is_a_retract_of X;
theorem :: TEX_2:70
for r being continuous Function of X,X0 holds r is
being_a_retraction implies for F being Subset of X0, E being Subset of X st F =
E holds r" F = Cl E;
theorem :: TEX_2:71
for r being continuous Function of X,X0 holds r is being_a_retraction
implies for a being Point of X0, b being Point of X st a = b holds r" {a} = Cl
{b};
reserve X0 for discrete non empty SubSpace of X;
theorem :: TEX_2:72
ex r being continuous Function of X,X0 st r is being_a_retraction;
theorem :: TEX_2:73
X0 is_a_retract_of X;