The abstract of the Mizar article:

Some Properties of Isomorphism between Relational Structures. On the Product of Topological Spaces

by

Jaroslaw Gryko, and

Artur Kornilowicz

Received June 22, 1999

MML identifier: YELLOW14

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FUNCT_1, BOOLE, FUNCT_4, CAT_1, ORDERS_1, PRE_TOPC,
      SUBSET_1, RELAT_2, WAYBEL_0, QUANTAL1, PRALG_1, MONOID_0, FUNCOP_1,
      SEQM_3, WAYBEL_9, WAYBEL24, YELLOW_0, GROUP_1, CARD_3, SGRAPH1, WELLORD1,
      LATTICE3, LATTICES, T_0TOPSP, TOPS_2, ORDINAL2, WAYBEL11, WAYBEL_6,
      YELLOW_8, COMPTS_1, SETFAM_1, FINSET_1, TARSKI, WAYBEL_3, TOPS_1,
      WAYBEL18, PBOOLE, RLVECT_2, BORSUK_1, CANTOR_1, WAYBEL_1, FUNCT_3,
      GROUP_6, TSP_1, URYSOHN1, SEQ_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FINSET_1,
      TOPS_2, FUNCT_1, PARTFUN1, FUNCT_4, CQC_LANG, FUNCT_7, CARD_3, MONOID_0,
      PBOOLE, PRALG_1, PRE_CIRC, STRUCT_0, PRE_TOPC, GRCAT_1, TOPS_1, COMPTS_1,
      T_0TOPSP, TSP_1, URYSOHN1, CANTOR_1, TMAP_1, ORDERS_1, LATTICE3,
      WAYBEL18, YELLOW_0, WAYBEL_0, WAYBEL_1, FUNCT_2, YELLOW_1, YELLOW_2,
      WAYBEL_3, YELLOW_6, YELLOW_8, WAYBEL_9, WAYBEL11, WAYBEL24;
 constructors BORSUK_3, CANTOR_1, CQC_LANG, FUNCT_7, GRCAT_1, ORDERS_3,
      PRE_CIRC, TMAP_1, TOLER_1, TOPS_1, TOPS_2, URYSOHN1, WAYBEL_1, WAYBEL17,
      WAYBEL18, WAYBEL24, YELLOW_8, MONOID_0;
 clusters BORSUK_3, FUNCT_1, TEX_4, PRE_TOPC, RELAT_1, YELLOW_8, CQC_LANG,
      RELSET_1, STRUCT_0, TEX_1, TSP_1, TOPGRP_1, YELLOW_0, YELLOW_1, YELLOW_6,
      YELLOW12, WAYBEL_0, WAYBEL_3, WAYBEL_7, WAYBEL12, WAYBEL18, WAYBEL19,
      WAYBEL24, SUBSET_1, PARTFUN1, FUNCT_2;
 requirements SUBSET, BOOLE;


begin  :: Preliminaries

theorem :: YELLOW14:1
   bool 1 = {0,1};

theorem :: YELLOW14:2
 for X being set, Y being Subset of X holds rng ((id X)|Y) = Y;

theorem :: YELLOW14:3
 for f being Function, a, b being set holds (f +* (a .--> b)).a = b;

definition
 cluster strict empty RelStr;
end;

