Copyright (c) 2000 Association of Mizar Users
environ
vocabulary FUNCT_1, BORSUK_1, RELAT_1, BOOLE, CARD_3, FUNCT_4, WAYBEL18,
WAYBEL_3, PBOOLE, RLVECT_2, SUBSET_1, PRE_TOPC, SETFAM_1, TARSKI,
COMPTS_1, FINSET_1, CANTOR_1, YELLOW_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
FUNCT_7, FINSET_1, PBOOLE, PRALG_1, PRALG_3, CARD_3, PRE_TOPC, TOPS_2,
COMPTS_1, CANTOR_1, YELLOW_1, WAYBEL_3, WAYBEL18;
constructors FUNCT_7, PRALG_3, TOPS_2, COMPTS_1, CANTOR_1, WAYBEL18;
clusters SUBSET_1, STRUCT_0, RELSET_1, WAYBEL_7, YELLOW_6, FINSET_1, PRALG_1,
PRE_TOPC, CANTOR_1, YELLOW_1, WAYBEL18, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, COMPTS_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_7, PRALG_3, CARD_3, PBOOLE,
PRE_TOPC, TOPS_2, COMPTS_1, YELLOW_1, WAYBEL_3, WAYBEL_7, YELLOW_6,
WAYBEL18, SETFAM_1, XBOOLE_0, XBOOLE_1, TOPMETR;
schemes ZFREFLE1, PRE_CIRC, COMPTS_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;
assume
A1: proj(F,i)"({xi}) /\ proj(F,i)"Ai <> {};
consider f being Element of proj(F,i)"({xi}) /\ proj(F,i)"Ai;
A2: f in proj(F,i)"({xi}) & f in proj(F,i)"Ai by A1,XBOOLE_0:def 3;
then proj(F,i).f in {xi} by FUNCT_1:def 13;
then proj(F,i).f = xi by TARSKI:def 1;
hence xi in Ai by A2,FUNCT_1:def 13;
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;
then dom f = dom F & for x being set st x in dom F holds f.x in
F.x by CARD_3:18;
then A3:
dom(f+*(i,xi)) = dom F by FUNCT_7:32;
for x being set st x in dom F holds (f+*(i,xi)).x in F.x
proof
let x be set;
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:33;
suppose not i in dom f;
then (f+*(i,xi)) =f by FUNCT_7:def 3;
hence thesis by A2,A4,CARD_3:18;
end;
suppose i<>x;
then (f+*(i,xi)).x = f.x by FUNCT_7:34;
hence (f+*(i,xi)).x in F.x by A2,A4,CARD_3:18;
end;
hence thesis by A3,CARD_3:18;
end;
theorem Th3:
for F being Function,
i being set st i in dom F & product F <> {} holds
rng proj(F,i) = F.i
proof
let F be Function,
i be set;
assume that
A1: i in dom F and
A2: product F <> {};
thus rng proj(F,i) c= F.i
proof
let x be set;
assume x in rng proj(F,i);
then consider f' being set such that
A3: f' in dom proj(F,i) and
A4: x = proj(F,i).f' by FUNCT_1:def 5;
f' in product F by A3,PRALG_3:def 2;
then consider f being Function such that
A5: f' = f and
dom f = dom F and
A6: for x being set 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,PRALG_3:def 2;
hence x in F.i by A1,A4,A5,A6;
end;
let x be set;
consider f' being Element of product F;
consider f being Function such that
A7: f' = f and
A8: dom f = dom F and
for x being set st x in dom F holds f.x in F.x by A2,CARD_3:def 5;
assume x in F.i;
then f+*(i,x)in product F by A2,A7,Th2;
then A9: f+*(i,x) in dom proj(F,i) by PRALG_3:def 2;
(f+*(i,x)).i = x by A1,A8,FUNCT_7:33;
then proj(F,i).(f+*(i,x)) = x by A9,PRALG_3:def 2;
hence x in rng proj(F,i) by A9,FUNCT_1:def 5;
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 PRALG_3:def 2;
hence proj(F,i)"(F.i) c= product F by RELAT_1:167;
let f' be set;
assume
A2: f' in product F;
then consider f being Function such that
A3: f' = f and
dom f = dom F and
A4: for x being set 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,PRALG_3:def 2;
f.i in F.i by A1,A4;
then proj(F,i).f in F.i by A5,PRALG_3:def 2;
hence f' in proj(F,i)"(F.i) by A3,A5,FUNCT_1:def 13;
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 PRALG_3:def 2;
i in dom f by A2,A3,CARD_3:18;
then (f+*(i,xi)).i = xi by FUNCT_7:33;
then (f+*(i,xi)).i in {xi} by TARSKI:def 1;
then proj(F,i).(f+*(i,xi)) in {xi} by A4,PRALG_3:def 2;
hence f+*(i,xi) in proj(F,i)"({xi}) by A4,FUNCT_1:def 13;
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,PRALG_3:def 2;
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 13;
then (g+*(i1,xi1)).i2 in Ai2 by PRALG_3:def 2;
then g.i2 in Ai2 by A1,FUNCT_7:34;
then proj(F,i2).g in Ai2 by A3,PRALG_3:def 2;
hence g in proj(F,i2)"Ai2 by A3,FUNCT_1:def 13;
end;
theorem Th6:
for F,f being Function,
i1,i2,xi1 being set,
Ai2 being Subset of F.i2
st xi1 in F.i1 & i1 in dom F & 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
i1 in dom F 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
assume
A4: f in proj(F,i2)"Ai2;
A5: (f+*(i1,xi1))+*(i1,f.i1) = f +*(i1,f.i1) by FUNCT_7:36
.= f by FUNCT_7:37;
f+*(i1,xi1) in product F by A1,A2,Th2;
hence f+*(i1,xi1) in proj(F,i2)"Ai2 by A3,A4,A5,Lm1;
end;
assume f+*(i1,xi1) in proj(F,i2)"Ai2;
hence f in proj(F,i2)"Ai2 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 <> {} & xi1 in F.i1 and
A2: i1 in dom F and
A3: i2 in dom F and
A4: Ai2<>F.i2;
not F.i2 c= Ai2 by A4,XBOOLE_0:def 10;
then consider xi2 being set such that
A5: xi2 in F.i2 and
A6: not xi2 in Ai2 by TARSKI:def 3;
reconsider xi2 as Element of F.i2 by A5;
consider f' being Element of product F;
consider f being Function such that
A7: f' = f and
A8: dom f = dom F and
for x being set st x in dom F holds f.x in F.x by A1,CARD_3:def 5;
A9: (f+*(i2,xi2)).i2 = xi2 by A3,A8,FUNCT_7:33;
thus proj(F,i1)"({xi1}) c= proj(F,i2)"Ai2 implies (i1 = i2 & xi1 in Ai2)
proof
assume
A10: proj(F,i1)"({xi1}) c= proj(F,i2)"Ai2;
thus
A11: i1 = i2
proof
assume
A12: i1<>i2;
A13: f+*(i2,xi2) in product F by A1,A5,A7,Th2;
then (f+*(i2,xi2))+*(i1,xi1) in proj(F,i1)"({xi1}) by A1,A2,Th5;
then f+*(i2,xi2) in proj(F,i2)"Ai2 by A1,A2,A10,A12,A13,Th6;
then f+*(i2,xi2) in dom proj(F,i2) & proj(F,i2).(f+*(i2,xi2)) in Ai2
by FUNCT_1:def 13;
hence contradiction by A6,A9,PRALG_3:def 2;
end;
xi1 in rng proj(F,i1) by A1,A2,Th3;
then {xi1} c= rng proj(F,i1) by ZFMISC_1:37;
then {xi1} c= Ai2 by A10,A11,FUNCT_1:158;
hence xi1 in Ai2 by ZFMISC_1:37;
end;
assume that
A14: i1 = i2 and
A15: xi1 in Ai2;
{xi1} c= Ai2 by A15,ZFMISC_1:37;
hence proj(F,i1)"({xi1}) c= proj(F,i2)"Ai2 by A14,RELAT_1:178;
end;
scheme ElProductEx { I()->non empty set,
J()->TopSpace-yielding non-Empty ManySortedSet of I(),
P[set,set] }:
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[set,set] means P[$2,$1] &
for i' being Element of I() st $1=i' holds $2 in the carrier of J().i';
A2:
for i being set st i in I() ex x being set st Q[i, x]
proof
let i be set;
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 i' be Element of I();
assume i=i';
hence x in the carrier of J().i';
end;
consider f being Function such that
A4: dom f = I() and
A5: for i being set st i in I() holds Q[i, f.i] from NonUniqFuncEx(A2);
A6: dom f = dom Carrier J() by A4,PBOOLE:def 3;
for x being set st x in dom Carrier J() holds f.x in (Carrier J()).x
proof
let x be set;
assume x in dom Carrier J();
then reconsider x'=x as Element of I() by PBOOLE:def 3;
f.x' in the carrier of J().x' by A5;
hence f.x in (Carrier J()).x by YELLOW_6:9;
end;
then f in product(Carrier J()) by A6,CARD_3:18;
then f in the carrier of product J() by WAYBEL18:def 3;
then reconsider f as Element of product J();
take f;
let i be Element of I();
thus P[f.i,i] by A5;
end;
theorem Th8:
for I being non empty set,
J being TopSpace-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 TopSpace-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 PRALG_3:def 2;
then proj(Carrier J,i).f=f.i by PRALG_3:def 2;
hence proj(J,i).f=f.i by WAYBEL18:def 4;
end;
theorem Th9:
for I being non empty set,
J being TopSpace-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 TopSpace-yielding non-Empty ManySortedSet of I,
i be Element of I,
xi be Element of J.i,
Ai be Subset of J.i;
Ai c= the carrier of J.i;
then A1: Ai c= (Carrier J).i by YELLOW_6:9;
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 proj(Carrier J,i)"({xi}) meets
proj(Carrier J,i)"Ai by XBOOLE_0:def 7;
hence xi in Ai by A1,Th1;
end;
theorem Th10:
for I being non empty set,
J being TopSpace-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 TopSpace-yielding non-Empty ManySortedSet of I,
i be Element of I;
i in I;
then i in dom Carrier J by PBOOLE:def 3;
then proj(Carrier J,i)"((Carrier J).i) = product Carrier J by Th4;
then proj(Carrier J,i)"((Carrier J).i) = the carrier of product J
by WAYBEL18:def 3;
then proj(Carrier J,i)"((Carrier J).i) = [#] product J by PRE_TOPC:12;
then proj(Carrier J,i)"(the carrier of J.i) = [#] product J by YELLOW_6:9;
then proj(Carrier J,i)"[#](J.i) = [#] product J by PRE_TOPC:12;
hence proj(J,i)"[#](J.i) = [#] product J by WAYBEL18:def 4;
end;
theorem Th11:
for I being non empty set,
J being TopSpace-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 TopSpace-yielding non-Empty ManySortedSet of I,
i be Element of I,
xi be Element of J.i,
f be Element of product J;
i in I;
then A1: i in dom Carrier J by PBOOLE:def 3;
reconsider xi'=xi as Element of (Carrier J).i by YELLOW_6:9;
f in the carrier of product J;
then f in product (Carrier J) by WAYBEL18:def 3;
then f+*(i,xi') in proj(Carrier J,i)"({xi'}) by A1,Th5;
hence f+*(i,xi) in proj(J,i)"({xi}) by WAYBEL18:def 4;
end;
theorem Th12:
for I being non empty set,
J being TopSpace-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 TopSpace-yielding non-Empty ManySortedSet of I,
i1,i2 be Element of I,
xi1 be Element of J.i1,
Ai2 be Subset of J.i2;
A1:
product Carrier J <> {};
i1 in I;
then A2: i1 in dom Carrier J by PBOOLE:def 3;
i2 in I;
then A3: i2 in dom Carrier J by PBOOLE:def 3;
assume
A4: Ai2<>[#](J.i2);
reconsider xi1'=xi1 as Element of (Carrier J).i1 by YELLOW_6:9;
reconsider Ai2'=Ai2 as Subset of (Carrier J).i2 by YELLOW_6:9;
Ai2<>the carrier of (J.i2) by A4,PRE_TOPC:12;
then Ai2' <> (Carrier J).i2 by YELLOW_6:9;
then proj(Carrier J,i1)"({xi1'}) c= proj(Carrier J,i2)"Ai2' iff
(i1 = i2 & xi1' in Ai2') by A1,A2,A3,Th7;
then proj(J,i1)"({xi1}) c= proj(Carrier J,i2)"Ai2 iff
(i1 = i2 & xi1' in Ai2') by WAYBEL18:def 4;
hence proj(J,i1)"({xi1}) c= proj(J,i2)"Ai2 iff (i1 = i2 & xi1 in Ai2)
by WAYBEL18:def 4;
end;
theorem Th13:
for I being non empty set,
J being TopSpace-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 TopSpace-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;
i1 in I;
then A1: i1 in dom Carrier J by PBOOLE:def 3;
assume
A2: i1<> i2;
reconsider xi1'=xi1 as Element of (Carrier J).i1 by YELLOW_6:9;
reconsider Ai2'=Ai2 as Subset of (Carrier J).i2 by YELLOW_6:9;
f in the carrier of product J;
then f in product (Carrier J) by WAYBEL18:def 3;
then f in proj(Carrier J,i2)"Ai2' iff f+*(i1,xi1') in proj(Carrier J,i2)"
Ai2'
by A1,A2,Th6;
hence f in proj(J,i2)"Ai2 iff f+*(i1,xi1) in
proj(J,i2)"Ai2 by WAYBEL18:def 4;
end;
begin
canceled;
theorem Th15:
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);
the carrier of T c= union(F) by A3,PRE_TOPC:12;
then F is_a_cover_of T by TOPMETR:1;
then consider G being Subset-Family of T such that
A4: G c= F and
A5: G is_a_cover_of T and
A6: G is finite by A1,A2,COMPTS_1:def 3;
take G;
the carrier of T c= union G by A5,TOPMETR:1;
hence G c= F & [#]T c= union G & G is finite by A4,A6,PRE_TOPC:12;
end;
assume
A7: (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
A8: F is_a_cover_of T and
A9: F is open;
the carrier of T c= union F by A8,TOPMETR:1;
then [#](T) c= union(F) by PRE_TOPC:12;
then consider G being Subset-Family of T such that
A10: G c= F and
A11: [#]T c= union G and
A12: G is finite by A7,A9;
take G;
the carrier of T c= union G by A11,PRE_TOPC:12;
hence G c= F & G is_a_cover_of T & G is finite by A10,A12,TOPMETR:1;
end;
theorem ::Alexander's Lemma
Th16:
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 x in the carrier of InclPoset the topology of T by YELLOW_1:1;
then reconsider x as Element of InclPoset the topology of T
;
A1:
x = [#]T by PRE_TOPC:12;
x is compact iff x << x by WAYBEL_3:def 2;
hence 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
by A1,WAYBEL_3:37,WAYBEL_7:35;
end;
begin ::The Tichonov Theorem
theorem Th17:
for I being non empty set,
J being TopSpace-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 TopSpace-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;
take i;
reconsider Ai as Subset of J.i by A3;
take Ai;
thus Ai is open by A2,A3;
thus proj(J,i)"Ai = A by A4,WAYBEL18:5;
end;
theorem Th18:
for I being non empty set,
J being TopSpace-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 TopSpace-yielding non-Empty ManySortedSet of I,
i be Element of I,
xi be Element of J.i,
A be set;
assume
A1: A in product_prebasis J;
assume
A2: proj(J,i)"({xi}) c= A;
assume
A3: not A = [#](product J);
consider i1 being Element of I, Ai1 being Subset of J.i1 such that
A4: Ai1 is open and
A5: proj(J,i1)"Ai1 = A by A1,Th17;
A6:
Ai1 <> [#](J.i1) by A3,A5,Th10;
then A7: J.i = J.i1 by A2,A5,Th12;
reconsider Ai=Ai1 as Subset of J.i by A2,A5,A6,Th12;
take Ai;
thus Ai <> [#](J.i) by A2,A5,A6,Th12;
thus xi in Ai by A2,A5,A6,Th12;
thus Ai is open by A4,A7;
thus A=proj(J,i)"Ai by A2,A5,A6,Th12;
end;
theorem Th19:
for I being non empty set,
J being TopSpace-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 {proj(J,i)"Ai where Ai is Element of Fi:not contradiction}
proof
let I be non empty set,
J be TopSpace-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 set;
assume
A2: f in [#](product J);
then A3: f in the carrier of product J;
reconsider f'=f as Element of product J by A2;
f'.i in the carrier of J.i;
then f'.i in [#](J.i) by PRE_TOPC:12;
then consider Ai0 being set such that
A4: f'.i in Ai0 and
A5: Ai0 in Fi by A1,TARSKI:def 4;
reconsider Ai0 as Element of Fi by A5;
A6:
proj(J,i)"Ai0 in {proj(J,i)"Ai where Ai is Element of Fi:not contradiction};
f' in product Carrier J by A3,WAYBEL18:def 3;
then f' in dom proj(Carrier J,i) by PRALG_3:def 2;
then A7:
f' in dom proj(J,i) by WAYBEL18:def 4;
proj(J,i).f' in Ai0 by A4,Th8;
then f' in proj(J,i)"Ai0 by A7,FUNCT_1:def 13;
hence f in union {proj(J,i)"Ai where Ai is Element of Fi:not contradiction}
by A6,TARSKI:def 4;
end;
theorem Th20:
for I being non empty set,
J being TopSpace-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 TopSpace-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 set;
assume f in [#](product J);
then reconsider f'=f as Element of product J;
set g = f'+*(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,Th17;
A7: not proj(J,i)"({xi}) c= proj(J,i2)"Ai2 by A2,A5,A6;
A8:
Ai2 <> [#](J.i2)
proof
assume Ai2 = [#](J.i2);
then proj(J,i2)"Ai2 = [#] product J by Th10
.= the carrier of product J by PRE_TOPC:12;
hence contradiction by A2,A5,A6;
end;
i<>i2
proof
assume
A9: i = i2;
then A10: not xi in Ai2 by A7,A8,Th12;
reconsider Ai2'=Ai2 as Subset of J.i by A9;
proj(J,i)"({xi}) /\ proj(J,i)"Ai2' <> {} by A3,A4,A6,A9,XBOOLE_0:def 3
;
then proj(J,i)"({xi}) meets proj(J,i)"Ai2' by XBOOLE_0:def 7;
hence contradiction by A10,Th9;
end;
then f in proj(J,i2)"Ai2 by A4,A6,Th13;
hence f in union G by A5,A6,TARSKI:def 4;
end;
theorem Th21:
for I being non empty set,
J being TopSpace-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 TopSpace-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 G'=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 G' by A2,Th20;
hence contradiction by A1;
end;
theorem Th22:
for I being non empty set,
J being TopSpace-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 TopSpace-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,Th21;
A <> [#](product J)
proof
assume
A5: A = [#](product J);
reconsider G1 = {A} as finite Subset of F by A3,ZFMISC_1:37;
union G1 = [#](product J) by A5,ZFMISC_1:31;
hence contradiction by A1;
end;
then consider Ai being Subset of J.i such that
A6: Ai <> [#](J.i) and
A7: xi in Ai and
A8: Ai is open and
A9: A=proj(J,i)"Ai by A2,A4,Th18;
take Ai;
thus Ai <> [#](J.i) by A6;
thus xi in Ai by A7;
thus proj(J,i)"Ai in G by A3,A9;
thus Ai is open by A8;
end;
theorem Th23:
for I being non empty set,
J being TopSpace-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
let I be non empty set,
J be TopSpace-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;
assume
A3: for xi being Element of J.i
ex G being finite Subset of F st proj(J,i)"({xi}) c= union G;
defpred P[set,set] means
$1 in $2 & proj(J,i)"$2 in F &
for V being Subset of J.i st V = $2 holds V is open;
A4:
for xi being set st xi in the carrier of J.i ex Ai being set
st Ai in bool the carrier of J.i & P[xi, Ai]
proof
let xi be set;
assume xi in the carrier of J.i;
then reconsider xi'=xi as Element of J.i;
consider G being finite Subset of F such that
A5: proj(J,i)"({xi'}) 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,Th22;
take Ai;
thus Ai in bool the carrier of J.i;
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 V is open 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 set st xi in the carrier of J.i holds P[xi, h.xi]
from NonUniqBoundFuncEx(A4);
reconsider bGip = rng h as Subset-Family of (J.i)
by A10,SETFAM_1:def 7;
reconsider bGip as Subset-Family of J.i;
A12:
[#](J.i) c= union bGip
proof
let x be set;
assume
A13: x in [#](J.i);
then A14: x in h.x by A11;
h.x in bGip by A9,A13,FUNCT_1:def 5;
hence x in union bGip by A14,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 set such that
A15: x in dom h and
A16: P = h.x by FUNCT_1:def 5;
thus P is open by A9,A11,A15,A16;
end;
then A17: 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
A18: Gip c= bGip and
A19: [#](J.i) c= union Gip and
A20: Gip is finite by A12,A17,Th15;
reconsider Gip as non empty finite
Subset-Family of J.i by A19,A20,XBOOLE_1:3,ZFMISC_1:2;
deffunc F(set) = proj(J,i)"$1;
defpred P[set] means not contradiction;
set Gp={F(Ai) where Ai is Element of Gip: P[Ai]};
A21: Gp is finite from FraenkelFinIm;
Gp c= F
proof
let A be set;
assume A in Gp;
then consider Ai being Element of Gip such that
A22: A= proj(J,i)"Ai;
Ai in Gip;
then consider x being set such that
A23: x in dom h and
A24: h.x = Ai by A18,FUNCT_1:def 5;
thus A in F by A9,A11,A22,A23,A24;
end;
then reconsider Gp as finite Subset of F by A21;
[#](product J) c= union Gp by A19,Th19;
hence contradiction by A2;
end;
theorem::The Tichonov Theorem
for I being non empty set,
J being TopSpace-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 TopSpace-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 Th16;
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,Th23;
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 the carrier of (product J);
then f in [#](product J) by PRE_TOPC:12;
then consider A being set such that
A6: f in A and
A7: A in F by A2,TARSKI:def 4;
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,Th17;
reconsider G = {A} as finite Subset of F by A7,ZFMISC_1:37;
proj(J,i).f in Ai by A6,A8,FUNCT_1:def 13;
then f.i in Ai by Th8;
then {f.i} c= Ai by ZFMISC_1:37;
then proj(J,i)"({f.i}) c= A by A8,RELAT_1:178;
then proj(J,i)"({f.i}) c= union G by ZFMISC_1:31;
hence contradiction by A5;
end;