:: Maximal Discrete Subspaces of Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received November 5, 1993
:: Copyright (c) 1993-2026 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;
definitions XBOOLE_0;
equalities XBOOLE_0, COMPTS_1, SUBSET_1, STRUCT_0;
expansions PRE_TOPC, XBOOLE_0, SUBSET_1, STRUCT_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, FUNCT_2, PRE_TOPC, TOPS_1, TOPS_2,
BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, TEX_1, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_1, FUNCT_2;
begin
:: 1. Proper Subsets of 1-sorted Structures.
theorem Th1:
for A being non empty set, B being 1-element set st A c=
B holds A = B
proof
let A be non empty set, B be 1-element set;
assume
A1: A c= B;
ex s being Element of B st B = {s} by SUBSET_1:46;
hence thesis by A1,ZFMISC_1:33;
end;
theorem
for A being 1-element set, B being set st A /\ B is non empty
holds A c= B
proof
let A be 1-element set, B be set;
A1: A /\ B c= B by XBOOLE_1:17;
assume A /\ B is non empty;
then consider a being object such that
A2: a in A /\ B;
A3: ex s being Element of A st A = {s} by SUBSET_1:46;
A /\ B c= A by XBOOLE_1:17;
then {a} c= A by A2,ZFMISC_1:31;
then {a} = A by A3,ZFMISC_1:18;
hence thesis by A2,A1,ZFMISC_1:31;
end;
registration
let S be 1-element set;
cluster proper -> empty for Subset of S;
coherence
proof
let A be Subset of S;
assume A is proper;
then
A1: A <> S;
ex s being Element of S st S = {s} by SUBSET_1:46;
hence thesis by A1,ZFMISC_1:33;
end;
cluster non empty -> non proper for Subset of S;
coherence;
end;
theorem
for S being non empty set, y being Element of S holds {y} is proper
implies S is non trivial;
theorem
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;
coherence;
end;
registration
let S be non trivial set;
cluster trivial -> proper for non empty Subset of S;
coherence;
cluster non proper -> non trivial for non empty Subset of S;
coherence;
end;
registration
let S be non trivial set;
cluster trivial proper for non empty Subset of S;
existence
proof
set A = the trivial non empty Subset of S;
take A;
thus thesis;
end;
cluster non trivial non proper for non empty Subset of S;
existence
proof
take [#]S;
thus thesis;
end;
end;
theorem
for Y being non empty 1-sorted, y being Element of Y holds {y} is
proper implies Y is non trivial;
theorem
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;
coherence;
cluster non proper -> trivial for non empty Subset of Y;
coherence;
end;
registration
let Y be non trivial 1-sorted;
cluster trivial -> proper for non empty Subset of Y;
coherence;
cluster non proper -> non trivial for non empty Subset of Y;
coherence;
end;
registration
let Y be non trivial 1-sorted;
cluster trivial proper for non empty Subset of Y;
existence
proof
set A = the trivial non empty Subset of Y;
take A;
thus thesis;
end;
cluster non trivial non proper for non empty Subset of Y;
existence
proof
take [#]Y;
thus thesis;
end;
end;
registration
let Y be non trivial 1-sorted;
cluster non empty trivial proper for Subset of Y;
existence
proof
set X = the trivial proper non empty Subset of Y;
reconsider X as Subset of Y;
take X;
thus thesis;
end;
end;
registration
let X be non empty set;
let A be proper Subset of X;
cluster A` -> non empty;
coherence
proof
assume A` is empty;
then A`` = X;
hence thesis by SUBSET_1:def 6;
end;
end;
begin
:: 2. Proper Subspaces of Topological Spaces.
theorem
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
:Def1:
for A being Subset of Y st A = the carrier of IT holds A is proper;
end;
reserve Y for TopStruct;
theorem
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;
Lm1: now
let Z be TopStruct;
let Z0 be SubSpace of Z;
[#]Z0 c= [#]Z by PRE_TOPC:def 4;
hence the carrier of Z0 is Subset of Z;
end;
theorem
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
for Y0 being SubSpace of Y holds the carrier of Y0 = the carrier
of Y implies Y0 is non proper
proof
let Y0 be SubSpace of Y;
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
assume
A1: the carrier of Y0 = the carrier of Y;
now
take A;
thus A = the carrier of Y0 & A is non proper by A1;
end;
hence thesis;
end;
registration
let Y be 1-element TopStruct;
cluster -> non proper for non empty SubSpace of Y;
coherence
proof
let Y0 be non empty SubSpace of Y;
reconsider A = the carrier of Y0 as non empty Subset of Y by Lm1;
now
take A;
thus A = the carrier of Y0 & A is non proper;
end;
hence thesis;
end;
cluster non proper -> trivial for non empty SubSpace of Y;
coherence;
end;
registration
let Y be non trivial TopStruct;
cluster trivial -> proper for non empty SubSpace of Y;
coherence;
cluster non proper -> non trivial for non empty SubSpace of Y;
coherence;
end;
registration
let Y be non empty TopStruct;
cluster non proper strict non empty for SubSpace of Y;
existence
proof
[#]Y = the carrier of Y;
then reconsider A0 = the carrier of Y as non empty Subset of Y;
set Y0 = Y|A0;
take Y0;
A0 = [#]Y0 by PRE_TOPC:def 5;
hence thesis;
end;
end;
theorem
for Y being non empty TopStruct, Y0 being non proper SubSpace of Y
holds the TopStruct of Y0 = the TopStruct of Y
proof
let Y be non empty TopStruct;
let Y0 be non proper SubSpace of Y;
A1: ex A being Subset of Y st A = the carrier of Y0 & A is non proper by Def1;
now
let D be object;
assume
A2: D in the topology of Y;
then reconsider E = D as Subset of Y;
reconsider C = E as Subset of Y0 by A1;
now
take E;
thus E in the topology of Y & C = E /\ [#]Y0 by A2,XBOOLE_1:28;
end;
hence D in the topology of Y0 by PRE_TOPC:def 4;
end;
then
A3: the topology of Y c= the topology of Y0 by TARSKI:def 3;
A4: the carrier of Y0 = the carrier of Y by A1;
now
let D be object;
assume
A5: D in the topology of Y0;
then reconsider C = D as Subset of Y0;
ex E being Subset of Y st E in the topology of Y & C = E /\ [#]Y0
by A5,PRE_TOPC:def 4;
hence D in the topology of Y by A4,XBOOLE_1:28;
end;
then the topology of Y0 c= the topology of Y by TARSKI:def 3;
then the topology of Y0 = the topology of Y by A3;
hence thesis by A1;
end;
registration
let Y be non empty TopStruct;
cluster discrete -> TopSpace-like for SubSpace of Y;
coherence;
cluster anti-discrete -> TopSpace-like for SubSpace of Y;
coherence;
cluster non TopSpace-like -> non discrete for SubSpace of Y;
coherence;
cluster non TopSpace-like -> non anti-discrete for SubSpace of Y;
coherence;
end;
theorem Th12:
for Y0, Y1 being TopStruct st the TopStruct of Y0 = the
TopStruct of Y1 holds Y0 is discrete implies Y1 is discrete
proof
let Y0, Y1 be TopStruct;
assume
A1: the TopStruct of Y0 = the TopStruct of Y1;
assume Y0 is discrete;
then the topology of Y0 = bool the carrier of Y0 by TDLAT_3:def 1;
hence thesis by A1,TDLAT_3:def 1;
end;
theorem
for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of
Y1 holds Y0 is anti-discrete implies Y1 is anti-discrete
proof
let Y0, Y1 be TopStruct;
assume
A1: the TopStruct of Y0 = the TopStruct of Y1;
assume Y0 is anti-discrete;
then the topology of Y0 = {{},the carrier of Y0} by TDLAT_3:def 2;
hence thesis by A1,TDLAT_3:def 2;
end;
registration
let Y be non empty TopStruct;
cluster discrete -> almost_discrete for SubSpace of Y;
coherence;
cluster non almost_discrete -> non discrete for SubSpace of Y;
coherence;
cluster anti-discrete -> almost_discrete for SubSpace of Y;
coherence;
cluster non almost_discrete -> non anti-discrete for SubSpace of Y;
coherence;
end;
theorem
for Y0, Y1 being TopStruct st the TopStruct of Y0 = the TopStruct of
Y1 holds Y0 is almost_discrete implies Y1 is almost_discrete
proof
let Y0, Y1 be TopStruct;
assume
A1: the TopStruct of Y0 = the TopStruct of Y1;
assume Y0 is almost_discrete;
then for A being Subset of Y0 st A in the topology of Y0 holds (the carrier
of Y0) \ A in the topology of Y0 by TDLAT_3:def 3;
hence thesis by A1,TDLAT_3:def 3;
end;
registration
let Y be non empty TopStruct;
cluster discrete anti-discrete -> trivial for non empty SubSpace of Y;
coherence;
cluster anti-discrete non trivial -> non discrete for
non empty SubSpace of Y;
coherence;
cluster discrete non trivial -> non anti-discrete for
non empty SubSpace of Y;
coherence;
end;
definition
let Y be non empty TopStruct, y be Point of Y;
func Sspace(y) -> strict non empty SubSpace of Y means
:Def2:
the carrier of it = {y};
existence
proof
reconsider D = {y} as non empty Subset of Y;
set Y0 = Y|D;
take Y0;
D = [#]Y0 by PRE_TOPC:def 5;
hence thesis;
end;
uniqueness
proof
let Y1, Y2 be strict non empty SubSpace of Y;
assume that
A1: the carrier of Y1 = {y} and
A2: the carrier of Y2 = {y};
set A1 = the carrier of Y1, A2 = the carrier of Y2;
A3: A2 = [#]Y2;
A4: A1 = [#]Y1;
then A1 c= [#]Y by PRE_TOPC:def 4;
then reconsider A1 as Subset of Y;
Y1 = Y|A1 by A4,PRE_TOPC:def 5;
hence thesis by A1,A2,A3,PRE_TOPC:def 5;
end;
end;
Lm2: now
let Y be non empty TopStruct, y be Point of Y;
set Y0 = Sspace(y);
the carrier of Y0 = {y} by Def2;
then reconsider y0 = y as Point of Y0 by TARSKI:def 1;
the carrier of Y0 = {y0} by Def2;
hence Sspace(y) is 1-element;
end;
registration
let Y be non empty TopStruct;
cluster strict 1-element for SubSpace of Y;
existence
proof
set y = the Point of Y;
take Sspace(y);
thus thesis by Lm2;
end;
end;
registration
let Y be non empty TopStruct, y be Point of Y;
cluster Sspace(y) -> 1-element;
coherence by Lm2;
end;
theorem
for Y being non empty TopStruct, y being Point of Y holds Sspace(y) is
proper iff {y} is proper
proof
let Y be non empty TopStruct, y be Point of Y;
hereby
reconsider A = the carrier of Sspace(y) as Subset of Y by Lm1;
assume
A1: Sspace(y) is proper;
A = {y} by Def2;
hence {y} is proper by A1;
end;
thus thesis by Def2;
end;
theorem
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;
existence
proof
take the trivial strict non empty SubSpace of Y;
thus thesis;
end;
end;
registration let Y be non empty TopStruct;
cluster 1-element for SubSpace of Y;
existence
proof
take Y0 = the trivial non empty SubSpace of Y;
thus thesis;
end;
end;
theorem
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)
proof
let Y be non empty TopStruct, Y0 be 1-element SubSpace of Y;
consider y0 being Element of Y0 such that
A1: the carrier of Y0 = {y0} by TEX_1:def 1;
the carrier of Y0 is Subset of Y by Lm1;
then reconsider y = y0 as Point of Y by A1,ZFMISC_1:31;
take y;
the carrier of Y0 = the carrier of Sspace(y) by A1,Def2;
hence thesis by TSEP_1:5;
end;
theorem
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;
coherence;
end;
registration
let X be non empty TopSpace;
cluster trivial strict TopSpace-like non empty for SubSpace of X;
existence
proof
set x = the Point of X;
take Sspace(x);
thus thesis;
end;
end;
registration
let X be non empty TopSpace, x be Point of X;
cluster Sspace(x) -> TopSpace-like;
coherence;
end;
registration
let X be non empty TopSpace;
cluster discrete anti-discrete strict non empty for SubSpace of X;
existence
proof
set x = the Point of X;
take Sspace(x);
thus thesis;
end;
end;
registration
let X be non empty TopSpace, x be Point of X;
cluster Sspace(x) -> discrete anti-discrete;
coherence;
end;
registration
let X be non empty TopSpace;
cluster non proper -> open closed for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
assume X0 is non proper;
then
A1: ex A being Subset of X st A = the carrier of X0 & A is non proper;
then
A2: for A be Subset of X st A = the carrier of X0 holds A is closed;
now
let A be Subset of X;
assume A = the carrier of X0;
then A = [#]X by A1;
hence A is open;
end;
hence thesis by A2,BORSUK_1:def 11,TSEP_1:def 1;
end;
cluster non open -> proper for SubSpace of X;
coherence;
cluster non closed -> proper for SubSpace of X;
coherence;
end;
registration
let X be non empty TopSpace;
cluster open closed strict for SubSpace of X;
existence
proof
set X0 = the non proper strict SubSpace of X;
take X0;
thus thesis;
end;
end;
registration
let X be discrete non empty TopSpace;
cluster anti-discrete -> trivial for non empty SubSpace of X;
coherence;
cluster non trivial -> non anti-discrete for non empty SubSpace of X;
coherence;
end;
registration
let X be discrete non trivial TopSpace;
cluster discrete open closed proper strict for SubSpace of X;
existence
proof
set X0 = the proper strict SubSpace of X;
take X0;
thus thesis;
end;
end;
registration
let X be anti-discrete non empty TopSpace;
cluster discrete -> trivial for non empty SubSpace of X;
coherence;
cluster non trivial -> non discrete for non empty SubSpace of X;
coherence;
end;
registration
let X be anti-discrete non trivial TopSpace;
cluster -> non open non closed for proper non empty SubSpace of X;
coherence
proof
let X0 be proper non empty SubSpace of X;
assume
A1: X0 is open or X0 is closed;
reconsider A = the carrier of X0 as non empty Subset of X by Lm1;
set B = A`;
A2: B <> the carrier of X by TOPS_3:1;
A3: A is proper by Def1;
then
A4: A <> the carrier of X;
now
per cases by A1;
suppose
X0 is open;
then A is open by TSEP_1:def 1;
then A in the topology of X;
then A in {{},the carrier of X} by TDLAT_3:def 2;
hence contradiction by A4,TARSKI:def 2;
end;
suppose
X0 is closed;
then A is closed by BORSUK_1:def 11;
then B in the topology of X by PRE_TOPC:def 2;
then B in {{},the carrier of X} by TDLAT_3:def 2;
hence contradiction by A3,A2,TARSKI:def 2;
end;
end;
hence thesis;
end;
cluster -> trivial proper for discrete non empty SubSpace of X;
coherence;
end;
registration
let X be anti-discrete non trivial TopSpace;
cluster anti-discrete non open non closed proper strict for SubSpace of X;
existence
proof
set X0 = the proper strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
registration
let X be almost_discrete non trivial TopSpace;
cluster almost_discrete proper strict non empty for SubSpace of X;
existence
proof
set X0 = the proper strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
begin
:: 3. Maximal Discrete Subsets and Subspaces.
definition
let Y be TopStruct, IT be Subset of Y;
attr IT is discrete means
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 :: redefines discrete (TEX_2, definition)
for D being Subset of Y st D c= A
ex F being Subset of Y st F is closed & A /\ F = D;
compatibility
proof
hereby
assume
A1: A is discrete;
let D be Subset of Y;
A \ D c= A by XBOOLE_1:36;
then consider G being Subset of Y such that
A2: G is open and
A3: A /\ G = A \ D by A1;
assume
A4: D c= A;
now
take F = [#]Y \ G;
G = [#]Y \ F by PRE_TOPC:3;
hence F is closed by A2;
A /\ [#]Y = A by XBOOLE_1:28;
then A /\ F = A \ G by XBOOLE_1:49;
then A /\ F = A \ (A \ D) by A3,XBOOLE_1:47;
then A /\ F = A /\ D by XBOOLE_1:48;
hence A /\ F = D by A4,XBOOLE_1:28;
end;
hence ex F being Subset of Y st F is closed & A /\ F = D;
end;
hereby
assume
A5: for D being Subset of Y st D c= A ex F being Subset of Y st F
is closed & A /\ F = D;
now
let D be Subset of Y;
consider F being Subset of Y such that
A6: F is closed and
A7: A /\ F = A \ D by A5,XBOOLE_1:36;
assume
A8: D c= A;
now
take G = [#]Y \ F;
thus G is open by A6;
A /\ [#]Y = A by XBOOLE_1:28;
then A /\ G = A \ F by XBOOLE_1:49;
then A /\ G = A \ (A \ D) by A7,XBOOLE_1:47;
then A /\ G = A /\ D by XBOOLE_1:48;
hence A /\ G = D by A8,XBOOLE_1:28;
end;
hence ex G being Subset of Y st G is open & A /\ G = D;
end;
hence A is discrete;
end;
end;
end;
theorem Th19:
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
proof
let Y0, Y1 be TopStruct, D0 be Subset of Y0, D1 be Subset of Y1;
assume
A1: the TopStruct of Y0 = the TopStruct of Y1;
assume
A2: D0 = D1;
assume
A3: D0 is discrete;
now
let D be Subset of Y1;
reconsider E = D as Subset of Y0 by A1;
assume D c= D1;
then consider G0 being Subset of Y0 such that
A4: G0 is open and
A5: D0 /\ G0 = E by A2,A3;
reconsider G = G0 as Subset of Y1 by A1;
now
take G;
G in the topology of Y1 by A1,A4;
hence G is open;
thus D1 /\ G = D by A2,A5;
end;
hence ex G being Subset of Y1 st G is open & D1 /\ G = D;
end;
hence thesis;
end;
theorem Th20:
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
proof
let Y be non empty TopStruct, Y0 be non empty SubSpace of Y, A be Subset of
Y;
assume
A1: A = the carrier of Y0;
A2: [#]Y = the carrier of Y;
[#]Y0 = the carrier of Y0;
then
A3: the carrier of Y0 c= the carrier of Y by A2,PRE_TOPC:def 4;
hereby
assume
A4: A is discrete;
now
let C be object;
assume C in bool the carrier of Y0;
then reconsider B = C as Subset of Y0;
reconsider D = B as Subset of Y by A3,XBOOLE_1:1;
consider G being Subset of Y such that
A5: G is open and
A6: A /\ G = D by A1,A4;
G in the topology of Y & B = G /\ [#]Y0 by A1,A6,A5;
hence C in the topology of Y0 by PRE_TOPC:def 4;
end;
then bool the carrier of Y0 c= the topology of Y0 by TARSKI:def 3;
then the topology of Y0 = bool the carrier of Y0;
hence Y0 is discrete by TDLAT_3:def 1;
end;
hereby
assume
A7: Y0 is discrete;
now
let D be Subset of Y;
assume D c= A;
then reconsider B = D as Subset of Y0 by A1;
B is open by A7,TDLAT_3:15;
then B in the topology of Y0;
then consider G being Subset of Y such that
A8: G in the topology of Y and
A9: B = G /\ [#]Y0 by PRE_TOPC:def 4;
reconsider G as Subset of Y;
take G;
thus G is open by A8;
thus A /\ G = D by A1,A9;
end;
hence A is discrete;
end;
end;
theorem Th21:
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
proof
let Y be non empty TopStruct, A be Subset of Y;
assume
A1: A = the carrier of Y;
hereby
assume
A2: A is discrete;
now
let C be object;
assume C in bool the carrier of Y;
then reconsider B = C as Subset of Y;
consider G being Subset of Y such that
A3: G is open and
A4: A /\ G = B by A1,A2;
G = B by A1,A4,XBOOLE_1:28;
hence C in the topology of Y by A3;
end;
then bool the carrier of Y c= the topology of Y by TARSKI:def 3;
then the topology of Y = bool the carrier of Y;
hence Y is discrete by TDLAT_3:def 1;
end;
hereby
assume Y is discrete;
then reconsider Y as discrete non empty TopStruct;
now
let D be Subset of Y;
assume
A5: D c= A;
reconsider G = D as Subset of Y;
take G;
thus G is open by TDLAT_3:15;
thus A /\ G = D by A5,XBOOLE_1:28;
end;
hence A is discrete;
end;
end;
theorem Th22:
for A, B being Subset of Y st B c= A holds A is discrete implies
B is discrete
proof
let A, B be Subset of Y;
assume
A1: B c= A;
assume
A2: A is discrete;
now
let D be Subset of Y;
assume
A3: D c= B;
then D c= A by A1,XBOOLE_1:1;
then consider G being Subset of Y such that
A4: G is open and
A5: A /\ G = D by A2;
hereby
take G;
D c= G by A5,XBOOLE_1:17;
then
A6: D c= B /\ G by A3,XBOOLE_1:19;
B /\ G c= A /\ G by A1,XBOOLE_1:26;
hence G is open & B /\ G = D by A4,A5,A6;
end;
end;
hence thesis;
end;
theorem
for A, B being Subset of Y holds A is discrete or B is discrete
implies A /\ B is discrete
proof
let A, B be Subset of Y;
assume
A1: A is discrete or B is discrete;
hereby
per cases by A1;
suppose
A is discrete;
hence thesis by Th22,XBOOLE_1:17;
end;
suppose
B is discrete;
hence thesis by Th22,XBOOLE_1:17;
end;
end;
end;
theorem Th24:
(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
proof
assume
A1: for P,Q being Subset of Y st P is open & Q is open holds P /\ Q is
open & P \/ Q is open;
let A, B be Subset of Y;
assume that
A2: A is open and
A3: B is open;
assume that
A4: A is discrete and
A5: B is discrete;
now
let D be Subset of Y;
D /\ A c= A by XBOOLE_1:17;
then consider G1 being Subset of Y such that
A6: G1 is open and
A7: A /\ G1 = D /\ A by A4;
D /\ B c= B by XBOOLE_1:17;
then consider G2 being Subset of Y such that
A8: G2 is open and
A9: B /\ G2 = D /\ B by A5;
assume D c= A \/ B;
then
A10: D = D /\ (A \/ B) by XBOOLE_1:28;
now
take G = (A /\ G1) \/ (B /\ G2);
A11: B /\ G2 is open by A1,A3,A8;
A /\ G1 is open by A1,A2,A6;
hence G is open by A1,A11;
thus (A \/ B) /\ G = D by A10,A7,A9,XBOOLE_1:23;
end;
hence ex G being Subset of Y st G is open & (A \/ B) /\ G = D;
end;
hence thesis;
end;
theorem Th25:
(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
proof
assume
A1: for P,Q being Subset of Y st P is closed & Q is closed holds P /\ Q
is closed & P \/ Q is closed;
let A, B be Subset of Y;
assume that
A2: A is closed and
A3: B is closed;
assume that
A4: A is discrete and
A5: B is discrete;
now
let D be Subset of Y;
D /\ A c= A by XBOOLE_1:17;
then consider F1 being Subset of Y such that
A6: F1 is closed and
A7: A /\ F1 = D /\ A by A4;
D /\ B c= B by XBOOLE_1:17;
then consider F2 being Subset of Y such that
A8: F2 is closed and
A9: B /\ F2 = D /\ B by A5;
assume D c= A \/ B;
then
A10: D = D /\ (A \/ B) by XBOOLE_1:28;
now
take F = (A /\ F1) \/ (B /\ F2);
A11: B /\ F2 is closed by A1,A3,A8;
A /\ F1 is closed by A1,A2,A6;
hence F is closed by A1,A11;
thus (A \/ B) /\ F = D by A10,A7,A9,XBOOLE_1:23;
end;
hence ex F being Subset of Y st F is closed & (A \/ B) /\ F = D;
end;
hence thesis;
end;
theorem Th26:
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}
proof
let A be Subset of Y;
assume
A1: A is discrete;
let x be Point of Y;
assume
A2: x in A;
then reconsider Y9 = Y as non empty TopStruct;
reconsider B = {x} as Subset of Y9 by ZFMISC_1:31;
reconsider A9 = A as Subset of Y9;
{x} c= A9 by A2,ZFMISC_1:31;
then consider G being Subset of Y9 such that
A3: G is open and
A4: A9 /\ G = B by A1;
reconsider G as Subset of Y;
take G;
thus thesis by A3,A4;
end;
theorem
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}
proof
let A be Subset of Y;
assume
A1: A is discrete;
let x be Point of Y;
assume
A2: x in A;
then reconsider Y9 = Y as non empty TopStruct;
reconsider B = {x} as Subset of Y9 by ZFMISC_1:31;
reconsider A9 = A as Subset of Y9;
{x} c= A9 by A2,ZFMISC_1:31;
then consider F being Subset of Y such that
A3: F is closed and
A4: A9 /\ F = B by A1;
take F;
thus thesis by A3,A4;
end;
reserve X for non empty TopSpace;
theorem Th28:
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
proof
let A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is discrete;
then reconsider X0 as discrete strict non empty SubSpace of X by A1,Th20;
take X0;
thus thesis by A1;
end;
theorem Th29:
for A being empty Subset of X holds A is discrete
proof
let A be empty Subset of X;
now
let D be Subset of X;
assume
A1: D c= A;
now
take G = {}X;
thus G is open & A /\ G = D by A1;
end;
hence ex G being Subset of X st G is open & A /\ G = D;
end;
hence thesis;
end;
theorem Th30:
for x being Point of X holds {x} is discrete
proof
let x be Point of X;
now
let D be Subset of X;
A1: now
assume
A2: D = {};
hereby
take G = {}X;
thus G is open & {x} /\ G = D by A2;
end;
end;
A3: now
assume
A4: D = {x};
hereby
take G = [#]X;
thus G is open & {x} /\ G = D by A4,XBOOLE_1:28;
end;
end;
assume D c= {x};
hence ex G being Subset of X st G is open & {x} /\ G = D by A1,A3,
ZFMISC_1:33;
end;
hence thesis;
end;
theorem Th31:
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
proof
let A be Subset of X;
assume
A1: for x being Point of X st x in A ex G being Subset of X st G is open
& A /\ G = {x};
hereby
per cases;
suppose
A is empty;
hence thesis by Th29;
end;
suppose
A is non empty;
then consider X0 being strict non empty SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
A3: [#]X = the carrier of X;
[#]X0 = the carrier of X0;
then
A4: the carrier of X0 c= the carrier of X by A3,PRE_TOPC:def 4;
now
let C be Subset of X0;
let y be Point of X0;
reconsider x = y as Point of X by A4,TARSKI:def 3;
consider G being Subset of X such that
A5: G is open and
A6: A /\ G = {x} by A1,A2;
assume
A7: C = {y};
G in the topology of X & G /\ [#]X0 = C by A2,A7,A6,A5;
then C in the topology of X0 by PRE_TOPC:def 4;
hence C is open;
end;
then X0 is discrete by TDLAT_3:17;
hence thesis by A2,Th20;
end;
end;
end;
theorem
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
proof
let A, B be Subset of X;
assume that
A1: A is open and
A2: B is open;
assume that
A3: A is discrete and
A4: B is discrete;
for P, Q being Subset of X st P is open & Q is open holds P /\ Q is open
& P \/ Q is open;
hence thesis by A1,A2,A3,A4,Th24;
end;
theorem
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
proof
let A, B be Subset of X;
assume that
A1: A is closed and
A2: B is closed;
assume that
A3: A is discrete and
A4: B is discrete;
for P, Q being Subset of X st P is closed & Q is closed holds P /\ Q is
closed & P \/ Q is closed;
hence thesis by A1,A2,A3,A4,Th25;
end;
Lm3: for P, Q being set st P c= Q & P <> Q holds Q \ P <> {}
proof
let P, Q be set;
assume P c= Q;
then
A1: Q = P \/ (Q \ P) by XBOOLE_1:45;
assume
A2: P <> Q;
assume Q \ P = {};
hence contradiction by A1,A2;
end;
theorem
for A being Subset of X st A is everywhere_dense holds A is discrete
implies A is open
proof
let A be Subset of X;
assume A is everywhere_dense;
then
A1: Cl Int A = the carrier of X by TOPS_3:def 5;
assume
A2: A is discrete;
assume A is not open;
then A \ Int A <> {} by Lm3,TOPS_1:16;
then consider a being object such that
A3: a in A \ Int A by XBOOLE_0:def 1;
reconsider a as Point of X by A3;
A \ Int A c= A by XBOOLE_1:36;
then consider G being Subset of X such that
A4: G is open and
A5: A /\ G = {a} by A2,A3,Th26;
A6: now
assume Int A /\ G = {a};
then {a} c= Int A by XBOOLE_1:17;
then a in Int A by ZFMISC_1:31;
hence contradiction by A3,XBOOLE_0:def 5;
end;
Int A /\ G c= {a} by A5,TOPS_1:16,XBOOLE_1:26;
then Int A /\ G = {} or Int A /\ G = {a} by ZFMISC_1:33;
then Int A misses G or Int A /\ G = {a};
then Cl Int A misses G by A4,A6,TSEP_1:36;
then
A7: Cl Int A /\ G = {};
{a} c= G by A5,XBOOLE_1:17;
hence contradiction by A1,A7,XBOOLE_1:3,19;
end;
theorem Th35:
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
proof
let A be Subset of X;
thus A is discrete implies for D being Subset of X st D c= A holds A /\ Cl D
= D
proof
assume
A1: A is discrete;
let D be Subset of X;
assume
A2: D c= A;
then consider F being Subset of X such that
A3: F is closed and
A4: A /\ F = D by A1;
Cl D c= F by A3,A4,TOPS_1:5,XBOOLE_1:17;
then
A5: A /\ Cl D c= D by A4,XBOOLE_1:26;
D c= Cl D by PRE_TOPC:18;
then D c= A /\ Cl D by A2,XBOOLE_1:19;
hence thesis by A5;
end;
assume
A6: for D being Subset of X st D c= A holds A /\ Cl D = D;
now
let D be Subset of X;
assume
A7: D c= A;
now
take F = Cl D;
thus F is closed;
thus A /\ F = D by A6,A7;
end;
hence ex F being Subset of X st F is closed & A /\ F = D;
end;
hence thesis;
end;
theorem Th36:
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}
by ZFMISC_1:31,Th35;
theorem
for X being discrete non empty TopSpace, A being Subset of X holds A
is discrete
proof
let X be discrete non empty TopSpace, A be Subset of X;
hereby
per cases;
suppose
A is empty;
hence thesis by Th29;
end;
suppose
A is non empty;
then
ex X0 being strict non empty SubSpace of X st A = the carrier of X0
by TSEP_1:10;
hence thesis by Th20;
end;
end;
end;
theorem Th38:
for X being anti-discrete non empty TopSpace, A being non empty
Subset of X holds A is discrete iff A is trivial
proof
let X be anti-discrete non empty TopSpace, A be non empty Subset of X;
hereby
consider a being object such that
A1: a in A by XBOOLE_0:def 1;
reconsider a as Point of X by A1;
assume A is discrete;
then consider G being Subset of X such that
A2: G is open and
A3: A /\ G = {a} by A1,Th26;
G <> {} by A3;
then
A4: G = the carrier of X by A2,TDLAT_3:18;
now
take a;
thus A = {a} by A3,A4,XBOOLE_1:28;
end;
hence A is trivial;
end;
hereby
assume A is trivial;
then ex a being Element of A st A = {a} by SUBSET_1:46;
hence A is discrete by Th30;
end;
end;
definition
let Y be TopStruct, IT be Subset of Y;
attr IT is maximal_discrete means
IT is discrete & for D being Subset
of Y st D is discrete & IT c= D holds IT = D;
end;
theorem
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
proof
let Y0, Y1 be TopStruct, D0 be Subset of Y0, D1 be Subset of Y1;
assume
A1: the TopStruct of Y0 = the TopStruct of Y1;
assume
A2: D0 = D1;
assume
A3: D0 is maximal_discrete;
A4: now
let D be Subset of Y1;
reconsider E = D as Subset of Y0 by A1;
assume D is discrete;
then
A5: E is discrete by A1,Th19;
assume D1 c= D;
hence D1 = D by A2,A3,A5;
end;
D0 is discrete by A3;
then D1 is discrete by A1,A2,Th19;
hence thesis by A4;
end;
theorem Th40:
for A being empty Subset of X holds A is not maximal_discrete
proof
consider a being object such that
A1: a in the carrier of X by XBOOLE_0:def 1;
reconsider a as Point of X by A1;
let A be empty Subset of X;
now
take C = {a};
thus C is discrete & A c= C & A <> C by Th30,XBOOLE_1:2;
end;
hence thesis;
end;
theorem Th41:
for A being Subset of X st A is open holds A is maximal_discrete
implies A is dense
proof
let A be Subset of X;
assume
A1: A is open;
assume
A2: A is maximal_discrete;
then
A3: A is discrete;
assume A is not dense;
then Cl A <> the carrier of X by TOPS_3:def 2;
then (the carrier of X) \ Cl A <> {} by Lm3;
then consider a being object such that
A4: a in (the carrier of X) \ Cl A by XBOOLE_0:def 1;
reconsider a as Point of X by A4;
set B = A \/ {a};
A5: A c= B by XBOOLE_1:7;
A6: now
let x be Point of X;
assume x in B;
then
A7: x in A or x in {a} by XBOOLE_0:def 3;
now
per cases by A7,TARSKI:def 1;
suppose
A8: x in A;
then
A9: ex G being Subset of X st G is open & A /\ G = {x} by A3,Th26;
now
take E = {x};
thus E is open by A1,A9;
{x} c= B by A5,A8,ZFMISC_1:31;
hence B /\ E = {x} by XBOOLE_1:28;
end;
hence ex E being Subset of X st E is open & B /\ E = {x};
end;
suppose
A10: x = a;
now
take G = [#]X \ Cl A;
A11: B /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
A12: G = (Cl A)`;
hence G is open;
A c= Cl A by PRE_TOPC:18;
then A misses G by A12,SUBSET_1:24;
then
A13: A /\ G = {};
{a} c= G by A4,ZFMISC_1:31;
hence B /\ G = {x} by A10,A13,A11,XBOOLE_1:28;
end;
hence ex G being Subset of X st G is open & B /\ G = {x};
end;
end;
hence ex G being Subset of X st G is open & B /\ G = {x};
end;
A c= Cl A by PRE_TOPC:18;
then
A14: not a in A by A4,XBOOLE_0:def 5;
ex D being Subset of X st D is discrete & A c= D & A <> D
proof
take B;
thus B is discrete by A6,Th31;
thus A c= B by XBOOLE_1:7;
A <> B by A14,ZFMISC_1:31,XBOOLE_1:7;
hence thesis;
end;
hence contradiction by A2;
end;
theorem
for A being Subset of X st A is dense holds A is discrete implies A is
maximal_discrete
proof
let A be Subset of X;
assume
A1: A is dense;
assume
A2: A is discrete;
assume A is not maximal_discrete;
then consider D being Subset of X such that
A3: D is discrete and
A4: A c= D and
A5: A <> D by A2;
D \ A <> {} by A4,A5,Lm3;
then consider a being object such that
A6: a in D \ A by XBOOLE_0:def 1;
reconsider a as Point of X by A6;
a in D by A6,XBOOLE_0:def 5;
then consider G being Subset of X such that
A7: G is open and
A8: D /\ G = {a} by A3,Th26;
A9: now
assume A /\ G = {a};
then {a} c= A by XBOOLE_1:17;
then a in A by ZFMISC_1:31;
hence contradiction by A6,XBOOLE_0:def 5;
end;
A /\ G c= D /\ G by A4,XBOOLE_1:26;
then A /\ G = {} or A /\ G = {a} by A8,ZFMISC_1:33;
then A misses G or A /\ G = {a};
then Cl A misses G by A7,A9,TSEP_1:36;
then
A10: Cl A /\ G = {};
now
assume Cl A = the carrier of X;
then G = {} by A10,XBOOLE_1:28;
hence contradiction by A8;
end;
hence contradiction by A1,TOPS_3:def 2;
end;
theorem Th43:
for X being discrete non empty TopSpace, A being Subset of X
holds A is maximal_discrete iff A is non proper
proof
let X be discrete non empty TopSpace, A be Subset of X;
hereby
X is SubSpace of X by TSEP_1:2;
then reconsider C = the carrier of X as Subset of X by TSEP_1:1;
assume
A1: A is maximal_discrete;
C is discrete by Th21;
then A = C by A1;
hence A is non proper;
end;
thus thesis by Th21,XBOOLE_0:def 10;
end;
theorem Th44:
for X being anti-discrete non empty TopSpace, A being non empty
Subset of X holds A is maximal_discrete iff A is trivial
proof
let X be anti-discrete non empty TopSpace, A be non empty Subset of X;
thus A is maximal_discrete implies A is trivial by Th38;
hereby
A1: now
let D be Subset of X;
assume
A2: D is discrete;
assume
A3: A c= D;
then reconsider E = D as non empty Subset of X;
E is trivial by A2,Th38;
hence A = D by A3,Th1;
end;
assume A is trivial;
then A is discrete by Th38;
hence A is maximal_discrete by A1;
end;
end;
definition
let Y be non empty TopStruct;
let IT be SubSpace of Y;
attr IT is maximal_discrete means
for A being Subset of Y st A = the carrier of IT holds A is maximal_discrete;
end;
theorem Th45:
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;
coherence
proof
let Y0 be non empty SubSpace of Y;
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
assume Y0 is maximal_discrete;
then A is maximal_discrete;
then A is discrete;
hence thesis by Th20;
end;
cluster non discrete -> non maximal_discrete for non empty SubSpace of Y;
coherence;
end;
theorem
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
proof
let X0 be non empty SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
hereby
assume X0 is maximal_discrete;
then
A1: A is maximal_discrete;
then A is discrete;
hence X0 is discrete by Th20;
thus for Y0 being discrete non empty SubSpace of X st X0 is SubSpace of Y0
holds the TopStruct of X0 = the TopStruct of Y0
proof
let Y0 be discrete non empty SubSpace of X;
reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1;
assume X0 is SubSpace of Y0;
then
A2: A c= D by TSEP_1:4;
D is discrete by Th20;
then A = D by A1,A2;
hence thesis by TSEP_1:5;
end;
end;
hereby
assume X0 is discrete;
then
A3: A is discrete by Th20;
assume
A4: for Y0 being discrete non empty SubSpace of X st X0 is SubSpace
of Y0 holds the TopStruct of X0 = the TopStruct of Y0;
now
let D be Subset of X;
assume
A5: D is discrete;
assume
A6: A c= D;
then D <> {};
then consider Y0 being discrete strict non empty SubSpace of X such that
A7: D = the carrier of Y0 by A5,Th28;
X0 is SubSpace of Y0 by A6,A7,TSEP_1:4;
hence A = D by A4,A7;
end;
then A is maximal_discrete by A3;
hence X0 is maximal_discrete;
end;
end;
theorem Th47:
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
proof
let A0 be non empty Subset of X;
assume
A1: A0 is maximal_discrete;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0;
thus thesis by A1,A2;
end;
registration
let X be discrete non empty TopSpace;
cluster maximal_discrete -> non proper for SubSpace of X;
coherence
proof
let Y0 be SubSpace of X;
reconsider A = the carrier of Y0 as Subset of X by Lm1;
assume Y0 is maximal_discrete;
then
A1: A is maximal_discrete;
A = the carrier of Y0 & A is non proper by A1,Th43;
hence thesis;
end;
cluster proper -> non maximal_discrete for SubSpace of X;
coherence;
cluster non proper -> maximal_discrete for SubSpace of X;
coherence
by Th43;
cluster non maximal_discrete -> proper for SubSpace of X;
coherence;
end;
registration
let X be anti-discrete non empty TopSpace;
cluster maximal_discrete -> trivial for non empty SubSpace of X;
coherence;
cluster non trivial -> non maximal_discrete for non empty SubSpace of X;
coherence;
cluster trivial -> maximal_discrete for non empty SubSpace of X;
coherence
by Th44;
cluster non maximal_discrete -> non trivial for non empty SubSpace of X;
coherence;
end;
begin
:: 4. Maximal Discrete Subspaces of Almost Discrete Spaces.
scheme
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
A1: for S being Subset of X() st S in F() ex x being Point of X() st P[S ,x]
proof
defpred X[object,object] means $2 in the carrier of X() & P[$1,$2];
A2: for S being object st S in F()
ex x being object st x in the carrier of X() & X[S,x]
proof
let S be object;
assume
A3: S in F();
then reconsider Q = S as Subset of X();
consider x being Point of X() such that
A4: P[Q,x] by A1,A3;
take x;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = F() and
A6: rng f c= the carrier of X() and
A7: for S being object st S in F() holds X[S,f.S] from FUNCT_1:sch 6(A2);
reconsider f as Function of F(),the carrier of X() by A5,A6,FUNCT_2:def 1
,RELSET_1:4;
take f;
thus thesis by A7;
end;
reserve X for almost_discrete non empty TopSpace;
theorem Th48:
for A being Subset of X holds Cl A = union {Cl {a} where a is
Point of X : a in A}
proof
let A be Subset of X;
set F = {Cl {a} where a is Point of X : a in A};
now
let C be object;
assume C in F;
then ex a being Point of X st C = Cl {a} & a in A;
hence C in bool the carrier of X;
end;
then reconsider F as Subset-Family of X by TARSKI:def 3;
reconsider F as Subset-Family of X;
now
let x be object;
assume
A1: x in A;
then reconsider a = x as Point of X;
Cl {a} in F by A1;
then
A2: Cl {a} c= union F by ZFMISC_1:74;
A3: {a} c= Cl {a} by PRE_TOPC:18;
a in {a} by TARSKI:def 1;
then a in Cl {a} by A3;
hence x in union F by A2;
end;
then
A4: A c= union F by TARSKI:def 3;
now
let C be set;
assume C in F;
then consider a being Point of X such that
A5: C = Cl {a} and
A6: a in A;
{a} c= A by A6,ZFMISC_1:31;
hence C c= Cl A by A5,PRE_TOPC:19;
end;
then
A7: union F c= Cl A by ZFMISC_1:76;
now
let G be Subset of X;
assume G in F;
then ex a being Point of X st G = Cl {a} & a in A;
hence G is open by TDLAT_3:22;
end;
then F is open by TOPS_2:def 1;
then union F is open by TOPS_2:19;
then union F is closed by TDLAT_3:21;
then Cl A c= union F by A4,TOPS_1:5;
hence thesis by A7;
end;
theorem Th49:
for a, b being Point of X holds a in Cl {b} implies Cl {a} = Cl {b}
proof
let a, b be Point of X;
assume a in Cl {b};
then
A1: {a} c= Cl {b} by ZFMISC_1:31;
b in Cl {a}
proof
assume not b in Cl {a};
then
A2: {b} misses Cl {a} by ZFMISC_1:50;
Cl {a} is open by TDLAT_3:22;
then Cl {b} misses Cl {a} by A2,TSEP_1:36;
then Cl {b} /\ Cl {a} = {};
then Cl {a} = {} by A1,TOPS_1:5,XBOOLE_1:28;
hence contradiction by PRE_TOPC:18,XBOOLE_1:3;
end;
then {b} c= Cl {a} by ZFMISC_1:31;
then
A3: Cl {b} c= Cl {a} by TOPS_1:5;
Cl {a} c= Cl {b} by A1,TOPS_1:5;
hence thesis by A3;
end;
theorem Th50:
for a, b being Point of X holds Cl {a} misses Cl {b} or Cl {a} = Cl {b}
proof
let a, b be Point of X;
assume Cl {a} /\ Cl {b} <> {};
then consider x being object such that
A1: x in Cl {a} /\ Cl {b} by XBOOLE_0:def 1;
reconsider x as Point of X by A1;
x in Cl {a} by A1,XBOOLE_0:def 4;
then
A2: Cl {x} = Cl {a} by Th49;
x in Cl {b} by A1,XBOOLE_0:def 4;
hence thesis by A2,Th49;
end;
theorem Th51:
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
proof
let A be Subset of X;
assume
A1: for x being Point of X st x in A ex F being Subset of X st F is
closed & A /\ F = {x};
now
let x be Point of X;
assume
A2: x in A;
now
consider F being Subset of X such that
A3: F is closed and
A4: A /\ F = {x} by A1,A2;
take F;
thus F is open by A3,TDLAT_3:22;
thus A /\ F = {x} by A4;
end;
hence ex G being Subset of X st G is open & A /\ G = {x};
end;
hence thesis by Th31;
end;
theorem Th52:
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
proof
let A be Subset of X;
assume
A1: for x being Point of X st x in A holds A /\ Cl {x} = {x};
now
let x be Point of X;
assume
A2: x in A;
now
take F = Cl {x};
thus F is closed;
thus A /\ F = {x} by A1,A2;
end;
hence ex F being Subset of X st F is closed & A /\ F = {x};
end;
hence thesis by Th51;
end;
theorem
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}
proof
let A be Subset of X;
thus A is discrete implies for a, b being Point of X st a in A & b in A
holds a <> b implies Cl {a} misses Cl {b}
proof
assume
A1: A is discrete;
let a, b be Point of X;
assume that
A2: a in A and
A3: b in A;
A4: A /\ Cl {b} = {b} by A1,A3,Th36;
assume
A5: a <> b;
assume Cl {a} /\ Cl {b} <> {};
then
A6: Cl {a} meets Cl {b};
A /\ Cl {a} = {a} by A1,A2,Th36;
then {a} = {b} by A4,A6,Th50;
hence contradiction by A5,ZFMISC_1:3;
end;
assume
A7: for a, b being Point of X st a in A & b in A holds a <> b implies
Cl {a} misses Cl {b};
now
let x be Point of X;
assume
A8: x in A;
assume
A9: A /\ Cl {x} <> {x};
A10: {x} c= Cl {x} by PRE_TOPC:18;
{x} c= A by A8,ZFMISC_1:31;
then (A /\ Cl {x}) \ {x} <> {} by A10,A9,Lm3,XBOOLE_1:19;
then consider y being object such that
A11: y in (A /\ Cl {x}) \ {x} by XBOOLE_0:def 1;
reconsider y as Point of X by A11;
not y in {x} by A11,XBOOLE_0:def 5;
then
A12: y <> x by TARSKI:def 1;
A13: y in A /\ Cl {x} by A11,XBOOLE_0:def 5;
then y in A by XBOOLE_0:def 4;
then Cl {y} misses Cl {x} by A7,A8,A12;
then
A14: Cl {y} /\ Cl {x} = {};
y in Cl {x} by A13,XBOOLE_0:def 4;
then Cl {y} = Cl {x} by Th49;
hence contradiction by A14,PRE_TOPC:18,XBOOLE_1:3;
end;
hence thesis by Th52;
end;
theorem Th54:
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}
proof
let A be Subset of X;
thus A is discrete implies 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}
proof
assume
A1: A is discrete;
let x be Point of X;
A2: Cl A = union {Cl {a} where a is Point of X : a in A} by Th48;
assume x in Cl A;
then consider C being set such that
A3: x in C and
A4: C in {Cl {a} where a is Point of X : a in A} by A2,TARSKI:def 4;
consider a being Point of X such that
A5: C = Cl {a} and
A6: a in A by A4;
now
take a;
thus a in A by A6;
Cl {x} = Cl {a} by A3,A5,Th49;
hence A /\ Cl {x} = {a} by A1,A6,Th36;
end;
hence thesis;
end;
assume
A7: 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};
for x being Point of X st x in A holds A /\ Cl {x} = {x}
proof
let x be Point of X;
assume
A8: x in A;
A c= Cl A by PRE_TOPC:18;
then
A9: ex a being Point of X st a in A & A /\ Cl {x} = {a} by A7,A8;
A10: {x} c= Cl {x} by PRE_TOPC:18;
{x} c= A by A8,ZFMISC_1:31;
hence thesis by A9,A10,XBOOLE_1:19,ZFMISC_1:18;
end;
hence thesis by Th52;
end;
theorem
for A being Subset of X st A is open or A is closed holds A is
maximal_discrete implies A is not proper
proof
let A be Subset of X;
assume
A1: A is open or A is closed;
then A is closed by TDLAT_3:21;
then
A2: A = Cl A by PRE_TOPC:22;
assume
A3: A is maximal_discrete;
A is open by A1,TDLAT_3:22;
then A is dense by A3,Th41;
then A = the carrier of X by A2,TOPS_3:def 2;
hence thesis;
end;
theorem Th56:
for A being Subset of X holds A is maximal_discrete implies A is dense
proof
let A be Subset of X;
assume
A1: A is maximal_discrete;
then
A2: A is discrete;
assume A is not dense;
then Cl A <> the carrier of X by TOPS_3:def 2;
then (the carrier of X) \ Cl A <> {} by Lm3;
then consider a being object such that
A3: a in (the carrier of X) \ Cl A by XBOOLE_0:def 1;
reconsider a as Point of X by A3;
set B = A \/ {a};
A4: A c= B by XBOOLE_1:7;
A5: now
let x be Point of X;
assume x in B;
then
A6: x in A or x in {a} by XBOOLE_0:def 3;
now
per cases by A6,TARSKI:def 1;
suppose
A7: x in A;
then consider G being Subset of X such that
A8: G is open and
A9: A /\ G = {x} by A2,Th26;
now
take E = Cl A /\ G;
A10: B /\ E = (A /\ E) \/ ({a} /\ E) by XBOOLE_1:23;
Cl A is open by TDLAT_3:22;
hence E is open by A8;
A11: {x} c= E by A9,PRE_TOPC:18,XBOOLE_1:26;
E c= Cl A by XBOOLE_1:17;
then not a in E by A3,XBOOLE_0:def 5;
then {a} misses E by ZFMISC_1:50;
then
A12: {a} /\ E = {};
{x} c= B by A4,A7,ZFMISC_1:31;
then
A13: {x} c= B /\ E by A11,XBOOLE_1:19;
A /\ E c= A /\ G by XBOOLE_1:17,26;
hence B /\ E = {x} by A9,A13,A12,A10;
end;
hence ex E being Subset of X st E is open & B /\ E = {x};
end;
suppose
A14: x = a;
now
take G = [#]X \ Cl A;
A15: B /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
A16: G = (Cl A)`;
hence G is open;
A c= Cl A by PRE_TOPC:18;
then A misses G by A16,SUBSET_1:24;
then
A17: A /\ G = {};
{a} c= G by A3,ZFMISC_1:31;
hence B /\ G = {x} by A14,A17,A15,XBOOLE_1:28;
end;
hence ex G being Subset of X st G is open & B /\ G = {x};
end;
end;
hence ex G being Subset of X st G is open & B /\ G = {x};
end;
A c= Cl A by PRE_TOPC:18;
then
A18: not a in A by A3,XBOOLE_0:def 5;
ex D being Subset of X st D is discrete & A c= D & A <> D
proof
take B;
thus B is discrete by A5,Th31;
thus A c= B by XBOOLE_1:7;
A <> B by A18,ZFMISC_1:31,XBOOLE_1:7;
hence thesis;
end;
hence contradiction by A1;
end;
theorem Th57:
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
proof
let A be Subset of X;
assume A is maximal_discrete;
then A is dense by Th56;
then Cl A = the carrier of X by TOPS_3:def 2;
hence thesis by Th48;
end;
theorem Th58:
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}
proof
let A be Subset of X;
thus A is maximal_discrete implies for x being Point of X ex a being Point
of X st a in A & A /\ Cl {x} = {a}
proof
assume
A1: A is maximal_discrete;
let x be Point of X;
the carrier of X = union {Cl {a} where a is Point of X : a in A} by A1,Th57
;
then consider C being set such that
A2: x in C and
A3: C in {Cl {a} where a is Point of X : a in A} by TARSKI:def 4;
consider a being Point of X such that
A4: C = Cl {a} and
A5: a in A by A3;
A6: A is discrete by A1;
now
take a;
thus a in A by A5;
Cl {x} = Cl {a} by A2,A4,Th49;
hence A /\ Cl {x} = {a} by A6,A5,Th36;
end;
hence thesis;
end;
assume
A7: for x being Point of X ex a being Point of X st a in A & A /\ Cl {x
} = {a};
A8: for D being Subset of X st D is discrete & A c= D holds A = D
proof
let D be Subset of X;
assume
A9: D is discrete;
assume
A10: A c= D;
now
let x be object;
assume
A11: x in D;
then reconsider y = x as Point of X;
A12: ex a being Point of X st a in A & A /\ Cl {y} = {a} by A7;
D /\ Cl {y} = {y} by A9,A11,Th36;
hence x in A by A10,A12,XBOOLE_1:26,ZFMISC_1:18;
end;
then D c= A by TARSKI:def 3;
hence thesis by A10;
end;
for x being Point of X st x in A holds A /\ Cl {x} = {x}
proof
let x be Point of X;
A13: {x} c= Cl {x} by PRE_TOPC:18;
assume x in A;
then
A14: {x} c= A by ZFMISC_1:31;
ex a being Point of X st a in A & A /\ Cl {x} = {a} by A7;
hence thesis by A14,A13,XBOOLE_1:19,ZFMISC_1:18;
end;
then A is discrete by Th52;
hence A is maximal_discrete by A8;
end;
theorem Th59:
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
proof
let A be Subset of X;
set D = [#]X \ Cl A;
set F = {Cl {d} where d is Point of X : d in D};
now
let C be object;
assume C in F;
then ex a being Point of X st C = Cl {a} & a in D;
hence C in bool the carrier of X;
end;
then reconsider F as Subset-Family of X by TARSKI:def 3;
assume
A1: A is discrete;
defpred X[set,set] means $2 in D & $2 in $1;
A2: D = (Cl A)`;
then D is closed by TDLAT_3:21;
then
A3: D = Cl D by PRE_TOPC:22;
A c= Cl A by PRE_TOPC:18;
then A misses D by A2,SUBSET_1:24;
then
A4: A /\ D = {};
reconsider F as Subset-Family of X;
A5: for S being Subset of X st S in F ex x being Point of X st X[S,x]
proof
let S be Subset of X;
assume S in F;
then consider d being Point of X such that
A6: S = Cl {d} and
A7: d in D;
take d;
{d} c= Cl {d} by PRE_TOPC:18;
hence thesis by A6,A7,ZFMISC_1:31;
end;
consider f being Function of F,the carrier of X such that
A8: for S being Subset of X st S in F holds X[S,f.S] from ExChoiceFCol(
A5);
set M = A \/ (f.: F);
now
let x be object;
assume x in f.: F;
then ex S being object st S in F & S in F & x = f.S by FUNCT_2:64;
hence x in D by A8;
end;
then
A9: f.: F c= D by TARSKI:def 3;
D misses Cl A by A2,SUBSET_1:24;
then
A10: Cl A misses (f.: F) by A9,XBOOLE_1:63;
thus ex M being Subset of X st A c= M & M is maximal_discrete
proof
take M;
thus
A11: A c= M by XBOOLE_1:7;
for x being Point of X ex a being Point of X st a in M & M /\ Cl {x} = {a}
proof
let x be Point of X;
A12: [#]X = Cl A \/ D by XBOOLE_1:45;
now
per cases by A12,XBOOLE_0:def 3;
suppose
A13: x in Cl A;
now
consider a being Point of X such that
A14: a in A and
A15: A /\ Cl {x} = {a} by A1,A13,Th54;
take a;
thus a in M by A11,A14;
{x} c= Cl A by A13,ZFMISC_1:31;
then (f.: F) misses Cl {x} by A10,TOPS_1:5,XBOOLE_1:63;
then (f.: F) /\ Cl {x} = {};
then M /\ Cl {x} = (A /\ Cl {x}) \/ {} by XBOOLE_1:23;
hence M /\ Cl {x} = {a} by A15;
end;
hence thesis;
end;
suppose
A16: x in D;
then
A17: Cl {x} in F;
now
reconsider a = f.(Cl {x}) as Point of X by A17,FUNCT_2:5;
take a;
A18: f.: F c= M by XBOOLE_1:7;
now
let y be object;
assume
A19: y in M /\ Cl {x};
then reconsider z = y as Point of X;
A20: z in Cl {x} by A19,XBOOLE_0:def 4;
A21: z in M by A19,XBOOLE_0:def 4;
{x} c= D by A16,ZFMISC_1:31;
then Cl {x} c= D by A3,PRE_TOPC:19;
then not z in A by A4,A20,XBOOLE_0:def 4;
then z in f.: F by A21,XBOOLE_0:def 3;
then consider C being object such that
A22: C in F and
C in F and
A23: z = f.C by FUNCT_2:64;
reconsider C as Subset of X by A22;
consider w being Point of X such that
A24: C = Cl {w} and
w in D by A22;
Cl {z} = Cl {x} by A20,Th49;
then f.(Cl {w}) = a by A8,A22,A23,A24,Th49;
hence y in {a} by A23,A24,TARSKI:def 1;
end;
then
A25: M /\ Cl {x} c= {a} by TARSKI:def 3;
A26: a in f.: F by A17,FUNCT_2:35;
hence a in M by A18;
a in Cl {x} by A8,A17;
then
A27: {a} c= Cl {x} by ZFMISC_1:31;
{a} c= M by A18,A26,ZFMISC_1:31;
then {a} c= M /\ Cl {x} by A27,XBOOLE_1:19;
hence M /\ Cl {x} = {a} by A25;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence M is maximal_discrete by Th58;
end;
end;
theorem Th60:
ex M being Subset of X st M is maximal_discrete
proof
set A = {}X;
A is discrete by Th29;
then consider M being Subset of X such that
A c= M and
A1: M is maximal_discrete by Th59;
take M;
thus thesis by A1;
end;
theorem Th61:
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
proof
let Y0 be discrete non empty SubSpace of X;
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
A is discrete by Th20;
then consider M being Subset of X such that
A1: A c= M and
A2: M is maximal_discrete by Th59;
M is non empty by A2,Th40;
then consider X0 being strict non empty SubSpace of X such that
A3: X0 is maximal_discrete and
A4: M = the carrier of X0 by A2,Th47;
take X0;
thus thesis by A1,A3,A4,TSEP_1:4;
end;
registration
let X be almost_discrete non discrete non empty TopSpace;
cluster maximal_discrete -> proper for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is maximal_discrete;
then A is maximal_discrete;
then A is discrete;
then
A1: X0 is discrete by Th20;
X0 is proper
proof
assume X0 is non proper;
then A is not proper;
then
A2: A = the carrier of X;
X is SubSpace of X by TSEP_1:2;
then the TopStruct of X0 = the TopStruct of X by A2,TSEP_1:5;
hence contradiction by A1,Th12;
end;
hence thesis;
end;
cluster non proper -> non maximal_discrete for non empty SubSpace of X;
coherence;
end;
registration
let X be almost_discrete non anti-discrete non empty TopSpace;
cluster maximal_discrete -> non trivial for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
reconsider A = the carrier of X0 as non empty Subset of X by Lm1;
assume X0 is maximal_discrete;
then A is maximal_discrete;
then A is dense by Th56;
then
A1: Cl A = the carrier of X by TOPS_3:def 2;
assume X0 is trivial;
then consider s being Element of X0 such that
A2: the carrier of X0 = {s} by SUBSET_1:46;
s in A;
then reconsider a = s as Point of X;
A = {a} by A2;
then for C being Subset of X, x being Point of X st C = {x} holds Cl C =
the carrier of X by A1,Th49;
hence contradiction by TDLAT_3:20;
end;
cluster trivial -> non maximal_discrete for non empty SubSpace of X;
coherence;
end;
registration
let X be almost_discrete non empty TopSpace;
cluster maximal_discrete strict non empty non empty for SubSpace of X;
existence
proof
consider M being Subset of X such that
A1: M is maximal_discrete by Th60;
M is non empty by A1,Th40;
then consider X0 being strict non empty SubSpace of X such that
A2: X0 is maximal_discrete and
M = the carrier of X0 by A1,Th47;
take X0;
thus thesis by A2;
end;
end;
begin
:: 5. Continuous Mappings and Almost Discrete Spaces.
reserve X,Y for non empty TopSpace;
theorem Th62:
for X being discrete TopSpace, Y being TopSpace, f being
Function of X,Y holds f is continuous
by TDLAT_3:16;
theorem
(for Y being non empty TopSpace, f being Function of X,Y holds f is
continuous) implies X is discrete
proof
set Y = 1TopSp(the carrier of X);
reconsider f = id the carrier of X as Function of X,Y;
assume for Y being non empty TopSpace, f being Function of X,Y holds f is
continuous;
then
A1: f is continuous;
for A being Subset of X holds A is closed
proof
let A be Subset of X;
reconsider B = A as Subset of Y;
A2: f"B = A by FUNCT_2:94;
B is closed by TDLAT_3:16;
hence thesis by A1,A2;
end;
hence thesis by TDLAT_3:16;
end;
theorem
for Y being anti-discrete non empty TopSpace, f being Function of X,Y
holds f is continuous
proof
let Y be anti-discrete non empty TopSpace, f be Function of X,Y;
now
let B be Subset of Y;
assume
A1: B is closed;
now
per cases by A1,TDLAT_3:19;
suppose
B = {};
then f" B = {}X;
hence f" B is closed;
end;
suppose
B = the carrier of Y;
then B = [#]Y;
then f" B = [#]X by TOPS_2:41;
hence f" B is closed;
end;
end;
hence f" B is closed;
end;
hence thesis;
end;
theorem
(for X being non empty TopSpace, f being Function of X,Y holds f is
continuous ) implies Y is anti-discrete
proof
set X = ADTS(the carrier of Y);
A1: X = TopStruct(#the carrier of Y, cobool the carrier of Y#) by TEX_1:def 3;
then reconsider f = id (the carrier of Y) as Function of X,Y;
assume for X being non empty TopSpace, f being Function of X,Y holds f is
continuous;
then
A2: f is continuous;
for A being Subset of Y st A is closed holds A = {} or A = the carrier of Y
proof
let A be Subset of Y;
reconsider B = A as Subset of X by A1;
A3: f"A = B by FUNCT_2:94;
assume A is closed;
then B is closed by A2,A3;
hence thesis by A1,TDLAT_3:19;
end;
hence thesis by TDLAT_3:19;
end;
reserve X for discrete non empty TopSpace,
X0 for non empty SubSpace of X;
theorem Th66:
ex r being continuous Function of X,X0 st r is being_a_retraction
proof
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
defpred X[set,set] means $1 in A implies $2 = $1;
A1: for x being Point of X ex a being Point of X0 st X[x,a];
consider r being Function of X,X0 such that
A2: for x being Point of X holds X[x,r.x] from FUNCT_2:sch 3(A1);
reconsider r as continuous Function of X,X0 by Th62;
take r;
thus thesis by A2,BORSUK_1:def 16;
end;
theorem
X0 is_a_retract_of X
proof
ex r being continuous Function of X,X0 st r is being_a_retraction by Th66;
hence thesis by BORSUK_1:def 17;
end;
reserve X for almost_discrete non empty TopSpace,
X0 for maximal_discrete non empty SubSpace of X;
theorem Th68:
ex r being continuous Function of X,X0 st r is being_a_retraction
proof
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
defpred X[Point of X,Point of X0] means A /\ Cl {$1} = {$2};
A1: A is maximal_discrete by Th45;
then
A2: A is discrete;
A3: for x being Point of X ex a being Point of X0 st X[x,a]
proof
let x be Point of X;
consider a being Point of X such that
A4: a in A and
A5: A /\ Cl {x} = {a} by A1,Th58;
reconsider a as Point of X0 by A4;
take a;
thus thesis by A5;
end;
consider r being Function of X,X0 such that
A6: for x being Point of X holds X[x,r.x] from FUNCT_2:sch 3(A3);
for F being Subset of X0 holds F is closed implies r" F is closed
proof
let F be Subset of X0;
assume F is closed;
F c= A;
then reconsider E = F as Subset of X by XBOOLE_1:1;
set R = {Cl {a} where a is Point of X : a in E};
now
let x be object;
assume
A7: x in r" F;
then reconsider b = x as Point of X;
A8: r.b in F by A7,FUNCT_2:38;
E c= the carrier of X;
then reconsider a = r.b as Point of X by A8;
Cl {a} in R by A8;
then
A9: Cl {a} c= union R by ZFMISC_1:74;
A /\ Cl {b} = {a} by A6;
then a in A /\ Cl {b} by ZFMISC_1:31;
then a in Cl {b} by XBOOLE_0:def 4;
then
A10: Cl {a} = Cl {b} by Th49;
A11: {b} c= Cl {b} by PRE_TOPC:18;
b in {b} by TARSKI:def 1;
then b in Cl {a} by A10,A11;
hence x in union R by A9;
end;
then
A12: r" F c= union R by TARSKI:def 3;
now
let C be set;
assume C in R;
then consider a being Point of X such that
A13: C = Cl {a} and
A14: a in E;
now
let x be object;
assume
A15: x in C;
then reconsider b = x as Point of X by A13;
A16: A /\ Cl {b} = {r.b} by A6;
A17: A /\ Cl {a} = {a} by A2,A14,Th36;
Cl {a} = Cl {b} by A13,A15,Th49;
then a = r.x by A17,A16,ZFMISC_1:3;
hence x in r" F by A13,A14,A15,FUNCT_2:38;
end;
hence C c= r" F by TARSKI:def 3;
end;
then
A18: union R c= r" F by ZFMISC_1:76;
Cl E = union R by Th48;
hence thesis by A18,A12,XBOOLE_0:def 10;
end;
then reconsider r as continuous Function of X,X0 by PRE_TOPC:def 6;
take r;
for x being Point of X st x in the carrier of X0 holds r.x = x
proof
let x be Point of X;
assume x in the carrier of X0;
then
A19: A /\ Cl {x} = {x} by A2,Th36;
A /\ Cl {x} = {r.x} by A6;
hence thesis by A19,ZFMISC_1:3;
end;
hence thesis by BORSUK_1:def 16;
end;
theorem
X0 is_a_retract_of X
proof
ex r being continuous Function of X,X0 st r is being_a_retraction by Th68;
hence thesis by BORSUK_1:def 17;
end;
Lm4: 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 Cl {b} c= r"
{a}
proof
let r be continuous Function of X,X0;
assume
A1: r is being_a_retraction;
let a be Point of X0, b be Point of X;
assume a = b;
then
A2: r.b = a by A1,BORSUK_1:def 16;
a in {a} by TARSKI:def 1;
then b in r" {a} by A2,FUNCT_2:38;
then
A3: {b} c= r" {a} by ZFMISC_1:31;
{a} is closed by TDLAT_3:16;
then r" {a} is closed by PRE_TOPC:def 6;
hence thesis by A3,TOPS_1:5;
end;
theorem Th70:
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
proof
let r be continuous Function of X,X0;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is maximal_discrete by Th45;
assume
A2: r is being_a_retraction;
A3: for a being Point of X holds A /\ Cl {a} = {r.a}
proof
let a be Point of X;
A4: {a} c= Cl {a} by PRE_TOPC:18;
consider c being Point of X such that
A5: c in A and
A6: A /\ Cl {a} = {c} by A1,Th58;
reconsider b = c as Point of X0 by A5;
{c} c= Cl {a} by A6,XBOOLE_1:17;
then
A7: c in Cl {a} by ZFMISC_1:31;
Cl {c} c= r" {b} by A2,Lm4;
then Cl {a} c= r" {b} by A7,Th49;
then {a} c= r" {b} by A4,XBOOLE_1:1;
then a in r" {b} by ZFMISC_1:31;
then r.a in {b} by FUNCT_2:38;
hence thesis by A6,TARSKI:def 1;
end;
let F be Subset of X0, E be Subset of X;
set R = {Cl {a} where a is Point of X : a in E};
assume
A8: F = E;
now
let x be object;
assume
A9: x in r" F;
then reconsider b = x as Point of X;
A10: r.b in F by A9,FUNCT_2:38;
then reconsider a = r.b as Point of X by A8;
Cl {a} in R by A8,A10;
then
A11: Cl {a} c= union R by ZFMISC_1:74;
A12: {b} c= Cl {b} by PRE_TOPC:18;
A /\ Cl {b} = {a} by A3;
then a in A /\ Cl {b} by ZFMISC_1:31;
then a in Cl {b} by XBOOLE_0:def 4;
then
A13: Cl {a} = Cl {b} by Th49;
b in {b} by TARSKI:def 1;
then b in Cl {a} by A13,A12;
hence x in union R by A11;
end;
then
A14: r" F c= union R by TARSKI:def 3;
A15: A is discrete by A1;
now
let C be set;
assume C in R;
then consider a being Point of X such that
A16: C = Cl {a} and
A17: a in E;
now
let x be object;
assume
A18: x in C;
then reconsider b = x as Point of X by A16;
A19: A /\ Cl {b} = {r.b} by A3;
A20: A /\ Cl {a} = {a} by A8,A15,A17,Th36;
Cl {a} = Cl {b} by A16,A18,Th49;
then a = r.x by A20,A19,ZFMISC_1:3;
hence x in r" F by A8,A16,A17,A18,FUNCT_2:38;
end;
hence C c= r" F by TARSKI:def 3;
end;
then
A21: union R c= r" F by ZFMISC_1:76;
Cl E = union R by Th48;
hence thesis by A21,A14;
end;
theorem
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} by Th70;
reserve X0 for discrete non empty SubSpace of X;
theorem Th72:
ex r being continuous Function of X,X0 st r is being_a_retraction
proof
consider Z0 being strict non empty SubSpace of X such that
A1: X0 is SubSpace of Z0 and
A2: Z0 is maximal_discrete by Th61;
reconsider Z0 as maximal_discrete strict non empty SubSpace of X by A2;
reconsider Z1 = Z0 as non empty TopSpace;
reconsider Z1 as discrete non empty TopSpace;
reconsider X1 = X0 as non empty SubSpace of Z1 by A1;
consider g being continuous Function of Z1,X1 such that
A3: g is being_a_retraction by Th66;
reconsider g as continuous Function of Z0,X0;
consider h being continuous Function of X,Z0 such that
A4: h is being_a_retraction by Th68;
reconsider r = g * h as continuous Function of X,X0;
take r;
for x being Point of X st x in the carrier of X0 holds r.x = x
proof
let x be Point of X;
assume
A5: x in the carrier of X0;
the carrier of X1 c= the carrier of Z1 by BORSUK_1:1;
then reconsider y = x as Point of Z1 by A5;
g.y = y by A3,A5,BORSUK_1:def 16;
then g.(h.x) = x by A4,BORSUK_1:def 16;
hence thesis by FUNCT_2:15;
end;
hence thesis by BORSUK_1:def 16;
end;
theorem
X0 is_a_retract_of X
proof
ex r being continuous Function of X,X0 st r is being_a_retraction by Th72;
hence thesis by BORSUK_1:def 17;
end;