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