:: Some Properties of Isomorphism between Relational Structures. On
:: the Product of Topological Spaces
::  by Jaros{\l}aw Gryko and Artur Korni{\l}owicz
::
:: Received June 22, 1999
:: Copyright (c) 1999-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 ZFMISC_1, CARD_1, SUBSET_1, RELAT_1, FUNCT_1, XBOOLE_0, STRUCT_0,
      RELAT_2, ORDERS_2, WAYBEL_0, FUNCOP_1, MONOID_0, YELLOW_6, XXREAL_0,
      SEQM_3, PRE_TOPC, WAYBEL_9, WAYBEL24, CAT_1, YELLOW_0, NEWTON, CARD_3,
      FUNCT_2, VALUED_1, WELLORD1, LATTICE3, XXREAL_2, LATTICES, TARSKI,
      T_0TOPSP, TOPS_2, ORDINAL2, WAYBEL11, RCOMP_1, CARD_FIL, YELLOW_8,
      SETFAM_1, FINSET_1, WAYBEL_3, TOPS_1, WAYBEL18, PBOOLE, RLVECT_2,
      FUNCT_4, CANTOR_1, WAYBEL_1, FUNCT_3, GROUP_6;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, TOPS_2, FUNCT_1,
      PBOOLE, RELSET_1, PARTFUN1, FUNCT_4, FUNCOP_1, ORDINAL1, NUMBERS,
      FUNCT_7, CARD_3, MONOID_0, SETFAM_1, FUNCT_2, DOMAIN_1, STRUCT_0,
      PRALG_1, PRE_TOPC, TOPS_1, COMPTS_1, T_0TOPSP, CANTOR_1, TMAP_1,
      ORDERS_2, LATTICE3, WAYBEL18, YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_1,
      YELLOW_2, WAYBEL_3, YELLOW_6, YELLOW_8, WAYBEL_9, WAYBEL11, WAYBEL24;
 constructors FINSUB_1, REALSET1, FUNCT_7, TOPS_1, TOPS_2, LATTICE3, TMAP_1,
      T_0TOPSP, CANTOR_1, MONOID_0, ORDERS_3, WAYBEL_1, YELLOW_8, WAYBEL11,
      WAYBEL18, WAYBEL24, COMPTS_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
      STRUCT_0, PRE_TOPC, TOPS_1, YELLOW_0, TEX_4, MONOID_0, WAYBEL_0,
      YELLOW_1, YELLOW_6, YELLOW_8, WAYBEL18, WAYBEL19, TOPGRP_1, BORSUK_3,
      WAYBEL24, RELSET_1, FINSET_1;
 requirements SUBSET, BOOLE;


begin  :: Preliminaries

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

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

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

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

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

theorem :: YELLOW14:6
  for S being 1-sorted, T being non empty 1-sorted, f being Function 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 Function 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;

registration
  cluster non empty constituted-Functions for 1-sorted;
end;

registration
  cluster strict non empty constituted-Functions for RelStr;
end;

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

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

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

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

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

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

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

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

theorem :: YELLOW14:8
  for S being non empty TopSpace, T being non empty TopSpace-like
TopRelStr, f, g being Function 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 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:9
  for S, T being RelStr, f being Function of S, T st f is
  isomorphic holds f is onto;

registration
  let S, T be RelStr;
  cluster isomorphic -> onto for Function of S, T;
end;

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

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

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

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

registration
  cluster empty -> bounded for RelStr;
end;

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

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

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

theorem :: YELLOW14:17
  for S, T being non empty RelStr, A being Subset of S, f being Function
  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:18
  for S, T being TopStruct st (S,T are_homeomorphic or ex f being
Function of S,T st dom f = [#]S & rng f = [#]T) holds S is empty iff T is empty
;

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

registration
  let T be Scott reflexive non empty TopRelStr;
  cluster open -> inaccessible upper for Subset of T;
  cluster inaccessible upper -> open for Subset of T;
end;

theorem :: YELLOW14:20
  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:21
  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:22
  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:23
  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:24
  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:25
  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:26
  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:27
  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:28
  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:29
  for M being non empty set, J being TopStruct-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:30
  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:31
  for M being non empty set, i being Element of M, J being
  TopStruct-yielding non-Empty ManySortedSet of M, x being Point of product J
  holds pi(Cl {x}, i) = Cl {x.i};

theorem :: YELLOW14:32
  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:33
  for X, Y being non empty TopStruct, f being Function of X, Y, g being
  Function 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:34
  for X, Y being non empty TopSpace, f being Function of X, Y st corestr
  f is continuous holds f is continuous;

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

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

theorem :: YELLOW14:36
  for Y being non empty TopSpace, W being non empty SubSpace of Y holds
  corestr incl W is being_homeomorphism;

theorem :: YELLOW14:37
  for M being non empty set, J being TopStruct-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;

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

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

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