The abstract of the Mizar article:

Properties of the Product of Compact Topological Spaces

by

Adam Grabowski

Received February 13, 1999

MML identifier: BORSUK_3

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, SUBSET_1, FUNCOP_1, ORDINAL2, RELAT_1, FUNCT_1, TOPS_2,
      T_0TOPSP, BOOLE, COMPTS_1, FUNCT_3, PARTFUN1, PBOOLE, TARSKI, BORSUK_1,
      TOPS_1, CONNSP_2, SETFAM_1, FINSET_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, FUNCT_1,
      STRUCT_0, PRE_TOPC, TOPS_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP, PBOOLE,
      FUNCT_2, FINSET_1, FUNCT_3, CAT_1, CONNSP_2, GRCAT_1;
 constructors TOPS_2, T_0TOPSP, TOPS_1, COMPTS_1, WAYBEL_3, GRCAT_1, BORSUK_1,
      MEMBERED;
 clusters STRUCT_0, PRE_TOPC, BORSUK_1, BORSUK_2, TOPS_1, WAYBEL_3, WAYBEL12,
      PSCOMP_1, RELSET_1, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

theorem :: BORSUK_3:1
  for S, T being TopSpace holds [#][:S, T:] = [:[#]S, [#]T:];

definition let X be set, Y be empty set;
  cluster [:X, Y:] -> empty;
end;

definition let X be empty set, Y be set;
  cluster [:X, Y:] -> empty;
end;

theorem :: BORSUK_3:2
  for X, Y being non empty TopSpace,
      x being Point of X holds
    Y --> x is continuous map of Y, X|{x};

definition let T be non empty TopStruct;
  cluster id T -> being_homeomorphism;
end;

definition let S, T be non empty TopStruct;
  redefine pred S, T are_homeomorphic;
  reflexivity;
  symmetry;
end;

theorem :: BORSUK_3:3
    for S, T, V being non empty TopSpace st
   S, T are_homeomorphic & T, V are_homeomorphic holds
    S, V are_homeomorphic;

begin :: On the projections and empty topological spaces

definition let T be TopStruct,
               P be empty Subset of T;
  cluster T | P -> empty;
end;

definition
  cluster strict empty TopSpace;
end;

theorem :: BORSUK_3:4
  for T1 being TopSpace,
      T2 being empty TopSpace holds [:T1, T2:] is empty & [:T2, T1:] is empty;

theorem :: BORSUK_3:5
  for T being empty TopSpace holds T is compact;

definition
  cluster empty -> compact TopSpace;
end;

definition let T1 be TopSpace, T2 be empty TopSpace;
  cluster [:T1, T2:] -> empty;
end;

theorem :: BORSUK_3:6
  for X, Y being non empty TopSpace,
      x being Point of X,
      f being map of [:Y, X | {x}:], Y st
    f = pr1(the carrier of Y, {x}) holds f is one-to-one;

theorem :: BORSUK_3:7
  for X, Y being non empty TopSpace,
      x being Point of X,
      f being map of [:X | {x}, Y:], Y st
    f = pr2({x}, the carrier of Y) holds f is one-to-one;

theorem :: BORSUK_3:8
  for X, Y being non empty TopSpace,
      x being Point of X,
      f being map of [:Y, X | {x}:], Y st
    f = pr1(the carrier of Y, {x}) holds f" = <:id Y, Y --> x:>;

theorem :: BORSUK_3:9
  for X, Y being non empty TopSpace,
      x being Point of X,
      f being map of [:X | {x}, Y:], Y st
    f = pr2({x}, the carrier of Y) holds f" = <:Y --> x, id Y:>;

theorem :: BORSUK_3:10
    for X, Y being non empty TopSpace,
      x being Point of X,
      f being map of [:Y, X | {x}:], Y st
    f = pr1(the carrier of Y, {x}) holds
   f is_homeomorphism;

theorem :: BORSUK_3:11
  for X, Y being non empty TopSpace,
      x being Point of X,
      f being map of [:X | {x}, Y:], Y st
    f = pr2({x}, the carrier of Y) holds
   f is_homeomorphism;

begin :: On the product of compact spaces

theorem :: BORSUK_3:12
    for X being non empty TopSpace, Y being compact non empty TopSpace,
      G being open Subset of [:X, Y:],
      x being set st
   x in { x' where x' is Point of X : [:{x'}, the carrier of Y:] c= G }
   ex f being ManySortedSet of the carrier of Y st
   for i being set st i in the carrier of Y
    ex G1 being Subset of X, H1 being Subset of Y st f.i = [G1,H1] &
     [x, i] in [:G1, H1:] & G1 is open & H1 is open & [:G1, H1:] c= G;

theorem :: BORSUK_3:13
  for X being non empty TopSpace, Y being compact non empty TopSpace,
      G being open Subset of [:Y, X:] holds
 for x being set st x in { y where y is Point of X : [:[#]Y, {y}:] c= G }
   holds
    ex R be open Subset of X st x in R &
      R c= { y where y is Point of X : [:[#]Y, {y}:] c= G };

theorem :: BORSUK_3:14
 for X being non empty TopSpace, Y being compact non empty TopSpace,
     G being open Subset of [:Y, X:] holds
      { x where x is Point of X : [:[#]Y, {x}:] c= G } in the topology of X;

theorem :: BORSUK_3:15
  for X, Y being non empty TopSpace,
      x being Point of X holds
    [: X | {x}, Y :], Y are_homeomorphic;

theorem :: BORSUK_3:16
  for S, T being non empty TopSpace st
    S, T are_homeomorphic & S is compact holds T is compact;

theorem :: BORSUK_3:17
  for X, Y being TopSpace,
      XV being SubSpace of X holds
    [:Y, XV:] is SubSpace of [:Y, X:];

theorem :: BORSUK_3:18
  for X being non empty TopSpace,
      Y being compact non empty TopSpace,
      x being Point of X,
      Z being Subset of [:Y, X:] st Z = [:[#]Y, {x}:] holds
   Z is compact;

theorem :: BORSUK_3:19
    for X being non empty TopSpace,
      Y being compact non empty TopSpace,
      x being Point of X holds
    [:Y, X|{x}:] is compact;

theorem :: BORSUK_3:20
    for X, Y being compact non empty TopSpace,
      R being Subset-Family of X st
   R = { Q where Q is open Subset of X : [:[#]Y, Q:] c=
     union Base-Appr [#][:Y, X:] } holds R is open & R is_a_cover_of [#]X;

theorem :: BORSUK_3:21
  for X, Y being compact non empty TopSpace,
      R being Subset-Family of X,
      F being Subset-Family of [:Y, X:] st
    F is_a_cover_of [:Y, X:] & F is open &
  R = { Q where Q is open Subset of X :
   ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite &
    [:[#]Y, Q:] c= union FQ } holds
      R is open & R is_a_cover_of X;

theorem :: BORSUK_3:22
  for X, Y being compact non empty TopSpace,
      R being Subset-Family of X,
      F being Subset-Family of [:Y, X:] st
    F is_a_cover_of [:Y, X:] & F is open &
  R = { Q where Q is open Subset of X :
   ex FQ being Subset-Family of [:Y, X:] st FQ c= F & FQ is finite &
  [:[#]Y, Q:] c= union FQ } holds
  ex C being Subset-Family of X st C c= R & C is finite & C is_a_cover_of X;

theorem :: BORSUK_3:23
  for X, Y being compact non empty TopSpace,
      F being Subset-Family of [:Y, X:] st
    F is_a_cover_of [:Y, X:] & F is open
      ex G being Subset-Family of [:Y, X:]
       st G c= F & G is_a_cover_of [:Y, X:] & G is finite;

theorem :: BORSUK_3:24
  for T1, T2 be TopSpace st T1 is compact & T2 is compact holds
    [:T1, T2:] is compact;

definition let T1, T2 be compact TopSpace;
  cluster [:T1, T2:] -> compact;
end;

theorem :: BORSUK_3:25
  for X, Y being non empty TopSpace,
      XV being non empty SubSpace of X,
      YV being non empty SubSpace of Y holds
   [:XV, YV:] is SubSpace of [:X, Y:];

theorem :: BORSUK_3:26
  for X, Y being non empty TopSpace,
      Z being non empty Subset of [:Y, X:],
      V being non empty Subset of X,
      W being non empty Subset of Y st Z = [:W, V:] holds
   the TopStruct of [:Y | W, X | V:] = the TopStruct of [:Y, X:] | Z;

definition let T be TopSpace;
  cluster compact Subset of T;
end;

definition let T be TopSpace, P be compact Subset of T;
  cluster T | P -> compact;
end;

theorem :: BORSUK_3:27
    for T1, T2 being TopSpace,
      S1 being Subset of T1,
      S2 being Subset of T2 st S1 is compact & S2 is compact holds
  [:S1, S2:] is compact Subset of [:T1, T2:];