:: The Tichonov Theorem
:: by Bart{\l}omiej Skorulski
::
:: Received May 23, 2000
:: Copyright (c) 2000-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, SUBSET_1, CARD_3, RELAT_1, XBOOLE_0, FUNCT_4, TARSKI,
WAYBEL18, WAYBEL_3, PBOOLE, STRUCT_0, RLVECT_2, PRE_TOPC, RCOMP_1,
SETFAM_1, FINSET_1, CANTOR_1, YELLOW_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_7, FINSET_1, PBOOLE, PRALG_1, CARD_3, PRE_TOPC, TOPS_2,
COMPTS_1, CANTOR_1, YELLOW_1, WAYBEL_3, WAYBEL18;
constructors SETFAM_1, FUNCT_7, TOPS_2, COMPTS_1, CANTOR_1, MONOID_0,
WAYBEL18, RELSET_1, FUNCT_4;
registrations SUBSET_1, RELSET_1, FINSET_1, CARD_3, STRUCT_0, PRE_TOPC,
MONOID_0, YELLOW_1, YELLOW_6, WAYBEL18;
requirements SUBSET, BOOLE;
definitions TARSKI, COMPTS_1, XBOOLE_0;
equalities XBOOLE_0, STRUCT_0;
expansions TARSKI, COMPTS_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_7, CARD_3, PRE_TOPC,
TOPS_2, YELLOW_1, WAYBEL_3, WAYBEL_7, YELLOW_6, WAYBEL18, XBOOLE_0,
XBOOLE_1, TOPMETR, PARTFUN1;
schemes CLASSES1, PRE_CIRC, FUNCT_1;
begin ::Some Properties of Products
theorem Th1:
for F being Function, i, xi being set, Ai being Subset of F.i
holds proj(F,i)"({xi}) meets proj(F,i)"Ai implies xi in Ai
proof
let F be Function, i be set, xi be set, Ai be Subset of F.i;
set f = the Element of proj(F,i)"({xi}) /\ proj(F,i)"Ai;
assume
A1: proj(F,i)"({xi}) /\ proj(F,i)"Ai <> {};
then f in proj(F,i)"({xi}) by XBOOLE_0:def 4;
then proj(F,i).f in {xi} by FUNCT_1:def 7;
then
A2: proj(F,i).f = xi by TARSKI:def 1;
f in proj(F,i)"Ai by A1,XBOOLE_0:def 4;
hence thesis by A2,FUNCT_1:def 7;
end;
theorem Th2:
for F,f being Function, i,xi being set st xi in F.i & f in product F
holds f+*(i,xi) in product F
proof
let F,f be Function, i,xi be set;
assume
A1: xi in F.i;
assume
A2: f in product F;
A3: for x being object st x in dom F holds (f+*(i,xi)).x in F.x
proof
let x be object;
assume
A4: x in dom F;
per cases;
suppose
A5: i=x;
thus (f+*(i,xi)).x in F.x
proof
per cases;
suppose
i in dom f;
hence thesis by A1,A5,FUNCT_7:31;
end;
suppose
not i in dom f;
then (f+*(i,xi)) =f by FUNCT_7:def 3;
hence thesis by A2,A4,CARD_3:9;
end;
end;
end;
suppose
i<>x;
then (f+*(i,xi)).x = f.x by FUNCT_7:32;
hence thesis by A2,A4,CARD_3:9;
end;
end;
dom f = dom F by A2,CARD_3:9;
then dom(f+*(i,xi)) = dom F by FUNCT_7:30;
hence thesis by A3,CARD_3:9;
end;
theorem Th3:
for F being Function, i being set st i in dom F holds rng proj(F,i) c= F.i &
(product F <> {} implies rng proj(F,i) = F.i)
proof
let F be Function, i be set;
assume
A1: i in dom F;
thus
A2: rng proj(F,i) c= F.i
proof
let x be object;
assume x in rng proj(F,i);
then consider f9 being object such that
A3: f9 in dom proj(F,i) and
A4: x = proj(F,i).f9 by FUNCT_1:def 3;
f9 in product F by A3;
then consider f being Function such that
A5: f9 = f and
dom f = dom F and
A6: for x being object st x in dom F holds f.x in F.x by CARD_3:def 5;
proj(F,i).f = f.i by A3,A5,CARD_3:def 16;
hence thesis by A1,A4,A5,A6;
end;
assume
A7: product F <> {};
thus rng proj(F,i) c= F.i by A2;
let x be object;
set f9 = the Element of product F;
consider f being Function such that
A8: f9 = f and
A9: dom f = dom F and
for x being object st x in dom F holds f.x in F.x by A7,CARD_3:def 5;
assume x in F.i;
then f+*(i,x)in product F by A7,A8,Th2;
then
A10: f+*(i,x) in dom proj(F,i) by CARD_3:def 16;
(f+*(i,x)).i = x by A1,A9,FUNCT_7:31;
then proj(F,i).(f+*(i,x)) = x by A10,CARD_3:def 16;
hence thesis by A10,FUNCT_1:def 3;
end;
theorem Th4:
for F being Function, i being set st i in dom F holds
proj(F,i)"(F.i) = product F
proof
let F be Function, i be set;
assume
A1: i in dom F;
dom proj(F,i)=product F by CARD_3:def 16;
hence proj(F,i)"(F.i) c= product F by RELAT_1:132;
let f9 be object;
assume
A2: f9 in product F;
then consider f being Function such that
A3: f9 = f and
dom f = dom F and
A4: for x being object st x in dom F holds f.x in F.x by CARD_3:def 5;
A5: f in dom proj(F,i) by A2,A3,CARD_3:def 16;
f.i in F.i by A1,A4;
then proj(F,i).f in F.i by A5,CARD_3:def 16;
hence thesis by A3,A5,FUNCT_1:def 7;
end;
theorem Th5:
for F,f being Function, i,xi being set st xi in F.i & i in dom F
& f in product F holds f+*(i,xi) in proj(F,i)"({xi})
proof
let F,f be Function, i,xi be set;
assume that
A1: xi in F.i and
A2: i in dom F and
A3: f in product F;
(f+*(i,xi))in product F by A1,A3,Th2;
then
A4: (f+*(i,xi))in dom proj(F,i) by CARD_3:def 16;
i in dom f by A2,A3,CARD_3:9;
then (f+*(i,xi)).i = xi by FUNCT_7:31;
then (f+*(i,xi)).i in {xi} by TARSKI:def 1;
then proj(F,i).(f+*(i,xi)) in {xi} by A4,CARD_3:def 16;
hence thesis by A4,FUNCT_1:def 7;
end;
Lm1: for F,g being Function, i1,i2,xi1 being set, Ai2 being Subset of F.i2 st
i1<>i2 & g in product F holds g+*(i1,xi1) in proj(F,i2)"Ai2 implies g in proj(F
,i2)"Ai2
proof
let F,g be Function, i1,i2,xi1 be set, Ai2 be Subset of F.i2;
assume that
A1: i1<>i2 and
A2: g in product F;
A3: g in dom proj(F,i2) by A2,CARD_3:def 16;
assume g+*(i1,xi1) in proj(F,i2)"Ai2;
then g+*(i1,xi1)in dom proj(F,i2) & proj(F,i2).(g+*(i1,xi1)) in Ai2 by
FUNCT_1:def 7;
then (g+*(i1,xi1)).i2 in Ai2 by CARD_3:def 16;
then g.i2 in Ai2 by A1,FUNCT_7:32;
then proj(F,i2).g in Ai2 by A3,CARD_3:def 16;
hence thesis by A3,FUNCT_1:def 7;
end;
theorem Th6:
for F,f being Function, i1,i2,xi1 being set, Ai2 being Subset of
F.i2 st xi1 in F.i1 & f in product F holds i1 <> i2 implies (f in proj(F,i2)"
Ai2 iff f+*(i1,xi1) in proj(F,i2)"Ai2)
proof
let F,f be Function, i1,i2,xi1 be set, Ai2 be Subset of F.i2;
assume that
A1: xi1 in F.i1 and
A2: f in product F;
assume
A3: i1 <> i2;
thus f in proj(F,i2)"Ai2 implies f+*(i1,xi1) in proj(F,i2)"Ai2
proof
A4: (f+*(i1,xi1))+*(i1,f.i1) = f +*(i1,f.i1) by FUNCT_7:34
.= f by FUNCT_7:35;
assume f in proj(F,i2)"Ai2;
hence thesis by A1,A2,A3,A4,Lm1,Th2;
end;
assume f+*(i1,xi1) in proj(F,i2)"Ai2;
hence thesis by A2,A3,Lm1;
end;
theorem Th7:
for F being Function, i1,i2,xi1 being set, Ai2 being Subset of F.
i2 st product F <> {} & xi1 in F.i1 & i1 in dom F & i2 in dom F & Ai2<>F.i2
holds proj(F,i1)"({xi1}) c= proj(F,i2)"Ai2 iff i1 = i2 & xi1 in Ai2
proof
let F be Function, i1,i2,xi1 be set, Ai2 be Subset of F.i2;
assume that
A1: product F <> {} and
A2: xi1 in F.i1 and
A3: i1 in dom F and
A4: i2 in dom F and
A5: Ai2<>F.i2;
set f9 = the Element of product F;
consider f being Function such that
A6: f9 = f and
A7: dom f = dom F and
for x being object st x in dom F holds f.x in F.x by A1,CARD_3:def 5;
not F.i2 c= Ai2 by A5;
then consider xi2 being object such that
A8: xi2 in F.i2 and
A9: not xi2 in Ai2;
reconsider xi2 as Element of F.i2 by A8;
A10: (f+*(i2,xi2)).i2 = xi2 by A4,A7,FUNCT_7:31;
thus proj(F,i1)"({xi1}) c= proj(F,i2)"Ai2 implies i1 = i2 & xi1 in Ai2
proof
assume
A11: proj(F,i1)"({xi1}) c= proj(F,i2)"Ai2;
thus
A12: i1 = i2
proof
assume
A13: i1<>i2;
f+*(i2,xi2) in product F & (f+*(i2,xi2))+*(i1,xi1) in proj(F,i1)"({
xi1}) by A1,A2,A3,A8,A6,Th2,Th5;
then f+*(i2,xi2) in proj(F,i2)"Ai2 by A2,A11,A13,Th6;
then f+*(i2,xi2) in dom proj(F,i2) & proj(F,i2).(f+*(i2,xi2)) in Ai2 by
FUNCT_1:def 7;
hence contradiction by A9,A10,CARD_3:def 16;
end;
xi1 in rng proj(F,i1) by A1,A2,A3,Th3;
then {xi1} c= rng proj(F,i1) by ZFMISC_1:31;
then {xi1} c= Ai2 by A11,A12,FUNCT_1:88;
hence thesis by ZFMISC_1:31;
end;
assume that
A14: i1 = i2 and
A15: xi1 in Ai2;
{xi1} c= Ai2 by A15,ZFMISC_1:31;
hence thesis by A14,RELAT_1:143;
end;
scheme
ElProductEx { I()->non empty set, J()->TopStruct-yielding non-Empty
ManySortedSet of I(), P[object,object] }:
ex f being Element of product J() st for i
being Element of I() holds P[f.i,i]
provided
A1: for i being Element of I() ex x being Element of J().i st P[x,i]
proof
defpred Q[object,object] means
P[$2,$1] & for i9 being Element of I() st $1=i9
holds $2 in the carrier of J().i9;
A2: for i being object st i in I() ex x being object st Q[i, x]
proof
let i be object;
assume i in I();
then reconsider i1=i as Element of I();
consider x being Element of J().i1 such that
A3: P[x,i1] by A1;
take x;
thus P[x,i] by A3;
let i9 be Element of I();
assume i=i9;
hence thesis;
end;
consider f being Function such that
A4: dom f = I() and
A5: for i being object st i in I() holds Q[i, f.i] from CLASSES1:sch 1(A2);
A6: for x being object st x in dom Carrier J() holds f.x in (Carrier J()).x
proof
let x be object;
assume x in dom Carrier J();
then reconsider x9=x as Element of I();
f.x9 in the carrier of J().x9 by A5;
hence thesis by YELLOW_6:2;
end;
dom f = dom Carrier J() by A4,PARTFUN1:def 2;
then f in product(Carrier J()) by A6,CARD_3:9;
then reconsider f as Element of product J() by WAYBEL18:def 3;
take f;
let i be Element of I();
thus thesis by A5;
end;
theorem Th8:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, f being Element of product J holds
proj(J,i).f=f.i
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, f be Element of product J;
f in the carrier of product J;
then f in product (Carrier J) by WAYBEL18:def 3;
then f in dom proj(Carrier J,i) by CARD_3:def 16;
then proj(Carrier J,i).f=f.i by CARD_3:def 16;
hence thesis by WAYBEL18:def 4;
end;
theorem Th9:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, xi being Element of J.i, Ai being
Subset of J.i holds proj(J,i)"({xi}) meets proj(J,i)"Ai implies xi in Ai
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, xi be Element of J.i, Ai be Subset of J.i;
assume proj(J,i)"({xi}) /\ proj(J,i)"Ai <> {};
then proj(Carrier J,i)"({xi}) /\ proj(J,i)"Ai <> {} by WAYBEL18:def 4;
then proj(Carrier J,i)"({xi}) /\ proj(Carrier J,i)"Ai <> {} by WAYBEL18:def 4
;
then
A1: proj(Carrier J,i)"({xi}) meets proj(Carrier J,i)"Ai;
Ai c= the carrier of J.i;
then Ai c= (Carrier J).i by YELLOW_6:2;
hence thesis by A1,Th1;
end;
theorem Th10:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I holds
proj(J,i)"[#](J.i) = [#] product J
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I;
i in I;
then i in dom Carrier J by PARTFUN1:def 2;
then proj(Carrier J,i)"((Carrier J).i) = product Carrier J by Th4;
then proj(Carrier J,i)"((Carrier J).i) = [#] product J by WAYBEL18:def 3;
then proj(Carrier J,i)"[#](J.i) = [#] product J by YELLOW_6:2;
hence thesis by WAYBEL18:def 4;
end;
theorem Th11:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, xi being Element of J.i, f being
Element of product J holds f+*(i,xi) in proj(J,i)"({xi})
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, xi be Element of J.i, f be Element of product J;
xi in the carrier of J.i;
then
A1: xi in (Carrier J).i by YELLOW_6:2;
f in the carrier of product J;
then
A2: f in product (Carrier J) by WAYBEL18:def 3;
i in I;
then i in dom Carrier J by PARTFUN1:def 2;
then f+*(i,xi) in proj(Carrier J,i)"({xi}) by A1,A2,Th5;
hence thesis by WAYBEL18:def 4;
end;
theorem Th12:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i1,i2 being Element of I, xi1 being Element of J.i1, Ai2
being Subset of J.i2 st Ai2<>[#](J.i2) holds proj(J,i1)"({xi1}) c= proj(J,i2)"
Ai2 iff i1 = i2 & xi1 in Ai2
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i1,i2 be Element of I, xi1 be Element of J.i1, Ai2 be Subset of J.i2;
reconsider Ai29=Ai2 as Subset of (Carrier J).i2 by YELLOW_6:2;
i2 in I;
then
A1: i2 in dom Carrier J by PARTFUN1:def 2;
assume Ai2<>[#](J.i2);
then
A2: Ai29 <> (Carrier J).i2 by YELLOW_6:2;
xi1 in the carrier of J.i1;
then
A3: xi1 in (Carrier J).i1 by YELLOW_6:2;
i1 in I;
then product Carrier J <> {} & i1 in dom Carrier J by PARTFUN1:def 2;
then
proj(Carrier J,i1)"({xi1}) c= proj(Carrier J,i2)"Ai29 iff i1 = i2 & xi1
in Ai29 by A1,A3,A2,Th7;
then proj(J,i1)"({xi1}) c= proj(Carrier J,i2)"Ai2 iff i1 = i2 & xi1 in Ai29
by WAYBEL18:def 4;
hence thesis by WAYBEL18:def 4;
end;
theorem Th13:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i1,i2 being Element of I, xi1 being Element of J.i1, Ai2
being Subset of J.i2, f being Element of product J st i1<> i2 holds f in proj(J
,i2)"Ai2 iff f+*(i1,xi1) in proj(J,i2)"Ai2
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i1,i2 be Element of I, xi1 be Element of J.i1, Ai2 be Subset of J.i2, f be
Element of product J;
reconsider Ai29=Ai2 as Subset of (Carrier J).i2 by YELLOW_6:2;
xi1 in the carrier of J.i1;
then
A1: xi1 in (Carrier J).i1 by YELLOW_6:2;
f in the carrier of product J;
then
A2: f in product (Carrier J) by WAYBEL18:def 3;
assume i1<> i2;
then
f in proj(Carrier J,i2)"Ai29 iff f+*(i1,xi1) in proj(Carrier J,i2)" Ai29
by A1,A2,Th6;
hence thesis by WAYBEL18:def 4;
end;
begin
theorem Th14:
for T being non empty TopStruct holds T is compact iff for F
being Subset-Family of T st F is open & [#](T) c= union(F) ex G being
Subset-Family of T st G c= F & [#]T c= union G & G is finite
proof
let T be non empty TopStruct;
thus T is compact implies for F being Subset-Family of T st F is open & [#](
T) c= union(F) ex G being Subset-Family of T st G c= F & [#]T c= union G & G is
finite
proof
assume
A1: T is compact;
let F be Subset-Family of T;
assume that
A2: F is open and
A3: [#](T) c= union(F);
F is Cover of T by A3,TOPMETR:1;
then consider G being Subset-Family of T such that
A4: G c= F & G is Cover of T & G is finite by A1,A2;
take G;
thus thesis by A4,TOPMETR:1;
end;
assume
A5: for F being Subset-Family of T st F is open & [#](T) c= union(F) ex
G being Subset-Family of T st G c= F & [#]T c= union G & G is finite;
let F be Subset-Family of T;
assume that
A6: F is Cover of T and
A7: F is open;
[#](T) c= union(F) by A6,TOPMETR:1;
then consider G being Subset-Family of T such that
A8: G c= F & [#]T c= union G & G is finite by A5,A7;
take G;
thus thesis by A8,TOPMETR:1;
end;
theorem Th15:
for T being non empty TopSpace, B being prebasis of T holds T is
compact iff for F being Subset of B st [#](T) c= union(F) ex G being finite
Subset of F st [#]T c= union G
proof
let T be non empty TopSpace, B be prebasis of T;
set x = the carrier of T;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then reconsider x as Element of InclPoset the topology of T by YELLOW_1:1;
x is compact iff x << x by WAYBEL_3:def 2;
hence thesis by WAYBEL_3:37,WAYBEL_7:31;
end;
begin ::The Tichonov Theorem
theorem Th16:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, A being set st A in product_prebasis J ex i being Element
of I, Ai being Subset of J.i st Ai is open & proj(J,i)"Ai = A
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
A be set;
assume A in product_prebasis J;
then consider i being set, T being TopStruct, Ai being Subset of T such that
A1: i in I and
A2: Ai is open and
A3: T = J.i and
A4: A = product ((Carrier J) +* (i,Ai)) by WAYBEL18:def 2;
reconsider i as Element of I by A1;
reconsider Ai as Subset of J.i by A3;
take i;
take Ai;
thus Ai is open by A2,A3;
thus thesis by A4,WAYBEL18:4;
end;
theorem Th17:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, xi being Element of J.i, A being set
st A in product_prebasis J & proj(J,i)"({xi}) c= A holds A = [#](product J) or
ex Ai being Subset of J.i st Ai <> [#](J.i) & xi in Ai & Ai is open & A=proj(J,
i)"Ai
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, xi be Element of J.i, A be set;
assume A in product_prebasis J;
then consider i1 being Element of I, Ai1 being Subset of J.i1 such that
A1: Ai1 is open and
A2: proj(J,i1)"Ai1 = A by Th16;
assume
A3: proj(J,i)"({xi}) c= A;
assume not A = [#](product J);
then
A4: Ai1 <> [#](J.i1) by A2,Th10;
then reconsider Ai=Ai1 as Subset of J.i by A3,A2,Th12;
take Ai;
thus Ai <> [#](J.i) by A3,A2,A4,Th12;
thus xi in Ai by A3,A2,A4,Th12;
J.i = J.i1 by A3,A2,A4,Th12;
hence Ai is open by A1;
thus thesis by A3,A2,A4,Th12;
end;
theorem Th18:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, Fi being non empty Subset-Family of J
.i st [#](J.i) c= union(Fi) holds [#](product J) c= union the set of all
proj(J,i)"Ai where
Ai is Element of Fi
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, Fi be non empty Subset-Family of J.i;
assume
A1: [#](J.i) c= union(Fi);
let f be object;
assume
A2: f in [#](product J);
then reconsider f9=f as Element of product J;
f9.i in [#](J.i);
then consider Ai0 being set such that
A3: f9.i in Ai0 and
A4: Ai0 in Fi by A1,TARSKI:def 4;
f9 in product Carrier J by A2,WAYBEL18:def 3;
then f9 in dom proj(Carrier J,i) by CARD_3:def 16;
then
A5: f9 in dom proj(J,i) by WAYBEL18:def 4;
reconsider Ai0 as Element of Fi by A4;
proj(J,i).f9 in Ai0 by A3,Th8;
then proj (J,i)"Ai0 in the set of all proj(J,i)"Ai where Ai is Element of Fi
& f9 in proj(J,i)"Ai0 by A5,FUNCT_1:def 7;
hence thesis by TARSKI:def 4;
end;
theorem Th19:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, xi being Element of J.i, G being
Subset of product_prebasis J st proj(J,i)"({xi}) c= union G & (for A being set
st A in product_prebasis J & A in G holds not proj(J,i)"({xi}) c= A) holds [#](
product J) c= union G
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, xi be Element of J.i, G be Subset of product_prebasis J;
assume that
A1: proj(J,i)"({xi}) c= union G and
A2: for A being set st A in product_prebasis J & A in G holds not proj(J
,i)"({xi}) c= A;
let f be object;
assume f in [#](product J);
then reconsider f9=f as Element of product J;
set g = f9+*(i,xi);
A3: g in proj(J,i)"({xi}) by Th11;
then consider Ag being set such that
A4: g in Ag and
A5: Ag in G by A1,TARSKI:def 4;
consider i2 being Element of I, Ai2 being Subset of J.i2 such that
Ai2 is open and
A6: proj(J,i2)"Ai2 = Ag by A5,Th16;
A7: Ai2 <> [#](J.i2)
proof
assume Ai2 = [#](J.i2);
then proj(J,i2)"Ai2 = [#] product J by Th10
.= the carrier of product J;
hence contradiction by A2,A5,A6;
end;
A8: not proj(J,i)"({xi}) c= proj(J,i2)"Ai2 by A2,A5,A6;
i<>i2
proof
assume
A9: i = i2;
then reconsider Ai29=Ai2 as Subset of J.i;
proj(J,i)"({xi}) /\ proj(J,i)"Ai29 <> {} by A3,A4,A6,A9,XBOOLE_0:def 4;
then
A10: proj(J,i)"({xi}) meets proj(J,i)"Ai29;
not xi in Ai2 by A8,A7,A9,Th12;
hence contradiction by A10,Th9;
end;
then f in proj(J,i2)"Ai2 by A4,A6,Th13;
hence thesis by A5,A6,TARSKI:def 4;
end;
theorem Th20:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, F being Subset of product_prebasis J
holds (for G being finite Subset of F holds not [#](product J) c= union G)
implies for xi being Element of J.i, G being finite Subset of F st proj(J,i)"({
xi}) c= union G ex A being set st A in product_prebasis J & A in G & proj(J,i)"
({xi}) c= A
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, F be Subset of product_prebasis J;
assume
A1: for G being finite Subset of F holds not [#](product J) c= union G;
let xi be Element of J.i, G be finite Subset of F;
reconsider G9=G as Subset of product_prebasis J by XBOOLE_1:1;
assume
A2: proj(J,i)"({xi}) c= union G;
assume for A being set st A in product_prebasis J & A in G holds not proj(J
,i)"({xi}) c= A;
then [#](product J) c= union G9 by A2,Th19;
hence contradiction by A1;
end;
theorem Th21:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, F being Subset of product_prebasis J
holds (for G being finite Subset of F holds not [#](product J) c= union G)
implies for xi being Element of J.i, G being finite Subset of F st proj(J,i)"({
xi}) c= union G holds ex Ai being Subset of J.i st Ai <> [#](J.i) & xi in Ai &
proj(J,i)"Ai in G & Ai is open
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, F be Subset of product_prebasis J;
assume
A1: for G being finite Subset of F holds not [#](product J) c= union G;
let xi be Element of J.i, G be finite Subset of F;
assume proj(J,i)"({xi}) c= union G;
then consider A being set such that
A2: A in product_prebasis J and
A3: A in G and
A4: proj(J,i)"({xi}) c= A by A1,Th20;
A <> [#](product J)
proof
reconsider G1 = {A} as finite Subset of F by A3,ZFMISC_1:31;
assume A = [#](product J);
then union G1 = [#](product J) by ZFMISC_1:25;
hence contradiction by A1;
end;
then consider Ai being Subset of J.i such that
A5: Ai <> [#](J.i) and
A6: xi in Ai and
A7: Ai is open and
A8: A=proj(J,i)"Ai by A2,A4,Th17;
take Ai;
thus Ai <> [#](J.i) by A5;
thus xi in Ai by A6;
thus proj(J,i)"Ai in G by A3,A8;
thus thesis by A7;
end;
theorem Th22:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, F being Subset of product_prebasis J
st (for i being Element of I holds J.i is compact) & (for G being finite Subset
of F holds not [#](product J) c= union G) ex xi being Element of J.i st for G
being finite Subset of F holds not proj(J,i)"({xi}) c= union G
proof
defpred P[set] means not contradiction;
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, F be Subset of product_prebasis J;
assume that
A1: for i being Element of I holds J.i is compact and
A2: for G being finite Subset of F holds not [#](product J) c= union G;
deffunc F(set) = proj(J,i)"$1;
defpred P[object,object] means
ex A being set st A = $2 &
$1 in A & proj(J,i)"A in F & for V being Subset
of J.i st V = $2 holds V is open;
assume
A3: for xi being Element of J.i ex G being finite Subset of F st proj(J,
i)"({xi}) c= union G;
A4: for xi being object st xi in the carrier of J.i
ex Ai being object st Ai in bool the carrier of J.i & P[xi, Ai]
proof
let xi be object;
assume xi in the carrier of J.i;
then reconsider xi9=xi as Element of J.i;
consider G being finite Subset of F such that
A5: proj(J,i)"({xi9}) c= union G by A3;
consider Ai being Subset of J.i such that
Ai <> [#](J.i) and
A6: xi in Ai and
A7: proj(J,i)"Ai in G and
A8: Ai is open by A2,A5,Th21;
take Ai;
thus Ai in bool the carrier of J.i;
take Ai;
thus Ai = Ai;
thus xi in Ai by A6;
thus proj(J,i)"Ai in F by A7;
let V be Subset of J.i;
assume V = Ai;
hence thesis by A8;
end;
consider h being Function such that
A9: dom h = the carrier of J.i and
A10: rng h c= bool the carrier of J.i and
A11: for xi being object st xi in the carrier of J.i holds P[xi, h.xi] from
FUNCT_1:sch 6(A4);
reconsider bGip = rng h as Subset-Family of (J.i) by A10;
reconsider bGip as Subset-Family of J.i;
A12: [#](J.i) c= union bGip
proof
let x be object;
assume
A13: x in [#](J.i);
then P[x,h.x] by A11;
then consider A being set such that
A14: A = h.x &
x in A & proj(J,i)"A in F & for V being Subset
of J.i st V = h.x holds V is open;
x in h.x & h.x in bGip by A9,FUNCT_1:def 3,A14,A13;
hence thesis by TARSKI:def 4;
end;
for P being Subset of J.i holds P in bGip implies P is open
proof
let P be Subset of J.i;
assume
P in bGip;
then consider x being object such that
A15: x in dom h & P = h.x by FUNCT_1:def 3;
P[x,h.x] by A9,A11,A15;
hence thesis by A15;
end;
then
A16: bGip is open by TOPS_2:def 1;
J.i is compact by A1;
then consider Gip being Subset-Family of J.i such that
A17: Gip c= bGip and
A18: [#](J.i) c= union Gip and
A19: Gip is finite by A12,A16,Th14;
reconsider Gip as non empty finite Subset-Family of J.i by A18,A19,ZFMISC_1:2
;
set Gp={F(Ai) where Ai is Element of Gip: P[Ai]};
A20: Gp c= F
proof
let A be object;
assume A in Gp;
then consider Ai being Element of Gip such that
A21: A= proj(J,i)"Ai;
Ai in Gip;
then consider x being object such that
A22: x in dom h & h.x = Ai by A17,FUNCT_1:def 3;
P[x,h.x] by A9,A11,A22;
hence thesis by A21,A22;
end;
Gp is finite from PRE_CIRC:sch 1;
then reconsider Gp as finite Subset of F by A20;
[#](product J) c= union Gp by A18,Th18;
hence contradiction by A2;
end;
::$N Tychonoff's theorem
theorem
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I st for i being Element of I holds J.i is compact holds
product J is compact
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I;
assume
A1: for i being Element of I holds J.i is compact;
reconsider B=product_prebasis J as prebasis of product J by WAYBEL18:def 3;
assume not product J is compact;
then consider F being Subset of B such that
A2: [#](product J) c= union(F) and
A3: for G being finite Subset of F holds not [#](product J) c= union G by Th15;
defpred P[set,Element of I] means for G being finite Subset of F holds not
proj(J,$2)"({$1}) c= union G;
A4: for i being Element of I ex xi being Element of J.i st P[xi, i] by A1,A3
,Th22;
consider f being Element of product J such that
A5: for i being Element of I holds P[f.i, i] from ElProductEx(A4);
f in [#](product J);
then consider A being set such that
A6: f in A and
A7: A in F by A2,TARSKI:def 4;
reconsider G = {A} as finite Subset of F by A7,ZFMISC_1:31;
consider i being Element of I, Ai being Subset of J.i such that
Ai is open and
A8: proj(J,i)"Ai = A by A7,Th16;
proj(J,i).f in Ai by A6,A8,FUNCT_1:def 7;
then f.i in Ai by Th8;
then {f.i} c= Ai by ZFMISC_1:31;
then proj(J,i)"({f.i}) c= A by A8,RELAT_1:143;
then proj(J,i)"({f.i}) c= union G by ZFMISC_1:25;
hence contradiction by A5;
end;