theorem :: YELLOW14:4
 for S being empty 1-sorted, T being 1-sorted, f being map of S, T st
  rng f = [#]T holds T is empty;

theorem :: YELLOW14:5
 for S being 1-sorted, T being empty 1-sorted, f being map of S, T st
  dom f = [#]S holds S is empty;

theorem :: YELLOW14:6
   for S being non empty 1-sorted, T being 1-sorted, f being map of S, T st
  dom f = [#]S holds T is non empty;

theorem :: YELLOW14:7
   for S being 1-sorted, T being non empty 1-sorted, f being map of S, T st
  rng f = [#]T holds S is non empty;

definition let S be non empty reflexive RelStr, T be non empty RelStr,
               f be map of S, T;
 redefine attr f is directed-sups-preserving means
:: YELLOW14:def 1
    for X being non empty directed Subset of S holds f preserves_sup_of X;
end;

definition let R be 1-sorted, N be NetStr over R;
 attr N is Function-yielding means
:: YELLOW14:def 2
  the mapping of N is Function-yielding;
end;

definition
 cluster strict non empty constituted-Functions 1-sorted;
end;

definition
 cluster strict non empty constituted-Functions RelStr;
end;

definition let R be constituted-Functions 1-sorted;
 cluster -> Function-yielding NetStr over R;
end;

definition let R be constituted-Functions 1-sorted;
 cluster strict Function-yielding NetStr over R;
end;

definition let R be non empty constituted-Functions 1-sorted;
 cluster strict non empty Function-yielding NetStr over R;
end;

definition let R be constituted-Functions 1-sorted,
               N be Function-yielding NetStr over R;
 cluster the mapping of N -> Function-yielding;
end;

definition let R be non empty constituted-Functions 1-sorted;
 cluster strict Function-yielding net of R;
end;

definition let S be non empty 1-sorted,
               N be non empty NetStr over S;
 cluster rng the mapping of N -> non empty;
end;

definition let S be non empty 1-sorted,
               N be non empty NetStr over S;
 cluster rng netmap (N,S) -> non empty;
end;

theorem :: YELLOW14:8
   for A, B, C being non empty RelStr, f being map of B, C,
     g, h being map of A, B st g <= h & f is monotone holds f * g <= f * h;

theorem :: YELLOW14:9
   for S being non empty TopSpace,
     T being non empty TopSpace-like TopRelStr,
     f, g being map of S, T,
     x, y being Element of ContMaps(S,T) st x = f & y = g holds
  x <= y iff f <= g;

definition let I be set,
               R be non empty RelStr;
 cluster -> Function-like Relation-like Element of R |^ I;
end;

definition let I be non empty set,
               R be non empty RelStr,
               f be Element of R |^ I,
               i be Element of I;
 redefine func f.i -> Element of R;
end;

begin  :: Some properties of isomorphism between relational structures

theorem :: YELLOW14:10
 for S, T being RelStr, f being map of S, T st f is isomorphic holds
  f is onto;

definition let S, T be RelStr;
 cluster isomorphic -> onto map of S, T;
end;

theorem :: YELLOW14:11
 for S, T being non empty RelStr, f being map of S, T st f is isomorphic holds
  f/" is isomorphic;

theorem :: YELLOW14:12
   for S, T being non empty RelStr st S, T are_isomorphic & S is with_infima
  holds T is with_infima;

theorem :: YELLOW14:13
   for S, T being non empty RelStr st S, T are_isomorphic & S is with_suprema
  holds T is with_suprema;

theorem :: YELLOW14:14
 for L being RelStr st L is empty holds L is bounded;

definition
 cluster empty -> bounded RelStr;
end;

theorem :: YELLOW14:15
   for S, T being RelStr st S, T are_isomorphic & S is lower-bounded
  holds T is lower-bounded;

theorem :: YELLOW14:16
   for S, T being RelStr st S, T are_isomorphic & S is upper-bounded
  holds T is upper-bounded;

theorem :: YELLOW14:17
   for S, T being non empty RelStr, A being Subset of S, f being map of S, T st
  f is isomorphic & ex_sup_of A, S holds ex_sup_of f.:A, T;

theorem :: YELLOW14:18
   for S, T being non empty RelStr, A being Subset of S, f being map of S, T st
  f is isomorphic & ex_inf_of A, S holds ex_inf_of f.:A, T;

begin  :: On the product of topological spaces

theorem :: YELLOW14:19
   for S, T being TopStruct st
  (S,T are_homeomorphic or
   ex f being map of S,T st dom f = [#]S & rng f = [#]T) holds
  S is empty iff T is empty;

theorem :: YELLOW14:20
   for T being non empty TopSpace holds T, the TopStruct of T are_homeomorphic;

definition let T be Scott (reflexive non empty TopRelStr);
 cluster open -> inaccessible upper Subset of T;
 cluster inaccessible upper -> open Subset of T;
end;

theorem :: YELLOW14:21
   for T being TopStruct, x, y being Point of T,
     X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds
  x in Cl Y;

theorem :: YELLOW14:22
   for T being TopStruct, x, y being Point of T,
     Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
  y in V;

theorem :: YELLOW14:23
   for T being TopStruct, x, y being Point of T,
     X, Y being Subset of T st X = {x} & Y = {y} holds
  (for V being Subset of T st V is open holds (x in V implies y in V)) implies
 Cl X c= Cl Y;

theorem :: YELLOW14:24
 for S, T being non empty TopSpace, A being irreducible Subset of S,
     B being Subset of T st A = B & the TopStruct of S = the TopStruct of T
  holds B is irreducible;

theorem :: YELLOW14:25
 for S, T being non empty TopSpace, a being Point of S, b being Point of T,
     A being Subset of S, B being Subset of T st
   a = b & A = B & the TopStruct of S = the TopStruct of T &
   a is_dense_point_of A
  holds b is_dense_point_of B;

theorem :: YELLOW14:26
 for S, T being TopStruct, A being Subset of S, B being Subset of T st
   A = B & the TopStruct of S = the TopStruct of T & A is compact
  holds B is compact;

theorem :: YELLOW14:27
   for S, T being non empty TopSpace st
  the TopStruct of S = the TopStruct of T & S is sober holds T is sober;

theorem :: YELLOW14:28
   for S, T being non empty TopSpace st
  the TopStruct of S = the TopStruct of T & S is locally-compact holds
 T is locally-compact;

theorem :: YELLOW14:29
   for S, T being TopStruct st
  the TopStruct of S = the TopStruct of T & S is compact holds
 T is compact;

definition let I be non empty set,
               T be non empty TopSpace,
               x be Point of product (I --> T),
               i be Element of I;
 redefine func x.i -> Element of T;
end;

theorem :: YELLOW14:30
 for M being non empty set,
     J being TopSpace-yielding non-Empty ManySortedSet of M,
     x, y being Point of product J holds
  x in Cl {y} iff for i being Element of M holds x.i in Cl {y.i};

theorem :: YELLOW14:31
   for M being non empty set, T being non empty TopSpace,
     x, y being Point of product (M --> T) holds
  x in Cl {y} iff for i being Element of M holds x.i in Cl {y.i};

theorem :: YELLOW14:32
 for M being non empty set, i being Element of M,
     J being TopSpace-yielding non-Empty ManySortedSet of M,
     x being Point of product J holds
  pi(Cl {x}, i) = Cl {x.i};

theorem :: YELLOW14:33
   for M being non empty set, i being Element of M,
     T being non empty TopSpace, x being Point of product (M --> T) holds
  pi(Cl {x}, i) = Cl {x.i};

theorem :: YELLOW14:34
   for X, Y being non empty TopStruct, f being map of X, Y, g being map of Y, X
  st f = id X & g = id X & f is continuous & g is continuous holds
 the TopStruct of X = the TopStruct of Y;

theorem :: YELLOW14:35
   for X, Y being non empty TopSpace, f being map of X, Y st
  corestr f is continuous holds f is continuous;

definition let X be non empty TopSpace,
               Y be non empty SubSpace of X;
 cluster incl Y -> continuous;
end;

theorem :: YELLOW14:36
   for T being non empty TopSpace, f being map of T, T st f*f = f
  holds corestr f * incl Image f = id Image f;

theorem :: YELLOW14:37
   for Y being non empty TopSpace, W being non empty SubSpace of Y holds
  corestr incl W is_homeomorphism;

theorem :: YELLOW14:38
 for M being non empty set,
     J being TopSpace-yielding non-Empty ManySortedSet of M st
   for i being Element of M holds J.i is T_0 TopSpace holds
 product J is T_0;

definition let I be non empty set,
               T be non empty T_0 TopSpace;
 cluster product (I --> T) -> T_0;
end;

theorem :: YELLOW14:39
 for M being non empty set,
     J being TopSpace-yielding non-Empty ManySortedSet of M st
   for i being Element of M holds J.i is being_T1 TopSpace-like holds
 product J is_T1;

definition let I be non empty set,
               T be non empty being_T1 TopSpace;
 cluster product (I --> T) -> being_T1;
end;