:: The Tichonov Theorem
:: by Bart{\l}omiej Skorulski
::
:: Received May 23, 2000
:: Copyright (c) 2000-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions 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;
registrations SUBSET_1, RELSET_1, FINSET_1, CARD_3, STRUCT_0, PRE_TOPC, MONOID_0, YELLOW_1, YELLOW_6, WAYBEL18;
constructors HIDDEN, SETFAM_1, FUNCT_7, TOPS_2, COMPTS_1, CANTOR_1, MONOID_0, WAYBEL18, RELSET_1, FUNCT_4;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, STRUCT_0;
expansions TARSKI, COMPTS_1, XBOOLE_0;


theorem Th1: :: YELLOW17:1
for F being Function
for i, xi being set
for Ai being Subset of (F . i) st (proj (F,i)) " {xi} meets (proj (F,i)) " Ai holds
xi in Ai
proof end;

theorem Th2: :: YELLOW17:2
for F, f being Function
for i, xi being set st xi in F . i & f in product F holds
f +* (i,xi) in product F
proof end;

theorem Th3: :: YELLOW17:3
for F being Function
for 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 end;

theorem Th4: :: YELLOW17:4
for F being Function
for i being set st i in dom F holds
(proj (F,i)) " (F . i) = product F
proof end;

theorem Th5: :: YELLOW17:5
for F, f being Function
for 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 end;

Lm1: for F, g being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st i1 <> i2 & g in product F & g +* (i1,xi1) in (proj (F,i2)) " Ai2 holds
g in (proj (F,i2)) " Ai2
proof end;

theorem Th6: :: YELLOW17:6
for F, f being Function
for i1, i2, xi1 being set
for Ai2 being Subset of (F . i2) st xi1 in F . i1 & f in product F & i1 <> i2 holds
( f in (proj (F,i2)) " Ai2 iff f +* (i1,xi1) in (proj (F,i2)) " Ai2 )
proof end;

theorem Th7: :: YELLOW17:7
for F being Function
for i1, i2, xi1 being set
for 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 end;

scheme :: YELLOW17:sch 1
ElProductEx{ F1() -> non empty set , F2() -> non-Empty TopStruct-yielding ManySortedSet of F1(), P1[ object , object ] } :
ex f being Element of (product F2()) st
for i being Element of F1() holds P1[f . i,i]
provided
A1: for i being Element of F1() ex x being Element of (F2() . i) st P1[x,i]
proof end;

theorem Th8: :: YELLOW17:8
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for f being Element of (product J) holds (proj (J,i)) . f = f . i
proof end;

theorem Th9: :: YELLOW17:9
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for Ai being Subset of (J . i) st (proj (J,i)) " {xi} meets (proj (J,i)) " Ai holds
xi in Ai
proof end;

theorem Th10: :: YELLOW17:10
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I holds (proj (J,i)) " ([#] (J . i)) = [#] (product J)
proof end;

theorem Th11: :: YELLOW17:11
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for f being Element of (product J) holds f +* (i,xi) in (proj (J,i)) " {xi}
proof end;

theorem Th12: :: YELLOW17:12
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for 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 end;

theorem Th13: :: YELLOW17:13
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i1, i2 being Element of I
for xi1 being Element of (J . i1)
for Ai2 being Subset of (J . i2)
for 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 end;

theorem Th14: :: 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 holds
ex G being Subset-Family of T st
( G c= F & [#] T c= union G & G is finite ) )
proof end;

theorem Th15: :: YELLOW17:15
for T being non empty TopSpace
for B being prebasis of T holds
( T is compact iff for F being Subset of B st [#] T c= union F holds
ex G being finite Subset of F st [#] T c= union G )
proof end;

theorem Th16: :: YELLOW17:16
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for A being set st A in product_prebasis J holds
ex i being Element of I ex Ai being Subset of (J . i) st
( Ai is open & (proj (J,i)) " Ai = A )
proof end;

theorem Th17: :: YELLOW17:17
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for A being set st A in product_prebasis J & (proj (J,i)) " {xi} c= A & not A = [#] (product J) holds
ex Ai being Subset of (J . i) st
( Ai <> [#] (J . i) & xi in Ai & Ai is open & A = (proj (J,i)) " Ai )
proof end;

theorem Th18: :: YELLOW17:18
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for 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 : verum }
proof end;

theorem Th19: :: YELLOW17:19
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for xi being Element of (J . i)
for 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 end;

theorem Th20: :: YELLOW17:20
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for G being finite Subset of F st (proj (J,i)) " {xi} c= union G holds
ex A being set st
( A in product_prebasis J & A in G & (proj (J,i)) " {xi} c= A )
proof end;

theorem Th21: :: YELLOW17:21
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for F being Subset of (product_prebasis J) st ( for G being finite Subset of F holds not [#] (product J) c= union G ) holds
for xi being Element of (J . i)
for 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 end;

theorem Th22: :: YELLOW17:22
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for i being Element of I
for 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 ) holds
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 end;

:: WP: Tichonov Theorem
theorem :: YELLOW17:23
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds J . i is compact ) holds
product J is compact
proof end;