:: Maximal Kolmogorov Subspaces of a Topological Space as Stone
:: Retracts of the Ambient Space
:: 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, TEX_4, RCOMP_1, TARSKI, STRUCT_0,
TOPS_1, ZFMISC_1, SETFAM_1, FUNCT_1, RELAT_1, NATTRA_1, ORDINAL2,
BORSUK_1, TSP_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELAT_1, RELSET_1,
FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_2,
TEX_3, TEX_4, TSP_1;
constructors TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_4, TSP_1, TEX_3;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TSP_1;
requirements BOOLE, SUBSET;
equalities SUBSET_1, STRUCT_0, RELAT_1;
expansions SUBSET_1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, BORSUK_1,
TSEP_1, TOPS_3, TEX_2, TEX_3, TEX_4, TSP_1, RELAT_1, XBOOLE_0, XBOOLE_1,
SUBSET_1, RELSET_1;
schemes TEX_2, FUNCT_2;
begin
:: 1. Maximal T_{0} Subsets.
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, definition)
for a, b being Point of X st a in A & b
in A holds a <> b implies MaxADSet(a) misses MaxADSet(b);
compatibility
proof
thus A is T_0 implies for a, b being Point of X st a in A & b in A holds a
<> b implies MaxADSet(a) misses MaxADSet(b)
proof
assume
A1: A is T_0;
let a, b be Point of X;
assume that
A2: a in A and
A3: b in A;
assume
A4: a <> b;
now
per cases by A1,A2,A3,A4,TSP_1:def 8;
suppose
ex V being Subset of X st V is open & a in V & not b in V;
then consider V being Subset of X such that
A5: V is open and
A6: a in V and
A7: not b in V;
now
take V;
thus V is open by A5;
thus MaxADSet(a) c= V by A5,A6,TEX_4:24;
b in [#]X \ V by A7,XBOOLE_0:def 5;
then MaxADSet(b) c= V` by A5,TEX_4:23;
hence V misses MaxADSet(b) by SUBSET_1:23;
end;
hence (ex V being Subset of X st V is open & MaxADSet(a) c= V & V
misses MaxADSet(b)) or ex W being Subset of X st W is open & W misses MaxADSet(
a) & MaxADSet(b) c= W;
end;
suppose
ex W being Subset of X st W is open & not a in W & b in W;
then consider W being Subset of X such that
A8: W is open and
A9: not a in W and
A10: b in W;
now
take W;
thus W is open by A8;
a in [#]X \ W by A9,XBOOLE_0:def 5;
then MaxADSet(a) c= W` by A8,TEX_4:23;
hence W misses MaxADSet(a) by SUBSET_1:23;
thus MaxADSet(b) c= W by A8,A10,TEX_4:24;
end;
hence (ex V being Subset of X st V is open & MaxADSet(a) c= V & V
misses MaxADSet(b)) or ex W being Subset of X st W is open & W misses MaxADSet(
a) & MaxADSet(b) c= W;
end;
end;
hence thesis by TEX_4:53;
end;
assume
A11: for a, b being Point of X st a in A & b in A holds a <> b implies
MaxADSet(a) misses MaxADSet(b);
now
let a, b be Point of X;
assume that
A12: a in A and
A13: b in A;
assume a <> b;
then
A14: MaxADSet(a) misses MaxADSet(b) by A11,A12,A13;
now
per cases by A14,TEX_4:53;
suppose
ex V being Subset of X st V is open & MaxADSet(a) c= V & V
misses MaxADSet(b);
then consider V being Subset of X such that
A15: V is open and
A16: MaxADSet(a) c= V and
A17: V misses MaxADSet(b);
now
take V;
thus V is open by A15;
{a} c= MaxADSet(a) by TEX_4:18;
then a in MaxADSet(a) by ZFMISC_1:31;
hence a in V by A16;
now
{b} c= MaxADSet(b) by TEX_4:18;
then
A18: b in MaxADSet(b) by ZFMISC_1:31;
assume b in V;
hence contradiction by A17,A18,XBOOLE_0:3;
end;
hence not b in V;
end;
hence (ex V being Subset of X st V is open & a in V & not b in V) or
ex W being Subset of X st W is open & not a in W & b in W;
end;
suppose
ex W being Subset of X st W is open & W misses MaxADSet(a)
& MaxADSet(b) c= W;
then consider W being Subset of X such that
A19: W is open and
A20: W misses MaxADSet(a) and
A21: MaxADSet(b) c= W;
now
take W;
thus W is open by A19;
now
{a} c= MaxADSet(a) by TEX_4:18;
then
A22: a in MaxADSet(a) by ZFMISC_1:31;
assume a in W;
hence contradiction by A20,A22,XBOOLE_0:3;
end;
hence not a in W;
{b} c= MaxADSet(b) by TEX_4:18;
then b in MaxADSet(b) by ZFMISC_1:31;
hence b in W by A21;
end;
hence (ex V being Subset of X st V is open & a in V & not b in V) or
ex W being Subset of X st W is open & not a in W & b in W;
end;
end;
hence
(ex V being Subset of X st V is open & a in V & not b in V) or ex W
being Subset of X st W is open & not a in W & b in W;
end;
hence thesis by TSP_1:def 8;
end;
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: redefines T_0 (TSP_2, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, definition)
for a being Point of X st a in A holds A /\ MaxADSet(a) = {a};
compatibility
proof
thus A is T_0 implies for a being Point of X st a in A holds A /\ MaxADSet
(a) = {a}
proof
assume
A1: A is T_0;
let a be Point of X;
assume
A2: a in A;
assume
A3: A /\ MaxADSet(a) <> {a};
{a} c= MaxADSet(a) by TEX_4:18;
then a in MaxADSet(a) by ZFMISC_1:31;
then a in A /\ MaxADSet(a) by A2,XBOOLE_0:def 4;
then consider b being object such that
A4: b in A /\ MaxADSet(a) and
A5: b <> a by A3,ZFMISC_1:35;
reconsider b as Point of X by A4;
b in A by A4,XBOOLE_0:def 4;
then
A6: MaxADSet(a) misses MaxADSet(b) by A1,A2,A5;
b in MaxADSet(a) by A4,XBOOLE_0:def 4;
hence contradiction by A6,TEX_4:21;
end;
assume
A7: for a being Point of X st a in A holds A /\ MaxADSet(a) = {a};
now
let a, b be Point of X;
assume that
A8: a in A and
A9: b in A;
A10: A /\ MaxADSet(a) = {a} by A7,A8;
A11: A /\ MaxADSet(b) = {b} by A7,A9;
assume
A12: a <> b;
assume MaxADSet(a) meets MaxADSet(b);
then {a} = {b} by A10,A11,TEX_4:22;
hence contradiction by A12,ZFMISC_1:3;
end;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: redefines T_0 (TSP_2, redefinition) → T_0 (TSP_2, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, definition)
for a being Point of X st a in A ex D being
Subset of X st D is maximal_anti-discrete & A /\ D = {a};
compatibility
proof
thus A is T_0 implies for a being Point of X st a in A ex D being Subset
of X st D is maximal_anti-discrete & A /\ D = {a}
proof
assume
A1: A is T_0;
let a be Point of X;
assume
A2: a in A;
take D = MaxADSet(a);
thus D is maximal_anti-discrete by TEX_4:20;
thus thesis by A1,A2;
end;
assume
A3: for a being Point of X st a in A ex D being Subset of X st D is
maximal_anti-discrete & A /\ D = {a};
now
let a be Point of X;
assume a in A;
then consider D being Subset of X such that
A4: D is maximal_anti-discrete and
A5: A /\ D = {a} by A3;
a in A /\ D by A5,ZFMISC_1:31;
then a in D by XBOOLE_0:def 4;
hence A /\ MaxADSet(a) = {a} by A4,A5,TEX_4:27;
end;
hence thesis;
end;
end;
definition
let Y be TopStruct;
let IT be Subset of Y;
attr IT is maximal_T_0 means
IT is T_0 & for D being Subset of Y st D is T_0 & 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_T_0 implies D1 is maximal_T_0
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_T_0;
A4: now
let D be Subset of Y1;
reconsider E = D as Subset of Y0 by A1;
assume D is T_0;
then
A5: E is T_0 by A1,TSP_1:3;
assume D1 c= D;
hence D1 = D by A2,A3,A5;
end;
D0 is T_0 by A3;
then D1 is T_0 by A1,A2,TSP_1:3;
hence thesis by A4;
end;
definition
let X be non empty TopSpace;
let M be Subset of X;
redefine attr M is maximal_T_0 means :: redefines maximal_T_0 (TSP_2, definition)
M is T_0 & MaxADSet(M) = the carrier of X;
compatibility
proof
thus M is maximal_T_0 implies M is T_0 & MaxADSet(M) = the carrier of X
proof
assume
A1: M is maximal_T_0;
hence
A2: M is T_0;
the carrier of X c= MaxADSet(M)
proof
assume not the carrier of X c= MaxADSet(M);
then consider x being object such that
A3: x in the carrier of X and
A4: not x in MaxADSet(M) by TARSKI:def 3;
reconsider x as Point of X by A3;
set A = M \/ {x};
for a being Point of X st a in A holds A /\ MaxADSet(a) = {a}
proof
let a be Point of X;
assume a in A;
then
A5: a in M or a in {x} by XBOOLE_0:def 3;
now
per cases by A5,TARSKI:def 1;
suppose
A6: a in M;
{x} /\ MaxADSet(a) = {}
proof
assume {x} /\ MaxADSet(a) <> {};
then {x} meets MaxADSet(a) by XBOOLE_0:def 7;
then
A7: x in MaxADSet(a) by ZFMISC_1:50;
{a} c= M by A6,ZFMISC_1:31;
then MaxADSet({a}) c= MaxADSet(M) by TEX_4:31;
then MaxADSet(a) c= MaxADSet(M) by TEX_4:28;
hence contradiction by A4,A7;
end;
then A /\ MaxADSet(a) = (M /\ MaxADSet(a)) \/ {} by XBOOLE_1:23
.= M /\ MaxADSet(a);
hence thesis by A2,A6;
end;
suppose
A8: a = x;
then
A9: {x} c= MaxADSet(a) by TEX_4:18;
M /\ MaxADSet(a) = {}
proof
A10: M c= MaxADSet(M) by TEX_4:32;
assume M /\ MaxADSet(a) <> {};
then MaxADSet(a) /\ MaxADSet(M) <> {} by A10,XBOOLE_1:3,26;
then MaxADSet(a) meets MaxADSet(M) by XBOOLE_0:def 7;
then
A11: MaxADSet(a) c= MaxADSet(M) by TEX_4:30;
x in MaxADSet(a) by A9,ZFMISC_1:31;
hence contradiction by A4,A11;
end;
then A /\ MaxADSet(a) = {} \/ ({x} /\ MaxADSet(a)) by XBOOLE_1:23
.= {x} /\ MaxADSet(a);
hence thesis by A8,TEX_4:18,XBOOLE_1:28;
end;
end;
hence thesis;
end;
then
A12: A is T_0;
A13: M c= MaxADSet(M) by TEX_4:32;
A14: {x} c= A by XBOOLE_1:7;
M c= A by XBOOLE_1:7;
then M = A by A1,A12;
then x in M by A14,ZFMISC_1:31;
hence contradiction by A4,A13;
end;
hence thesis by XBOOLE_0:def 10;
end;
assume
A15: M is T_0;
assume
A16: MaxADSet(M) = the carrier of X;
for D being Subset of X st D is T_0 & M c= D holds M = D
proof
let D be Subset of X;
assume
A17: D is T_0;
assume
A18: M c= D;
D c= M
proof
assume not D c= M;
then consider x being object such that
A19: x in D and
A20: not x in M by TARSKI:def 3;
A21: x in the carrier of X by A19;
reconsider x as Point of X by A19;
x in union {MaxADSet(a) where a is Point of X : a in M} by A16,A21,
TEX_4:def 11;
then consider C being set such that
A22: x in C and
A23: C in {MaxADSet(a) where a is Point of X : a in M} by TARSKI:def 4;
consider a being Point of X such that
A24: C = MaxADSet(a) and
A25: a in M by A23;
M /\ MaxADSet(x) c= D /\ MaxADSet(x) by A18,XBOOLE_1:26;
then
A26: M /\ MaxADSet(x) c= {x} by A17,A19;
MaxADSet(a) = MaxADSet(x) by A22,A24,TEX_4:21;
then M /\ MaxADSet(x) = {a} by A15,A25;
hence contradiction by A20,A25,A26,ZFMISC_1:18;
end;
hence thesis by A18,XBOOLE_0:def 10;
end;
hence thesis by A15;
end;
end;
reserve X for non empty TopSpace;
theorem Th2:
for M being Subset of X holds M is maximal_T_0 implies M is dense
proof
let M be Subset of X;
assume
A1: M is maximal_T_0;
then MaxADSet(M) = [#]X;
then
A2: Cl MaxADSet(M) = MaxADSet(M) by PRE_TOPC:22;
MaxADSet(M) = the carrier of X by A1;
then Cl M = the carrier of X by A2,TEX_4:62;
hence thesis by TOPS_3:def 2;
end;
theorem Th3:
for A being Subset of X st A is open or A is closed holds A is
maximal_T_0 implies A is not proper
by TEX_4:56,TEX_4:60;
theorem Th4:
for A being empty Subset of X holds A is not maximal_T_0
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 T_0 & A c= C & A <> C by TSP_1:12,XBOOLE_1:2;
end;
hence thesis;
end;
theorem Th5:
for M being Subset of X st M is maximal_T_0 for A being Subset of
X st A is closed holds A = MaxADSet(M /\ A)
proof
let M be Subset of X;
assume
A1: M is maximal_T_0;
let A be Subset of X;
assume
A2: A is closed;
then MaxADSet(M /\ A) = MaxADSet(M) /\ MaxADSet(A) by TEX_4:64;
then
A3: MaxADSet(M /\ A) = MaxADSet(M) /\ A by A2,TEX_4:60;
A = (the carrier of X) /\ A by XBOOLE_1:28;
hence thesis by A1,A3;
end;
theorem Th6:
for M being Subset of X st M is maximal_T_0 for A being Subset of
X st A is open holds A = MaxADSet(M /\ A)
proof
let M be Subset of X;
assume
A1: M is maximal_T_0;
let A be Subset of X;
assume
A2: A is open;
then MaxADSet(M /\ A) = MaxADSet(M) /\ MaxADSet(A) by TEX_4:65;
then
A3: MaxADSet(M /\ A) = MaxADSet(M) /\ A by A2,TEX_4:56;
A = (the carrier of X) /\ A by XBOOLE_1:28;
hence thesis by A1,A3;
end;
theorem
for M being Subset of X st M is maximal_T_0 for A being Subset of X
holds Cl A = MaxADSet(M /\ Cl A) by Th5;
theorem
for M being Subset of X st M is maximal_T_0 for A being Subset of X
holds Int A = MaxADSet(M /\ Int A) by Th6;
definition
let X be non empty TopSpace;
let M be Subset of X;
redefine attr M is maximal_T_0 means :: redefines maximal_T_0 (TSP_2, redefinition) → maximal_T_0 (TSP_2, definition)
for x being Point of X ex a
being Point of X st a in M & M /\ MaxADSet(x) = {a};
compatibility
proof
thus M is maximal_T_0 implies for x being Point of X ex a being Point of X
st a in M & M /\ MaxADSet(x) = {a}
proof
assume
A1: M is maximal_T_0;
then
A2: M is T_0;
let x be Point of X;
x in MaxADSet(M) by A1;
then x in union {MaxADSet(a) where a is Point of X : a in M} by
TEX_4:def 11;
then consider C being set such that
A3: x in C and
A4: C in {MaxADSet(a) where a is Point of X : a in M} by TARSKI:def 4;
consider a being Point of X such that
A5: C = MaxADSet(a) and
A6: a in M by A4;
MaxADSet(a) = MaxADSet(x) by A3,A5,TEX_4:21;
then M /\ MaxADSet(x) = {a} by A2,A6;
hence thesis by A6;
end;
assume
A7: for x being Point of X ex a being Point of X st a in M & M /\
MaxADSet(x) = {a};
now
let x be object;
A8: M c= MaxADSet(M) by TEX_4:32;
assume x in the carrier of X;
then reconsider y = x as Point of X;
consider a being Point of X such that
A9: a in M and
A10: M /\ MaxADSet(y) = {a} by A7;
{a} c= MaxADSet(y) by A10,XBOOLE_1:17;
then a in MaxADSet(y) by ZFMISC_1:31;
then MaxADSet(y) /\ MaxADSet(M) <> {} by A9,A8,XBOOLE_0:def 4;
then MaxADSet(y) meets MaxADSet(M) by XBOOLE_0:def 7;
then
A11: MaxADSet(y) c= MaxADSet(M) by TEX_4:30;
{y} c= MaxADSet(y) by TEX_4:18;
then y in MaxADSet(y) by ZFMISC_1:31;
hence x in MaxADSet(M) by A11;
end;
then the carrier of X c= MaxADSet(M) by TARSKI:def 3;
then
A12: MaxADSet(M) = the carrier of X by XBOOLE_0:def 10;
for b being Point of X st b in M holds M /\ MaxADSet(b) = {b}
proof
let b be Point of X;
A13: ex a being Point of X st a in M & M /\ MaxADSet(b) = {a} by A7;
{b} c= MaxADSet(b) by TEX_4:18;
then
A14: b in MaxADSet(b) by ZFMISC_1:31;
assume b in M;
then b in M /\ MaxADSet(b) by A14,XBOOLE_0:def 4;
hence thesis by A13,TARSKI:def 1;
end;
then M is T_0;
hence thesis by A12;
end;
end;
theorem Th9:
for A being Subset of X holds A is T_0 implies ex M being Subset
of X st A c= M & M is maximal_T_0
proof
let A be Subset of X;
set D = [#]X \ MaxADSet(A);
set F = {MaxADSet(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 = MaxADSet(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 T_0;
defpred X[Subset of X,set] means $2 in D & $2 in $1;
A2: D = (MaxADSet(A))`;
then
A3: MaxADSet(A) misses D by SUBSET_1:24;
A c= MaxADSet(A) by TEX_4:32;
then A misses D by A2,SUBSET_1:24;
then
A4: A /\ D = {} by XBOOLE_0:def 7;
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 = MaxADSet(d) and
A7: d in D;
take d;
{d} c= MaxADSet(d) by TEX_4: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 TEX_2:sch 1(
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 f.: F c= D by TARSKI:def 3;
then
A9: MaxADSet(A) misses (f.:F) by A3,XBOOLE_1:63;
thus ex M being Subset of X st A c= M & M is maximal_T_0
proof
take M;
thus
A10: A c= M by XBOOLE_1:7;
for x being Point of X ex a being Point of X st a in M & M /\
MaxADSet(x) = {a}
proof
let x be Point of X;
A11: [#]X = MaxADSet(A) \/ D by XBOOLE_1:45;
now
per cases by A11,XBOOLE_0:def 3;
suppose
A12: x in MaxADSet(A);
now
{x} c= MaxADSet(A) by A12,ZFMISC_1:31;
then MaxADSet({x}) c= MaxADSet(A) by TEX_4:34;
then MaxADSet(x) c= MaxADSet(A) by TEX_4:28;
then (f.: F) misses MaxADSet(x) by A9,XBOOLE_1:63;
then (f.: F) /\ MaxADSet(x) = {} by XBOOLE_0:def 7;
then
A13: M /\ MaxADSet(x) = (A /\ MaxADSet(x)) \/ {} by XBOOLE_1:23;
x in union {MaxADSet(a) where a is Point of X : a in A} by A12,
TEX_4:def 11;
then consider C being set such that
A14: x in C and
A15: C in {MaxADSet(a) where a is Point of X : a in A} by TARSKI:def 4;
consider a being Point of X such that
A16: C = MaxADSet(a) and
A17: a in A by A15;
take a;
thus a in M by A10,A17;
MaxADSet(a) = MaxADSet(x) by A14,A16,TEX_4:21;
hence M /\ MaxADSet(x) = {a} by A1,A17,A13;
end;
hence thesis;
end;
suppose
A18: x in D;
then
A19: MaxADSet(x) in F;
now
reconsider a = f.(MaxADSet(x)) as Point of X by A19,FUNCT_2:5;
take a;
A20: f.: F c= M by XBOOLE_1:7;
now
let y be object;
assume
A21: y in M /\ MaxADSet(x);
then reconsider z = y as Point of X;
A22: z in M by A21,XBOOLE_0:def 4;
A23: z in MaxADSet(x) by A21,XBOOLE_0:def 4;
then
A24: MaxADSet(z) = MaxADSet(x) by TEX_4:21;
now
assume not MaxADSet(x) c= D;
then MaxADSet(x) meets MaxADSet(A) by A2,SUBSET_1:23;
then
A25: MaxADSet(x) c= MaxADSet(A) by TEX_4:30;
{x} c= MaxADSet(x) by TEX_4:18;
then x in MaxADSet(x) by ZFMISC_1:31;
hence contradiction by A3,A18,A25,XBOOLE_0:3;
end;
then not z in A by A4,A23,XBOOLE_0:def 4;
then z in f.: F by A22,XBOOLE_0:def 3;
then consider C being object such that
A26: C in F and
C in F and
A27: z = f.C by FUNCT_2:64;
reconsider C as Subset of X by A26;
consider w being Point of X such that
A28: C = MaxADSet(w) and
w in D by A26;
z in MaxADSet(w) by A8,A26,A27,A28;
then f.(MaxADSet(w)) = a by A24,TEX_4:21;
hence y in {a} by A27,A28,TARSKI:def 1;
end;
then
A29: M /\ MaxADSet(x) c= {a} by TARSKI:def 3;
A30: a in f.: F by A19,FUNCT_2:35;
hence a in M by A20;
a in MaxADSet(x) by A8,A19;
then
A31: {a} c= MaxADSet(x) by ZFMISC_1:31;
{a} c= M by A20,A30,ZFMISC_1:31;
then {a} c= M /\ MaxADSet(x) by A31,XBOOLE_1:19;
hence M /\ MaxADSet(x) = {a} by A29,XBOOLE_0:def 10;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence M is maximal_T_0;
end;
end;
theorem Th10:
ex M being Subset of X st M is maximal_T_0
proof
set A = {}X;
A is discrete by TEX_2:29;
then consider M being Subset of X such that
A c= M and
A1: M is maximal_T_0 by Th9,TSP_1:9;
take M;
thus thesis by A1;
end;
begin
:: 2. Maximal Kolmogorov Subspaces.
definition
let Y be non empty TopStruct;
let IT be SubSpace of Y;
attr IT is maximal_T_0 means
for A being Subset of Y st A = the carrier of IT holds A is maximal_T_0;
end;
theorem Th11:
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_T_0 iff Y0 is
maximal_T_0;
Lm1: now
let Z be non empty 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;
registration
let Y be non empty TopStruct;
cluster maximal_T_0 -> T_0 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_T_0;
then A is maximal_T_0;
then A is T_0;
hence thesis by TSP_1:13;
end;
cluster non T_0 -> non maximal_T_0 for non empty SubSpace of Y;
coherence;
end;
definition
let X be non empty TopSpace;
let X0 be non empty SubSpace of X;
redefine attr X0 is maximal_T_0 means :: redefines maximal_T_0 (TSP_2, definition)
X0 is T_0 & for Y0 being T_0 non empty
SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct
of Y0;
compatibility
proof
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus X0 is maximal_T_0 implies X0 is T_0 & for Y0 being T_0 non empty
SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct
of Y0
proof
assume X0 is maximal_T_0;
then
A1: A is maximal_T_0;
then A is T_0;
hence X0 is T_0 by TSP_1:13;
thus for Y0 being T_0 non empty SubSpace of X st X0 is SubSpace of Y0
holds the TopStruct of X0 = the TopStruct of Y0
proof
let Y0 be T_0 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 T_0 by TSP_1:13;
then A = D by A1,A2;
hence thesis by TSEP_1:5;
end;
end;
assume X0 is T_0;
then
A3: A is T_0 by TSP_1:13;
assume
A4: for Y0 being T_0 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 T_0;
assume
A6: A c= D;
then D <> {};
then consider Y0 being T_0 strict non empty SubSpace of X such that
A7: D = the carrier of Y0 by A5,TSP_1:18;
X0 is SubSpace of Y0 by A6,A7,TSEP_1:4;
hence A = D by A4,A7;
end;
then A is maximal_T_0 by A3;
hence thesis;
end;
end;
reserve X for non empty TopSpace;
theorem Th12:
for A0 being non empty Subset of X st A0 is maximal_T_0 ex X0
being strict non empty SubSpace of X st X0 is maximal_T_0 & A0 = the carrier of
X0
proof
let A0 be non empty Subset of X;
assume
A1: A0 is maximal_T_0;
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 non empty TopSpace;
cluster maximal_T_0 -> dense for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is maximal_T_0;
then A is maximal_T_0;
then A is dense by Th2;
hence thesis by TEX_3:9;
end;
cluster non dense -> non maximal_T_0 for SubSpace of X;
coherence;
cluster open maximal_T_0 -> non proper for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is open;
then
A1: A is open by TSEP_1:16;
assume X0 is maximal_T_0;
then A is maximal_T_0;
then A is non proper by A1,Th3;
hence thesis by TEX_2:8;
end;
cluster open proper -> non maximal_T_0 for SubSpace of X;
coherence;
cluster proper maximal_T_0 -> non open for SubSpace of X;
coherence;
cluster closed maximal_T_0 -> non proper for SubSpace of X;
coherence
proof
let X0 be SubSpace of X;
reconsider A = the carrier of X0 as Subset of X by Lm1;
assume X0 is closed;
then
A2: A is closed by TSEP_1:11;
assume X0 is maximal_T_0;
then A is maximal_T_0;
then A is non proper by A2,Th3;
hence thesis by TEX_2:8;
end;
cluster closed proper -> non maximal_T_0 for SubSpace of X;
coherence;
cluster proper maximal_T_0 -> non closed for SubSpace of X;
coherence;
end;
theorem
for Y0 being T_0 non empty SubSpace of X ex X0 being strict SubSpace
of X st Y0 is SubSpace of X0 & X0 is maximal_T_0
proof
let Y0 be T_0 non empty SubSpace of X;
reconsider A = the carrier of Y0 as Subset of X by Lm1;
A is T_0 by TSP_1:13;
then consider M being Subset of X such that
A1: A c= M and
A2: M is maximal_T_0 by Th9;
M is non empty by A2,Th4;
then consider X0 being strict non empty SubSpace of X such that
A3: X0 is maximal_T_0 and
A4: M = the carrier of X0 by A2,Th12;
take X0;
thus thesis by A1,A3,A4,TSEP_1:4;
end;
registration
let X be non empty TopSpace;
cluster maximal_T_0 strict non empty for SubSpace of X;
existence
proof
consider M being Subset of X such that
A1: M is maximal_T_0 by Th10;
M is non empty by A1,Th4;
then consider X0 being strict non empty SubSpace of X such that
A2: X0 is maximal_T_0 and
M = the carrier of X0 by A1,Th12;
take X0;
thus thesis by A2;
end;
end;
definition
let X be non empty TopSpace;
mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X;
end;
theorem Th14:
for X0 being maximal_Kolmogorov_subspace of X for G being Subset
of X, G0 being Subset of X0 st G0 = G holds G0 is open iff MaxADSet(G) is open
& G0 = MaxADSet(G) /\ the carrier of X0
proof
let X0 be maximal_Kolmogorov_subspace of X;
let G be Subset of X, G0 be Subset of X0;
reconsider M = the carrier of X0 as Subset of X by Lm1;
assume
A1: G0 = G;
A2: M is maximal_T_0 by Th11;
thus G0 is open implies MaxADSet(G) is open & G0 = MaxADSet(G) /\ the
carrier of X0
proof
assume G0 is open;
then
A3: ex H being Subset of X st H is open & G0 = H /\ M by TSP_1:def 1;
hence MaxADSet(G) is open by A2,A1,Th6;
thus thesis by A2,A1,A3,Th6;
end;
assume
A4: MaxADSet(G) is open;
assume G0 = MaxADSet(G) /\ the carrier of X0;
hence thesis by A4,TSP_1:def 1;
end;
theorem
for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X
holds G is open iff G = MaxADSet(G) & ex G0 being Subset of X0 st G0 is open &
G0 = G /\ the carrier of X0
proof
let X0 be maximal_Kolmogorov_subspace of X;
let G be Subset of X;
reconsider M = the carrier of X0 as Subset of X by Lm1;
thus G is open implies G = MaxADSet(G) & ex G0 being Subset of X0 st G0 is
open & G0 = G /\ the carrier of X0
proof
reconsider G0 = G /\ M as Subset of X0 by XBOOLE_1:17;
reconsider G0 as Subset of X0;
assume
A1: G is open;
hence G = MaxADSet(G) by TEX_4:56;
take G0;
thus G0 is open by A1,TSP_1:def 1;
thus thesis;
end;
assume
A2: G = MaxADSet(G);
given G0 being Subset of X0 such that
A3: G0 is open and
A4: G0 = G /\ the carrier of X0;
set E = G0;
E c= M;
then reconsider E as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet(G) by A2,A4,XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
for x being object st x in G holds x in MaxADSet(E)
proof
let x be object;
assume
A7: x in G;
then reconsider a = x as Point of X;
consider b being Point of X such that
A8: b in M and
A9: M /\ MaxADSet(a) = {b} by A6;
A10: {b} c= MaxADSet(a) by A9,XBOOLE_1:17;
{a} c= G by A7,ZFMISC_1:31;
then MaxADSet({a}) c= G by A2,TEX_4:34;
then MaxADSet(a) c= G by TEX_4:28;
then {b} c= G by A10,XBOOLE_1:1;
then b in G by ZFMISC_1:31;
then b in E by A4,A8,XBOOLE_0:def 4;
then {b} c= E by ZFMISC_1:31;
then MaxADSet({b}) c= MaxADSet(E) by TEX_4:31;
then
A11: MaxADSet(b) c= MaxADSet(E) by TEX_4:28;
b in MaxADSet(a) by A10,ZFMISC_1:31;
then MaxADSet(b) = MaxADSet(a) by TEX_4:21;
then {a} c= MaxADSet(b) by TEX_4:18;
then a in MaxADSet(b) by ZFMISC_1:31;
hence thesis by A11;
end;
then
A12: G c= MaxADSet(E) by TARSKI:def 3;
MaxADSet(E) is open by A3,Th14;
hence thesis by A2,A5,A12,TEX_4:35;
end;
theorem Th16:
for X0 being maximal_Kolmogorov_subspace of X for F being Subset
of X, F0 being Subset of X0 st F0 = F holds F0 is closed iff MaxADSet(F) is
closed & F0 = MaxADSet(F) /\ the carrier of X0
proof
let X0 be maximal_Kolmogorov_subspace of X;
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
let F be Subset of X, F0 be Subset of X0;
assume
A1: F0 = F;
A2: M is maximal_T_0 by Th11;
thus F0 is closed implies MaxADSet(F) is closed & F0 = MaxADSet(F) /\ the
carrier of X0
proof
assume F0 is closed;
then
A3: ex H being Subset of X st H is closed & F0 = H /\ M by TSP_1:def 2;
hence MaxADSet(F) is closed by A2,A1,Th5;
thus thesis by A2,A1,A3,Th5;
end;
assume
A4: MaxADSet(F) is closed;
assume F0 = MaxADSet(F) /\ the carrier of X0;
hence thesis by A4,TSP_1:def 2;
end;
theorem
for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X
holds F is closed iff F = MaxADSet(F) & ex F0 being Subset of X0 st F0 is
closed & F0 = F /\ the carrier of X0
proof
let X0 be maximal_Kolmogorov_subspace of X;
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
let F be Subset of X;
thus F is closed implies F = MaxADSet(F) & ex F0 being Subset of X0 st F0 is
closed & F0 = F /\ the carrier of X0
proof
set F0 = F /\ M;
reconsider F0 as Subset of X0 by XBOOLE_1:17;
assume
A1: F is closed;
hence F = MaxADSet(F) by TEX_4:60;
take F0;
thus F0 is closed by A1,TSP_1:def 2;
thus thesis;
end;
assume
A2: F = MaxADSet(F);
given F0 being Subset of X0 such that
A3: F0 is closed and
A4: F0 = F /\ the carrier of X0;
set E = F0;
E c= M;
then reconsider E as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet(F) by A2,A4,XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
for x being object st x in F holds x in MaxADSet(E)
proof
let x be object;
assume
A7: x in F;
then reconsider a = x as Point of X;
consider b being Point of X such that
A8: b in M and
A9: M /\ MaxADSet(a) = {b} by A6;
A10: {b} c= MaxADSet(a) by A9,XBOOLE_1:17;
{a} c= F by A7,ZFMISC_1:31;
then MaxADSet({a}) c= F by A2,TEX_4:34;
then MaxADSet(a) c= F by TEX_4:28;
then {b} c= F by A10,XBOOLE_1:1;
then b in F by ZFMISC_1:31;
then b in E by A4,A8,XBOOLE_0:def 4;
then {b} c= E by ZFMISC_1:31;
then MaxADSet({b}) c= MaxADSet(E) by TEX_4:31;
then
A11: MaxADSet(b) c= MaxADSet(E) by TEX_4:28;
b in MaxADSet(a) by A10,ZFMISC_1:31;
then MaxADSet(b) = MaxADSet(a) by TEX_4:21;
then {a} c= MaxADSet(b) by TEX_4:18;
then a in MaxADSet(b) by ZFMISC_1:31;
hence thesis by A11;
end;
then
A12: F c= MaxADSet(E) by TARSKI:def 3;
MaxADSet(E) is closed by A3,Th16;
hence thesis by A2,A5,A12,TEX_4:35;
end;
begin
:: 3. Stone Retraction Mapping Theorems.
reserve X for non empty TopSpace,
X0 for non empty maximal_Kolmogorov_subspace of X;
theorem Th18:
for r being Function of X,X0 for M being Subset of X st M = the
carrier of X0 holds (for a being Point of X holds M /\ MaxADSet(a) = {r.a})
implies r is continuous Function of X,X0
proof
let r be Function of X,X0;
let M be Subset of X;
assume
A1: M = the carrier of X0;
reconsider N = M as Subset of X;
assume
A2: for a being Point of X holds M /\ MaxADSet(a) = {r.a};
A3: N is maximal_T_0 by A1,Th11;
then
A4: N is T_0;
for F being Subset of X0 holds F is closed implies r" F is closed
proof
let F be Subset of X0;
reconsider E = F as Subset of X by A1,XBOOLE_1:1;
set R = {MaxADSet(a) where a is Point of X : a in E};
now
let x be object;
assume
A5: x in r" F;
then reconsider b = x as Point of X;
A6: r.b in F by A5,FUNCT_2:38;
E c= the carrier of X;
then reconsider a = r.b as Point of X by A6;
MaxADSet(a) in R by A6;
then
A7: MaxADSet(a) c= union R by ZFMISC_1:74;
M /\ MaxADSet(b) = {a} by A2;
then a in M /\ MaxADSet(b) by ZFMISC_1:31;
then a in MaxADSet(b) by XBOOLE_0:def 4;
then
A8: MaxADSet(a) = MaxADSet(b) by TEX_4:21;
A9: {b} c= MaxADSet(b) by TEX_4:18;
b in {b} by TARSKI:def 1;
then b in MaxADSet(a) by A8,A9;
hence x in union R by A7;
end;
then
A10: r" F c= union R by TARSKI:def 3;
assume F is closed;
then ex P being Subset of X st P is closed & P /\ [#]X0 = F by PRE_TOPC:13;
then
A11: MaxADSet(E) is closed by A1,A3,Th5;
now
let C be set;
assume C in R;
then consider a being Point of X such that
A12: C = MaxADSet(a) and
A13: a in E;
now
let x be object;
assume
A14: x in C;
then reconsider b = x as Point of X by A12;
A15: M /\ MaxADSet(b) = {r.b} by A2;
A16: M /\ MaxADSet(a) = {a} by A1,A4,A13;
MaxADSet(a) = MaxADSet(b) by A12,A14,TEX_4:21;
then a = r.x by A16,A15,ZFMISC_1:3;
hence x in r" F by A12,A13,A14,FUNCT_2:38;
end;
hence C c= r" F by TARSKI:def 3;
end;
then
A17: union R c= r" F by ZFMISC_1:76;
union R = MaxADSet(E) by TEX_4:def 11;
hence thesis by A11,A17,A10,XBOOLE_0:def 10;
end;
hence thesis by PRE_TOPC:def 6;
end;
theorem
for r being Function of X,X0 holds (for a being Point of X holds r.a
in MaxADSet(a)) implies r is continuous Function of X,X0
proof
let r be Function of X,X0;
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
assume
A1: for a being Point of X holds r.a in MaxADSet(a);
M is maximal_T_0 by Th11;
then
A2: M is T_0;
A3: M c= the carrier of X;
for a being Point of X holds M /\ MaxADSet(a) = {r.a}
proof
let a be Point of X;
reconsider s = r.a as Point of X by A3,TARSKI:def 3;
A4: s in MaxADSet(a) by A1;
M /\ MaxADSet(s) = {s} by A2;
hence thesis by A4,TEX_4:21;
end;
hence thesis by Th18;
end;
theorem Th20:
for r being continuous Function of X,X0 for M being Subset of X
st M = the carrier of X0 holds (for a being Point of X holds M /\ MaxADSet(a) =
{r.a}) implies r is being_a_retraction
proof
let r be continuous Function of X,X0;
let M be Subset of X;
reconsider N = M as Subset of X;
assume
A1: M = the carrier of X0;
then N is maximal_T_0 by Th11;
then
A2: N is T_0;
assume
A3: for a being Point of X holds M /\ MaxADSet(a) = {r.a};
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
A4: M /\ MaxADSet(x) = {x} by A1,A2;
M /\ MaxADSet(x) = {r.x} by A3;
hence thesis by A4,ZFMISC_1:3;
end;
hence thesis by BORSUK_1:def 16;
end;
theorem Th21:
for r being continuous Function of X,X0 holds (for a being Point
of X holds r.a in MaxADSet(a)) implies r is being_a_retraction
proof
let r be continuous Function of X,X0;
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
assume
A1: for a being Point of X holds r.a in MaxADSet(a);
M is maximal_T_0 by Th11;
then
A2: M is T_0;
A3: M c= the carrier of X;
for a being Point of X holds M /\ MaxADSet(a) = {r.a}
proof
let a be Point of X;
reconsider s = r.a as Point of X by A3,TARSKI:def 3;
A4: s in MaxADSet(a) by A1;
M /\ MaxADSet(s) = {s} by A2;
hence thesis by A4,TEX_4:21;
end;
hence thesis by Th20;
end;
theorem Th22:
ex r being continuous Function of X,X0 st r is being_a_retraction
proof
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
defpred X[Point of X,set] means M /\ MaxADSet $1 = {$2};
A1: M is maximal_T_0 by Th11;
A2: 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
A3: a in M and
A4: M /\ MaxADSet(x) = {a} by A1;
reconsider a as Point of X0 by A3;
take a;
thus thesis by A4;
end;
consider r being Function of X,X0 such that
A5: for x being Point of X holds X[x,r.x] from FUNCT_2:sch 3(A2);
reconsider r as continuous Function of X,X0 by A5,Th18;
take r;
thus thesis by A5,Th20;
end;
theorem
X0 is_a_retract_of X
proof
ex r being continuous Function of X,X0 st r is being_a_retraction by Th22;
hence thesis by BORSUK_1:def 17;
end;
Lm2: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for a being Point of X, b being Point of X0 st a = b holds r" Cl {b} =
Cl {a}
proof
let r be continuous Function of X,X0;
assume
A1: r is being_a_retraction;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X, b be Point of X0;
A2: b in {b} by TARSKI:def 1;
assume
A3: a = b;
then r.a = b by A1,BORSUK_1:def 16;
then
A4: a in r" {b} by A2,FUNCT_2:38;
A5: A is maximal_T_0 by Th11;
A6: r" Cl {b} c= Cl {a}
proof
assume not r" Cl {b} c= Cl {a};
then consider c being object such that
A7: c in r" Cl {b} and
A8: not c in Cl {a} by TARSKI:def 3;
reconsider c as Point of X by A7;
consider d being Point of X such that
A9: d in A and
A10: A /\ MaxADSet(c) = {d} by A5;
A11: {d} c= MaxADSet(c) by A10,XBOOLE_1:17;
r" Cl {b} is closed by PRE_TOPC:def 6;
then MaxADSet(c) c= r" Cl {b} by A7,TEX_4:23;
then {d} c= r" Cl {b} by A11,XBOOLE_1:1;
then
A12: d in r" Cl {b} by ZFMISC_1:31;
reconsider e = d as Point of X0 by A9;
{c} c= MaxADSet(c) by TEX_4:18;
then
A13: c in MaxADSet(c) by ZFMISC_1:31;
A14: Cl {b} c= Cl {a} by A3,TOPS_3:53;
r.d = e by A1,BORSUK_1:def 16;
then e in Cl {b} by A12,FUNCT_2:38;
then
A15: MaxADSet(d) c= Cl {a} by A14,TEX_4:23;
d in MaxADSet(c) by A11,ZFMISC_1:31;
then MaxADSet(d) = MaxADSet(c) by TEX_4:21;
hence contradiction by A8,A13,A15;
end;
A16: r" Cl {b} is closed by PRE_TOPC:def 6;
r" {b} c= r" Cl {b} by PRE_TOPC:18,RELAT_1:143;
then {a} c= r" Cl {b} by A4,ZFMISC_1:31;
then Cl {a} c= r" Cl {b} by A16,TOPS_1:5;
hence thesis by A6,XBOOLE_0:def 10;
end;
Lm3: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for A being Subset of X st A = the carrier of X0 for a being Point of X
holds A /\ MaxADSet(a) = {r.a}
proof
let r be continuous Function of X,X0;
assume
A1: r is being_a_retraction;
let A be Subset of X;
reconsider N = A as Subset of X;
assume
A2: A = the carrier of X0;
let a be Point of X;
A3: N is maximal_T_0 by A2,Th11;
then consider c being Point of X such that
A4: c in A and
A5: A /\ MaxADSet(a) = {c};
A6: {c} c= MaxADSet(c) by TEX_4:18;
r.a in A by A2;
then reconsider d = r.a as Point of X;
{r.a} c= Cl {r.a} by PRE_TOPC:18;
then
A7: r.a in Cl {r.a} by ZFMISC_1:31;
{c} c= MaxADSet(a) by A5,XBOOLE_1:17;
then c in MaxADSet(a) by ZFMISC_1:31;
then
A8: MaxADSet(c) = MaxADSet(a) by TEX_4:21;
reconsider b = c as Point of X0 by A2,A4;
A9: {a} c= MaxADSet(a) by TEX_4:18;
A10: r" Cl {b} = Cl {c} by A1,Lm2;
then {c} c= r" Cl {b} by PRE_TOPC:18;
then c in r" Cl {b} by ZFMISC_1:31;
then MaxADSet(a) c= r" Cl {b} by A10,A8,TEX_4:23;
then {a} c= r" Cl {b} by A9,XBOOLE_1:1;
then a in r" Cl {b} by ZFMISC_1:31;
then
A11: r.a in Cl {b} by FUNCT_2:38;
r" Cl {r.a} = Cl {d} by A1,Lm2;
then a in Cl {d} by A7,FUNCT_2:38;
then MaxADSet(c) c= Cl {d} by A8,TEX_4:23;
then {c} c= Cl {d} by A6,XBOOLE_1:1;
then
A12: Cl {c} c= Cl {d} by TOPS_1:5;
Cl {b} c= Cl {c} by TOPS_3:53;
then {d} c= Cl {c} by A11,ZFMISC_1:31;
then Cl {d} c= Cl {c} by TOPS_1:5;
then Cl {d} = Cl {c} by A12,XBOOLE_0:def 10;
then
A13: MaxADSet(d) = MaxADSet(a) by A8,TEX_4:49;
N is T_0 by A3;
hence thesis by A2,A13;
end;
Lm4: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for a being Point of X, b being Point of X0 st a = b holds MaxADSet(a)
c= r" {b}
proof
let r be continuous Function of X,X0;
assume
A1: r is being_a_retraction;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X, b be Point of X0;
assume
A2: a = b;
assume not MaxADSet(a) c= r" {b};
then consider s being object such that
A3: s in MaxADSet(a) and
A4: not s in r" {b} by TARSKI:def 3;
reconsider s as Point of X by A3;
A5: MaxADSet(a) = MaxADSet(s) by A3,TEX_4:21;
A6: {s} c= MaxADSet(s) by TEX_4:18;
A7: r" Cl {b} = Cl {a} by A1,A2,Lm2;
then {a} c= r" Cl {b} by PRE_TOPC:18;
then a in r" Cl {b} by ZFMISC_1:31;
then MaxADSet(s) c= r" Cl {b} by A7,A5,TEX_4:23;
then {s} c= r" Cl {b} by A6,XBOOLE_1:1;
then s in r" Cl {b} by ZFMISC_1:31;
then
A8: r.s in Cl {b} by FUNCT_2:38;
A c= the carrier of X;
then reconsider d = r.s as Point of X by TARSKI:def 3;
{r.s} c= Cl {r.s} by PRE_TOPC:18;
then
A9: r.s in Cl {r.s} by ZFMISC_1:31;
A10: {a} c= MaxADSet(a) by TEX_4:18;
r" Cl {r.s} = Cl {d} by A1,Lm2;
then s in Cl {d} by A9,FUNCT_2:38;
then MaxADSet(a) c= Cl {d} by A5,TEX_4:23;
then {a} c= Cl {d} by A10,XBOOLE_1:1;
then
A11: Cl {a} c= Cl {d} by TOPS_1:5;
Cl {b} c= Cl {a} by A2,TOPS_3:53;
then {d} c= Cl {a} by A8,ZFMISC_1:31;
then Cl {d} c= Cl {a} by TOPS_1:5;
then Cl {d} = Cl {a} by A11,XBOOLE_0:def 10;
then
A12: MaxADSet(d) = MaxADSet(a) by TEX_4:49;
A is maximal_T_0 by Th11;
then
A13: A is T_0;
r.a = b by A1,A2,BORSUK_1:def 16;
then A /\ MaxADSet(a) = {b} by A1,Lm3;
then {b} = {r.s} by A13,A12;
then r.s in {b} by ZFMISC_1:31;
hence contradiction by A4,FUNCT_2:38;
end;
Lm5: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for a being Point of X, b being Point of X0 st a = b holds r" {b} =
MaxADSet(a)
proof
let r be continuous Function of X,X0;
assume
A1: r is being_a_retraction;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X, b be Point of X0;
assume
A2: a = b;
A3: r" {b} c= MaxADSet(a)
proof
assume not r" {b} c= MaxADSet(a);
then consider s being object such that
A4: s in r" {b} and
A5: not s in MaxADSet(a) by TARSKI:def 3;
reconsider s as Point of X by A4;
r.s in {b} by A4,FUNCT_2:38;
then {r.s} c= {b} by ZFMISC_1:31;
then {r.s} = {b} by ZFMISC_1:18;
then A /\ MaxADSet(s) = {b} by A1,Lm3;
then {a} c= MaxADSet(s) by A2,XBOOLE_1:17;
then a in MaxADSet(s) by ZFMISC_1:31;
then
A6: MaxADSet(s) = MaxADSet(a) by TEX_4:21;
{s} c= MaxADSet(s) by TEX_4:18;
hence contradiction by A5,A6,ZFMISC_1:31;
end;
MaxADSet(a) c= r" {b} by A1,A2,Lm4;
hence thesis by A3,XBOOLE_0:def 10;
end;
Lm6: for r being continuous Function of X,X0 holds r is being_a_retraction
implies for E being Subset of X, F being Subset of X0 st F = E holds r" F =
MaxADSet(E)
proof
let r be continuous Function of X,X0;
assume
A1: r is being_a_retraction;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let E be Subset of X, F be Subset of X0;
set R = {MaxADSet(a) where a is Point of X : a in E};
assume
A2: F = E;
now
let x be object;
assume
A3: x in r" F;
then reconsider b = x as Point of X;
A4: r.b in F by A3,FUNCT_2:38;
then reconsider a = r.b as Point of X by A2;
MaxADSet(a) in R by A2,A4;
then
A5: MaxADSet(a) c= union R by ZFMISC_1:74;
A /\ MaxADSet(b) = {a} by A1,Lm3;
then a in A /\ MaxADSet(b) by ZFMISC_1:31;
then a in MaxADSet(b) by XBOOLE_0:def 4;
then
A6: MaxADSet(a) = MaxADSet(b) by TEX_4:21;
{b} c= MaxADSet(b) by TEX_4:18;
then b in MaxADSet(a) by A6,ZFMISC_1:31;
hence x in union R by A5;
end;
then
A7: r" F c= union R by TARSKI:def 3;
A is maximal_T_0 by Th11;
then
A8: A is T_0;
now
let C be set;
assume C in R;
then consider a being Point of X such that
A9: C = MaxADSet(a) and
A10: a in E;
now
let x be object;
assume
A11: x in C;
then reconsider b = x as Point of X by A9;
A12: A /\ MaxADSet(b) = {r.b} by A1,Lm3;
A13: A /\ MaxADSet(a) = {a} by A2,A8,A10;
MaxADSet(a) = MaxADSet(b) by A9,A11,TEX_4:21;
then a = r.x by A13,A12,ZFMISC_1:3;
hence x in r" F by A2,A9,A10,A11,FUNCT_2:38;
end;
hence C c= r" F by TARSKI:def 3;
end;
then
A14: union R c= r" F by ZFMISC_1:76;
MaxADSet(E) = union R by TEX_4:def 11;
hence thesis by A14,A7,XBOOLE_0:def 10;
end;
definition
let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
X;
func Stone-retraction(X,X0) -> continuous Function of X,X0 means
:Def9:
it is being_a_retraction;
existence by Th22;
uniqueness
proof
reconsider M = the carrier of X0 as non empty Subset of X by TSEP_1:1;
let r1, r2 be continuous Function of X,X0;
assume that
A1: r1 is being_a_retraction and
A2: r2 is being_a_retraction;
for x being object st x in the carrier of X holds r1.x = r2.x
proof
let x be object;
assume x in the carrier of X;
then reconsider a = x as Point of X;
A3: M /\ MaxADSet(a) = {r2.a} by A2,Lm3;
M /\ MaxADSet(a) = {r1.a} by A1,Lm3;
hence thesis by A3,ZFMISC_1:3;
end;
hence r1 = r2 by FUNCT_2:12;
end;
end;
theorem
for a being Point of X, b being Point of X0 st a = b holds (
Stone-retraction(X,X0))" Cl {b} = Cl {a}
by Def9,Lm2;
theorem Th25:
for a being Point of X, b being Point of X0 st a = b holds (
Stone-retraction(X,X0))" {b} = MaxADSet(a)
by Def9,Lm5;
theorem Th26:
for E being Subset of X, F being Subset of X0 st F = E holds (
Stone-retraction(X,X0))" (F) = MaxADSet(E)
by Def9,Lm6;
definition
let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
X;
redefine func Stone-retraction(X,X0) means :: redefines Stone-retraction (TSP_2, definition)
:
Def10: for
M being Subset of X st M = the carrier of X0 for a being Point of X
holds M /\ MaxADSet(a) = {it.a};
compatibility
proof
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
let r be continuous Function of X,X0;
thus r = Stone-retraction(X,X0) implies for M being Subset of X st M = the
carrier of X0 for a being Point of X holds M /\ MaxADSet(a) = {r.a}
by Def9,Lm3;
assume for A being Subset of X st A = the carrier of X0 for a being Point
of X holds A /\ MaxADSet(a) = {r.a};
then for a being Point of X holds M /\ MaxADSet(a) = {r.a};
then r is being_a_retraction by Th20;
hence r = Stone-retraction(X,X0) by Def9;
end;
end;
definition
let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
X;
redefine func Stone-retraction(X,X0) means :: redefines Stone-retraction (TSP_2, redefinition) → Stone-retraction (TSP_2, definition)
:
Def11: for a being Point of X holds it.a in MaxADSet(a);
compatibility
proof
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let r be continuous Function of X,X0;
thus r = Stone-retraction(X,X0) implies for a being Point of X holds r.a
in MaxADSet(a)
proof
assume
A1: r = Stone-retraction(X,X0);
let a be Point of X;
A /\ MaxADSet(a) = {r.a} by A1,Def10;
then {r.a} c= MaxADSet(a) by XBOOLE_1:17;
hence thesis by ZFMISC_1:31;
end;
assume for a being Point of X holds r.a in MaxADSet(a);
then r is being_a_retraction by Th21;
hence r = Stone-retraction(X,X0) by Def9;
end;
end;
theorem Th27:
for a being Point of X holds (Stone-retraction(X,X0))" {(
Stone-retraction(X,X0)).a} = MaxADSet(a)
proof
let a be Point of X;
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction(X,X0);
r.a in A;
then reconsider b = r.a as Point of X;
A1: r.a in MaxADSet(a) by Def11;
r" {r.a} = MaxADSet(b) by Th25;
hence thesis by A1,TEX_4:21;
end;
theorem
for a being Point of X holds Im(Stone-retraction(X,X0),a) = (
Stone-retraction(X,X0)).: MaxADSet(a)
proof
let a be Point of X;
set r = Stone-retraction(X,X0);
A1: dom r = [#]X by FUNCT_2:def 1;
A2: r.: r" {r.a} c= {r.a} by FUNCT_1:75;
A3: r"{r.a} = MaxADSet(a) by Th27;
then r.: r" {r.a} <> {} by A1,RELAT_1:119;
then r.: r" {r.a} = {r.a} by A2,ZFMISC_1:33;
hence thesis by A1,A3,FUNCT_1:59;
end;
definition
let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of
X;
redefine func Stone-retraction(X,X0) means :: redefines Stone-retraction (TSP_2, redefinition) → Stone-retraction (TSP_2, redefinition) → Stone-retraction (TSP_2, definition)
:
Def12: for
M being Subset of X st M = the carrier of X0 for A being Subset of X
holds M /\ MaxADSet(A) = it.: A;
compatibility
proof
let r be continuous Function of X,X0;
thus r = Stone-retraction(X,X0) implies for M being Subset of X st M = the
carrier of X0 for A being Subset of X holds M /\ MaxADSet(A) = r.: A
proof
assume
A1: r = Stone-retraction(X,X0);
let M be Subset of X;
reconsider N = M as Subset of X;
assume
A2: M = the carrier of X0;
let A be Subset of X;
N is maximal_T_0 by A2,Th11;
then
A3: N is T_0;
for x being object st x in M /\ MaxADSet(A) holds x in r.: A
proof
let x be object;
assume
A4: x in M /\ MaxADSet(A);
then reconsider c = x as Point of X;
c in M by A4,XBOOLE_0:def 4;
then
A5: M /\ MaxADSet(c) = {c} by A3;
c in MaxADSet(A) by A4,XBOOLE_0:def 4;
then c in union {MaxADSet(a) where a is Point of X : a in A} by
TEX_4:def 11;
then consider D being set such that
A6: c in D and
A7: D in {MaxADSet(a) where a is Point of X : a in A} by TARSKI:def 4;
consider a being Point of X such that
A8: D = MaxADSet(a) and
A9: a in A by A7;
MaxADSet(c) = MaxADSet(a) by A6,A8,TEX_4:21;
then {r.a} = {c} by A1,A2,A5,Def10;
hence thesis by A9,FUNCT_2:35,ZFMISC_1:3;
end;
then
A10: M /\ MaxADSet(A) c= r.: A by TARSKI:def 3;
for x being object st x in r.: A holds x in M /\ MaxADSet(A)
proof
let x be object;
assume
A11: x in r.: A;
then reconsider b = x as Point of X0;
consider a being object such that
A12: a in the carrier of X and
A13: a in A and
A14: b = r.a by A11,FUNCT_2:64;
reconsider a as Point of X by A12;
{a} c= A by A13,ZFMISC_1:31;
then MaxADSet({a}) c= MaxADSet(A) by TEX_4:31;
then MaxADSet(a) c= MaxADSet(A) by TEX_4:28;
then
A15: M /\ MaxADSet(a) c= M /\ MaxADSet(A) by XBOOLE_1:26;
M /\ MaxADSet(a) = {b} by A1,A2,A14,Def10;
hence thesis by A15,ZFMISC_1:31;
end;
then r.: A c= M /\ MaxADSet(A) by TARSKI:def 3;
hence thesis by A10,XBOOLE_0:def 10;
end;
assume
A16: for M being Subset of X st M = the carrier of X0 for A being
Subset of X holds M /\ MaxADSet(A) = r.: A;
A17: dom r = [#]X by FUNCT_2:def 1;
for M being Subset of X st M = the carrier of X0 for a being Point of
X holds M /\ MaxADSet(a) = {r.a}
proof
let M be Subset of X;
assume
A18: M = the carrier of X0;
let a be Point of X;
M /\ MaxADSet({a}) = Im(r,a) by A16,A18;
then M /\ MaxADSet(a) = Im(r,a) by TEX_4:28;
hence thesis by A17,FUNCT_1:59;
end;
hence r = Stone-retraction(X,X0) by Def10;
end;
end;
theorem Th29:
for A being Subset of X holds (Stone-retraction(X,X0))"((
Stone-retraction(X,X0)).: A) = MaxADSet(A)
proof
let A be Subset of X;
reconsider C = the carrier of X0 as non empty Subset of X by TSEP_1:1;
set r = Stone-retraction(X,X0);
C c= the carrier of X;
then reconsider B = r.: A as Subset of X by XBOOLE_1:1;
C /\ MaxADSet(A) = B by Def12;
then
A1: B c= MaxADSet(A) by XBOOLE_1:17;
A2: r" (r.: A) = MaxADSet(B) by Th26;
then A c= MaxADSet(B) by FUNCT_2:42;
hence thesis by A2,A1,TEX_4:35;
end;
theorem
for A being Subset of X holds (Stone-retraction(X,X0)).: A = (
Stone-retraction(X,X0)).: MaxADSet(A)
proof
let A be Subset of X;
set r = Stone-retraction(X,X0);
A1: rng r = r.: the carrier of X by RELSET_1:22;
r.: r" (r.: A) = r.: MaxADSet(A) by Th29;
hence thesis by A1,FUNCT_1:77,RELAT_1:123;
end;
theorem
for A, B being Subset of X holds (Stone-retraction(X,X0)).:(A \/ B) =
(Stone-retraction(X,X0)).:(A) \/ (Stone-retraction(X,X0)).:(B)
proof
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction(X,X0);
let A, B be Subset of X;
r.: (A \/ B) = M /\ (MaxADSet(A \/ B)) by Def12
.= M /\ (MaxADSet(A) \/ MaxADSet(B)) by TEX_4:36
.= (M /\ MaxADSet(A)) \/ (M /\ MaxADSet(B)) by XBOOLE_1:23
.= (r.: A) \/ (M /\ MaxADSet(B)) by Def12
.= (r.: A) \/ (r.: B) by Def12;
hence thesis;
end;
theorem
for A, B being Subset of X st A is open or B is open holds (
Stone-retraction(X,X0)).:(A /\ B) = (Stone-retraction(X,X0)).:(A) /\ (
Stone-retraction(X,X0)).:(B)
proof
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction(X,X0);
let A, B be Subset of X;
assume
A1: A is open or B is open;
r.: (A /\ B) = M /\ (MaxADSet(A /\ B)) by Def12
.= (M /\ M) /\ (MaxADSet(A) /\ MaxADSet(B)) by A1,TEX_4:65
.= M /\ (M /\ (MaxADSet(A) /\ MaxADSet(B))) by XBOOLE_1:16
.= ((M /\ MaxADSet(A)) /\ MaxADSet(B)) /\ M by XBOOLE_1:16
.= (M /\ MaxADSet(A)) /\ (M /\ MaxADSet(B)) by XBOOLE_1:16
.= (r.: A) /\ (M /\ MaxADSet(B)) by Def12
.= (r.: A) /\ (r.: B) by Def12;
hence thesis;
end;
theorem
for A, B being Subset of X st A is closed or B is closed holds (
Stone-retraction(X,X0)).:(A /\ B) = (Stone-retraction(X,X0)).:(A) /\ (
Stone-retraction(X,X0)).:(B)
proof
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction(X,X0);
let A, B be Subset of X;
assume
A1: A is closed or B is closed;
r.: (A /\ B) = M /\ (MaxADSet(A /\ B)) by Def12
.= (M /\ M) /\ (MaxADSet(A) /\ MaxADSet(B)) by A1,TEX_4:64
.= M /\ (M /\ (MaxADSet(A) /\ MaxADSet(B))) by XBOOLE_1:16
.= ((M /\ MaxADSet(A)) /\ MaxADSet(B)) /\ M by XBOOLE_1:16
.= (M /\ MaxADSet(A)) /\ (M /\ MaxADSet(B)) by XBOOLE_1:16
.= (r.: A) /\ (M /\ MaxADSet(B)) by Def12
.= (r.: A) /\ (r.: B) by Def12;
hence thesis;
end;
theorem
for A being Subset of X holds A is open implies (Stone-retraction(X,X0
)).:(A) is open
proof
let A be Subset of X;
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set B = (Stone-retraction(X,X0)).:(A);
assume
A1: A is open;
then A = MaxADSet(A) by TEX_4:56;
then A /\ M = B by Def12;
hence thesis by A1,TSP_1:def 1;
end;
theorem
for A being Subset of X holds A is closed implies (Stone-retraction(X,
X0)).:(A) is closed
proof
let A be Subset of X;
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set B = (Stone-retraction(X,X0)).:(A);
assume
A1: A is closed;
then A = MaxADSet(A) by TEX_4:60;
then A /\ M = B by Def12;
hence thesis by A1,TSP_1:def 2;
end;