:: The Tichonov Theorem
:: by Bart{\l}omiej Skorulski
::
:: Received May 23, 2000
:: Copyright (c) 2000-2021 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;
begin ::Some Properties of Products
theorem :: YELLOW17:1
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;
theorem :: YELLOW17:2
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;
theorem :: YELLOW17:3
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);
theorem :: YELLOW17:4
for F being Function, i being set st i in dom F holds
proj(F,i)"(F.i) = product F;
theorem :: YELLOW17:5
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});
theorem :: YELLOW17:6
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);
theorem :: YELLOW17:7
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;
scheme :: YELLOW17:sch 1
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
for i being Element of I() ex x being Element of J().i st P[x,i];
theorem :: YELLOW17:8
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;
theorem :: YELLOW17:9
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;
theorem :: YELLOW17:10
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;
theorem :: YELLOW17:11
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});
theorem :: YELLOW17:12
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;
theorem :: YELLOW17:13
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;
begin
theorem :: YELLOW17:14
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;
theorem :: YELLOW17:15
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;
begin ::The Tichonov Theorem
theorem :: YELLOW17:16
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;
theorem :: YELLOW17:17
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;
theorem :: YELLOW17:18
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;
theorem :: YELLOW17:19
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;
theorem :: YELLOW17:20
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;
theorem :: YELLOW17:21
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;
theorem :: YELLOW17:22
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;
::$N Tychonoff's theorem
theorem :: YELLOW17:23
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;