:: 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-2018 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;
definitions TARSKI, MONOID_0, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, T_0TOPSP,
LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3, YELLOW_8, FUNCT_2,
XBOOLE_0, FUNCOP_1;
equalities ORDINAL1, STRUCT_0, FUNCOP_1;
expansions TARSKI, PRE_TOPC, TOPS_2, T_0TOPSP, WAYBEL_0, FUNCT_2, XBOOLE_0;
theorems TARSKI, PRE_TOPC, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_7, PRALG_1,
FUNCOP_1, CARD_3, BORSUK_1, TOPS_2, TOPS_3, YELLOW_0, YELLOW_1, YELLOW_2,
YELLOW_9, YELLOW12, WAYBEL_0, WAYBEL_1, WAYBEL_9, WAYBEL11, WAYBEL10,
WAYBEL13, WAYBEL18, WAYBEL24, YELLOW_8, TMAP_1, TSP_1, FUNCT_4, URYSOHN1,
XBOOLE_0, XBOOLE_1, SETFAM_1, CARD_1, PARTFUN1, RELSET_1;
begin :: Preliminaries
theorem
bool {0} = {0,1} by CARD_1:49,ZFMISC_1:24;
theorem Th2:
for X being set, Y being Subset of X holds rng ((id X)|Y) = Y
proof
let X be set, Y be Subset of X;
set f = id X;
A1: f|Y is Function of Y,X by FUNCT_2:32;
hereby
let y be object;
assume y in rng (f|Y);
then consider x being object such that
A2: x in dom (f|Y) and
A3: y = (f|Y).x by FUNCT_1:def 3;
(f|Y).x = f.x by A2,FUNCT_1:47
.= x by A2,FUNCT_1:17;
hence y in Y by A1,A2,A3,FUNCT_2:def 1;
end;
let y be object;
X = {} implies Y = {};
then
A4: dom (f|Y) = Y by A1,FUNCT_2:def 1;
assume
A5: y in Y;
then (f|Y).y = f.y by FUNCT_1:49
.= y by A5,FUNCT_1:18;
hence thesis by A4,A5,FUNCT_1:def 3;
end;
theorem
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
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
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
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
for X being non empty directed Subset of S holds f preserves_sup_of X;
compatibility;
end;
definition
let R be 1-sorted, N be NetStr over R;
attr N is Function-yielding means
:Def2:
the mapping of N is Function-yielding;
end;
registration
cluster non empty constituted-Functions for 1-sorted;
existence
proof
take A = 1-sorted (#{{}}#);
thus the carrier of A is non empty;
let a be Element of A;
thus thesis;
end;
end;
registration
cluster strict non empty constituted-Functions for RelStr;
existence
proof
take A = RelStr (#{{}}, id {{}}#);
thus A is strict non empty;
let a be Element of A;
thus thesis;
end;
end;
registration
let R be constituted-Functions 1-sorted;
cluster -> Function-yielding for NetStr over R;
coherence
proof
let N be NetStr over R;
let x be object;
assume x in dom the mapping of N;
then (the mapping of N).x in rng the mapping of N by FUNCT_1:def 3;
hence thesis;
end;
end;
registration
let R be constituted-Functions 1-sorted;
cluster strict Function-yielding for NetStr over R;
existence
proof
take A = NetStr (#the carrier of R, id the carrier of R, id the carrier of
R#);
thus A is strict;
let x be object;
assume x in dom the mapping of A;
hence thesis by FUNCT_1:18;
end;
end;
registration
let R be non empty constituted-Functions 1-sorted;
cluster strict non empty Function-yielding for NetStr over R;
existence
proof
take A = NetStr (#the carrier of R, id the carrier of R, id the carrier of
R#);
thus A is strict non empty;
let x be object;
assume x in dom the mapping of A;
hence thesis by FUNCT_1:18;
end;
end;
registration
let R be constituted-Functions 1-sorted, N be Function-yielding NetStr over
R;
cluster the mapping of N -> Function-yielding;
coherence by Def2;
end;
registration
let R be non empty constituted-Functions 1-sorted;
cluster strict Function-yielding for net of R;
existence
proof
set p = the Element of R;
set N = the net of R;
take ConstantNet(N,p);
thus thesis;
end;
end;
registration
let S be non empty 1-sorted, N be non empty NetStr over S;
cluster rng the mapping of N -> non empty;
coherence;
end;
registration
let S be non empty 1-sorted, N be non empty NetStr over S;
cluster rng netmap (N,S) -> non empty;
coherence;
end;
theorem
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
proof
let A, B, C be non empty RelStr, f be Function of B, C, g, h be Function of
A, B such that
A1: g <= h and
A2: for x, y being Element of B st x <= y holds f.x <= f.y;
for x being Element of A holds (f*g).x <= (f*h).x
proof
let x be Element of A;
A3: (f*g).x = f.(g.x) & (f*h).x = f.(h.x) by FUNCT_2:15;
g.x <= h.x by A1,YELLOW_2:9;
hence thesis by A2,A3;
end;
hence thesis by YELLOW_2:9;
end;
theorem
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
proof
let S be non empty TopSpace, T be non empty TopSpace-like TopRelStr, f, g be
Function of S, T, x, y be Element of ContMaps(S,T) such that
A1: x = f & y = g;
A2: ContMaps(S,T) is full SubRelStr of T |^ the carrier of S by WAYBEL24:def 3;
then reconsider x1 = x, y1 = y as Element of T |^ the carrier of S by
YELLOW_0:58;
hereby
assume x <= y;
then x1 <= y1 by A2,YELLOW_0:59;
hence f <= g by A1,WAYBEL10:11;
end;
assume f <= g;
then x1 <= y1 by A1,WAYBEL10:11;
hence thesis by A2,YELLOW_0:60;
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;
coherence
proof
reconsider g = f as Element of product (I --> R) by YELLOW_1:def 5;
g.i is Element of (I --> R).i;
hence thesis by FUNCOP_1:7;
end;
end;
begin :: Some properties of isomorphism between relational structures
theorem Th9:
for S, T being RelStr, f being Function of S, T st f is
isomorphic holds f is onto
proof
let S, T be RelStr, f be Function of S, T such that
A1: f is isomorphic;
per cases;
suppose
S is non empty & T is non empty;
hence rng f = the carrier of T by A1,WAYBEL_0:66;
end;
suppose
S is empty or T is empty;
then T is empty by A1,WAYBEL_0:def 38;
then the carrier of T = {};
hence rng f = the carrier of T;
end;
end;
registration
let S, T be RelStr;
cluster isomorphic -> onto for Function of S, T;
coherence by Th9;
end;
theorem Th10:
for S, T being non empty RelStr, f being Function of S, T st f
is isomorphic holds f/" is isomorphic
proof
let S, T be non empty RelStr, f be Function of S, T;
assume
A1: f is isomorphic;
then (ex g being Function of T, S st g = f qua Function" & g is monotone )&
rng f = the carrier of T by WAYBEL_0:66,def 38;
hence thesis by A1,TOPS_2:def 4,WAYBEL_0:68;
end;
theorem
for S, T being non empty RelStr st S, T are_isomorphic & S is
with_infima holds T is with_infima
proof
let S, T be non empty RelStr;
given f being Function of S, T such that
A1: f is isomorphic;
assume
A2: for a, b being Element of S ex c being Element of S st c <= a & c <=
b & for c9 being Element of S st c9 <= a & c9 <= b holds c9 <= c;
let x, y be Element of T;
consider c being Element of S such that
A3: c <= f/".x & c <= f/".y and
A4: for c9 being Element of S st c9 <= f/".x & c9 <= f/".y holds c9 <= c by A2;
take f.c;
A5: ex g being Function of T, S st g = f qua Function" & g is monotone by A1,
WAYBEL_0:def 38;
A6: rng f = the carrier of T by A1,WAYBEL_0:66;
A7: f/" = (f qua Function)" by A1,TOPS_2:def 4;
f.c <= f.(f/".x) & f.c <= f.(f/".y) by A1,A3,WAYBEL_0:66;
hence f.c <= x & f.c <= y by A1,A6,A7,FUNCT_1:35;
let z9 be Element of T;
assume z9 <= x & z9 <= y;
then f/".z9 <= f/".x & f/".z9 <= f/".y by A7,A5,WAYBEL_1:def 2;
then f/".z9 <= c by A4;
then f.(f/".z9) <= f.c by A1,WAYBEL_0:66;
hence thesis by A1,A6,A7,FUNCT_1:35;
end;
theorem
for S, T being non empty RelStr st S, T are_isomorphic & S is
with_suprema holds T is with_suprema
proof
let S, T be non empty RelStr;
given f being Function of S, T such that
A1: f is isomorphic;
assume
A2: for a, b being Element of S ex c being Element of S st a <= c & b <=
c & for c9 being Element of S st a <= c9 & b <= c9 holds c <= c9;
let x, y be Element of T;
consider c being Element of S such that
A3: f/".x <= c & f/".y <= c and
A4: for c9 being Element of S st f/".x <= c9 & f/".y <= c9 holds c <= c9 by A2;
take f.c;
A5: ex g being Function of T, S st g = f qua Function" & g is monotone by A1,
WAYBEL_0:def 38;
A6: rng f = the carrier of T by A1,WAYBEL_0:66;
A7: f/" = (f qua Function)" by A1,TOPS_2:def 4;
f.(f/".x) <= f.c & f.(f/".y) <= f.c by A1,A3,WAYBEL_0:66;
hence x <= f.c & y <= f.c by A1,A6,A7,FUNCT_1:35;
let z9 be Element of T;
assume x <= z9 & y <= z9;
then f/".x <= f/".z9 & f/".y <= f/".z9 by A7,A5,WAYBEL_1:def 2;
then c <= f/".z9 by A4;
then f.c <= f.(f/".z9) by A1,WAYBEL_0:66;
hence thesis by A1,A6,A7,FUNCT_1:35;
end;
theorem Th13:
for L being RelStr st L is empty holds L is bounded
proof
let L be RelStr such that
A1: L is empty;
set x = the Element of L;
thus L is lower-bounded
proof
take x;
let a be Element of L;
assume a in the carrier of L;
hence thesis by A1;
end;
take x;
let a be Element of L;
assume a in the carrier of L;
hence thesis by A1;
end;
registration
cluster empty -> bounded for RelStr;
coherence by Th13;
end;
theorem
for S, T being RelStr st S, T are_isomorphic & S is lower-bounded
holds T is lower-bounded
proof
let S, T be RelStr;
given f being Function of S, T such that
A1: f is isomorphic;
per cases;
suppose
S is non empty & T is non empty;
then reconsider s = S, t = T as non empty RelStr;
given X being Element of S such that
A2: X is_<=_than the carrier of S;
reconsider x = X as Element of s;
reconsider g = f as Function of s, t;
reconsider y = g.x as Element of T;
take y;
y is_<=_than g.:[#]S by A1,A2,YELLOW_2:13;
then y is_<=_than rng g by RELSET_1:22;
hence thesis by A1,WAYBEL_0:66;
end;
suppose
S is empty or T is empty;
then T is empty by A1,WAYBEL_0:def 38;
then reconsider T as bounded RelStr;
T is lower-bounded;
hence thesis;
end;
end;
theorem
for S, T being RelStr st S, T are_isomorphic & S is upper-bounded
holds T is upper-bounded
proof
let S, T be RelStr;
given f being Function of S, T such that
A1: f is isomorphic;
per cases;
suppose
S is non empty & T is non empty;
then reconsider s = S, t = T as non empty RelStr;
given X being Element of S such that
A2: X is_>=_than the carrier of S;
reconsider x = X as Element of s;
reconsider g = f as Function of s, t;
reconsider y = g.x as Element of T;
take y;
y is_>=_than g.:[#]S by A1,A2,YELLOW_2:14;
then y is_>=_than rng g by RELSET_1:22;
hence thesis by A1,WAYBEL_0:66;
end;
suppose
S is empty or T is empty;
then T is empty by A1,WAYBEL_0:def 38;
then reconsider T as bounded RelStr;
T is lower-bounded;
hence thesis;
end;
end;
theorem
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
proof
let S, T be non empty RelStr, A be Subset of S, f be Function of S, T such
that
A1: f is isomorphic;
A2: f"(f.:A) c= A by A1,FUNCT_1:82;
A3: rng f = [#]T by A1,WAYBEL_0:66;
A4: f/" = f qua Function " by A1,TOPS_2:def 4;
given a being Element of S such that
A5: A is_<=_than a and
A6: for b being Element of S st A is_<=_than b holds b >= a and
A7: for c being Element of S st A is_<=_than c & for b being Element of
S st A is_<=_than b holds b >= c holds c = a;
take f.a;
thus f.:A is_<=_than f.a by A1,A5,WAYBEL13:19;
A8: f/" is isomorphic by A1,Th10;
A9: dom f = the carrier of S by FUNCT_2:def 1;
then A c= f"(f.:A) by FUNCT_1:76;
then
A10: f"(f.:A) = A by A2;
hereby
let b be Element of T;
assume f.:A is_<=_than b;
then f/".:(f.:A) is_<=_than f/".b by A8,WAYBEL13:19;
then f"(f.:A) is_<=_than f/".b by A1,A3,TOPS_2:55;
then f/".b >= a by A6,A10;
then f.(f/".b) >= f.a by A1,WAYBEL_0:66;
hence b >= f.a by A1,A3,A4,FUNCT_1:35;
end;
let c be Element of T;
assume
A11: f.:A is_<=_than c;
assume
A12: for b being Element of T st f.:A is_<=_than b holds b >= c;
A13: for b being Element of S st A is_<=_than b holds b >= f/".c
proof
let b be Element of S;
assume A is_<=_than b;
then f.:A is_<=_than f.b by A1,WAYBEL13:19;
then f.b >= c by A12;
then f/".(f.b) >= f/".c by A8,WAYBEL_0:66;
hence thesis by A1,A4,A9,FUNCT_1:34;
end;
f/".:(f.:A) is_<=_than f/".c by A8,A11,WAYBEL13:19;
then A is_<=_than f/".c by A1,A3,A10,TOPS_2:55;
then f/".c = a by A7,A13;
hence thesis by A1,A3,A4,FUNCT_1:35;
end;
theorem
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
proof
let S, T be non empty RelStr, A be Subset of S, f be Function of S, T such
that
A1: f is isomorphic;
A2: f"(f.:A) c= A by A1,FUNCT_1:82;
A3: rng f = [#]T by A1,WAYBEL_0:66;
A4: f/" = f qua Function " by A1,TOPS_2:def 4;
given a being Element of S such that
A5: A is_>=_than a and
A6: for b being Element of S st A is_>=_than b holds b <= a and
A7: for c being Element of S st A is_>=_than c & for b being Element of
S st A is_>=_than b holds b <= c holds c = a;
take f.a;
thus f.:A is_>=_than f.a by A1,A5,WAYBEL13:18;
A8: f/" is isomorphic by A1,Th10;
A9: dom f = the carrier of S by FUNCT_2:def 1;
then A c= f"(f.:A) by FUNCT_1:76;
then
A10: f"(f.:A) = A by A2;
hereby
let b be Element of T;
assume f.:A is_>=_than b;
then f/".:(f.:A) is_>=_than f/".b by A8,WAYBEL13:18;
then f"(f.:A) is_>=_than f/".b by A1,A3,TOPS_2:55;
then f/".b <= a by A6,A10;
then f.(f/".b) <= f.a by A1,WAYBEL_0:66;
hence b <= f.a by A1,A3,A4,FUNCT_1:35;
end;
let c be Element of T;
assume
A11: f.:A is_>=_than c;
assume
A12: for b being Element of T st f.:A is_>=_than b holds b <= c;
A13: for b being Element of S st A is_>=_than b holds b <= f/".c
proof
let b be Element of S;
assume A is_>=_than b;
then f.:A is_>=_than f.b by A1,WAYBEL13:18;
then f.b <= c by A12;
then f/".(f.b) <= f/".c by A8,WAYBEL_0:66;
hence thesis by A1,A4,A9,FUNCT_1:34;
end;
f/".:(f.:A) is_>=_than f/".c by A8,A11,WAYBEL13:18;
then A is_>=_than f/".c by A1,A3,A10,TOPS_2:55;
then f/".c = a by A7,A13;
hence thesis by A1,A3,A4,FUNCT_1:35;
end;
begin :: On the product of topological spaces
theorem
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
proof
let S, T be TopStruct;
assume
A1: S,T are_homeomorphic or ex f being Function of S,T st dom f = [#]S &
rng f = [#]T;
per cases by A1;
suppose
S,T are_homeomorphic;
then consider f being Function of S, T such that
A2: f is being_homeomorphism;
rng f = [#]T & dom f = [#]S by A2;
hence thesis;
end;
suppose
ex f being Function of S,T st dom f = [#]S & rng f = [#]T;
hence thesis;
end;
end;
theorem
for T being non empty TopSpace holds T, the TopStruct of T are_homeomorphic
proof
let T be non empty TopSpace;
reconsider f = id T as Function of T, the TopStruct of T;
take f;
thus dom f = [#]T;
thus rng f = [#]T
.= [#]the TopStruct of T;
thus f is one-to-one;
thus f is continuous by YELLOW12:36;
thus thesis by YELLOW12:36;
end;
registration
let T be Scott reflexive non empty TopRelStr;
cluster open -> inaccessible upper for Subset of T;
coherence by WAYBEL11:def 4;
cluster inaccessible upper -> open for Subset of T;
coherence by WAYBEL11:def 4;
end;
theorem
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
proof
let T be TopStruct, x, y be Point of T, X, Y be Subset of T such that
A1: X = {x} and
A2: Cl X c= Cl Y;
X c= Cl X by PRE_TOPC:18;
then
A3: X c= Cl Y by A2;
x in X by A1,TARSKI:def 1;
hence thesis by A3;
end;
theorem
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
proof
let T be TopStruct, x, y be Point of T, Y, V be Subset of T such that
A1: Y = {y};
assume x in Cl Y & V is open & x in V;
then Y meets V by PRE_TOPC:def 7;
hence thesis by A1,ZFMISC_1:50;
end;
theorem
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
proof
let T be TopStruct, x, y be Point of T, X, Y be Subset of T;
assume that
A1: X = {x} and
A2: Y = {y} & for V being Subset of T st V is open holds x in V implies y in V;
let z be object;
assume
A3: z in Cl X;
for V being Subset of T st V is open holds z in V implies Y meets V
proof
let V be Subset of T;
assume that
A4: V is open and
A5: z in V;
X meets V by A3,A4,A5,PRE_TOPC:def 7;
then x in V by A1,ZFMISC_1:50;
hence thesis by A2,A4,ZFMISC_1:48;
end;
hence thesis by A3,PRE_TOPC:def 7;
end;
theorem Th23:
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
proof
let S, T be non empty TopSpace, A be irreducible Subset of S, B be Subset of
T such that
A1: A = B and
A2: the TopStruct of S = the TopStruct of T;
A is non empty closed by YELLOW_8:def 3;
hence B is non empty closed by A1,A2,TOPS_3:79;
let B1, B2 be Subset of T such that
A3: B1 is closed & B2 is closed and
A4: B = B1 \/ B2;
reconsider A1 = B1, A2 = B2 as Subset of S by A2;
A1 is closed & A2 is closed by A2,A3,TOPS_3:79;
hence thesis by A1,A4,YELLOW_8:def 3;
end;
theorem Th24:
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
proof
let S, T be non empty TopSpace, a be Point of S, b be Point of T, A be
Subset of S, B be Subset of T;
assume a = b & A = B & the TopStruct of S = the TopStruct of T & a in A & A
c= Cl{a};
hence b in B & B c= Cl{b} by TOPS_3:80;
end;
theorem Th25:
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
proof
let S, T be TopStruct, A be Subset of S, B be Subset of T such that
A1: A = B and
A2: the TopStruct of S = the TopStruct of T and
A3: for F being Subset-Family of S st F is Cover of A & F is open ex G
being Subset-Family of S st G c= F & G is Cover of A & G is finite;
let F be Subset-Family of T such that
A4: F is Cover of B & F is open;
reconsider K = F as Subset-Family of S by A2;
consider L being Subset-Family of S such that
A5: L c= K & L is Cover of A & L is finite by A1,A2,A3,A4,WAYBEL_9:19;
reconsider G = L as Subset-Family of T by A2;
take G;
thus thesis by A1,A5;
end;
theorem
for S, T being non empty TopSpace st the TopStruct of S = the
TopStruct of T & S is sober holds T is sober
proof
let S, T be non empty TopSpace such that
A1: the TopStruct of S = the TopStruct of T and
A2: for A be irreducible Subset of S ex a being Point of S st a
is_dense_point_of A & for b being Point of S st b is_dense_point_of A holds a =
b;
let B be irreducible Subset of T;
reconsider A = B as irreducible Subset of S by A1,Th23;
consider a being Point of S such that
A3: a is_dense_point_of A and
A4: for b being Point of S st b is_dense_point_of A holds a = b by A2;
reconsider p = a as Point of T by A1;
take p;
thus p is_dense_point_of B by A1,A3,Th24;
let q be Point of T;
reconsider b = q as Point of S by A1;
assume q is_dense_point_of B;
then b is_dense_point_of A by A1,Th24;
hence thesis by A4;
end;
theorem
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
proof
let S, T be non empty TopSpace such that
A1: the TopStruct of S = the TopStruct of T and
A2: for x being Point of S, X being Subset of S st x in X & X is open ex
Y being Subset of S st x in Int Y & Y c= X & Y is compact;
let x be Point of T, X be Subset of T such that
A3: x in X & X is open;
reconsider A = X as Subset of S by A1;
consider B being Subset of S such that
A4: x in Int B & B c= A & B is compact by A1,A2,A3,TOPS_3:76;
reconsider Y = B as Subset of T by A1;
take Y;
thus thesis by A1,A4,Th25,TOPS_3:77;
end;
theorem
for S, T being TopStruct st the TopStruct of S = the TopStruct of T &
S is compact holds T is compact
proof
let S, T be TopStruct such that
A1: the TopStruct of S = the TopStruct of T and
A2: for F being Subset-Family of S st F is Cover of S & F is open ex G
being Subset-Family of S st G c= F & G is Cover of S & G is finite;
let F be Subset-Family of T such that
A3: F is Cover of T & F is open;
reconsider K = F as Subset-Family of S by A1;
consider L being Subset-Family of S such that
A4: L c= K & L is Cover of S & L is finite by A1,A2,A3,WAYBEL_9:19;
reconsider G = L as Subset-Family of T by A1;
take G;
thus thesis by A1,A4;
end;
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;
coherence
proof
x.i is Point of T by FUNCOP_1:7;
hence thesis;
end;
end;
theorem Th29:
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}
proof
let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M,
x, y be Point of product J;
hereby
assume
A1: x in Cl {y};
let i be Element of M;
x in the carrier of product J;
then x in product Carrier J by WAYBEL18:def 3;
then consider f being Function such that
A2: x = f and
A3: dom f = dom Carrier J and
A4: for z being object st z in dom Carrier J holds f.z in (Carrier J).z
by CARD_3:def 5;
A5: i in M;
for G being Subset of J.i st G is open holds x.i in G implies {y.i} meets G
proof
let G be Subset of J.i;
assume that
A6: G is open and
A7: x.i in G;
reconsider G9 = G as Subset of J.i;
[#](J.i) <> {} & proj(J,i) is continuous by WAYBEL18:5;
then
A8: proj(J,i)"G9 is open by A6,TOPS_2:43;
A9: for z being object st z in dom ((Carrier J)+*(i,G)) holds f.z in ((
Carrier J)+*(i,G)).z
proof
let z be object;
assume z in dom ((Carrier J)+*(i,G));
then
A10: z in dom Carrier J by FUNCT_7:30;
per cases;
suppose
z = i;
hence thesis by A2,A7,A10,FUNCT_7:31;
end;
suppose
z <> i;
then ((Carrier J)+*(i,G)).z = (Carrier J).z by FUNCT_7:32;
hence thesis by A4,A10;
end;
end;
A11: product ((Carrier J) +* (i,G9)) = proj(J,i)"G9 by WAYBEL18:4;
dom f = dom ((Carrier J) +* (i,G)) by A3,FUNCT_7:30;
then x in product ((Carrier J) +* (i,G)) by A2,A9,CARD_3:def 5;
then {y} meets proj(J,i)"G9 by A1,A8,A11,PRE_TOPC:def 7;
then y in product ((Carrier J) +* (i,G)) by A11,ZFMISC_1:50;
then consider g being Function such that
A12: y = g and
dom g = dom ((Carrier J) +* (i,G)) and
A13: for z being object st z in dom ((Carrier J) +* (i,G)) holds g.z in
((Carrier J) +* (i,G)).z by CARD_3:def 5;
A14: i in dom Carrier J by A5,PARTFUN1:def 2;
then i in dom ((Carrier J) +* (i,G)) by FUNCT_7:30;
then g.i in ((Carrier J) +* (i,G)).i by A13;
then g.i in G by A14,FUNCT_7:31;
hence thesis by A12,ZFMISC_1:48;
end;
hence x.i in Cl {y.i} by PRE_TOPC:def 7;
end;
reconsider K = product_prebasis J as prebasis of product J by WAYBEL18:def 3;
assume
A15: for i being Element of M holds x.i in Cl {y.i};
for Z being finite Subset-Family of product J st Z c= K & x in
Intersect Z holds Intersect Z meets {y}
proof
let Z be finite Subset-Family of product J;
assume that
A16: Z c= K and
A17: x in Intersect Z;
for Y being set st Y in Z holds y in Y
proof
let Y be set;
y in the carrier of product J;
then y in product Carrier J by WAYBEL18:def 3;
then consider g being Function such that
A18: y = g and
A19: dom g = dom Carrier J and
A20: for z being object st z in dom Carrier J holds g.z in (Carrier J).
z by CARD_3:def 5;
assume
A21: Y in Z;
then Y in K by A16;
then consider
i being set, W being TopStruct, V being Subset of W such that
A22: i in M and
A23: V is open and
A24: W = J.i and
A25: Y = product ((Carrier J)+*(i,V)) by WAYBEL18:def 2;
reconsider i as Element of M by A22;
reconsider V as Subset of (J.i) by A24;
x in Y by A17,A21,SETFAM_1:43;
then
A26: ex f being Function st x = f & dom f = dom ((Carrier J)+* (i,V)) &
for z being object st z in dom ((Carrier J)+*(i,V))
holds f.z in (( Carrier J)+*(i
,V)).z by A25,CARD_3:def 5;
x.i in Cl {y.i} by A15;
then
A27: x.i in V implies {y.i} meets V by A23,A24,PRE_TOPC:def 7;
A28: for z being object st z in dom ((Carrier J)+*(i,V)) holds g.z in ((
Carrier J)+*(i,V)).z
proof
let z be object;
assume
A29: z in dom ((Carrier J)+*(i,V));
then
A30: z in dom Carrier J by FUNCT_7:30;
per cases;
suppose
A31: z = i;
then ((Carrier J)+*(i,V)).z = V by A30,FUNCT_7:31;
hence thesis by A27,A26,A18,A29,A31,ZFMISC_1:50;
end;
suppose
z <> i;
then ((Carrier J)+*(i,V)).z = (Carrier J).z by FUNCT_7:32;
hence thesis by A20,A30;
end;
end;
dom g = dom ((Carrier J)+*(i,V)) by A19,FUNCT_7:30;
hence thesis by A25,A18,A28,CARD_3:def 5;
end;
then y in {y} & y in Intersect Z by SETFAM_1:43,TARSKI:def 1;
hence thesis by XBOOLE_0:3;
end;
hence thesis by YELLOW_9:38;
end;
theorem
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}
proof
let M be non empty set, T be non empty TopSpace, x, y be Point of product (M
--> T);
reconsider J = M --> T as TopStruct-yielding non-Empty ManySortedSet of M;
reconsider x9 = x, y9 = y as Point of product J;
thus x in Cl {y} implies for i being Element of M holds x.i in Cl {y.i}
proof
assume
A1: x in Cl {y};
let i be Element of M;
x9.i in Cl {y9.i} by A1,Th29;
hence thesis by FUNCOP_1:7;
end;
assume
A2: for i being Element of M holds x.i in Cl {y.i};
for i being Element of M holds x9.i in Cl {y9.i}
proof
let i be Element of M;
x.i in Cl {y.i} by A2;
hence thesis by FUNCOP_1:7;
end;
hence thesis by Th29;
end;
theorem Th31:
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}
proof
let M be non empty set, i be Element of M, J be TopStruct-yielding non-Empty
ManySortedSet of M, x be Point of product J;
consider f being object such that
A1: f in Cl {x} by XBOOLE_0:def 1;
A2: f in the carrier of product J by A1;
thus pi(Cl {x}, i) c= Cl {x.i}
proof
let a be object;
assume a in pi(Cl {x}, i);
then ex f being Function st f in Cl {x} & a = f.i by CARD_3:def 6;
hence thesis by Th29;
end;
reconsider f as Element of product J by A1;
let a be object;
set y = f +* (i .--> a);
A3: dom Carrier J = M by PARTFUN1:def 2;
A4: f in product Carrier J by A2,WAYBEL18:def 3;
then
A5: dom f = M by A3,CARD_3:9;
A6: dom (i .--> a) = {i} by FUNCOP_1:13;
assume
A7: a in Cl {x.i};
A8: for m being object st m in dom Carrier J holds y.m in (Carrier J).m
proof
let m be object;
assume
A9: m in dom Carrier J;
then
A10: ex R being 1-sorted st R = J.m & Carrier J.m = the carrier of R by
PRALG_1:def 13;
per cases;
suppose
A11: m = i;
then y.m = a by FUNCT_7:94;
hence thesis by A7,A10,A11;
end;
suppose
m <> i;
then not m in dom (i .--> a) by A6,TARSKI:def 1;
then y.m = f.m by FUNCT_4:11;
hence thesis by A4,A9,CARD_3:9;
end;
end;
dom y = dom f \/ dom (i .--> a) by FUNCT_4:def 1
.= M \/ {i} by A5,FUNCOP_1:13
.= M by ZFMISC_1:40;
then y in product Carrier J by A3,A8,CARD_3:9;
then reconsider y = f +* (i .--> a) as Element of product J by WAYBEL18:def 3
;
for m being Element of M holds y.m in Cl {x.m}
proof
let m be Element of M;
per cases;
suppose
m = i;
hence thesis by A7,FUNCT_7:94;
end;
suppose
m <> i;
then not m in dom (i .--> a) by A6,TARSKI:def 1;
then y.m = f.m by FUNCT_4:11;
hence thesis by A1,Th29;
end;
end;
then
A12: f +* (i .--> a) in Cl {x} by Th29;
(f +* (i .--> a)).i = a by FUNCT_7:94;
hence thesis by A12,CARD_3:def 6;
end;
theorem
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}
proof
let M be non empty set, i be Element of M, T be non empty TopSpace, x be
Point of product (M --> T);
(M --> T).i = T by FUNCOP_1:7;
hence thesis by Th31;
end;
theorem
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
proof
let X, Y be non empty TopStruct, f be Function of X, Y, g be Function of Y,
X such that
A1: f = id X and
A2: g = id X and
A3: f is continuous and
A4: g is continuous;
A5: the carrier of X = dom f by FUNCT_2:def 1
.= the carrier of Y by A2,FUNCT_2:def 1;
A6: [#]Y <> {};
A7: [#]X <> {};
the topology of X = the topology of Y
proof
hereby
let A be object;
assume
A8: A in the topology of X;
then reconsider B = A as Subset of X;
B is open by A8;
then
A9: g"B is open by A4,A7,TOPS_2:43;
g"B = B by A2,FUNCT_2:94;
hence A in the topology of Y by A9;
end;
let A be object;
assume
A10: A in the topology of Y;
then reconsider B = A as Subset of Y;
B is open by A10;
then
A11: f"B is open by A3,A6,TOPS_2:43;
f"B = B by A1,A5,FUNCT_2:94;
hence thesis by A11;
end;
hence thesis by A5;
end;
theorem
for X, Y being non empty TopSpace, f being Function of X, Y st corestr
f is continuous holds f is continuous
proof
let X, Y be non empty TopSpace, f be Function of X, Y such that
A1: corestr f is continuous;
corestr f = f by WAYBEL18:def 7;
hence thesis by A1,PRE_TOPC:26;
end;
registration
let X be non empty TopSpace, Y be non empty SubSpace of X;
cluster incl Y -> continuous;
coherence by TMAP_1:87;
end;
theorem
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
proof
let T be non empty TopSpace, f be Function of T, T such that
A1: f*f = f;
set cf = corestr f, i = incl Image f;
for x being object st x in the carrier of Image f holds (cf*i).x = (id
Image f).x
proof
A2: the carrier of Image f c= the carrier of T by BORSUK_1:1;
let x be object;
assume
A3: x in the carrier of Image f;
the carrier of Image f = rng f by WAYBEL18:9;
then
A4: ex y being object st y in dom f & f.y = x by A3,FUNCT_1:def 3;
thus (cf*i).x = cf.(i.x) by A3,FUNCT_2:15
.= cf.x by A3,A2,TMAP_1:84
.= f.x by WAYBEL18:def 7
.= x by A1,A4,FUNCT_2:15
.= (id Image f).x by A3,FUNCT_1:18;
end;
hence thesis;
end;
theorem
for Y being non empty TopSpace, W being non empty SubSpace of Y holds
corestr incl W is being_homeomorphism
proof
let Y be non empty TopSpace, W be non empty SubSpace of Y;
set ci = corestr incl W;
thus dom ci = [#]W by FUNCT_2:def 1;
thus
A1: rng ci = [#]Image incl W by FUNCT_2:def 3;
A2: ci = incl W by WAYBEL18:def 7
.= (id Y)|W by TMAP_1:def 6
.= (id the carrier of Y)|the carrier of W by TMAP_1:def 4;
hence
A3: ci is one-to-one by FUNCT_1:52;
A4: for P being Subset of W st P is open holds ci/""P is open
proof
let P be Subset of W;
assume P in the topology of W;
then
A5: ex Q being Subset of Y st Q in the topology of Y & P = Q /\ [#]W by
PRE_TOPC:def 4;
A6: the carrier of W is non empty Subset of Y by BORSUK_1:1;
then
A7: P is Subset of Y by XBOOLE_1:1;
A8: [#]W = rng ((id the carrier of Y)|the carrier of W) by A6,Th2
.= rng ((id Y)|W) by TMAP_1:def 4
.= rng incl W by TMAP_1:def 6
.= [#]Image incl W by WAYBEL18:9;
ci/""P = ((id the carrier of Y)|the carrier of W).:P by A1,A2,A3,TOPS_2:54
.= (id the carrier of Y).:P by FUNCT_2:97
.= P by A7,FUNCT_1:92;
hence ci/""P in the topology of Image incl W by A5,A8,PRE_TOPC:def 4;
end;
thus ci is continuous by WAYBEL18:10;
[#]W <> {};
hence thesis by A4,TOPS_2:43;
end;
theorem Th37:
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
proof
let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M
such that
A1: for i be Element of M holds J.i is T_0 TopSpace;
for x, y being Point of product J st x <> y holds Cl {x} <> Cl {y}
proof
let x, y be Point of product J such that
A2: x <> y and
A3: Cl {x} = Cl {y};
y in the carrier of product J;
then y in product Carrier J by WAYBEL18:def 3;
then dom y = dom Carrier J by CARD_3:9;
then
A4: dom y = M by PARTFUN1:def 2;
x in the carrier of product J;
then x in product Carrier J by WAYBEL18:def 3;
then dom x = dom Carrier J by CARD_3:9;
then dom x = M by PARTFUN1:def 2;
then consider i being object such that
A5: i in M and
A6: x.i <> y.i by A2,A4,FUNCT_1:2;
reconsider i as Element of M by A5;
A7: pi(Cl {y}, i) = Cl {y.i} by Th31;
J.i is T_0 TopSpace & pi(Cl {x}, i) = Cl {x.i} by A1,Th31;
hence contradiction by A3,A6,A7,TSP_1:def 5;
end;
hence thesis by TSP_1:def 5;
end;
registration
let I be non empty set, T be non empty T_0 TopSpace;
cluster product (I --> T) -> T_0;
coherence
proof
for i being Element of I holds (I --> T).i is T_0 TopSpace by FUNCOP_1:7;
hence thesis by Th37;
end;
end;
theorem Th38:
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
proof
let M be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of M
such that
A1: for i be Element of M holds J.i is T_1 TopSpace-like;
for p being Point of product J holds {p} is closed
proof
let p be Point of product J;
{p} = Cl {p}
proof
thus {p} c= Cl {p} by PRE_TOPC:18;
let a be object;
assume
A2: a in Cl {p};
then reconsider a, p as Element of product J;
A3: for i being object st i in M holds a.i = p.i
proof
let i be object;
assume i in M;
then reconsider i as Element of M;
J.i is TopSpace & J.i is T_1 by A1;
then
A4: {p.i} is closed by URYSOHN1:19;
a.i in Cl {p.i} by A2,Th29;
then a.i in {p.i} by A4,PRE_TOPC:22;
hence thesis by TARSKI:def 1;
end;
p in the carrier of product J;
then p in product Carrier J by WAYBEL18:def 3;
then dom p = dom Carrier J by CARD_3:9;
then
A5: dom p = M by PARTFUN1:def 2;
a in the carrier of product J;
then a in product Carrier J by WAYBEL18:def 3;
then dom a = dom Carrier J by CARD_3:9;
then dom a = M by PARTFUN1:def 2;
then a = p by A5,A3,FUNCT_1:2;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
hence thesis by URYSOHN1:19;
end;
registration
let I be non empty set, T be non empty T_1 TopSpace;
cluster product (I --> T) -> T_1;
coherence
proof
for i being Element of I holds (I --> T).i is T_1 TopSpace-like by
FUNCOP_1:7;
hence thesis by Th38;
end;
end;