The Mizar abstract of YELLOW17

Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users
The abstract of the Mizar article:: The Tichonov Theorem
by
Bartlomiej Skorulski
Received May 23, 2000
MML identifier: YELLOW17
[ Mizar article, MML identifier index ]
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;


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 & product F <> {} holds
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 & 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);

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 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
  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 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;

theorem :: YELLOW17:9
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;

theorem :: YELLOW17:10
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;

theorem :: YELLOW17:11
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});

theorem :: YELLOW17:12
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);

theorem :: YELLOW17:13
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;

begin

canceled;

theorem :: YELLOW17:15
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:16 ::Alexander's Lemma

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:17
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;

theorem :: YELLOW17:18
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;

theorem :: YELLOW17:19
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};

theorem :: YELLOW17:20
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;

theorem :: YELLOW17:21
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;

theorem :: YELLOW17:22
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;

theorem :: YELLOW17:23
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;

theorem :: YELLOW17:24::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;
The abstract of the Mizar article:

The Tichonov Theorem
