:: Maximal Anti-Discrete Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994-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, 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;
definitions TARSKI, XBOOLE_0, STRUCT_0;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, SUBSET_1;
theorems TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, TOPS_2,
PCOMPS_1, TSEP_1, TDLAT_3, TEX_2, XBOOLE_0, XBOOLE_1;
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;
coherence by PCOMPS_1:2;
end;
registration
let X be TopSpace, A be empty Subset of X;
cluster Cl A -> empty;
coherence by PRE_TOPC:22;
end;
registration
let X be non empty TopSpace, A be non proper Subset of X;
cluster Cl A -> non proper;
coherence
proof
A = [#]X by SUBSET_1:def 6;
hence thesis by TOPS_1:2;
end;
end;
registration
let X be non trivial TopSpace, A be non trivial Subset of X;
cluster Cl A -> non trivial;
coherence
proof
A c= Cl A by PRE_TOPC:18;
hence thesis;
end;
end;
reserve X for non empty TopSpace;
theorem Th1:
for A being Subset of X holds
Cl A = meet {F where F is Subset of X: F is closed & A c= F}
proof
let A be Subset of X;
set G = {F where F is Subset of X : F is closed & A c= F};
A1: G c= bool the carrier of X
proof
let C be object;
assume C in G;
then ex P being Subset of X st C = P & P is closed & A c= P;
hence thesis;
end;
[#]X in G;
then reconsider G as non empty Subset-Family of X by A1;
now
let P be set;
assume P in G;
then ex F being Subset of X st F = P & F is closed & A c= F;
hence A c= P;
end;
then
A2: A c= meet G by SETFAM_1:5;
A c= Cl A by PRE_TOPC:18;
then Cl A in G;
then
A3: meet G c= Cl A by SETFAM_1:3;
now
let S be Subset of X;
assume S in G;
then ex F being Subset of X st F = S & F is closed & A c= F;
hence S is closed;
end;
then G is closed by TOPS_2:def 2;
then Cl A c= meet G by A2,TOPS_1:5,TOPS_2:22;
hence thesis by A3;
end;
theorem Th2:
for x being Point of X holds
Cl {x} = meet {F where F is Subset of X : F is closed & x in F}
proof
let x be Point of X;
set G = {F where F is Subset of X : F is closed & x in F};
set H = {F where F is Subset of X : F is closed & {x} c= F};
now
let P be object;
assume P in G;
then consider F being Subset of X such that
A1: F = P and
A2: F is closed and
A3: x in F;
{x} c= F by A3,ZFMISC_1:31;
hence P in H by A1,A2;
end;
then
A4: G c= H;
now
let P be object;
assume P in H;
then consider F being Subset of X such that
A5: F = P and
A6: F is closed and
A7: {x} c= F;
x in F by A7,ZFMISC_1:31;
hence P in G by A5,A6;
end;
then
A8: H c= G;
Cl {x} = meet H by Th1;
hence thesis by A4,A8,XBOOLE_0:def 10;
end;
registration
let X be non empty TopSpace, A be non proper Subset of X;
cluster Int A -> non proper;
coherence
proof
A = [#]X by SUBSET_1:def 6;
hence thesis by TOPS_1:15;
end;
end;
registration
let X be non empty TopSpace, A be proper Subset of X;
cluster Int A -> proper;
coherence
proof
now
assume Int A is non proper;
then
A1: Int A = [#]X;
Int A c= A by TOPS_1:16;
hence contradiction by A1,XBOOLE_0:def 10;
end;
hence thesis;
end;
end;
registration
let X be non empty TopSpace, A be empty Subset of X;
cluster Int A -> empty;
coherence;
end;
theorem
for A being Subset of X holds
Int A = union {G where G is Subset of X : G is open & G c= A}
proof
let A be Subset of X;
set F = {G where G is Subset of X : G is open & G c= A};
A1: F c= bool the carrier of X
proof
let C be object;
assume C in F;
then ex P being Subset of X st C = P & P is open & P c= A;
hence thesis;
end;
{} c= A;
then {}X in F;
then reconsider F as non empty Subset-Family of X by A1;
now
let P be set;
assume P in F;
then ex G being Subset of X st G = P & G is open & G c= A;
hence P c= A;
end;
then
A2: union F c= A by ZFMISC_1:76;
Int A c= A by TOPS_1:16;
then Int A in F;
then
A3: Int A c= union F by ZFMISC_1:74;
now
let S be Subset of X;
assume S in F;
then ex G being Subset of X st G = S & G is open & G c= A;
hence S is open;
end;
then F is open by TOPS_2:def 1;
then union F c= Int A by A2,TOPS_1:24,TOPS_2:19;
hence thesis by A3;
end;
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
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 :: redefines anti-discrete (TEX_4, definition)
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;
compatibility
proof
hereby
assume
A1: A is anti-discrete;
let x be Point of Y, F be Subset of Y;
set G = [#]Y \ F;
A2: A \ F c= G by XBOOLE_1:33;
assume F is closed;
then
A3: G is open by PRE_TOPC:def 3;
assume
A4: x in F;
assume
A5: x in A;
assume not A c= F;
then A \ F <> {} by XBOOLE_1:37;
then consider a being object such that
A6: a in A \ F by XBOOLE_0:def 1;
a in A by A6,XBOOLE_0:def 5;
then A c= G by A1,A6,A2,A3;
then
A7: A misses G` by SUBSET_1:24;
A8: G` = (F`)` .= F;
A /\ F is non empty by A4,A5,XBOOLE_0:def 4;
hence contradiction by A8,A7;
end;
hereby
assume
A9: 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;
now
let x be Point of Y, G be Subset of Y;
set F = [#]Y \ G;
A10: A \ G c= F by XBOOLE_1:33;
A11: G = [#]Y \ F by PRE_TOPC:3;
assume G is open;
then
A12: F is closed by A11,PRE_TOPC:def 3;
assume
A13: x in G;
assume
A14: x in A;
assume not A c= G;
then A \ G <> {} by XBOOLE_1:37;
then consider a being object such that
A15: a in A \ G by XBOOLE_0:def 1;
A16: F = G`;
a in A by A15,XBOOLE_0:def 5;
then A c= F by A9,A15,A10,A12;
then A misses F` by SUBSET_1:24;
hence contradiction by A13,A14,A16,XBOOLE_0:3;
end;
hence A is anti-discrete;
end;
end;
end;
definition
let Y be TopStruct;
let A be Subset of Y;
redefine attr A is anti-discrete means :: redefines anti-discrete (TEX_4, definition)
for G being Subset of Y st G is open holds A misses G or A c= G;
compatibility
proof
hereby
assume
A1: A is anti-discrete;
let G be Subset of Y;
assume
A2: G is open;
assume A meets G;
then consider a being object such that
A3: a in A /\ G by XBOOLE_0:4;
reconsider a as Point of Y by A3;
A4: a in G by A3,XBOOLE_0:def 4;
a in A by A3,XBOOLE_0:def 4;
hence A c= G by A1,A2,A4;
end;
assume
A5: for G being Subset of Y st G is open holds A misses G or A c= G;
for x be Point of Y, G be Subset of Y st G is open & x in G & x in A
holds A c= G by A5,XBOOLE_0:3;
hence thesis;
end;
end;
definition
let Y be TopStruct;
let A be Subset of Y;
redefine attr A is anti-discrete means :: redefines anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, definition)
for F being Subset of Y st F is closed holds A misses F or A c= F;
compatibility
proof
hereby
assume
A1: A is anti-discrete;
let G be Subset of Y;
assume G is closed;
then [#]Y \ G is open by PRE_TOPC:def 3;
then
A2: A misses G` or A c= G` by A1;
assume A meets G;
then A c= (G`)` by A2,SUBSET_1:23;
hence A c= G;
end;
hereby
assume
A3: for G being Subset of Y st G is closed holds A misses G or A c= G;
now
let G be Subset of Y;
A4: G = [#]Y \ ([#]Y \ G) by PRE_TOPC:3;
assume G is open;
then [#]Y \ G is closed by A4,PRE_TOPC:def 3;
then
A5: A misses G` or A c= G` by A3;
assume A meets G;
then A c= G`` by A5,SUBSET_1:23;
hence A c= G;
end;
hence A is anti-discrete;
end;
end;
end;
theorem Th4:
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
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 anti-discrete;
now
let D be Subset of Y1;
reconsider E = D as Subset of Y0 by A1;
assume D is open;
then E in the topology of Y0 by A1,PRE_TOPC:def 2;
then E is open by PRE_TOPC:def 2;
hence D1 misses D or D1 c= D by A2,A3;
end;
hence thesis;
end;
reserve Y for non empty TopStruct;
theorem Th5:
for A, B being Subset of Y st B c= A holds A is anti-discrete
implies B is anti-discrete
proof
let A, B be Subset of Y;
assume
A1: B c= A;
assume
A2: A is anti-discrete;
now
let G be Subset of Y;
assume
A3: G is open;
assume B meets G;
then B /\ G <> {};
then A /\ G <> {} by A1,XBOOLE_1:3,26;
then A meets G;
then A c= G by A2,A3;
hence B c= G by A1;
end;
hence thesis;
end;
theorem Th6:
for x being Point of Y holds {x} is anti-discrete
proof
let x be Point of Y;
now
let G be Subset of Y such that
G is open;
assume {x} meets G;
then consider a being object such that
A1: a in {x} /\ G by XBOOLE_0:4;
a in {x} by A1,XBOOLE_0:def 4;
then
A2: a = x by TARSKI:def 1;
a in G by A1,XBOOLE_0:def 4;
hence {x} c= G by A2,ZFMISC_1:31;
end;
hence thesis;
end;
theorem
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
for A being Subset of Y st A in IT holds A is anti-discrete;
end;
theorem Th8:
for F being Subset-Family of Y st F is anti-discrete-set-family
holds meet F <> {} implies union F is anti-discrete
proof
let F be Subset-Family of Y;
assume
A1: F is anti-discrete-set-family;
assume
A2: meet F <> {};
for G being Subset of Y st G is open holds (union F) misses G or union F c= G
proof
let G be Subset of Y;
assume
A3: G is open;
assume union F meets G;
then consider A0 being set such that
A4: A0 in F and
A5: A0 meets G by ZFMISC_1:80;
reconsider A0 as Subset of Y by A4;
A0 is anti-discrete by A1,A4;
then
A6: A0 c= G by A3,A5;
meet F c= A0 by A4,SETFAM_1:3;
then
A7: meet F c= G by A6;
for B being set st B in F holds B c= G
proof
let B be set;
assume
A8: B in F;
then reconsider B0 = B as Subset of Y;
meet F c= B0 by A8,SETFAM_1:3;
then B0 /\ G <> {} by A2,A7,XBOOLE_1:3,19;
then
A9: B0 meets G;
B0 is anti-discrete by A1,A8;
hence thesis by A3,A9;
end;
hence thesis by ZFMISC_1:76;
end;
hence thesis;
end;
theorem
for F being Subset-Family of Y st F is anti-discrete-set-family holds
meet F is anti-discrete
proof
let F be Subset-Family of Y;
assume
A1: F is anti-discrete-set-family;
hereby
per cases;
suppose
meet F = {};
hence thesis;
end;
suppose
meet F <> {};
meet F c= union F by SETFAM_1:2;
hence thesis by A1,Th5,Th8;
end;
end;
end;
definition
let Y be TopStruct, x be Point of Y;
func MaxADSF(x) -> Subset-Family of Y equals
{A where A is Subset of Y : A
is anti-discrete & x in A};
coherence
proof
set F = {A where A is Subset of Y : A is anti-discrete & x in A};
F c= bool the carrier of Y
proof
let C be object;
assume C in F;
then ex A being Subset of Y st C = A & A is anti-discrete & x in A;
hence thesis;
end;
hence thesis;
end;
end;
registration
let Y be non empty TopStruct, x be Point of Y;
cluster MaxADSF(x) -> non empty;
coherence
proof
set F = {A where A is Subset of Y : A is anti-discrete & x in A};
A1: x in {x} by TARSKI:def 1;
{x} is anti-discrete by Th6;
then {x} in F by A1;
hence thesis;
end;
end;
reserve x for Point of Y;
theorem Th10:
MaxADSF(x) is anti-discrete-set-family
proof
now
let A be Subset of Y;
assume A in MaxADSF(x);
then ex C being Subset of Y st C = A & C is anti-discrete & x in C;
hence A is anti-discrete;
end;
hence thesis;
end;
theorem Th11:
{x} = meet MaxADSF(x)
proof
A1: x in {x} by TARSKI:def 1;
now
let A be set;
assume A in MaxADSF(x);
then ex C being Subset of Y st C = A & C is anti-discrete & x in C;
hence {x} c= A by ZFMISC_1:31;
end;
then
A2: {x} c= meet MaxADSF(x) by SETFAM_1:5;
{x} is anti-discrete by Th6;
then {x} in MaxADSF(x) by A1;
then meet MaxADSF(x) c= {x} by SETFAM_1:3;
hence thesis by A2;
end;
theorem Th12:
{x} c= union MaxADSF(x)
proof
{x} = meet MaxADSF(x) by Th11;
hence thesis by SETFAM_1:2;
end;
theorem Th13:
union MaxADSF(x) is anti-discrete
proof
{x} = meet MaxADSF(x) by Th11;
hence thesis by Th8,Th10;
end;
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
IT is anti-discrete & for D
being Subset of Y st D is anti-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_anti-discrete implies D1 is maximal_anti-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_anti-discrete;
A4: now
let D be Subset of Y1;
reconsider E = D as Subset of Y0 by A1;
assume D is anti-discrete;
then
A5: E is anti-discrete by A1,Th4;
assume D1 c= D;
hence D1 = D by A2,A3,A5;
end;
D0 is anti-discrete by A3;
then D1 is anti-discrete by A1,A2,Th4;
hence thesis by A4;
end;
reserve Y for non empty TopStruct;
theorem Th15:
for A being empty Subset of Y holds A is not maximal_anti-discrete
proof
consider a being object such that
A1: a in the carrier of Y by XBOOLE_0:def 1;
reconsider a as Point of Y by A1;
let A be empty Subset of Y;
now
take C = {a};
thus C is anti-discrete & A c= C & A <> C by Th6;
end;
hence thesis;
end;
theorem Th16:
for A being non empty Subset of Y holds A is anti-discrete & A
is open implies A is maximal_anti-discrete
proof
let A be non empty Subset of Y;
assume
A1: A is anti-discrete;
assume
A2: A is open;
for D being Subset of Y st D is anti-discrete & A c= D holds A = D
proof
let D be Subset of Y;
assume D is anti-discrete;
then D misses A or D c= A by A2;
then
A3: D /\ A = {} or D c= A;
assume A c= D;
hence thesis by A3,XBOOLE_1:28;
end;
hence thesis by A1;
end;
theorem Th17:
for A being non empty Subset of Y holds A is anti-discrete & A
is closed implies A is maximal_anti-discrete
proof
let A be non empty Subset of Y;
assume
A1: A is anti-discrete;
assume
A2: A is closed;
for D being Subset of Y st D is anti-discrete & A c= D holds A = D
proof
let D be Subset of Y;
assume D is anti-discrete;
then D misses A or D c= A by A2;
then
A3: D /\ A = {} or D c= A;
assume A c= D;
hence thesis by A3,XBOOLE_1:28;
end;
hence thesis by A1;
end;
definition
let Y be TopStruct, x be Point of Y;
func MaxADSet(x) -> Subset of Y equals
union MaxADSF(x);
coherence;
end;
registration
let Y be non empty TopStruct, x be Point of Y;
cluster MaxADSet(x) -> non empty;
coherence
proof
{x} c= union MaxADSF(x) by Th12;
hence thesis;
end;
end;
theorem
for x being Point of Y holds {x} c= MaxADSet(x) by Th12;
theorem Th19:
for D being Subset of Y, x being Point of Y st D is
anti-discrete & x in D holds D c= MaxADSet(x)
proof
let D be Subset of Y, x be Point of Y;
assume
A1: D is anti-discrete;
assume x in D;
then D in {A where A is Subset of Y : A is anti-discrete & x in A} by A1;
hence thesis by ZFMISC_1:74;
end;
theorem Th20:
for x being Point of Y holds MaxADSet(x) is maximal_anti-discrete
proof
let x be Point of Y;
A1: for D being Subset of Y st D is anti-discrete & MaxADSet(x) c= D holds
MaxADSet(x) = D
proof
let D be Subset of Y;
assume
A2: D is anti-discrete;
assume
A3: MaxADSet(x) c= D;
{x} c= MaxADSet(x) by Th12;
then {x} c= D by A3;
then x in D by ZFMISC_1:31;
then D c= MaxADSet(x) by A2,Th19;
hence thesis by A3;
end;
MaxADSet(x) is anti-discrete by Th13;
hence thesis by A1;
end;
theorem Th21:
for x, y being Point of Y holds y in MaxADSet(x) iff MaxADSet(y)
= MaxADSet(x)
proof
let x, y be Point of Y;
MaxADSet(y) is maximal_anti-discrete by Th20;
then
A1: MaxADSet(y) is anti-discrete;
A2: MaxADSet(x) is maximal_anti-discrete by Th20;
then
A3: MaxADSet(x) is anti-discrete;
thus y in MaxADSet(x) implies MaxADSet(y) = MaxADSet(x)
proof
assume y in MaxADSet(x);
then
MaxADSet(x) in {A where A is Subset of Y : A is anti-discrete & y in A
} by A3;
then MaxADSet(x) c= MaxADSet(y) by ZFMISC_1:74;
hence thesis by A2,A1;
end;
assume
A4: MaxADSet(y) = MaxADSet(x);
{y} c= MaxADSet(y) by Th12;
hence thesis by A4,ZFMISC_1:31;
end;
theorem Th22:
for x, y being Point of Y holds MaxADSet(x) misses MaxADSet(y)
or MaxADSet(x) = MaxADSet(y)
proof
let x, y be Point of Y;
assume MaxADSet(x) /\ MaxADSet(y) <> {};
then consider a being object such that
A1: a in MaxADSet(x) /\ MaxADSet(y) by XBOOLE_0:def 1;
reconsider a as Point of Y by A1;
a in MaxADSet(x) by A1,XBOOLE_0:def 4;
then
A2: MaxADSet(a) = MaxADSet(x) by Th21;
a in MaxADSet(y) by A1,XBOOLE_0:def 4;
hence thesis by A2,Th21;
end;
theorem Th23:
for F being Subset of Y, x being Point of Y st F is closed & x
in F holds MaxADSet(x) c= F
proof
let F be Subset of Y, x be Point of Y;
assume that
A1: F is closed and
A2: x in F;
{x} c= MaxADSet(x) by Th12;
then
A3: x in MaxADSet(x) by ZFMISC_1:31;
MaxADSet(x) is maximal_anti-discrete by Th20;
then MaxADSet(x) is anti-discrete;
hence thesis by A1,A2,A3;
end;
theorem Th24:
for G being Subset of Y, x being Point of Y st G is open & x in
G holds MaxADSet(x) c= G
proof
let G be Subset of Y, x be Point of Y;
assume that
A1: G is open and
A2: x in G;
{x} c= MaxADSet(x) by Th12;
then
A3: x in MaxADSet(x) by ZFMISC_1:31;
MaxADSet(x) is maximal_anti-discrete by Th20;
then MaxADSet(x) is anti-discrete;
hence thesis by A1,A2,A3;
end;
theorem
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}
proof
let Y be non empty TopSpace;
let x be Point of Y;
set G = {F where F is Subset of Y : F is closed & x in F};
[#]Y in G; then
A1: G <> {};
G c= bool the carrier of Y
proof
let C be object;
assume C in G;
then ex P being Subset of Y st C = P & P is closed & x in P;
hence thesis;
end;
then reconsider G as Subset-Family of Y;
now
let C be set;
assume C in G;
then ex F being Subset of Y st F = C & F is closed & x in F;
hence MaxADSet(x) c= C by Th23;
end;
hence thesis by SETFAM_1:5,A1;
end;
theorem
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}
proof
let Y be non empty TopSpace;
let x be Point of Y;
set F = {G where G is Subset of Y : G is open & x in G};
[#]Y in F; then
A1: F <> {};
F c= bool the carrier of Y
proof
let C be object;
assume C in F;
then ex P being Subset of Y st C = P & P is open & x in P;
hence thesis;
end;
then reconsider F as Subset-Family of Y;
now
let C be set;
assume C in F;
then ex G being Subset of Y st G = C & G is open & x in G;
hence MaxADSet(x) c= C by Th24;
end;
hence thesis by SETFAM_1:5,A1;
end;
definition
let Y be non empty TopStruct;
let A be Subset of Y;
redefine attr A is maximal_anti-discrete means :: redefines maximal_anti-discrete (TEX_4, definition)
ex x being Point of Y st x in A & A = MaxADSet(x);
compatibility
proof
thus A is maximal_anti-discrete implies ex x being Point of Y st x in A &
A = MaxADSet(x)
proof
assume
A1: A is maximal_anti-discrete;
then A <> {} by Th15;
then consider x being object such that
A2: x in A by XBOOLE_0:def 1;
reconsider x as Point of Y by A2;
take x;
thus x in A by A2;
MaxADSet(x) is maximal_anti-discrete by Th20;
then
A3: MaxADSet(x) is anti-discrete;
A is anti-discrete by A1;
then A c= MaxADSet(x) by A2,Th19;
hence thesis by A1,A3;
end;
assume ex x being Point of Y st x in A & A = MaxADSet(x);
hence thesis by Th20;
end;
end;
theorem Th27:
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) by Th21;
definition
let Y be non empty TopStruct;
let A be non empty Subset of Y;
redefine attr A is maximal_anti-discrete means :: redefines maximal_anti-discrete (TEX_4, redefinition) → maximal_anti-discrete (TEX_4, definition)
for x being Point of Y st x in A holds A = MaxADSet(x);
compatibility
proof
thus A is maximal_anti-discrete implies for x being Point of Y st x in A
holds A = MaxADSet(x) by Th27;
consider a being object such that
A1: a in A by XBOOLE_0:def 1;
reconsider a as Point of Y by A1;
assume
A2: for x being Point of Y st x in A holds A = MaxADSet(x);
now
take a;
thus a in A by A1;
thus A = MaxADSet(a) by A2,A1;
end;
hence thesis;
end;
end;
definition
let Y be non empty TopStruct, A be Subset of Y;
func MaxADSet(A) -> Subset of Y equals
union {MaxADSet(a) where a is Point
of Y : a in A};
coherence
proof
set M = {MaxADSet(a) where a is Point of Y : a in A};
M c= bool the carrier of Y
proof
let C be object;
assume C in M;
then ex a being Point of Y st C = MaxADSet(a) & a in A;
hence thesis;
end;
then reconsider M as Subset-Family of Y;
union M is Subset of Y;
hence thesis;
end;
end;
theorem Th28:
for x being Point of Y holds MaxADSet(x) = MaxADSet({x})
proof
let x be Point of Y;
set M = {MaxADSet(a) where a is Point of Y : a in {x}};
now
let P be set;
assume P in M;
then ex a being Point of Y st P = MaxADSet(a) & a in {x};
hence P c= MaxADSet(x) by TARSKI:def 1;
end;
then
A1: MaxADSet({x}) c= MaxADSet(x) by ZFMISC_1:76;
x in {x} by TARSKI:def 1;
then MaxADSet(x) in M;
then MaxADSet(x) c= MaxADSet({x}) by ZFMISC_1:74;
hence thesis by A1;
end;
theorem Th29:
for A being Subset of Y, x being Point of Y holds MaxADSet(x)
meets MaxADSet(A) implies MaxADSet(x) meets A
proof
let A be Subset of Y, x be Point of Y;
set E = {MaxADSet(a) where a is Point of Y : a in A};
assume MaxADSet(x) /\ MaxADSet(A) <> {};
then consider z being object such that
A1: z in MaxADSet(x) /\ MaxADSet(A) by XBOOLE_0:def 1;
reconsider z as Point of Y by A1;
z in MaxADSet(A) by A1,XBOOLE_0:def 4;
then consider C being set such that
A2: z in C and
A3: C in E by TARSKI:def 4;
z in MaxADSet(x) by A1,XBOOLE_0:def 4;
then
A4: MaxADSet(z) = MaxADSet(x) by Th21;
consider b being Point of Y such that
A5: C = MaxADSet(b) and
A6: b in A by A3;
MaxADSet(b) = MaxADSet(z) by A2,A5,Th21;
then {b} c= MaxADSet(x) by A4,Th12;
then b in MaxADSet(x) by ZFMISC_1:31;
hence thesis by A6,XBOOLE_0:3;
end;
theorem Th30:
for A being Subset of Y, x being Point of Y holds MaxADSet(x)
meets MaxADSet(A) implies MaxADSet(x) c= MaxADSet(A)
proof
let A be Subset of Y, x be Point of Y;
set F = {MaxADSet(b) where b is Point of Y : b in A};
assume MaxADSet(x) meets MaxADSet(A);
then MaxADSet(x) meets A by Th29;
then consider z being object such that
A1: z in MaxADSet(x) /\ A by XBOOLE_0:4;
reconsider z as Point of Y by A1;
set E = {MaxADSet(a) where a is Point of Y : a in {z}};
z in A by A1,XBOOLE_0:def 4;
then
A2: {z} c= A by ZFMISC_1:31;
E c= F
proof
let C be object;
assume C in E;
then ex a being Point of Y st C = MaxADSet(a) & a in {z};
hence thesis by A2;
end;
then MaxADSet({z}) c= MaxADSet(A) by ZFMISC_1:77;
then
A3: MaxADSet(z) c= MaxADSet(A) by Th28;
z in MaxADSet(x) by A1,XBOOLE_0:def 4;
hence thesis by A3,Th21;
end;
theorem Th31:
for A, B being Subset of Y holds A c= B implies MaxADSet(A) c= MaxADSet(B)
proof
let A, B be Subset of Y;
set E = {MaxADSet(a) where a is Point of Y : a in A};
set F = {MaxADSet(b) where b is Point of Y : b in B};
assume
A1: A c= B;
E c= F
proof
let C be object;
assume C in E;
then ex a being Point of Y st C = MaxADSet(a) & a in A;
hence thesis by A1;
end;
hence thesis by ZFMISC_1:77;
end;
theorem Th32:
for A being Subset of Y holds A c= MaxADSet(A)
proof
let A be Subset of Y;
let x be object;
assume
A1: x in A;
then reconsider a = x as Point of Y;
{a} c= A by A1,ZFMISC_1:31;
then MaxADSet({a}) c= MaxADSet(A) by Th31;
then
A2: MaxADSet(a) c= MaxADSet(A) by Th28;
A3: a in {a} by TARSKI:def 1;
{a} c= MaxADSet(a) by Th12;
then {a} c= MaxADSet(A) by A2;
hence x in MaxADSet(A) by A3;
end;
theorem Th33:
for A being Subset of Y holds MaxADSet(A) = MaxADSet(MaxADSet(A) )
proof
let A be Subset of Y;
A1: MaxADSet(MaxADSet(A)) c= MaxADSet(A)
proof
let x be object;
assume x in MaxADSet(MaxADSet(A));
then consider C being set such that
A2: x in C and
A3: C in {MaxADSet(a) where a is Point of Y : a in MaxADSet(A)} by TARSKI:def 4
;
consider a being Point of Y such that
A4: C = MaxADSet(a) and
A5: a in MaxADSet(A) by A3;
consider D being set such that
A6: a in D and
A7: D in {MaxADSet(b) where b is Point of Y : b in A} by A5,TARSKI:def 4;
consider b being Point of Y such that
A8: D = MaxADSet(b) and
b in A by A7;
MaxADSet(a) = MaxADSet(b) by A6,A8,Th21;
hence thesis by A2,A4,A7,A8,TARSKI:def 4;
end;
MaxADSet(A) c= MaxADSet(MaxADSet(A)) by Th32;
hence thesis by A1;
end;
theorem Th34:
for A, B being Subset of Y holds A c= MaxADSet(B) implies
MaxADSet(A) c= MaxADSet(B)
proof
let A, B be Subset of Y;
assume A c= MaxADSet(B);
then MaxADSet(A) c= MaxADSet(MaxADSet(B)) by Th31;
hence thesis by Th33;
end;
theorem Th35:
for A, B being Subset of Y st
B c= MaxADSet(A) & A c= MaxADSet(B) holds MaxADSet(A) = MaxADSet(B)
by Th34;
theorem
for A, B being Subset of Y holds MaxADSet(A \/ B) = MaxADSet(A) \/
MaxADSet(B)
proof
let A, B be Subset of Y;
A1: MaxADSet(A \/ B) c= MaxADSet(A) \/ MaxADSet(B)
proof
let x be object;
assume x in MaxADSet(A \/ B);
then consider C being set such that
A2: x in C and
A3: C in {MaxADSet(a) where a is Point of Y : a in A \/ B} by TARSKI:def 4;
consider a being Point of Y such that
A4: C = MaxADSet(a) and
A5: a in A \/ B by A3;
now
per cases by A5,XBOOLE_0:def 3;
suppose
A6: a in A;
now
take C;
thus x in C by A2;
thus C in {MaxADSet(c) where c is Point of Y : c in A} by A4,A6;
end;
then
A7: x in MaxADSet(A) by TARSKI:def 4;
MaxADSet(A) c= MaxADSet(A) \/ MaxADSet(B) by XBOOLE_1:7;
hence thesis by A7;
end;
suppose
A8: a in B;
now
take C;
thus x in C by A2;
thus C in {MaxADSet(c) where c is Point of Y : c in B} by A4,A8;
end;
then
A9: x in MaxADSet(B) by TARSKI:def 4;
MaxADSet(B) c= MaxADSet(A) \/ MaxADSet(B) by XBOOLE_1:7;
hence thesis by A9;
end;
end;
hence thesis;
end;
A10: MaxADSet(B) c= MaxADSet(A \/ B) by Th31,XBOOLE_1:7;
MaxADSet(A) c= MaxADSet(A \/ B) by Th31,XBOOLE_1:7;
then MaxADSet(A) \/ MaxADSet(B) c= MaxADSet(A \/ B) by A10,XBOOLE_1:8;
hence thesis by A1;
end;
theorem Th37:
for A, B being Subset of Y holds MaxADSet(A /\ B) c= MaxADSet(A)
/\ MaxADSet(B)
proof
let A, B be Subset of Y;
A1: MaxADSet(A /\ B) c= MaxADSet(B) by Th31,XBOOLE_1:17;
MaxADSet(A /\ B) c= MaxADSet(A) by Th31,XBOOLE_1:17;
hence thesis by A1,XBOOLE_1:19;
end;
registration
let Y be non empty TopStruct, A be non empty Subset of Y;
cluster MaxADSet(A) -> non empty;
coherence by Th32,XBOOLE_1:3;
end;
registration
let Y be non empty TopStruct, A be empty Subset of Y;
cluster MaxADSet(A) -> empty;
coherence
proof
now
assume MaxADSet(A) is non empty;
then consider x being object such that
A1: x in MaxADSet(A);
reconsider a = x as Point of Y by A1;
consider D being set such that
a in D and
A2: D in {MaxADSet(b) where b is Point of Y : b in A} by A1,TARSKI:def 4;
ex b being Point of Y st D = MaxADSet(b) & b in A by A2;
hence contradiction;
end;
hence thesis;
end;
end;
registration
let Y be non empty TopStruct, A be non proper Subset of Y;
cluster MaxADSet(A) -> non proper;
coherence
proof
A = the carrier of Y by SUBSET_1:def 6;
then the carrier of Y c= MaxADSet(A) by Th32;
then MaxADSet(A) = the carrier of Y;
hence thesis;
end;
end;
registration
let Y be non trivial TopStruct, A be non trivial Subset of Y;
cluster MaxADSet(A) -> non trivial;
coherence
proof
A c= MaxADSet(A) by Th32;
hence thesis;
end;
end;
theorem Th38:
for G being Subset of Y, A being Subset of Y st G is open & A c=
G holds MaxADSet(A) c= G
proof
let G be Subset of Y, A be Subset of Y;
assume
A1: G is open;
assume
A2: A c= G;
MaxADSet(A) c= G
proof
let x be object;
assume
A3: x in MaxADSet(A);
then reconsider a = x as Point of Y;
consider D being set such that
A4: a in D and
A5: D in {MaxADSet(b) where b is Point of Y : b in A} by A3,TARSKI:def 4;
consider b being Point of Y such that
A6: D = MaxADSet(b) and
A7: b in A by A5;
A8: MaxADSet(a) = MaxADSet(b) by A4,A6,Th21;
A9: {a} c= MaxADSet(a) by Th12;
MaxADSet(b) c= G by A1,A2,A7,Th24;
then {a} c= G by A8,A9;
hence thesis by ZFMISC_1:31;
end;
hence thesis;
end;
theorem Th39:
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}
proof
let Y be non empty TopSpace;
let A be Subset of Y;
set F = {G where G is Subset of Y : G is open & A c= G};
[#]Y in F; then
A1: F <> {};
F c= bool the carrier of Y
proof
let C be object;
assume C in F;
then ex P being Subset of Y st C = P & P is open & A c= P;
hence thesis;
end;
then reconsider F as Subset-Family of Y;
now
let C be set;
assume C in F;
then ex G being Subset of Y st G = C & G is open & A c= G;
hence MaxADSet(A) c= C by Th38;
end;
hence thesis by A1,SETFAM_1:5;
end;
theorem Th40:
for F being Subset of Y, A being Subset of Y st F is closed & A
c= F holds MaxADSet(A) c= F
proof
let F be Subset of Y, A be Subset of Y;
assume
A1: F is closed;
assume
A2: A c= F;
MaxADSet(A) c= F
proof
let x be object;
assume
A3: x in MaxADSet(A);
then reconsider a = x as Point of Y;
consider D being set such that
A4: a in D and
A5: D in {MaxADSet(b) where b is Point of Y : b in A} by A3,TARSKI:def 4;
consider b being Point of Y such that
A6: D = MaxADSet(b) and
A7: b in A by A5;
A8: MaxADSet(a) = MaxADSet(b) by A4,A6,Th21;
A9: {a} c= MaxADSet(a) by Th12;
MaxADSet(b) c= F by A1,A2,A7,Th23;
then {a} c= F by A8,A9;
hence thesis by ZFMISC_1:31;
end;
hence thesis;
end;
theorem Th41:
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}
proof
let Y be non empty TopSpace;
let A be Subset of Y;
set G = {F where F is Subset of Y : F is closed & A c= F};
G c= bool the carrier of Y
proof
let C be object;
assume C in G;
then ex P being Subset of Y st C = P & P is closed & A c= P;
hence thesis;
end;
then reconsider G as Subset-Family of Y;
A1: now
let C be set;
assume C in G;
then ex F being Subset of Y st F = C & F is closed & A c= F;
hence MaxADSet(A) c= C by Th40;
end;
[#]Y in G; then
G <> {};
hence thesis by A1,SETFAM_1:5;
end;
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 :: redefines anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, definition)
for x being Point of X st x in A holds A c= Cl {x};
compatibility
proof
thus A is anti-discrete implies for x being Point of X st x in A holds A
c= Cl {x}
proof
assume
A1: A is anti-discrete;
let x be Point of X;
assume
A2: x in A;
{x} c= Cl {x} by PRE_TOPC:18;
then
A3: x in Cl {x} by ZFMISC_1:31;
A misses Cl {x} or A c= Cl {x} by A1;
hence A c= Cl {x} by A2,A3,XBOOLE_0:3;
end;
thus (for x being Point of X st x in A holds A c= Cl {x}) implies A is
anti-discrete
proof
assume
A4: for x being Point of X st x in A holds A c= Cl {x};
now
let F be Subset of X;
assume
A5: F is closed;
assume A meets F;
then consider a being object such that
A6: a in A /\ F by XBOOLE_0:4;
reconsider a as Point of X by A6;
a in F by A6,XBOOLE_0:def 4;
then {a} c= F by ZFMISC_1:31;
then
A7: Cl {a} c= F by A5,TOPS_1:5;
a in A by A6,XBOOLE_0:def 4;
then A c= Cl {a} by A4;
hence A c= F by A7;
end;
hence thesis;
end;
end;
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :: redefines anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, definition)
for x being Point of X st x in A holds Cl A = Cl {x};
compatibility
proof
thus A is anti-discrete implies for x being Point of X st x in A holds Cl
A = Cl {x}
by ZFMISC_1:31,PRE_TOPC:19,TOPS_1:5;
assume
A1: for x being Point of X st x in A holds Cl A = Cl {x};
now
let x be Point of X;
assume x in A;
then Cl A = Cl {x} by A1;
hence A c= Cl {x} by PRE_TOPC:18;
end;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is anti-discrete means :: redefines anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, redefinition) → anti-discrete (TEX_4, definition)
for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y};
compatibility
proof
thus A is anti-discrete implies for x, y being Point of X st x in A & y in
A holds Cl {x} = Cl {y}
proof
assume
A1: A is anti-discrete;
let x, y be Point of X;
assume that
A2: x in A and
A3: y in A;
A c= Cl {y} by A1,A3;
then {x} c= Cl {y} by A2,ZFMISC_1:31;
then
A4: Cl {x} c= Cl {y} by TOPS_1:5;
A c= Cl {x} by A1,A2;
then {y} c= Cl {x} by A3,ZFMISC_1:31;
then Cl {y} c= Cl {x} by TOPS_1:5;
hence thesis by A4;
end;
thus (for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y})
implies A is anti-discrete
proof
assume
A5: for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y};
now
let x be Point of X;
assume
A6: x in A;
now
let a be object;
assume
A7: a in A;
then reconsider y = a as Point of X;
{y} c= Cl {y} by PRE_TOPC:18;
then y in Cl {y} by ZFMISC_1:31;
hence a in Cl {x} by A5,A6,A7;
end;
hence A c= Cl {x};
end;
hence thesis;
end;
end;
end;
reserve X for non empty TopSpace;
theorem
for x being Point of X, D being Subset of X st D is anti-discrete & Cl
{x} c= D holds D = Cl {x}
proof
let x be Point of X, D be Subset of X;
assume D is anti-discrete;
then D misses Cl {x} or D c= Cl {x};
then
A1: D /\ Cl {x} = {} or D c= Cl {x};
assume Cl {x} c= D;
hence thesis by A1,XBOOLE_1:28;
end;
theorem
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}
proof
let A be Subset of X;
thus A is anti-discrete & A is closed implies for x being Point of X st x in
A holds A = Cl {x}
by ZFMISC_1:31,TOPS_1:5;
thus (for x being Point of X st x in A holds A = Cl {x}) implies A is
anti-discrete & A is closed
proof
assume
A1: for x being Point of X st x in A holds A = Cl {x};
then for x be Point of X st x in A holds A c= Cl {x};
hence A is anti-discrete;
hereby
per cases;
suppose
A is empty;
hence thesis;
end;
suppose
A is non empty;
then consider a being object such that
A2: a in A;
reconsider a as Point of X by A2;
A = Cl {a} by A1,A2;
hence thesis;
end;
end;
end;
end;
theorem
for A being Subset of X holds A is anti-discrete & A is not open
implies A is boundary
proof
let A be Subset of X;
A1: Int A c= A by TOPS_1:16;
assume A is anti-discrete;
then A misses Int A or A c= Int A;
then
A2: A /\ Int A = {} or A c= Int A;
assume
A3: A is not open;
assume A is not boundary;
then Int A <> {} by TOPS_1:48;
hence contradiction by A3,A2,A1,XBOOLE_0:def 10,XBOOLE_1:28;
end;
theorem Th45:
for x being Point of X st Cl {x} = {x} holds {x} is maximal_anti-discrete
proof
let x be Point of X;
assume
A1: Cl {x} = {x};
{x} is anti-discrete by Th6;
hence thesis by A1,Th17;
end;
reserve x,y for Point of X;
theorem Th46:
MaxADSet(x) c= meet {G where G is Subset of X : G is open & x in G}
proof
set F = {G where G is Subset of X : G is open & x in G};
[#]X in F; then
A1: F <> {};
F c= bool the carrier of X
proof
let C be object;
assume C in F;
then ex P being Subset of X st C = P & P is open & x in P;
hence thesis;
end;
then reconsider F as Subset-Family of X;
now
let C be set;
assume C in F;
then ex G being Subset of X st G = C & G is open & x in G;
hence MaxADSet(x) c= C by Th24;
end;
hence thesis by A1,SETFAM_1:5;
end;
theorem Th47:
MaxADSet(x) c= meet {F where F is Subset of X : F is closed & x in F}
proof
set G = {F where F is Subset of X : F is closed & x in F};
[#]X in G; then
A1: G <> {};
G c= bool the carrier of X
proof
let C be object;
assume C in G;
then ex P being Subset of X st C = P & P is closed & x in P;
hence thesis;
end;
then reconsider G as Subset-Family of X;
now
let C be set;
assume C in G;
then ex F being Subset of X st F = C & F is closed & x in F;
hence MaxADSet(x) c= C by Th23;
end;
hence thesis by A1,SETFAM_1:5;
end;
theorem Th48:
MaxADSet(x) c= Cl {x}
proof
Cl {x} = meet {F where F is Subset of X : F is closed & x in F} by Th2;
hence thesis by Th47;
end;
Lm1: MaxADSet(x) = MaxADSet(y) implies Cl {x} = Cl {y}
proof
assume
A1: MaxADSet(x) = MaxADSet(y);
then
A2: y in MaxADSet(x) by Th21;
MaxADSet(y) is maximal_anti-discrete by Th20;
then
A3: MaxADSet(y) is anti-discrete;
x in MaxADSet(y) by A1,Th21;
hence thesis by A1,A2,A3;
end;
theorem Th49:
MaxADSet(x) = MaxADSet(y) iff Cl {x} = Cl {y}
proof
A1: MaxADSet(x) c= MaxADSet(x) \/ MaxADSet(y) by XBOOLE_1:7;
thus MaxADSet(x) = MaxADSet(y) implies Cl {x} = Cl {y} by Lm1;
A2: MaxADSet(y) c= MaxADSet(x) \/ MaxADSet(y) by XBOOLE_1:7;
assume
A3: Cl {x} = Cl {y};
now
let a be Point of X;
assume
A4: a in MaxADSet(x) \/ MaxADSet(y);
now
per cases by A4,XBOOLE_0:def 3;
suppose
a in MaxADSet(x);
then
A5: MaxADSet(a) = MaxADSet(x) by Th21;
then Cl {a} = Cl {x} by Lm1;
then
A6: MaxADSet(y) c= Cl {a} by A3,Th48;
MaxADSet(x) c= Cl {a} by A5,Th48;
hence MaxADSet(x) \/ MaxADSet(y) c= Cl {a} by A6,XBOOLE_1:8;
end;
suppose
a in MaxADSet(y);
then
A7: MaxADSet(a) = MaxADSet(y) by Th21;
then Cl {a} = Cl {y} by Lm1;
then
A8: MaxADSet(x) c= Cl {a} by A3,Th48;
MaxADSet(y) c= Cl {a} by A7,Th48;
hence MaxADSet(x) \/ MaxADSet(y) c= Cl {a} by A8,XBOOLE_1:8;
end;
end;
hence MaxADSet(x) \/ MaxADSet(y) c= Cl {a};
end;
then
A9: MaxADSet(x) \/ MaxADSet(y) is anti-discrete;
A10: MaxADSet(y) is maximal_anti-discrete by Th20;
MaxADSet(x) is maximal_anti-discrete by Th20;
then MaxADSet(x) = MaxADSet(x) \/ MaxADSet(y) by A9,A1;
hence thesis by A9,A10,A2;
end;
theorem
MaxADSet(x) misses MaxADSet(y) iff Cl {x} <> Cl {y} by Th49,Th22;
definition
let X be non empty TopSpace, x be Point of X;
redefine func MaxADSet(x) -> non empty Subset of X equals :: redefines MaxADSet (TEX_4, definition)
(Cl {x}) /\ meet {
G where G is Subset of X : G is open & x in G};
compatibility
proof
set F = {G where G is Subset of X : G is open & x in G};
F c= bool the carrier of X
proof
let C be object;
assume C in F;
then ex P being Subset of X st C = P & P is open & x in P;
hence thesis;
end;
then reconsider F as Subset-Family of X;
A1: MaxADSet(x) c= Cl {x} by Th48;
A2: (Cl {x}) /\ meet F c= MaxADSet(x)
proof
assume not (Cl {x}) /\ meet F c= MaxADSet(x);
then ((Cl {x}) /\ meet F) \ MaxADSet(x) <> {} by XBOOLE_1:37;
then consider a being object such that
A3: a in ((Cl {x}) /\ meet F) \ MaxADSet(x) by XBOOLE_0:def 1;
A4: a in (Cl {x}) /\ meet F by A3,XBOOLE_0:def 5;
reconsider a as Point of X by A3;
not a in MaxADSet(x) by A3,XBOOLE_0:def 5;
then
A5: MaxADSet(a) <> MaxADSet(x) by Th21;
now
set G = (Cl{a})`;
{a} c= Cl {a} by PRE_TOPC:18;
then
A6: a in Cl {a} by ZFMISC_1:31;
assume not x in Cl {a};
then x in G by SUBSET_1:29;
then G in F;
then
A7: meet F c= G by SETFAM_1:3;
a in meet F by A4,XBOOLE_0:def 4;
hence contradiction by A7,A6,XBOOLE_0:def 5;
end;
then {x} c= Cl {a} by ZFMISC_1:31;
then
A8: Cl {x} c= Cl {a} by TOPS_1:5;
a in Cl {x} by A4,XBOOLE_0:def 4;
then {a} c= Cl {x} by ZFMISC_1:31;
then Cl {a} c= Cl {x} by TOPS_1:5;
then Cl {x} = Cl {a} by A8;
hence contradiction by A5,Th49;
end;
MaxADSet(x) c= meet F by Th46;
then MaxADSet(x) c= (Cl {x}) /\ meet F by A1,XBOOLE_1:19;
hence thesis by A2;
end;
coherence;
end;
theorem Th51:
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}
proof
let x, y be Point of X;
set FX = {G where G is Subset of X : G is open & x in G};
set FY = {G where G is Subset of X : G is open & y in G};
A1: [#]X in FX;
thus Cl {x} c= Cl {y} implies 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}
proof
assume
A2: Cl {x} c= Cl {y};
now
let P be object;
assume P in FX;
then consider G being Subset of X such that
A3: G = P and
A4: G is open and
A5: x in G;
now
assume not y in G;
then {y} misses G by ZFMISC_1:50;
then
A6: (Cl {y}) misses G by A4,TSEP_1:36;
{x} c= Cl {x} by PRE_TOPC:18;
then x in Cl {x} by ZFMISC_1:31;
hence contradiction by A2,A5,A6,XBOOLE_0:3;
end;
hence P in FY by A3,A4;
end;
then FX c= FY;
hence thesis by A1,SETFAM_1:6;
end;
assume
A7: 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};
set G = (Cl {y})`;
assume
A8: not Cl {x} c= Cl {y};
not x in Cl {y} by A8,TOPS_1:5,ZFMISC_1:31;
then x in G by SUBSET_1:29;
then G in FX;
then meet FX c= G by SETFAM_1:3;
then
A9: meet FY c= G by A7;
{y} c= Cl {y} by PRE_TOPC:18;
then
A10: y in Cl {y} by ZFMISC_1:31;
{y} c= MaxADSet(y) by Th12;
then
A11: y in MaxADSet(y) by ZFMISC_1:31;
MaxADSet(y) c= meet FY by Th46;
then y in meet FY by A11;
hence contradiction by A9,A10,XBOOLE_0:def 5;
end;
theorem
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}
proof
let x, y be Point of X;
set FY = {G where G is Subset of X : G is open & y in G};
FY c= bool the carrier of X
proof
let C be object;
assume C in FY;
then ex P being Subset of X st C = P & P is open & y in P;
hence thesis;
end;
then reconsider FY as Subset-Family of X;
set FX = {G where G is Subset of X : G is open & x in G};
FX c= bool the carrier of X
proof
let C be object;
assume C in FX;
then ex P being Subset of X st C = P & P is open & x in P;
hence thesis;
end;
then reconsider FX as Subset-Family of X;
thus Cl {x} c= Cl {y} implies MaxADSet(y) c= meet {G where G is Subset of X
: G is open & x in G}
proof
assume Cl {x} c= Cl {y};
then
A1: meet FY c= meet FX by Th51;
(Cl {y}) /\ meet FY c= meet FY by XBOOLE_1:17;
hence thesis by A1;
end;
{y} c= MaxADSet(y) by Th12;
then
A2: y in MaxADSet(y) by ZFMISC_1:31;
assume MaxADSet(y) c= meet {G where G is Subset of X : G is open & x in G};
then
A3: y in meet FX by A2;
set G = (Cl {y})`;
assume
A4: not Cl {x} c= Cl {y};
not x in Cl {y} by A4,TOPS_1:5,ZFMISC_1:31;
then x in G by SUBSET_1:29;
then G in FX;
then
A5: meet FX c= G by SETFAM_1:3;
{y} c= Cl {y} by PRE_TOPC:18;
then y in Cl {y} by ZFMISC_1:31;
hence contradiction by A5,A3,XBOOLE_0:def 5;
end;
theorem Th53:
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
proof
let x, y be Point of X;
thus MaxADSet(x) misses MaxADSet(y) implies (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
proof
set V = (Cl {y})`;
set W = (Cl {x})`;
assume
A1: MaxADSet(x) /\ MaxADSet(y) = {};
assume
A2: for V being Subset of X holds V is open & MaxADSet(x) c= V implies
V meets MaxADSet(y);
now
take W;
thus W is open;
MaxADSet(x) c= Cl {x} by Th48;
hence W misses MaxADSet(x) by SUBSET_1:24;
now
MaxADSet(y) c= Cl {y} by Th48;
then V misses MaxADSet(y) by SUBSET_1:24;
then not MaxADSet(x) c= V by A2;
then MaxADSet(x) \ V <> {} by XBOOLE_1:37;
then consider b being object such that
A3: b in MaxADSet(x) \ V by XBOOLE_0:def 1;
A4: b in MaxADSet(x) by A3,XBOOLE_0:def 5;
reconsider b as Point of X by A3;
not b in V by A3,XBOOLE_0:def 5;
then b in Cl {y} by SUBSET_1:29;
then
A5: {b} c= Cl {y} by ZFMISC_1:31;
MaxADSet(b) = MaxADSet(x) by A4,Th21;
then Cl {b} = Cl {x} by Th49;
then
A6: Cl {x} c= Cl {y} by A5,TOPS_1:5;
assume not MaxADSet(y) c= W;
then MaxADSet(y) \ W <> {} by XBOOLE_1:37;
then consider a being object such that
A7: a in MaxADSet(y) \ W by XBOOLE_0:def 1;
A8: a in MaxADSet(y) by A7,XBOOLE_0:def 5;
reconsider a as Point of X by A7;
not a in W by A7,XBOOLE_0:def 5;
then a in Cl {x} by SUBSET_1:29;
then
A9: {a} c= Cl {x} by ZFMISC_1:31;
MaxADSet(a) = MaxADSet(y) by A8,Th21;
then Cl {a} = Cl {y} by Th49;
then Cl {y} c= Cl {x} by A9,TOPS_1:5;
then Cl {x} = Cl {y} by A6;
then MaxADSet(x) = MaxADSet(y) by Th49;
hence contradiction by A1;
end;
hence MaxADSet(y) c= W;
end;
hence thesis;
end;
assume
A10: (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;
assume MaxADSet(x) meets MaxADSet(y);
then
A11: MaxADSet(x) = MaxADSet(y) by Th22;
now
per cases by A10;
suppose
ex V being Subset of X st V is open & MaxADSet(x) c= V & V
misses MaxADSet(y);
then consider V being Subset of X such that
V is open and
A12: MaxADSet(x) c= V and
A13: V misses MaxADSet(y);
V /\ MaxADSet(y) = {} by A13;
hence contradiction by A11,A12,XBOOLE_1:28;
end;
suppose
ex W being Subset of X st W is open & W misses MaxADSet(x) &
MaxADSet(y) c= W;
then consider W being Subset of X such that
W is open and
A14: W misses MaxADSet(x) and
A15: MaxADSet(y) c= W;
W /\ MaxADSet(x) = {} by A14;
hence contradiction by A11,A15,XBOOLE_1:28;
end;
end;
hence contradiction;
end;
theorem
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
proof
let x, y be Point of X;
thus MaxADSet(x) misses MaxADSet(y) implies (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
proof
assume
A1: MaxADSet(x) misses MaxADSet(y);
hereby
per cases by A1,Th53;
suppose
ex V being Subset of X st V is open & MaxADSet(x) c= V & V
misses MaxADSet(y);
then consider V being Subset of X such that
A2: V is open and
A3: MaxADSet(x) c= V and
A4: V misses MaxADSet(y);
now
take F = V`;
thus F is closed by A2;
thus F misses MaxADSet(x) by A3,SUBSET_1:24;
thus MaxADSet(y) c= F by A4,SUBSET_1:23;
end;
hence thesis;
end;
suppose
ex W being Subset of X st W is open & W misses MaxADSet(x) &
MaxADSet(y) c= W;
then consider W being Subset of X such that
A5: W is open and
A6: W misses MaxADSet(x) and
A7: MaxADSet(y) c= W;
now
take E = W`;
thus E is closed by A5;
thus MaxADSet(x) c= E by A6,SUBSET_1:23;
thus E misses MaxADSet(y) by A7,SUBSET_1:24;
end;
hence thesis;
end;
end;
end;
assume
A8: (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;
assume MaxADSet(x) meets MaxADSet(y);
then
A9: MaxADSet(x) = MaxADSet(y) by Th22;
now
per cases by A8;
suppose
ex E being Subset of X st E is closed & MaxADSet(x) c= E & E
misses MaxADSet(y);
then consider E being Subset of X such that
E is closed and
A10: MaxADSet(x) c= E and
A11: E misses MaxADSet(y);
E /\ MaxADSet(y) = {} by A11;
hence contradiction by A9,A10,XBOOLE_1:28;
end;
suppose
ex F being Subset of X st F is closed & F misses MaxADSet(x) &
MaxADSet(y) c= F;
then consider F being Subset of X such that
F is closed and
A12: F misses MaxADSet(x) and
A13: MaxADSet(y) c= F;
F /\ MaxADSet(x) = {} by A12;
hence contradiction by A9,A13,XBOOLE_1:28;
end;
end;
hence contradiction;
end;
reserve A, B for Subset of X;
reserve P, Q for Subset of X;
theorem Th55:
MaxADSet(A) c= meet {G where G is Subset of X : G is open & A c= G} by Th39;
theorem Th56:
P is open implies MaxADSet(P) = P
proof
set F = {G where G is Subset of X : G is open & P c= G};
A1: P c= MaxADSet(P) by Th32;
assume P is open;
then P in F;
then
A2: meet F c= P by SETFAM_1:3;
MaxADSet(P) c= meet F by Th55;
then MaxADSet(P) c= P by A2;
hence thesis by A1;
end;
theorem
MaxADSet(Int A) = Int A by Th56;
theorem Th58:
MaxADSet(A) c= meet {F where F is Subset of X : F is closed & A c= F}
by Th41;
theorem Th59:
MaxADSet(A) c= Cl A
proof
Cl A = meet {F where F is Subset of X : F is closed & A c= F} by Th1;
hence thesis by Th58;
end;
theorem Th60:
P is closed implies MaxADSet(P) = P
proof
assume P is closed;
then
A1: Cl P = P by PRE_TOPC:22;
A2: P c= MaxADSet(P) by Th32;
MaxADSet(P) c= Cl P by Th59;
hence thesis by A1,A2;
end;
theorem
MaxADSet(Cl A) = Cl A by Th60;
theorem
Cl MaxADSet(A) = Cl A by Th59,TOPS_1:5,Th32,PRE_TOPC:19;
theorem
MaxADSet(A) = MaxADSet(B) implies Cl A = Cl B
proof
A1: MaxADSet(A) c= Cl A by Th59;
A2: MaxADSet(B) c= Cl B by Th59;
assume
A3: MaxADSet(A) = MaxADSet(B);
then A c= MaxADSet(B) by Th32;
then A c= Cl B by A2;
then
A4: Cl A c= Cl B by TOPS_1:5;
B c= MaxADSet(A) by A3,Th32;
then B c= Cl A by A1;
then Cl B c= Cl A by TOPS_1:5;
hence thesis by A4;
end;
theorem
P is closed or Q is closed implies MaxADSet(P /\ Q) = MaxADSet(P) /\
MaxADSet(Q)
proof
assume
A1: P is closed or Q is closed;
A2: MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q)
proof
assume not MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q);
then consider x being object such that
A3: x in MaxADSet(P) /\ MaxADSet(Q) and
A4: not x in MaxADSet(P /\ Q);
reconsider x as Point of X by A3;
now
per cases by A1;
suppose
A5: P is closed;
then P = MaxADSet(P) by Th60;
then x in P by A3,XBOOLE_0:def 4;
then
A6: MaxADSet(x) c= P by A5,Th23;
A7: P /\ Q c= MaxADSet(P /\ Q) by Th32;
x in MaxADSet(Q) by A3,XBOOLE_0:def 4;
then consider D being set such that
A8: x in D and
A9: D in {MaxADSet(b) where b is Point of X : b in Q} by TARSKI:def 4;
consider b being Point of X such that
A10: D = MaxADSet(b) and
A11: b in Q by A9;
{b} c= MaxADSet(b) by Th12;
then
A12: b in MaxADSet(b) by ZFMISC_1:31;
MaxADSet(x) = MaxADSet(b) by A8,A10,Th21;
then b in P /\ Q by A6,A11,A12,XBOOLE_0:def 4;
then MaxADSet(b) meets MaxADSet(P /\ Q) by A12,A7,XBOOLE_0:3;
then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
hence contradiction by A4,A8,A10;
end;
suppose
A13: Q is closed;
then Q = MaxADSet(Q) by Th60;
then x in Q by A3,XBOOLE_0:def 4;
then
A14: MaxADSet(x) c= Q by A13,Th23;
A15: P /\ Q c= MaxADSet(P /\ Q) by Th32;
x in MaxADSet(P) by A3,XBOOLE_0:def 4;
then consider D being set such that
A16: x in D and
A17: D in {MaxADSet(b) where b is Point of X : b in P} by TARSKI:def 4;
consider b being Point of X such that
A18: D = MaxADSet(b) and
A19: b in P by A17;
{b} c= MaxADSet(b) by Th12;
then
A20: b in MaxADSet(b) by ZFMISC_1:31;
MaxADSet(x) = MaxADSet(b) by A16,A18,Th21;
then b in P /\ Q by A14,A19,A20,XBOOLE_0:def 4;
then MaxADSet(b) meets MaxADSet(P /\ Q) by A20,A15,XBOOLE_0:3;
then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
hence contradiction by A4,A16,A18;
end;
end;
hence contradiction;
end;
MaxADSet(P /\ Q) c= MaxADSet(P) /\ MaxADSet(Q) by Th37;
hence thesis by A2;
end;
theorem
P is open or Q is open implies MaxADSet(P /\ Q) = MaxADSet(P) /\ MaxADSet(Q)
proof
assume
A1: P is open or Q is open;
A2: MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q)
proof
assume not MaxADSet(P) /\ MaxADSet(Q) c= MaxADSet(P /\ Q);
then consider x being object such that
A3: x in MaxADSet(P) /\ MaxADSet(Q) and
A4: not x in MaxADSet(P /\ Q);
reconsider x as Point of X by A3;
now
per cases by A1;
suppose
A5: P is open;
then P = MaxADSet(P) by Th56;
then x in P by A3,XBOOLE_0:def 4;
then
A6: MaxADSet(x) c= P by A5,Th24;
A7: P /\ Q c= MaxADSet(P /\ Q) by Th32;
x in MaxADSet(Q) by A3,XBOOLE_0:def 4;
then consider D being set such that
A8: x in D and
A9: D in {MaxADSet(b) where b is Point of X : b in Q} by TARSKI:def 4;
consider b being Point of X such that
A10: D = MaxADSet(b) and
A11: b in Q by A9;
{b} c= MaxADSet(b) by Th12;
then
A12: b in MaxADSet(b) by ZFMISC_1:31;
MaxADSet(x) = MaxADSet(b) by A8,A10,Th21;
then b in P /\ Q by A6,A11,A12,XBOOLE_0:def 4;
then MaxADSet(b) meets MaxADSet(P /\ Q) by A12,A7,XBOOLE_0:3;
then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
hence contradiction by A4,A8,A10;
end;
suppose
A13: Q is open;
then Q = MaxADSet(Q) by Th56;
then x in Q by A3,XBOOLE_0:def 4;
then
A14: MaxADSet(x) c= Q by A13,Th24;
A15: P /\ Q c= MaxADSet(P /\ Q) by Th32;
x in MaxADSet(P) by A3,XBOOLE_0:def 4;
then consider D being set such that
A16: x in D and
A17: D in {MaxADSet(b) where b is Point of X : b in P} by TARSKI:def 4;
consider b being Point of X such that
A18: D = MaxADSet(b) and
A19: b in P by A17;
{b} c= MaxADSet(b) by Th12;
then
A20: b in MaxADSet(b) by ZFMISC_1:31;
MaxADSet(x) = MaxADSet(b) by A16,A18,Th21;
then b in P /\ Q by A14,A19,A20,XBOOLE_0:def 4;
then MaxADSet(b) meets MaxADSet(P /\ Q) by A20,A15,XBOOLE_0:3;
then MaxADSet(b) c= MaxADSet(P /\ Q) by Th30;
hence contradiction by A4,A16,A18;
end;
end;
hence contradiction;
end;
MaxADSet(P /\ Q) c= MaxADSet(P) /\ MaxADSet(Q) by Th37;
hence thesis by A2;
end;
begin
:: 5. Maximal Anti-discrete Subspaces.
reserve Y for non empty TopStruct;
theorem Th66:
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
proof
let Y0 be SubSpace of Y, A be Subset of Y;
assume
A1: A = the carrier of Y0;
assume Y0 is anti-discrete;
then
A2: the topology of Y0 = {{}, the carrier of Y0} by TDLAT_3:def 2;
now
let G be Subset of Y;
reconsider H = A /\ G as Subset of Y0 by A1,XBOOLE_1:17;
assume
A3: G is open;
G in the topology of Y & H = G /\ [#]Y0 by A1,A3,PRE_TOPC:def 2;
then H in the topology of Y0 by PRE_TOPC:def 4;
then A /\ G = {} or A /\ G = the carrier of Y0 by A2,TARSKI:def 2;
hence A misses G or A c= G by A1,XBOOLE_1:17;
end;
hence thesis;
end;
theorem Th67:
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
proof
let Y0 be SubSpace of Y;
assume
A1: Y0 is TopSpace-like;
then
A2: the carrier of Y0 in the topology of Y0 by PRE_TOPC:def 1;
let A be Subset of Y;
assume
A3: A = the carrier of Y0;
assume
A4: A is anti-discrete;
now
let D be object;
assume
A5: D in the topology of Y0;
then reconsider C = D as Subset of Y0;
consider E being Subset of Y such that
A6: E in the topology of Y and
A7: C = E /\ [#]Y0 by A5,PRE_TOPC:def 4;
reconsider E as Subset of Y;
A8: E is open by A6,PRE_TOPC:def 2;
now
per cases by A4,A8;
suppose
A misses E;
hence C = {} or C = A by A3,A7;
end;
suppose
A c= E;
hence C = {} or C = A by A3,A7,XBOOLE_1:28;
end;
end;
hence D in {{},the carrier of Y0} by A3,TARSKI:def 2;
end;
then
A9: the topology of Y0 c= {{},the carrier of Y0};
{} in the topology of Y0 by A1,PRE_TOPC:1;
then {{},the carrier of Y0} c= the topology of Y0 by A2,ZFMISC_1:32;
then the topology of Y0 = {{},the carrier of Y0} by A9;
hence thesis by TDLAT_3:def 2;
end;
reserve X for non empty TopSpace,
Y0 for non empty SubSpace of X;
theorem
(for X0 being open SubSpace of X holds Y0 misses X0 or Y0 is SubSpace
of X0) implies Y0 is anti-discrete
proof
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
assume
A1: for X0 being open SubSpace of X holds Y0 misses X0 or Y0 is SubSpace of X0;
now
let G be Subset of X;
assume
A2: G is open;
now
per cases;
suppose
G is empty;
hence A misses G or A c= G;
end;
suppose
G is non empty;
then consider X0 being strict open non empty SubSpace of X such that
A3: G = the carrier of X0 by A2,TSEP_1:20;
Y0 misses X0 or Y0 is SubSpace of X0 by A1;
hence A misses G or A c= G by A3,TSEP_1:4,def 3;
end;
end;
hence A misses G or A c= G;
end;
then A is anti-discrete;
hence thesis by Th67;
end;
theorem
(for X0 being closed SubSpace of X holds Y0 misses X0 or Y0 is
SubSpace of X0) implies Y0 is anti-discrete
proof
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
assume
A1: for X0 being closed SubSpace of X holds Y0 misses X0 or Y0 is
SubSpace of X0;
now
let G be Subset of X;
assume
A2: G is closed;
now
per cases;
suppose
G is empty;
hence A misses G or A c= G;
end;
suppose
G is non empty;
then consider X0 being strict closed non empty SubSpace of X such that
A3: G = the carrier of X0 by A2,TSEP_1:15;
Y0 misses X0 or Y0 is SubSpace of X0 by A1;
hence A misses G or A c= G by A3,TSEP_1:4,def 3;
end;
end;
hence A misses G or A c= G;
end;
then A is anti-discrete;
hence thesis by Th67;
end;
theorem
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
proof
let Y0 be anti-discrete SubSpace of X;
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
let X0 be open SubSpace of X;
reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;
A1: G is open by TSEP_1:16;
A is anti-discrete by Th66;
then A misses G or A c= G by A1;
hence thesis by TSEP_1:4,def 3;
end;
theorem
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
proof
let Y0 be anti-discrete SubSpace of X;
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
let X0 be closed SubSpace of X;
reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;
A1: G is closed by TSEP_1:11;
A is anti-discrete by Th66;
then A misses G or A c= G by A1;
hence thesis by TSEP_1:4,def 3;
end;
definition
let Y be non empty TopStruct;
let IT be SubSpace of Y;
attr IT is maximal_anti-discrete means
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;
coherence;
cluster non anti-discrete -> non maximal_anti-discrete for SubSpace of Y;
coherence;
end;
theorem Th72:
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
proof
let Y0 be non empty SubSpace of X, A be Subset of X;
assume
A1: A = the carrier of Y0;
thus Y0 is maximal_anti-discrete implies A is maximal_anti-discrete
proof
assume
A2: Y0 is maximal_anti-discrete;
A3: now
let D be Subset of X;
assume
A4: D is anti-discrete;
assume
A5: A c= D;
then D <> {} by A1;
then consider X0 being strict non empty SubSpace of X such that
A6: D = the carrier of X0 by TSEP_1:10;
X0 is anti-discrete by A4,A6,Th67;
hence A = D by A1,A2,A5,A6;
end;
A is anti-discrete by A1,A2,Th66;
hence thesis by A3;
end;
assume
A7: A is maximal_anti-discrete;
A8: now
let X0 be SubSpace of X;
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is anti-discrete;
then
A9: D is anti-discrete by Th66;
assume the carrier of Y0 c= the carrier of X0;
hence the carrier of Y0 = the carrier of X0 by A1,A7,A9;
end;
A is anti-discrete by A7;
then Y0 is anti-discrete by A1,Th67;
hence thesis by A8;
end;
registration
let X be non empty TopSpace;
cluster open anti-discrete -> maximal_anti-discrete 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 TSEP_1:1;
assume X0 is open;
then
A1: A is open by TSEP_1:16;
assume X0 is anti-discrete;
then A is anti-discrete by Th66;
then A is maximal_anti-discrete by A1,Th16;
hence thesis by Th72;
end;
cluster open non maximal_anti-discrete -> non anti-discrete for non empty
SubSpace of X;
coherence;
cluster anti-discrete non maximal_anti-discrete -> non open for non empty
SubSpace of X;
coherence;
cluster closed anti-discrete -> maximal_anti-discrete 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 TSEP_1:1;
assume X0 is closed;
then
A2: A is closed by TSEP_1:11;
assume X0 is anti-discrete;
then A is anti-discrete by Th66;
then A is maximal_anti-discrete by A2,Th17;
hence thesis by Th72;
end;
cluster closed non maximal_anti-discrete -> non anti-discrete for non empty
SubSpace of X;
coherence;
cluster anti-discrete non maximal_anti-discrete -> non closed for non empty
SubSpace of X;
coherence;
end;
definition
let Y be TopStruct, x be Point of Y;
func MaxADSspace(x) -> strict SubSpace of Y means
:Def17:
the carrier of it = MaxADSet(x);
existence
proof
set D = MaxADSet(x);
set Y0 = Y|D;
take Y0;
D = [#]Y0 by PRE_TOPC:def 5;
hence thesis;
end;
uniqueness
proof
let Y1, Y2 be strict SubSpace of Y;
assume that
A1: the carrier of Y1 = MaxADSet(x) and
A2: the carrier of Y2 = MaxADSet(x);
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;
registration
let Y be non empty TopStruct, x be Point of Y;
cluster MaxADSspace(x) -> non empty;
coherence
proof
the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
hence the carrier of MaxADSspace(x) is non empty;
end;
end;
Lm2: for X1, X2 being SubSpace of Y holds the carrier of X1 c= the carrier of
X2 implies X1 is SubSpace of X2
proof
let X1, X2 be SubSpace of Y;
set A1 = the carrier of X1, A2 = the carrier of X2;
A1: A1 = [#]X1;
assume
A2: A1 c= A2;
A3: A2 = [#]X2;
for P being Subset of X1 holds P in the topology of X1 iff ex Q being
Subset of X2 st Q in the topology of X2 & P = Q /\ A1
proof
let P be Subset of X1;
thus P in the topology of X1 implies ex Q being Subset of X2 st Q in the
topology of X2 & P = Q /\ A1
proof
assume P in the topology of X1;
then consider R being Subset of Y such that
A4: R in the topology of Y and
A5: P = R /\ A1 by A1,PRE_TOPC:def 4;
reconsider Q = R /\ A2 as Subset of X2 by XBOOLE_1:17;
take Q;
thus Q in the topology of X2 by A3,A4,PRE_TOPC:def 4;
Q /\ A1 = R /\ (A2 /\ A1) by XBOOLE_1:16
.= R /\ A1 by A2,XBOOLE_1:28;
hence thesis by A5;
end;
given Q being Subset of X2 such that
A6: Q in the topology of X2 and
A7: P = Q /\ A1;
consider R being Subset of Y such that
A8: R in the topology of Y and
A9: Q = R /\ [#]X2 by A6,PRE_TOPC:def 4;
P = R /\ (A2 /\ A1) by A7,A9,XBOOLE_1:16
.= R /\ A1 by A2,XBOOLE_1:28;
hence thesis by A1,A8,PRE_TOPC:def 4;
end;
hence thesis by A1,A3,A2,PRE_TOPC:def 4;
end;
theorem
for x being Point of Y holds Sspace(x) is SubSpace of MaxADSspace(x)
proof
let x be Point of Y;
A1: the carrier of Sspace(x) = {x} by TEX_2:def 2;
the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
hence thesis by A1,Lm2,Th12;
end;
theorem
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)
proof
let x, y be Point of Y;
A1: the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
thus y is Point of MaxADSspace(x) implies the TopStruct of MaxADSspace(y) =
the TopStruct of MaxADSspace(x)
proof
assume y is Point of MaxADSspace(x);
then MaxADSet(y) = MaxADSet(x) by A1,Th21;
hence thesis by A1,Def17;
end;
assume
A2: the TopStruct of MaxADSspace(y) = the TopStruct of MaxADSspace(x);
the carrier of MaxADSspace(y) = MaxADSet(y) by Def17;
hence thesis by A2,Th21;
end;
theorem
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)
proof
let x, y be Point of Y;
assume
A1: the carrier of MaxADSspace(x) meets the carrier of MaxADSspace(y);
A2: the carrier of MaxADSspace(y) = MaxADSet(y) by Def17;
the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
hence thesis by A2,A1,Th22,TSEP_1:5;
end;
registration
let X be non empty TopSpace;
cluster maximal_anti-discrete strict for SubSpace of X;
existence
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;
consider X0 being strict non empty SubSpace of X such that
A2: MaxADSet(a) = the carrier of X0 by TSEP_1:10;
take X0;
MaxADSet(a) is maximal_anti-discrete by Th20;
hence thesis by A2,Th72;
end;
end;
registration
let X be non empty TopSpace, x be Point of X;
cluster MaxADSspace(x) -> maximal_anti-discrete;
coherence
proof
A1: MaxADSet(x) is maximal_anti-discrete by Th20;
MaxADSet(x) = the carrier of MaxADSspace(x) by Def17;
hence thesis by A1,Th72;
end;
end;
theorem
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
proof
let X0 be closed non empty SubSpace of X, x be Point of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is closed by TSEP_1:11;
assume x is Point of X0;
then MaxADSet(x) c= A by A1,Th23;
then the carrier of MaxADSspace(x) c= the carrier of X0 by Def17;
hence thesis by Lm2;
end;
theorem
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
proof
let X0 be open non empty SubSpace of X, x be Point of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is open by TSEP_1:16;
assume x is Point of X0;
then MaxADSet(x) c= A by A1,Th24;
then the carrier of MaxADSspace(x) c= the carrier of X0 by Def17;
hence thesis by Lm2;
end;
theorem
for x being Point of X st Cl {x} = {x} holds Sspace(x) is
maximal_anti-discrete
proof
let x be Point of X;
assume Cl {x} = {x};
then
A1: {x} is maximal_anti-discrete by Th45;
the carrier of Sspace(x) = {x} by TEX_2:def 2;
hence thesis by A1,Th72;
end;
notation
let Y be TopStruct, A be Subset of Y;
synonym Sspace(A) for Y|A;
end;
Lm3: for Y being TopStruct, A being Subset of Y holds the carrier of (Y|A) = A
proof
let Y be TopStruct, A be Subset of Y;
[#](Y|A) = A by PRE_TOPC:def 5;
hence thesis;
end;
theorem
for A being non empty Subset of Y holds A is Subset of Sspace(A)
proof
let A be non empty Subset of Y;
the carrier of Sspace(A) c= the carrier of Sspace(A);
hence thesis by Lm3;
end;
theorem
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
proof
let Y0 be SubSpace of Y, A be non empty Subset of Y;
assume A is Subset of Y0;
then A c= the carrier of Y0;
then the carrier of Sspace(A) c= the carrier of Y0 by Lm3;
hence thesis by Lm2;
end;
registration
let Y be non trivial TopStruct;
cluster non proper strict 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 by TEX_2:10;
end;
end;
registration
let Y be non trivial TopStruct, A be non trivial Subset
of Y;
cluster Sspace(A) -> non trivial;
coherence by Lm3;
end;
registration
let Y be non empty TopStruct, A be non proper Subset of Y;
cluster Sspace(A) -> non proper;
coherence
proof
now
assume
A1: Sspace(A) is proper;
the carrier of Sspace(A) = A by Lm3;
hence contradiction by A1,TEX_2:8;
end;
hence thesis;
end;
end;
definition
let Y be non empty TopStruct, A be Subset of Y;
func MaxADSspace(A) -> strict SubSpace of Y means
:Def18:
the carrier of it = MaxADSet(A);
existence
proof
set D = MaxADSet(A);
set Y0 = Y|D;
take Y0;
D = [#]Y0 by PRE_TOPC:def 5;
hence thesis;
end;
uniqueness
proof
let Y1, Y2 be strict SubSpace of Y;
assume that
A1: the carrier of Y1 = MaxADSet(A) and
A2: the carrier of Y2 = MaxADSet(A);
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;
registration
let Y be non empty TopStruct, A be non empty Subset of Y;
cluster MaxADSspace(A) -> non empty;
coherence
proof
the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence the carrier of MaxADSspace(A) is non empty;
end;
end;
theorem
for A being non empty Subset of Y holds A is Subset of MaxADSspace(A)
proof
let A be non empty Subset of Y;
the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence thesis by Th32;
end;
theorem
for A being non empty Subset of Y holds Sspace(A) is SubSpace of
MaxADSspace(A)
proof
let A be non empty Subset of Y;
A1: the carrier of Sspace(A) = A by Lm3;
the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence thesis by A1,Lm2,Th32;
end;
theorem
for x being Point of Y holds the TopStruct of MaxADSspace(x) = the
TopStruct of MaxADSspace({x})
proof
let x be Point of Y;
A1: the carrier of MaxADSspace({x}) = MaxADSet({x}) by Def18;
the carrier of MaxADSspace(x) = MaxADSet(x) by Def17;
hence thesis by A1,Th28,TSEP_1:5;
end;
theorem
for A, B being non empty Subset of Y holds A c= B implies MaxADSspace(
A) is SubSpace of MaxADSspace(B)
proof
let A, B be non empty Subset of Y;
assume
A1: A c= B;
A2: the carrier of MaxADSspace(B) = MaxADSet(B) by Def18;
the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence thesis by A2,A1,Lm2,Th31;
end;
theorem
for A being non empty Subset of Y holds the TopStruct of MaxADSspace(A
) = the TopStruct of MaxADSspace(MaxADSet(A))
proof
let A be non empty Subset of Y;
A1: the carrier of MaxADSspace(MaxADSet(A)) = MaxADSet(MaxADSet(A)) by Def18;
the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence thesis by A1,Th33,TSEP_1:5;
end;
theorem
for A, B being non empty Subset of Y holds A is Subset of MaxADSspace(
B) implies MaxADSspace(A) is SubSpace of MaxADSspace(B)
proof
let A, B be non empty Subset of Y;
assume
A1: A is Subset of MaxADSspace(B);
A2: the carrier of MaxADSspace(B) = MaxADSet(B) by Def18;
the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence thesis by A2,A1,Lm2,Th34;
end;
theorem
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)
proof
let A, B be non empty Subset of Y;
A1: the carrier of MaxADSspace(B) = MaxADSet(B) by Def18;
A2: the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence B is Subset of MaxADSspace(A) & A is Subset of MaxADSspace(B) implies
the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(B) by A1,Th35,
TSEP_1:5;
assume the TopStruct of MaxADSspace(A) = the TopStruct of MaxADSspace(B);
hence thesis by A2,A1,Th32;
end;
registration
let Y be non trivial TopStruct, A be non trivial Subset of Y;
cluster MaxADSspace(A) -> non trivial;
coherence
proof
MaxADSet(A) is not trivial;
hence thesis by Def18;
end;
end;
registration
let Y be non empty TopStruct, A be non proper Subset of Y;
cluster MaxADSspace(A) -> non proper;
coherence
proof
now
assume
A1: MaxADSspace(A) is proper;
the carrier of MaxADSspace(A) = MaxADSet(A) by Def18;
hence contradiction by A1,TEX_2:8;
end;
hence thesis;
end;
end;
theorem
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
proof
let X0 be open SubSpace of X, A be non empty Subset of X;
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
A1: D is open by TSEP_1:16;
assume A is Subset of X0;
then MaxADSet(A) c= D by A1,Th38;
then the carrier of MaxADSspace(A) c= the carrier of X0 by Def18;
hence thesis by Lm2;
end;
theorem
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
proof
let X0 be closed SubSpace of X, A be non empty Subset of X;
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
A1: D is closed by TSEP_1:11;
assume A is Subset of X0;
then MaxADSet(A) c= D by A1,Th40;
then the carrier of MaxADSspace(A) c= the carrier of X0 by Def18;
hence thesis by Lm2;
end;