:: Some Remarks about Product Spaces
:: by Sebastian Koch
::
:: Received September 29, 2018
:: Copyright (c) 2018-2026 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 STRUCT_0, SUBSET_1, PRE_TOPC, FUNCT_1, FUNCT_2, RELAT_1,
XBOOLE_0, TARSKI, ZFMISC_1, ORDINAL2, TOPS_2, RCOMP_1, T_0TOPSP,
SETFAM_1, RLVECT_3, CARD_1, EQREL_1, CARD_3, PARTFUN1, FUNCT_7, WAYBEL18,
FUNCOP_1, TOPS_5, PBOOLE, RLVECT_2, WAYBEL_3, PRALG_1, FUNCT_4, CANTOR_1,
FINSET_1, ALGSPEC1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, SETFAM_1, PBOOLE,
RELAT_1, FUNCT_1, FINSET_1, ORDINAL1, RELSET_1, PARTFUN1, TOPS_2,
FUNCT_2, FUNCT_3, DOMAIN_1, CARD_1, CARD_3, FUNCOP_1, FUNCT_4, FUNCT_7,
EQREL_1, STRUCT_0, PRALG_1, ALGSPEC1, PRE_TOPC, BORSUK_1, T_0TOPSP,
CANTOR_1, BORSUK_2, BORSUK_3, WAYBEL_3, WAYBEL18;
constructors TOPS_2, CANTOR_1, TOPALG_6, MONOID_0, WAYBEL18, FUNCT_4, FUNCT_7,
ALGSPEC1, BORSUK_3;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_1,
BORSUK_1, RELSET_1, CARD_1, ORDINAL1, NAT_1, XBOOLE_0, MONOID_0,
PRE_POLY, FUNCOP_1, CARD_3, FUNCT_4, FINSET_1, WAYBEL18, RELAT_1, PBOOLE,
TOPGRP_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI;
theorems TARSKI, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, EQREL_1,
ORDERS_5, TOPS_2, T_0TOPSP, TOPREALA, STRUCT_0, PRE_TOPC, YELLOW12,
BORSUK_1, XBOOLE_1, ENUMSET1, ZFMISC_1, WAYBEL18, WAYBEL_3, FUNCOP_1,
PARTFUN1, CARD_1, CARD_3, PENCIL_3, CANTOR_1, SETFAM_1, FINSET_1,
YELLOW_9, FUNCT_7, FUNCT_4, CARD_2, YELLOW_8, RELSET_2, FUNCT_3,
YELLOW17, PRALG_1, NECKLACE, PBOOLE, ALGSPEC1, PUA2MSS1, XTUPLE_0,
LATTICE2;
schemes FUNCT_1, FUNCT_2, SUBSET_1, PBOOLE;
begin :: Preliminaries
:: into FUNCT_1 ?
:: compare FUNCT_1:4
theorem Th1:
for f being one-to-one Function, y being object st rng f = {y}
holds dom f = {f".y}
proof
let f be one-to-one Function, y be object;
assume A1: rng f = {y};
then y in rng f by TARSKI:def 1;
then consider x0 being object such that
A2: x0 in dom f & f.x0 = y by FUNCT_1:def 3;
for x being object holds x in dom f iff x = f".y
proof
let x be object;
hereby
assume A3: x in dom f;
then f.x in rng f by FUNCT_1:3;
then f.x = y by A1, TARSKI:def 1;
hence x = f".y by A3, FUNCT_1:34;
end;
assume x = f".y;
hence thesis by A2, FUNCT_1:34;
end;
hence thesis by TARSKI:def 1;
end;
:: into FUNCT_1 ?
theorem Th2:
for f being one-to-one Function, y1, y2 being object st rng f = {y1, y2}
holds dom f = {f".y1, f".y2}
proof
let f be one-to-one Function, y1, y2 be object;
assume A1: rng f = {y1,y2};
then A2: y1 in rng f & y2 in rng f by TARSKI:def 2;
then consider x1 being object such that
A3: x1 in dom f & f.x1 = y1 by FUNCT_1:def 3;
consider x2 being object such that
A4: x2 in dom f & f.x2 = y2 by A2, FUNCT_1:def 3;
for x being object holds x in dom f iff x = f".y1 or x = f".y2
proof
let x be object;
thus x in dom f implies x = f".y1 or x = f".y2
proof
assume A5: x in dom f;
then f.x in rng f by FUNCT_1:3;
then f.x = y1 or f.x = y2 by A1, TARSKI:def 2;
hence thesis by A5, FUNCT_1:34;
end;
thus thesis by A3,A4, FUNCT_1:34;
end;
hence thesis by TARSKI:def 2;
end;
:: into PARTFUN1 ?
registration
let X, Y be set;
cluster empty X-defined Y-valued one-to-one for Function;
existence
proof
take f = the empty one-to-one Function;
dom f = {} & rng f = {};
hence thesis by RELAT_1:def 18, RELAT_1:def 19, XBOOLE_1:2;
end;
end;
:: into FINSET_1 ?
registration
let T,S be set;
let f be Function of T,S;
let G be finite Subset-Family of T;
cluster f.:G -> finite;
coherence
proof
defpred P[object,object] means
ex A being Subset of T st $1 = A & $2 = f.:A;
A1: for x,y1,y2 be object st x in G & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x being object st x in G ex y being object st P[x,y]
proof
let x be object;
assume x in G;
then reconsider A = x as Subset of T;
take f.:A, A;
thus thesis;
end;
consider g being Function such that
A3: dom g = G & for x being object st x in G holds P[x,g.x]
from FUNCT_1:sch 2(A1,A2);
for y being object holds y in rng g iff y in f.:G
proof
let y be object;
hereby
assume y in rng g;
then consider x being object such that
A4: x in dom g & g.x = y by FUNCT_1:def 3;
ex A being Subset of T st
x = A & y = f.:A by A3, A4;
hence y in f.:G by A3, A4, FUNCT_2:def 10;
end;
assume A6: y in f.:G;
then reconsider B = y as Subset of S;
consider A being Subset of T such that
A7: A in G & B = f.:A by A6, FUNCT_2:def 10;
ex A0 being Subset of T st
A = A0 & g.A = f.:A0 by A3, A7;
hence thesis by A3, A7, FUNCT_1:def 3;
end;
then rng g = f.:G by TARSKI:2;
hence thesis by A3, FINSET_1:8;
end;
end;
:: into RELSET_2 ?
theorem Th3:
for A being set, F being Subset-Family of A, R be Relation holds
R.: meet F c= meet {R.:X where X is Subset of A : X in F}
proof
let A be set, F be Subset-Family of A, R be Relation;
per cases;
suppose meet F = {};
then R.: meet F = {};
hence thesis by XBOOLE_1:2;
end;
suppose meet F <> {};
then consider X0 being object such that
A1: X0 in F by SETFAM_1:1, XBOOLE_0:def 1;
reconsider X0 as Subset of A by A1;
A2: R.:X0 in {R.:X where X is Subset of A : X in F} by A1;
let y be object;
assume y in R.: meet F;
then consider x being object such that
A3: [x,y] in R & x in meet F by RELAT_1:def 13;
now
let Y be set;
assume Y in {R.:X where X is Subset of A : X in F};
then consider X being Subset of A such that
A4: Y = R.:X & X in F;
x in X by A3, A4, SETFAM_1:def 1;
hence y in Y by A3, A4, RELAT_1:def 13;
end;
hence y in meet {R.:X where X is Subset of A : X in F}
by A2, SETFAM_1:def 1;
end;
end;
:: into RELSET_2 ?
theorem Th4:
for A being set, F being Subset-Family of A, f be one-to-one Function holds
f.: meet F = meet {f.:X where X is Subset of A : X in F}
proof
let A be set, F be Subset-Family of A, f be one-to-one Function;
set S = {f.:X where X is Subset of A : X in F};
A7: meet S c= f.: meet F
proof
let y be object;
assume A1: y in meet S;
then consider z being object such that
A2: z in S by XBOOLE_0:def 1, SETFAM_1:1;
consider X0 being Subset of A such that
A3: z = f.:X0 & X0 in F by A2;
A4: y in f.:X0 by A1, A2, A3, SETFAM_1:def 1;
ex x being object st x in dom f & x in meet F & y = f.x
proof
consider x0 being object such that
A5: x0 in dom f & x0 in X0 & y = f.x0 by A4, FUNCT_1:def 6;
take x0;
for X being set st X in F holds x0 in X
proof
let X be set;
assume X in F;
then f.:X in S;
then y in f.:X by A1, SETFAM_1:def 1;
then consider x being object such that
A6: x in dom f & x in X & y = f.x by FUNCT_1:def 6;
thus thesis by A5, A6, FUNCT_1:def 4;
end;
hence thesis by A3, A5, SETFAM_1:def 1;
end;
hence thesis by FUNCT_1:def 6;
end;
f.: meet F c= meet S by Th3;
hence thesis by A7, XBOOLE_0:def 10;
end;
:: into EQREL_1 ?
theorem Th5:
for X being set, Y being non empty set, f being Function of X, Y
holds {f"{y} where y is Element of Y : y in rng f} is a_partition of X
proof
let X be set, Y be non empty set, f be Function of X, Y;
set P = {f"{y} where y is Element of Y : y in rng f};
for x being object holds x in X iff ex A being set st x in A & A in P
proof
let x be object;
hereby
assume A1: x in X;
then A2: f.x in rng f & f.x in Y by FUNCT_2:4, FUNCT_2:5;
reconsider A = f"{f.x} as set;
take A;
f.x in {f.x} by TARSKI:def 1;
hence x in A by A1, FUNCT_2:38;
thus A in P by A2;
end;
given A being set such that
A3: x in A & A in P;
consider y being Element of Y such that
A4: f"{y} = A & y in rng f by A3;
thus x in X by A3, A4;
end;
then A5: union P = X by TARSKI:def 4;
A6: for A being Subset of X st A in P holds A <> {} &
for B being Subset of X st B in P holds A = B or A misses B
proof
let A be Subset of X;
assume A in P;
then consider y1 being Element of Y such that
A7: A = f"{y1} & y1 in rng f;
consider x being object such that
A8: x in X & y1 = f.x by A7, FUNCT_2:11;
f.x in {y1} by A8, TARSKI:def 1;
hence A <> {} by A7, A8, FUNCT_2:38;
let B be Subset of X;
assume B in P;
then ex y2 being Element of Y st B = f"{y2} & y2 in rng f;
hence thesis by A7, ZFMISC_1:11, FUNCT_1:71;
end;
P c= bool X
proof
let x be object;
assume x in P;
then ex y being Element of Y st f"{y} = x & y in rng f;
hence thesis;
end;
hence thesis by A5, A6, EQREL_1:def 4;
end;
:: into FUNCOP_1 ?
theorem
for X being non empty set, x,y being object st X --> x = X --> y holds x = y
proof
let X be non empty set, x,y be object;
assume A1: X --> x = X --> y;
rng(X --> x) = {x} & rng(X --> y) = {y} by FUNCOP_1:8;
hence thesis by A1, ZFMISC_1:3;
end;
:: into FUNCOP_1 ?
theorem Th7:
for i being object, J being ManySortedSet of {i} holds J = {i} --> J.i
proof
let i be object, J be ManySortedSet of {i};
A1: dom J = {i} by PARTFUN1:def 2
.= dom ({i} --> J.i);
for x being object st x in dom J holds J.x = ({i} --> J.i).x
proof
let x be object;
assume x in dom J;
then A2: x = i by TARSKI:def 1;
({i} --> J.i).i = (i .--> J.i).i by FUNCOP_1:def 9 .= J.i by FUNCOP_1:72;
hence thesis by A2;
end;
hence thesis by A1, FUNCT_1:2;
end;
:: into CARD_1 ?
theorem Th8:
for I being 2-element set, i,j being Element of I st i <> j holds I = {i,j}
proof
let I be 2-element set;
let i,j be Element of I;
assume A1: i <> j;
for x being object holds x = i or x = j iff x in I
proof
let x be object;
thus x = i or x = j implies x in I;
assume A2: x in I;
assume x <> i & x <> j;
then A3: card {x,i,j} = 3 by A1, CARD_2:58;
{x,i,j} c= I
proof
let z be object;
assume z in {x,i,j};
then z = x or z = i or z = j by ENUMSET1:def 1;
hence thesis by A2;
end;
then card {x,i,j} c= card I by CARD_1:11;
then A4: {0,1,2} c= 2 by A3, CARD_1:def 7, CARD_1:51;
2 in {0,1,2} by ENUMSET1:def 1;
then 2 in 2 by A4;
hence contradiction;
end;
hence I = {i,j} by TARSKI:def 2;
end;
:: into FUNCT_4 ?
:: compare FUNCT_4:66
theorem Th9:
for I being 2-element set, f being ManySortedSet of I
for i,j being Element of I st i <> j holds f = (i,j) --> (f.i,f.j)
proof
let I be 2-element set, f be ManySortedSet of I;
let i,j be Element of I;
assume A1: i <> j;
dom f = I by PARTFUN1:def 2
.= {i,j} by A1, Th8;
hence thesis by FUNCT_4:66;
end;
:: into FUNCT_4 ?
theorem Th10:
for a,b,c,d being object st a <> b holds (a,b) --> (c,d) = (b,a) --> (d,c)
proof
let a,b,c,d be object;
assume A1: a <> b;
A2: dom (a,b) --> (c,d) = {a,b} by FUNCT_4:62;
then A3: dom (a,b) --> (c,d) = dom (b,a) --> (d,c) by FUNCT_4:62;
for x being object st x in dom (a,b) --> (c,d)
holds ((a,b) --> (c,d)).x = ((b,a) --> (d,c)).x
proof
let x be object;
assume x in dom (a,b) --> (c,d);
then per cases by A2, TARSKI:def 2;
suppose A4: x = a;
hence ((a,b) --> (c,d)).x = c by A1, FUNCT_4:63
.= ((b,a) --> (d,c)).x by A4, FUNCT_4:63;
end;
suppose A5: x = b;
hence ((a,b) --> (c,d)).x = d by FUNCT_4:63
.= ((b,a) --> (d,c)).x by A1, A5, FUNCT_4:63;
end;
end;
hence thesis by A3, FUNCT_1:2;
end;
:: into FUNCT_4 ?
theorem Th11:
for f being Function, i, j being object st i in dom f & j in dom f
holds f = f +* (i,j) --> (f.i,f.j)
proof
let f be Function, i, j be object;
assume A1: i in dom f & j in dom f;
thus f = f +* (j .--> f.j) by A1, FUNCT_4:7, LATTICE2:5
.= (f +* (i .--> f.i)) +* (j .--> f.j) by A1, FUNCT_4:7, LATTICE2:5
.= f +* ((i .--> f.i) +* (j .--> f.j)) by FUNCT_4:14
.= f +* (i,j) --> (f.i,f.j) by FUNCT_4:def 4;
end;
:: into FUNCT_4 ?
:: compare FUNCT_7:15, FUNCT_4:114
theorem Th12:
for x,y,z being object holds (x .--> y) +* (x .--> z) = x .--> z
proof
let x,y,z be object;
A1: dom (x .--> y) = dom ({x} --> y) by FUNCOP_1:def 9
.= {x};
dom (x .--> z) = dom ({x} --> z) by FUNCOP_1:def 9
.= {x};
hence thesis by A1, FUNCT_4:19;
end;
:: into PBOOLE ?
registration
cluster non non-empty for Function;
existence
proof
take the empty-yielding ManySortedSet of the non empty set;
thus thesis;
end;
end;
:: BEGIN into CARD_3 ?
theorem Th13:
for X, Y being non empty set, y being Element of Y
holds X --> y in product (X --> Y)
proof
let X, Y be non empty set, y be Element of Y;
set f = X --> y;
A1: dom f = X
.= dom (X --> Y);
for x being object st x in dom (X --> Y) holds f.x in (X --> Y).x
proof
let x be object;
assume A2: x in dom (X --> Y);
then A3: (X --> Y).x = Y by FUNCOP_1:7;
f.x = y by A2, FUNCOP_1:7;
hence thesis by A3;
end;
hence thesis by A1, CARD_3:def 5;
end;
theorem Th14:
for X being non empty set, Y being set, Z being Subset of Y
holds product(X --> Z) c= product (X --> Y)
proof
let X be non empty set, Y be set, Z be Subset of Y;
let x be object;
assume x in product(X --> Z);
then consider g being Function such that
A1: x = g & dom g = dom (X --> Z) and
A2: for y being object st y in dom (X --> Z) holds g.y in (X --> Z).y
by CARD_3:def 5;
now
let y be object;
assume a4: y in dom (X --> Y);
then A4: y in X;
A5: (X --> Z).y = Z & (X --> Y).y = Y by a4,FUNCOP_1:7;
y in dom (X --> Z) by A4;
then g.y in (X --> Z).y by A2;
hence g.y in (X --> Y).y by A5;
end;
hence thesis by A1, CARD_3:def 5;
end;
theorem Th15:
for X being non empty set, i being object holds
product ({i} --> X) = {{i} --> x where x is Element of X : not contradiction}
proof
let X be non empty set, i be object;
set S = {{i} --> x where x is Element of X : not contradiction};
for z being object holds z in product ({i} --> X) iff z in S
proof
let z be object;
hereby
assume z in product ({i} --> X);
then consider f being Function such that
A1: z = f & dom f = dom ({i} --> X) and
A2: for y being object st y in dom ({i} --> X)
holds f.y in ({i} --> X).y by CARD_3:def 5;
A3: dom f = {i} by A1;
for y being object st y in dom f holds f.y = f.i
by A1,TARSKI:def 1;
then A4: f = {i} --> f.i by A3, FUNCOP_1:11;
i in dom ({i} --> X) by TARSKI:def 1;
then f.i in ({i} --> X).i by A2;
then f.i in (i .--> X). i by FUNCOP_1:def 9;
then f.i in X by FUNCOP_1:72;
hence z in S by A1, A4;
end;
assume z in S;
then ex x being Element of X st
z = {i} --> x;
hence thesis by Th13;
end;
hence thesis by TARSKI:2;
end;
theorem Th16:
for X being non empty set, i, f being object
holds f in product({i} --> X) iff ex x being Element of X st f = {i} --> x
proof
let X be non empty set, i,f be object;
hereby
assume f in product({i} --> X);
then f in {{i} --> x where x is Element of X : not contradiction} by Th15;
hence ex x being Element of X st f = {i} --> x;
end;
assume ex x being Element of X st f = {i} --> x;
then f in {{i} --> x where x is Element of X : not contradiction};
hence thesis by Th15;
end;
:: compare YELLOW17:8
theorem
for X being non empty set, i being object, x being Element of X
holds proj({i} --> X,i).({i} --> x) = x
proof
let X be non empty set, i be object, x be Element of X;
{i} --> x in product ({i} --> X) by Th13;
then {i} --> x in dom proj({i} --> X,i) by CARD_3:def 16;
hence proj({i} --> X,i).({i} --> x) = ({i} --> x).i by CARD_3:def 16
.= (i .--> x).i by FUNCOP_1:def 9
.= x by FUNCOP_1:72;
end;
:: corrolary from CARD_3:26
Lm1:
for f being Function holds rng f = {{}} implies product f = {}
proof
let f be Function;
assume rng f = {{}};
then {} in rng f by TARSKI:def 1;
hence thesis by CARD_3:26;
end;
:: compare CARD_3:26
theorem
for X, Y being set holds X <> {} & Y = {} iff product (X --> Y) = {}
proof
let X, Y be set;
hereby
assume X <> {} & Y = {};
then rng(X --> Y) = {{}} by FUNCOP_1:8;
then {} in rng(X --> Y) by TARSKI:def 1;
hence product(X --> Y) = {} by CARD_3:26;
end;
assume product (X --> Y) = {};
hence thesis;
end;
registration
let f be empty Function, x be object;
cluster proj(f,x) -> trivial;
coherence
proof
dom proj(f,x) = {{}} by CARD_3:10, CARD_3:def 16;
hence thesis;
end;
end;
theorem Th19:
for f being trivial Function, x being object st x in dom f
holds proj(f,x) is one-to-one
proof
let f be trivial Function, x be object;
assume A1: x in dom f;
then consider t being object such that
A2: dom f = {t} by ZFMISC_1:131;
A3: dom f = {x} by A1, A2, TARSKI:def 1;
set F = proj(f,x);
for y, z being object st y in dom F & z in dom F & F.y = F.z holds y = z
proof
let y,z be object;
assume A4: y in dom F & z in dom F & F.y = F.z;
then consider g being Function such that
A5: y = g & dom g = dom f and
for s being object st s in dom f holds g.s in f.s
by CARD_3:def 5;
consider h being Function such that
A6: z = h & dom h = dom f and
for s being object st s in dom f holds h.s in f.s
by A4, CARD_3:def 5;
A7: g.x = F.z by A4, A5, CARD_3:def 16
.= h.x by A4, A6, CARD_3:def 16;
for s being object st s in dom g holds g.s = h.s
proof
let s be object;
assume s in dom g;
then s = x by A3, A5, TARSKI:def 1;
hence thesis by A7;
end;
hence thesis by A5, A6, FUNCT_1:2;
end;
hence thesis by FUNCT_1:def 4;
end;
registration
let x,y be object;
cluster proj(x .--> y,x) -> one-to-one;
coherence
proof
x in {x} by TARSKI:def 1;
then x in dom({x} --> y);
then A1: x in dom(x .--> y) by FUNCOP_1:def 9;
x is set & y is set by TARSKI:1;
hence thesis by A1, Th19;
end;
end;
registration
let I be 1-element set, J be ManySortedSet of I, i be Element of I;
cluster proj(J,i) -> one-to-one;
coherence
proof
dom J = I by PARTFUN1:def 2;
then J is trivial & i in dom J;
hence thesis by Th19;
end;
end;
theorem
for X being non empty set, Y being Subset of X, i being object
holds proj({i} --> X,i).:product ({i} --> Y) = Y
proof
let X be non empty set, Y be Subset of X, i be object;
per cases;
suppose A1: Y is empty;
then rng ({i} --> Y) = {{}} by FUNCOP_1:8;
then product ({i} --> Y) = {} by Lm1;
hence thesis by A1;
end;
suppose A2: Y is non empty;
for x being object holds x in proj({i} --> X,i).:product ({i} --> Y)
iff x in Y
proof
let x be object;
hereby
assume x in proj({i} --> X,i).:product ({i} --> Y);
then consider y being object such that
A3: y in dom proj({i} --> X,i) & y in product ({i} --> Y) and
A4: x = proj({i} --> X,i).y by FUNCT_1:def 6;
consider z being Element of Y such that
A5: y = {i} --> z by A2, A3, Th16;
reconsider y as Function by A5;
x = y.i by A3, A4, CARD_3:def 16
.= (i .--> z).i by A5, FUNCOP_1:def 9
.= z by FUNCOP_1:72;
hence x in Y by A2;
end;
assume x in Y;
then reconsider z = x as Element of Y;
ex y being object st y in dom proj({i} --> X,i) &
y in product ({i} --> Y) & x = proj({i} --> X,i).y
proof
set y = {i} --> z;
take y;
y in product ({i} --> Y) by A2, Th13;
then y in product ({i} --> X) by Th14, TARSKI:def 3;
hence A7: y in dom proj({i} --> X,i) &
y in product ({i} --> Y) by A2,Th13,CARD_3:def 16;
thus x = (i .--> z).i by FUNCOP_1:72
.= y.i by FUNCOP_1:def 9
.= proj({i} --> X,i).y by A7, CARD_3:def 16;
end;
hence thesis by FUNCT_1:def 6;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th21:
for f, g being non-empty Function, i, x being object
st x in product f /\ product(f+*g) holds proj(f,i).x = proj(f+*g,i).x
proof
let f, g be non-empty Function, i, x being object;
assume A1: x in product f /\ product(f+*g);
then x in product f by XBOOLE_0:def 4;
then reconsider h = x as Function;
x in product f & x in product(f+*g) by A1, XBOOLE_0:def 4;
then A2: x in dom proj(f,i) & x in dom proj(f+*g,i) by CARD_3:def 16;
hence proj(f,i).x = h.i by CARD_3:def 16
.= proj(f+*g,i).x by A2, CARD_3:def 16;
end;
theorem Th22:
for f, g being non-empty Function, i being object, A being set
st A c= product f /\ product(f+*g) holds proj(f,i).:A = proj(f+*g,i).:A
proof
let f, g be non-empty Function, i being object, A being set;
assume A1: A c= product f /\ product(f+*g);
for y being object holds y in proj(f,i).:A iff y in proj(f+*g,i).:A
proof
let y be object;
hereby
assume y in proj(f,i).:A;
then consider x being object such that
A2: x in dom proj(f,i) & x in A & y = proj(f,i).x by FUNCT_1:def 6;
x in product(f+*g) by A1,A2,XBOOLE_0:def 4;
then A4: x in dom proj(f+*g,i) by CARD_3:def 16;
y = proj(f+*g,i).x by A2, A1, Th21;
hence y in proj(f+*g,i).:A by A2, A4, FUNCT_1:def 6;
end;
assume y in proj(f+*g,i).:A;
then consider x being object such that
A5: x in dom proj(f+*g,i) & x in A & y = proj(f+*g,i).x by FUNCT_1:def 6;
x in product f by A1,A5,XBOOLE_0:def 4;
then A7: x in dom proj(f,i) by CARD_3:def 16;
y = proj(f,i).x by A5, A1, Th21;
hence y in proj(f,i).:A by A5, A7, FUNCT_1:def 6;
end;
hence thesis by TARSKI:2;
end;
theorem Th23:
for f, g being non-empty Function
st dom g c= dom f & for i being object st i in dom g holds g.i c= f.i
holds product(f+*g) c= product f
proof
let f, g be non-empty Function;
assume that
A1: dom g c= dom f and
A2: for i being object st i in dom g holds g.i c= f.i;
A3: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
.= dom f by A1, XBOOLE_1:12;
now
let x be object;
assume x in dom (f+*g);
thus (f+*g).x c= f.x
proof
let i be object;
assume A4: i in (f+*g).x;
per cases;
suppose a5: x in dom g;
then A5: i in g.x by A4, FUNCT_4:13;
g.x c= f.x by a5,A2;
hence i in f.x by A5;
end;
suppose not x in dom g;
hence i in f.x by A4, FUNCT_4:11;
end;
end;
end;
hence product(f+*g) c= product f by A3, CARD_3:27;
end;
theorem Th24:
for f, g being non-empty Function
st dom g c= dom f & for i being object st i in dom g holds g.i c= f.i holds
for i being object st i in dom f \ dom g
holds proj(f,i).:product(f+*g) = f.i
proof
let f, g be non-empty Function;
assume that
A1: dom g c= dom f and
A2: for i being object st i in dom g holds g.i c= f.i;
A3: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
.= dom f by A1, XBOOLE_1:12;
A4: product(f+*g) = product f /\ product(f+*g) by A1, A2, Th23,XBOOLE_1:28;
let i be object;
assume a5: i in dom f \ dom g;
then A5: i in dom f & not i in dom g by XBOOLE_0:def 5;
thus proj(f,i).:product(f+*g) = proj(f+*g,i).:product(f+*g) by A4, Th22
.= proj(f+*g,i).:dom proj(f+*g,i) by CARD_3:def 16
.= rng proj(f+*g,i) by RELAT_1:113
.= (f+*g).i by A3, a5, YELLOW17:3
.= f.i by A5, FUNCT_4:11;
end;
theorem Th25:
for f, g being non-empty Function
st dom g c= dom f & for i being object st i in dom g holds g.i c= f.i
holds for i being object st i in dom g holds proj(f,i).:product(f+*g) = g.i
proof
let f, g be non-empty Function;
assume that
A1: dom g c= dom f and
A2: for i being object st i in dom g holds g.i c= f.i;
A3: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
.= dom f by A1, XBOOLE_1:12;
A4: product(f+*g) = product f /\ product(f+*g) by A1, A2, Th23,XBOOLE_1:28;
let i be object;
assume A5: i in dom g;
thus proj(f,i).:product(f+*g) = proj(f+*g,i).:product(f+*g) by A4, Th22
.= proj(f+*g,i).:dom proj(f+*g,i) by CARD_3:def 16
.= rng proj(f+*g,i) by RELAT_1:113
.= (f+*g).i by A1, A3, A5, YELLOW17:3
.= g.i by A5, FUNCT_4:13;
end;
theorem Th26:
for f, g being non-empty Function
st dom g = dom f & for i being object st i in dom g holds g.i c= f.i
holds for i being object st i in dom g holds proj(f,i).:product g = g.i
proof
let f, g be non-empty Function;
assume that
A1: dom g = dom f and
A2: for i being object st i in dom g holds g.i c= f.i;
let i be object;
assume A3: i in dom g;
thus proj(f,i).:product g = proj(f,i).:product(f +* g) by A1, FUNCT_4:19
.= g.i by A1, A2, A3, Th25;
end;
theorem Th27:
for f being Function, X, Y being set, i being object st X c= Y
holds product(f +* (i .--> X)) c= product(f +* (i .--> Y))
proof
let f be Function, X, Y be set, i be object;
assume A1: X c= Y;
dom (f +* (i .--> X)) = dom f \/ dom(i .--> X) by FUNCT_4:def 1
.= dom f \/ dom({i} --> X) by FUNCOP_1:def 9
.= dom f \/ {i};
then A3: dom (f +* (i .--> X)) = dom f \/ dom({i} --> Y)
.= dom f \/ dom(i .--> Y) by FUNCOP_1:def 9
.= dom (f +* (i .--> Y)) by FUNCT_4:def 1;
now
let x be object;
assume x in dom (f +* (i .--> X));
per cases;
suppose A4: x = i;
then x in {i} by TARSKI:def 1;
then x in dom({i} --> X) & x in dom({i} --> Y);
then A5: x in dom(i .--> X) & x in dom(i .--> Y) by FUNCOP_1:def 9;
then A6: (f +* (i .--> X)).x = (i .--> X).x by FUNCT_4:13
.= X by A4, FUNCOP_1:72;
(f +* (i .--> Y)).x = (i .--> Y).x by A5, FUNCT_4:13
.= Y by A4, FUNCOP_1:72;
hence (f +* (i .--> X)).x c= (f +* (i .--> Y)).x by A1, A6;
end;
suppose x <> i;
then not x in dom(i .--> X) & not x in dom(i .--> Y) by TARSKI:def 1;
then (f +* (i .--> X)).x = f.x & (f +* (i .--> Y)).x = f.x by FUNCT_4:11;
hence (f +* (i .--> X)).x c= (f +* (i .--> Y)).x;
end;
end;
hence thesis by A3, CARD_3:27;
end;
theorem Th28:
for i,j being object, A, B, C, D being set st A c= C & B c= D
holds product((i,j) --> (A,B)) c= product((i,j) --> (C,D))
proof
let i,j be object, A,B,C,D be set;
assume A1: A c= C & B c= D;
per cases;
suppose A2: i <> j;
let x be object;
assume x in product((i,j) --> (A,B));
then consider g being Function such that
A3: g = x & dom g = dom (i,j) --> (A,B) and
A4: for y being object st y in dom (i,j) --> (A,B)
holds g.y in ((i,j) --> (A,B)).y by CARD_3:def 5;
A5: dom (i,j) --> (A,B) = {i,j} by FUNCT_4:62
.= dom (i,j) --> (C,D) by FUNCT_4:62;
for y being object st y in dom (i,j) --> (C,D) holds
g.y in ((i,j) --> (C,D)).y
proof
let y be object;
assume A6: y in dom (i,j) --> (C,D);
then y in {i,j} by FUNCT_4:62;
then per cases by TARSKI:def 2;
suppose A7: y = i;
then g.y in ((i,j) --> (A,B)).i by A4, A5, A6;
then g.y in A by A2, FUNCT_4:63;
then g.y in C by A1;
hence thesis by A2, A7, FUNCT_4:63;
end;
suppose A8: y = j;
then g.y in ((i,j) --> (A,B)).j by A4, A5, A6;
then g.y in B by FUNCT_4:63;
then g.y in D by A1;
hence thesis by A8, FUNCT_4:63;
end;
end;
hence thesis by A3, A5, CARD_3:def 5;
end;
suppose A9: i = j;
then A10: (i,j) --> (A,B) = i .--> B by FUNCT_4:81
.= {i} --> B by FUNCOP_1:def 9;
(i,j) --> (C,D) = i .--> D by A9, FUNCT_4:81
.= {i} --> D by FUNCOP_1:def 9;
hence thesis by A1, A10, Th14;
end;
end;
theorem Th29:
for X, Y being set, f, i, j being object st i <> j
holds f in product((i,j) --> (X,Y)) iff
ex x,y being object st x in X & y in Y & f = (i,j) --> (x,y)
proof
let X,Y be set, f, i, j be object;
assume A1: i <> j;
thus f in product((i,j) --> (X,Y)) implies
ex x,y being object st x in X & y in Y & f = (i,j) --> (x,y)
proof
assume f in product((i,j) --> (X,Y));
then consider g being Function such that
A2: g = f & dom g = dom (i,j) --> (X,Y) and
A3: for z being object st z in dom (i,j) --> (X,Y)
holds g.z in ((i,j) --> (X,Y)).z by CARD_3:def 5;
take g.i, g.j;
A4: dom (i,j) --> (X,Y) = {i,j} by FUNCT_4:62;
then i in dom (i,j) --> (X,Y) by TARSKI:def 2;
then g.i in ((i,j) --> (X,Y)).i by A3;
hence g.i in X by A1, FUNCT_4:63;
j in dom (i,j) --> (X,Y) by A4, TARSKI:def 2;
then g.j in ((i,j) --> (X,Y)).j by A3;
hence thesis by A2, A4, FUNCT_4:66,FUNCT_4:63;
end;
given x,y being object such that
A5: x in X & y in Y & f = (i,j) --> (x,y);
reconsider g = f as Function by A5;
A6: dom g = {i,j} by A5, FUNCT_4:62
.= dom (i,j) --> (X,Y) by FUNCT_4:62;
for z being object st z in dom (i,j) --> (X,Y)
holds g.z in ((i,j) --> (X,Y)).z
proof
let z be object;
assume z in dom (i,j) --> (X,Y);
then z in {i,j} by FUNCT_4:62;
then per cases by TARSKI:def 2;
suppose A7: z = i;
then g.z = x by A1, A5, FUNCT_4:63;
hence thesis by A1, A5, A7, FUNCT_4:63;
end;
suppose A8: z = j;
then g.z = y by A5, FUNCT_4:63;
hence thesis by A5, A8, FUNCT_4:63;
end;
end;
hence thesis by A6, CARD_3:9;
end;
theorem Th30:
for f being non-empty Function, X, Y being set, i, j, x, y being object
for g being Function
st x in X & y in Y & i <> j & g in product f
holds g +* (i,j) --> (x,y) in product(f +* (i,j) --> (X,Y))
proof
let f be non-empty Function, X, Y be set;
let i,j,x,y be object, g be Function;
assume that
A1: x in X & y in Y and
A2: i <> j & g in product f;
A3: dom(g +* (i,j) --> (x,y))
= dom g \/ dom (i,j) --> (x,y) by FUNCT_4:def 1
.= dom g \/ {i,j} by FUNCT_4:62
.= dom f \/ {i,j} by A2, CARD_3:9
.= dom f \/ dom (i,j) --> (X,Y) by FUNCT_4:62
.= dom(f +* (i,j) --> (X,Y)) by FUNCT_4:def 1;
for z being object st z in dom(f +* (i,j) --> (X,Y))
holds (g +* (i,j) --> (x,y)).z in (f +* (i,j) --> (X,Y)).z
proof
let z be object;
assume A4: z in dom(f +* (i,j) --> (X,Y));
per cases;
suppose A5: z in {i,j};
then z in dom (i,j) --> (x,y) by FUNCT_4:62;
then A6: (g +* (i,j) --> (x,y)).z = ((i,j) --> (x,y)).z by FUNCT_4:13;
z in dom (i,j) --> (X,Y) by A5, FUNCT_4:62;
then A7: (f +* (i,j) --> (X,Y)).z = ((i,j) --> (X,Y)).z by FUNCT_4:13;
per cases by A5, TARSKI:def 2;
suppose A8: z = i;
then (g +* (i,j) --> (x,y)).z = x by A2, A6, FUNCT_4:63;
hence thesis by A1, A2, A7, A8, FUNCT_4:63;
end;
suppose A9: z = j;
then (g +* (i,j) --> (x,y)).z = y by A6, FUNCT_4:63;
hence thesis by A1, A7, A9, FUNCT_4:63;
end;
end;
suppose A10: not z in {i,j};
then not z in dom (i,j) --> (x,y) by FUNCT_4:62;
then A11: (g +* (i,j) --> (x,y)).z = g.z by FUNCT_4:11;
not z in dom (i,j) --> (X,Y) by A10, FUNCT_4:62;
then A12: (f +* (i,j) --> (X,Y)).z = f.z by FUNCT_4:11;
z in dom f \/ dom (i,j) --> (X,Y) by A4, FUNCT_4:def 1;
then z in dom f \/ {i,j} by FUNCT_4:62;
then z in dom f by A10, XBOOLE_0:def 3;
hence thesis by A2, A11, A12, CARD_3:9;
end;
end;
hence thesis by A3, CARD_3:9;
end;
theorem Th31:
for f being Function, A, B, C, D being set, i, j being object
st A c= C & B c= D
holds product(f +* (i,j) --> (A,B)) c= product(f +* (i,j) --> (C,D))
proof
let f be Function, A,B,C,D be set, i,j be object;
assume A1: A c= C & B c= D;
per cases;
suppose i = j;
then (i,j) --> (A,B) = i .--> B & (i,j) --> (C,D) = i .--> D by FUNCT_4:81;
hence thesis by A1, Th27;
end;
suppose A2: i <> j;
dom(f +* (i,j) --> (A,B)) = dom f \/ dom (i,j) --> (A,B) by FUNCT_4:def 1
.= dom f \/ {i,j} by FUNCT_4:62;
then A3: dom(f +* (i,j) --> (A,B))
= dom f \/ dom (i,j) --> (C,D) by FUNCT_4:62
.= dom(f +* (i,j) --> (C,D)) by FUNCT_4:def 1;
for x being object st x in dom(f +* (i,j) --> (A,B))
holds (f +* (i,j) --> (A,B)).x c= (f +* (i,j) --> (C,D)).x
proof
let x be object;
assume x in dom(f +* (i,j) --> (A,B));
per cases;
suppose A4: x in {i,j};
then x in dom (i,j) --> (A,B) by FUNCT_4:62;
then A5: (f +* (i,j) --> (A,B)).x = ((i,j) --> (A,B)).x by FUNCT_4:13;
x in dom (i,j) --> (C,D) by A4, FUNCT_4:62;
then A6: (f +* (i,j) --> (C,D)).x = ((i,j) --> (C,D)).x by FUNCT_4:13;
per cases by A4, TARSKI:def 2;
suppose A7: x = i;
then (f +* (i,j) --> (A,B)).x = A by A2, A5, FUNCT_4:63;
hence thesis by A1, A2, A6, A7, FUNCT_4:63;
end;
suppose A9: x = j;
then (f +* (i,j) --> (A,B)).x = B by A5, FUNCT_4:63;
hence thesis by A1, A6, A9, FUNCT_4:63;
end;
end;
suppose A11: not x in {i,j};
then not x in dom (i,j) --> (A,B) by FUNCT_4:62;
then A12: (f +* (i,j) --> (A,B)).x = f.x by FUNCT_4:11;
not x in dom (i,j) --> (C,D) by A11, FUNCT_4:62;
hence thesis by A12, FUNCT_4:11;
end;
end;
hence thesis by A3, CARD_3:27;
end;
end;
theorem
for f being Function, A, B being set, i, j being object
st i in dom f & j in dom f & A c= f.i & B c= f.j
holds product(f +* (i,j) --> (A,B)) c= product f
proof
let f be Function, A, B be set, i, j be object;
assume A1: i in dom f & j in dom f & A c= f.i & B c= f.j;
then product f = product(f +* (i,j) --> (f.i,f.j)) by Th11;
hence thesis by A1, Th31;
end;
:: $\prod_{i\in I} A_i \cap \prod_{i\in I} B_i = \prod_{i\in I} (A_i \cap B_i)$
:: compare MSUALG_2:1
theorem Th33:
for I being set, f, g being ManySortedSet of I
holds product f /\ product g = product(f (/\) g)
proof
let I be set, f, g be ManySortedSet of I;
for x being object holds x in product f /\ product g iff
ex h being Function st h = x & dom h = dom(f (/\) g) &
for y being object st y in dom(f (/\) g)
holds h.y in (f (/\) g).y
proof
let x be object;
hereby
assume x in product f /\ product g;
then A1: x in product f & x in product g by XBOOLE_0:def 4;
then consider h being Function such that
A2: h = x & dom h = dom f and
A3: for y being object st y in dom f holds h.y in f.y by CARD_3:def 5;
take h;
thus h = x by A2;
thus dom h = I by A2, PARTFUN1:def 2
.= dom(f (/\) g) by PARTFUN1:def 2;
let y be object;
assume a4: y in dom(f (/\) g);
then A4: y in I;
A5: y in dom f & y in dom g by A4, PARTFUN1:def 2;
then A6: h.y in f.y by A3;
h.y in g.y by A1, A2, A5, CARD_3:9;
then h.y in f.y /\ g.y by A6, XBOOLE_0:def 4;
hence h.y in (f (/\) g).y by a4, PBOOLE:def 5;
end;
given h being Function such that
A7: h = x & dom h = dom(f (/\) g) and
A8: for y being object st y in dom(f (/\) g)
holds h.y in (f (/\) g).y;
a9: dom h = I by A7, PARTFUN1:def 2;
then A9: dom h = dom f & dom h = dom g by PARTFUN1:def 2;
A10: now
let y be object;
assume A11: (y in dom f or y in dom g);
h.y in (f (/\) g).y by A7, A8, a9, A11;
then h.y in f.y /\ g.y by A11, PBOOLE:def 5;
hence h.y in f.y & h.y in g.y by XBOOLE_0:def 4;
end;
for y being object st y in dom f holds h.y in f.y by A10;
then A13: h in product f by A9, CARD_3:9;
for y being object st y in dom g holds h.y in g.y by A10;
then h in product g by A9, CARD_3:9;
hence x in product f /\ product g by A7, A13, XBOOLE_0:def 4;
end;
hence thesis by CARD_3:def 5;
end;
:: END into CARD_3 ?
:: BEGIN into FUNCT_7 ?
Lm2:
for I being 2-element set, f being ManySortedSet of I
for i, j being Element of I, x being object st i <> j
holds f +* (i,x) = (i,j) --> (x,f.j)
proof
let I be 2-element set, f be ManySortedSet of I;
let i,j be Element of I, x be object;
assume A1: i <> j;
then a2:I = {i,j} by Th8;
then A2: dom f = {i,j} by PARTFUN1:def 2;
A3: dom(f +* (i,x)) = dom f by FUNCT_7:30
.= dom (i,j) --> (x,f.j) by A2, FUNCT_4:62;
for z being object st z in dom(f +* (i,x))
holds (f +* (i,x)).z = ((i,j) --> (x,f.j)).z
proof
let z be object;
assume z in dom(f +* (i,x));
then per cases by a2,TARSKI:def 2;
suppose A5: z = i;
hence (f +* (i,x)).z = x by A2, a2, FUNCT_7:31
.= ((i,j) --> (x,f.j)).z by A1, A5, FUNCT_4:63;
end;
suppose A6: z = j;
hence (f +* (i,x)).z = f.j by A1, FUNCT_7:32
.= ((i,j) --> (x,f.j)).z by A6, FUNCT_4:63;
end;
end;
hence thesis by A3, FUNCT_1:2;
end;
theorem Th34:
for I being 2-element set, f being ManySortedSet of I
for i, j being Element of I, x being object st i <> j
holds f +* (i,x) = (i,j) --> (x,f.j) & f +* (j,x) = (i,j) --> (f.i,x)
proof
let I be 2-element set, f be ManySortedSet of I;
let i, j be Element of I, x be object;
assume A1: i <> j;
thus f +* (i,x) = (i,j) --> (x,f.j) by A1, Lm2;
thus f +* (j,x) = (j,i) --> (x,f.i) by A1, Lm2
.= (i,j) --> (f.i,x) by A1, Th10;
end;
theorem Th35:
for f being non-empty Function, X being set, i being object st i in dom f
holds f +* (i,X) is non-empty iff X is non empty
proof
let f be non-empty Function, X be set, i be object;
assume A1: i in dom f;
hereby
assume A2: f +* (i,X) is non-empty;
i in dom(f +* (i,X)) by A1, FUNCT_7:30;
then (f +* (i,X)).i <> {} by A2, FUNCT_1:def 9;
hence X is non empty by A1, FUNCT_7:31;
end;
assume A3: X is non empty;
for x being object st x in dom(f +* (i,X)) holds (f +* (i,X)).x is non empty
proof
let x be object;
assume A4: x in dom(f +* (i,X));
A5: x in dom f by A4, FUNCT_7:30;
x <> i implies (f +* (i,X)).x = f.x by FUNCT_7:32;
hence thesis by A5, FUNCT_1:def 9, A3, FUNCT_7:31;
end;
hence thesis by FUNCT_1:def 9;
end;
theorem Th36:
for f being non-empty Function, X being set, i being object st i in dom f
holds product(f +* (i,X)) = {} iff X is empty
proof
let f be non-empty Function, X be set, i be object;
assume A1: i in dom f;
then A2: i in dom(f +* (i,X)) by FUNCT_7:30;
hereby
assume product(f +* (i,X)) = {};
then f +* (i,X) is non non-empty;
hence X is empty by A1, Th35;
end;
assume X is empty;
then (f +* (i,X)).i = {} by A1, FUNCT_7:31;
then {} in rng (f +* (i,X)) by A2, FUNCT_1:def 3;
hence thesis by CARD_3:26;
end;
theorem Th37:
for f being non-empty Function, X being set, i, x being object
for g being Function st i in dom f & x in X & g in product f
holds g +* (i,x) in product(f +* (i,X))
proof
let f be non-empty Function, X be set, i,x be object;
let g be Function;
assume A1: i in dom f & x in X & g in product f;
A2: dom(g +* (i,x)) = dom g by FUNCT_7:30
.= dom f by A1, CARD_3:9
.= dom(f +* (i,X)) by FUNCT_7:30;
for y being object st y in dom(f+*(i,X)) holds (g+*(i,x)).y in (f+*(i,X)).y
proof
let y be object;
assume A3: y in dom(f+*(i,X));
then A4:y in dom f by FUNCT_7:30;
per cases;
suppose A5: i = y;
y in dom f by A3, FUNCT_7:30;
then y in dom g by A1, CARD_3:9;
then (g+*(i,x)).y = x by A5, FUNCT_7:31;
hence thesis by A1, A5, FUNCT_7:31;
end;
suppose i <> y;
then (g+*(i,x)).y = g.y & (f+*(i,X)).y = f.y by FUNCT_7:32;
hence thesis by A4,A1,CARD_3:9;
end;
end;
hence thesis by A2, CARD_3:9;
end;
theorem Th38:
for f being Function, X, Y being set, i being object st i in dom f & X c= Y
holds product(f +* (i,X)) c= product(f +* (i,Y))
proof
let f be Function, X, Y be set, i be object;
assume A1: i in dom f & X c= Y;
then f +* (i,X) = f +* (i .--> X) & f +* (i,Y) = f +* (i .--> Y)
by FUNCT_7:def 3;
hence thesis by A1, Th27;
end;
:: compare YELLOW17:2
theorem Th39:
for f being Function, X being set, i being object st i in dom f & X c= f.i
holds product(f +* (i,X)) c= product(f)
proof
let f be Function, X be set, i be object;
I: i is set by TARSKI:1;
assume i in dom f & X c= f.i;
then product(f +* (i,X)) c= product(f +* (i,f.i)) by Th38;
hence thesis by I, FUNCT_7:35;
end;
theorem
for f being non-empty Function, X, Y being non empty set, i, j being object
st i in dom f & j in dom f & (not X c= f.i or not f.j c= Y) &
product (f +* (i,X)) c= product (f +* (j,Y))
holds i = j & X c= Y
proof
let f be non-empty Function, X, Y be non empty set, i, j be object;
assume that
A1: i in dom f & j in dom f and
A2: not X c= f.i or not f.j c= Y and
A3: product (f +* (i,X)) c= product (f +* (j,Y));
a4: f +* (i,X) is non-empty & f +* (j,Y) is non-empty by A1, Th35;
thus A5: i = j
proof
assume A6: i <> j;
A7: i in dom(f +* (i,X)) & j in dom(f +* (i,X)) by A1, FUNCT_7:30;
(f +* (i,X)).i c= (f +* (j,Y)).i by a4, A7, A3, PUA2MSS1:1;
then a8: X c= (f +* (j,Y)).i by A1, FUNCT_7:31;
(f +* (i,X)).j c= (f +* (j,Y)).j by a4, A7, A3, PUA2MSS1:1;
then (f +* (i,X)).j c= Y by A1, FUNCT_7:31;
hence contradiction by A2, a8, A6, FUNCT_7:32;
end;
let x be object;
assume A9: x in X;
set g = the Element of product f;
A10: g +* (i,x) in product(f +* (i,X)) by A1, A9, Th37;
i in dom(f +* (j,Y)) by A1, FUNCT_7:30;
then (g +* (i,x)).i in (f +* (j,Y)).i by A3, A10, CARD_3:9;
then A11: (g +* (i,x)).i in Y by A1, A5, FUNCT_7:31;
i in dom g by A1, CARD_3:9;
hence thesis by A11, FUNCT_7:31;
end;
theorem
for f being non-empty Function, X being set, i being object
st i in dom f & product(f +* (i,X)) c= product f holds X c= f.i
proof
let f be non-empty Function, X be set, i be object;
assume A1: i in dom f & product(f +* (i,X)) c= product f;
let x be object;
assume A2: x in X;
set g = the Element of product f;
a3: g +* (i,x) in product(f +* (i,X)) by A1, A2, Th37;
i in dom g by A1, CARD_3:9;
then (g +* (i,x)).i = x by FUNCT_7:31;
hence thesis by A1, a3, CARD_3:9;
end;
theorem Th42:
for f being non-empty Function, X, Y being non empty set, i, j being object
st i in dom f & j in dom f & (X <> f.i or Y <> f.j) &
product (f +* (i,X)) = product (f +* (j,Y))
holds i = j & X = Y
proof
let f be non-empty Function, X, Y be non empty set, i, j be object;
assume that
A1: i in dom f & j in dom f and
A2: X <> f.i or Y <> f.j and
A3: product (f +* (i,X)) = product (f +* (j,Y));
f +* (i,X) is non-empty & f +* (j,Y) is non-empty by A1, Th35;
then A4: f +* (i,X) = f +* (j,Y) by A3, PUA2MSS1:2;
thus A5: i = j
proof
assume A6: i <> j;
A7: X = (f +* (i,X)).i by A1, FUNCT_7:31
.= f.i by A4, A6, FUNCT_7:32;
Y = (f +* (j,Y)).j by A1, FUNCT_7:31
.= f.j by A4, A6, FUNCT_7:32;
hence contradiction by A2, A7;
end;
thus X = (f +* (j,Y)).i by A1, A4, FUNCT_7:31
.= Y by A1, A5, FUNCT_7:31;
end;
theorem Th43:
for f being non-empty Function, X being set, i being object
st i in dom f & X c= f.i holds proj(f,i).:product(f +* (i,X)) = X
proof
let f be non-empty Function, X be set, i be object;
assume A1: i in dom f & X c= f.i;
then A2: f +* (i,X) = f +* (i .--> X) by FUNCT_7:def 3
.= f +* ({i} --> X) by FUNCOP_1:def 9;
A3: i in dom (f +* (i,X)) by A1, FUNCT_7:30;
per cases;
suppose A4: X is non empty;
{i} c= dom f by A1, ZFMISC_1:31;
then A5: dom ({i} --> X) c= dom f;
A6: for j being object st j in dom ({i} --> X) holds ({i} --> X).j c= f.j
proof
let j be object;
assume A7: j in dom ({i} --> X);
then i = j by TARSKI:def 1;
hence thesis by A1, A7, FUNCOP_1:7;
end;
A8: i in {i} by TARSKI:def 1;
then i in dom ({i} --> X);
then proj(f,i).:product(f +* ({i} --> X)) = ({i} --> X).i
by A5, A6, A4, Th25;
hence thesis by A2,A8, FUNCOP_1:7;
end;
suppose A9: X is empty;
then (f +* (i,X)).i is empty by A1, FUNCT_7:31;
then {} in rng (f +* (i,X)) by A3, FUNCT_1:3;
then product(f +* (i,X)) = {} by CARD_3:26;
hence thesis by A9;
end;
end;
theorem Th44:
for x,y,z being object holds (x .--> y) +* (x,z) = x .--> z
proof
let x,y,z be object;
dom (x .--> y) = dom ({x} --> y) by FUNCOP_1:def 9
.= {x};
then x in dom (x .--> y) by TARSKI:def 1;
then (x .--> y) +* (x,z) = (x .--> y) +* (x .--> z) by FUNCT_7:def 3;
hence thesis by Th12;
end;
:: END into FUNCT_7 ?
:: into PRALG_1 ?
registration
let I being non empty set;
let J being 1-sorted-yielding non-Empty ManySortedSet of I;
cluster Carrier J -> non-empty;
coherence
proof
assume Carrier J is non non-empty;
then {} in rng Carrier J by RELAT_1:def 9;
then consider i being object such that
A1: i in dom Carrier J & (Carrier J).i = {} by FUNCT_1:def 3;
reconsider i as set by TARSKI:1;
consider R being 1-sorted such that
A2: R = J.i & (Carrier J).i = the carrier of R by A1, PRALG_1:def 15;
dom J = I by PARTFUN1:def 2;
then R in rng J by A1, A2, FUNCT_1:3;
then R is non empty by WAYBEL_3:def 7;
hence contradiction by A1, A2;
end;
end;
begin :: Remarks about Product Spaces
theorem Th45:
for T,S being TopSpace, f being Function of T,S
holds f is open iff
ex B being Basis of T st
for V being Subset of T st V in B holds f.:V is open
proof
let T,S be TopSpace, f be Function of T,S;
hereby
assume A1: f is open;
reconsider B = the Basis of T as Basis of T;
take B;
let V be Subset of T;
assume V in B;
hence f.:V is open by A1, TOPS_2:def 1, T_0TOPSP:def 2;
end;
given B being Basis of T such that
A2: for V being Subset of T st V in B holds f.:V is open;
now
let A be Subset of T;
set Y = { G where G is Subset of T : G in B & G c= A };
Y c= bool the carrier of T
proof
let g be object;
assume g in Y;
then ex G being Subset of T st g = G & G in B & G c= A;
hence thesis;
end;
then reconsider Y as Subset-Family of T;
set Z = { f.:G where G is Subset of T : G in Y };
Z c= bool the carrier of S
proof
let h be object;
assume h in Z;
then ex G being Subset of T st
h = f.:G & G in Y;
hence thesis;
end;
then reconsider Z as Subset-Family of S;
A7: for P being Subset of S holds P in Z implies P is open
proof
let P be Subset of S;
assume P in Z;
then consider G1 being Subset of T such that
A5: P = f.:G1 & G1 in Y;
ex G2 being Subset of T st
G1 = G2 & G2 in B & G2 c= A by A5;
hence thesis by A2, A5;
end;
assume A is open;
then A = union Y by YELLOW_8:9;
then f.:A = union Z by RELSET_2:14; :: f(UY) = Uf(Y)
hence f.:A is open by A7, TOPS_2:19,TOPS_2:def 1;
end;
hence thesis by T_0TOPSP:def 2;
end;
theorem
for T1,T2,S1,S2 being non empty TopSpace
for f being Function of T1, S1, g being Function of T2, S2
st f is open & g is open holds [: f,g :] is open
proof
let T1,T2,S1,S2 be non empty TopSpace;
let f be Function of T1, S1, g be Function of T2, S2;
assume A1: f is open & g is open;
ex B being Basis of [: T1,T2 :] st
for P being Subset of [: T1, T2 :] st P in B holds [: f,g :].:P is open
proof
set B1 = the Basis of T1;
set B2 = the Basis of T2;
set B = {[: V,W :] where V is Subset of T1, W is Subset of T2 :
V in B1 & W in B2};
reconsider B as Basis of [: T1, T2 :] by YELLOW_9:40;
take B;
let P be Subset of [: T1, T2 :];
assume P in B;
then consider V being Subset of T1, W being Subset of T2 such that
A2: P = [: V,W :] & V in B1 & W in B2;
A3: f.:V is open & g.:W is open by A1, T_0TOPSP:def 2,A2, TOPS_2:def 1;
[: f,g :].:P = [: f.:V,g.:W :] by A2, FUNCT_3:72;
hence thesis by A3, BORSUK_1:6;
end;
hence thesis by Th45;
end;
theorem Th47:
for S,T being non empty TopSpace, f being Function of S,T
st f is bijective &
ex K being Basis of S, L being Basis of T st f.:K = L
holds f is being_homeomorphism
proof
let S, T be non empty TopSpace, f be Function of S,T;
assume A1: f is bijective;
given K being Basis of S, L being Basis of T such that
A2: f.:K = L;
for W being Subset of T st W in L holds f"W is open
proof
let W be Subset of T;
assume W in L;
then consider V being Subset of S such that
A3: V in K & W = f.:V by A2, FUNCT_2:def 10;
dom f = the carrier of S by FUNCT_2:def 1;
then V = f"W by A1, A3, FUNCT_1:94;
hence thesis by A3, TOPS_2:def 1;
end;
then A4: f is continuous by YELLOW_9:34;
for V being Subset of S st V in K holds f.:V is open
proof
let V be Subset of S;
assume V in K;
then f.:V in f.:K by FUNCT_2:def 10;
hence thesis by A2, TOPS_2:def 1;
end;
then f is open by Th45;
then A5: f" is continuous by A1, TOPREALA:14;
A6: rng f = the carrier of T by A1, FUNCT_2:def 3
.= [#]T by STRUCT_0:def 3;
dom f = the carrier of S by FUNCT_2:def 1
.= [#]S by STRUCT_0:def 3;
hence thesis by A1, A5, A4, A6, TOPS_2:def 5;
end;
theorem Th48:
for S,T being non empty TopSpace, f being Function of S,T
st f is bijective &
ex K being prebasis of S, L being prebasis of T st f.:K = L
holds f is being_homeomorphism
proof
let S, T be non empty TopSpace, f be Function of S,T;
assume A1: f is bijective;
given K being prebasis of S, L being prebasis of T such that
A2: f.:K = L;
:: the basic idea is to take the canonical bases from the prebases and
:: show the condition of the theorem above
reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;
reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;
reconsider g = f" as Function of T, S;
reconsider f0 = f as one-to-one Function by A1;
a3: f0" = g by A1, TOPS_2:def 4;
for W being Subset of T holds W in L0 iff
ex V being Subset of S st V in K0 & f.:V = W
proof
let W be Subset of T;
thus W in L0 implies ex V being Subset of S st V in K0 & f.:V = W
proof
assume W in L0;
then consider Y being Subset-Family of T such that
A4: Y c= L & Y is finite & W = Intersect Y by CANTOR_1:def 3;
per cases;
suppose A5: Y <> {};
then A6: W = meet Y by A4, SETFAM_1:def 9;
reconsider X = g.:Y as Subset-Family of S;
reconsider V = meet X as Subset of S;
take V;
:: we use V := meet f"Y, then f.:V = f.:meet f"Y = meet f.:f"Y = meet Y
ex Z being Subset-Family of S st Z c= K & Z is finite & V = Intersect Z
proof
take X;
for x being object st x in X holds x in K
proof
let x be object;
assume x in X;
then consider B being Subset of T such that
A7: B in Y & x = g.:B by FUNCT_2:def 10;
consider A being Subset of S such that
A8: A in K & B = f.:A by A2, A4, A7, FUNCT_2:def 10;
A9: dom f = the carrier of S by FUNCT_2:def 1;
x = f"(f.:A) by a3,FUNCT_1:85, A7, A8
.= A by A1, A9, FUNCT_1:94;
hence thesis by A8;
end;
hence X c= K & X is finite by A4, TARSKI:def 3;
consider B being object such that
A10: B in Y by A5, XBOOLE_0:def 1;
reconsider B as Subset of T by A10;
g.:B in X by A10, FUNCT_2:def 10;
hence thesis by SETFAM_1:def 9;
end;
hence V in K0 by CANTOR_1:def 3;
set Z = { f.:A where A is Subset of S : A in X };
for x being object holds x in Z iff x in Y
proof
let x be object;
A11: rng f = the carrier of T by A1, FUNCT_2:def 3;
hereby
assume x in Z;
then consider A being Subset of S such that
A12: f.:A = x & A in X;
consider B being Subset of T such that
A13: B in Y & A = g.:B by A12, FUNCT_2:def 10;
x = f.:(f"B) by a3,FUNCT_1:85, A12, A13
.= B by A11, FUNCT_1:77;
hence x in Y by A13;
end;
assume A14: x in Y;
then reconsider B = x as Subset of T;
A15: g.:B in X by A14, FUNCT_2:def 10;
f.:(g.:B) = f.:(f"B) by a3,FUNCT_1:85
.= B by A11, FUNCT_1:77;
hence thesis by A15;
end;
then Z = Y by TARSKI:2;
hence f.:V = W by A1, A6, Th4;
end;
suppose Y = {};
then A16: W = the carrier of T by A4, SETFAM_1:def 9;
set V = [#]S;
take V;
set Z = the empty Subset-Family of S;
Intersect Z = the carrier of S by SETFAM_1:def 9;
then Z c= K & Z is finite & V = Intersect Z
by XBOOLE_1:2,STRUCT_0:def 3;
hence V in K0 by CANTOR_1:def 3;
thus f.:V = f.:the carrier of S by STRUCT_0:def 3
.= f.:dom f by FUNCT_2:def 1
.= rng f by RELAT_1:113
.= W by A16, A1, FUNCT_2:def 3;
end;
end;
given V being Subset of S such that
A17: V in K0 & f.:V = W;
consider X being Subset-Family of S such that
A18: X c= K & X is finite & V = Intersect X by A17, CANTOR_1:def 3;
per cases;
suppose A19: X <> {};
then A20: V = meet X by A18, SETFAM_1:def 9;
ex Y being Subset-Family of T st Y c= L & Y is finite & W = Intersect Y
proof
reconsider Y = f.:X as Subset-Family of T;
take Y;
thus Y c= L
proof
let x be object;
assume x in Y;
then ex A being Subset of S st
A in X & f.:A = x by FUNCT_2:def 10;
hence thesis by A2, FUNCT_2:def 10, A18;
end;
thus Y is finite by A18;
set Z = { f.:A where A is Subset of S : A in X };
for x being object holds x in Y iff x in Z
proof
let x be object;
hereby
assume x in Y;
then ex A being Subset of S st
A in X & f.:A = x by FUNCT_2:def 10;
hence x in Z;
end;
assume x in Z;
then ex A being Subset of S st f.:A = x & A in X;
hence thesis by FUNCT_2:def 10;
end;
then Y = Z by TARSKI:2;
then A24: meet Y = W by A1, A17, A20, Th4;
consider A being object such that
A25: A in X by A19, XBOOLE_0:def 1;
reconsider A as Subset of S by A25;
f.:A in f.:X by A25, FUNCT_2:def 10;
hence thesis by A24, SETFAM_1:def 9;
end;
hence thesis by CANTOR_1:def 3;
end;
suppose X = {};
then A26: V = the carrier of S by A18, SETFAM_1:def 9;
set Y = the empty Subset-Family of T;
B1: Y c= L & Y is finite by XBOOLE_1:2;
W = f.:dom f by A17, A26, FUNCT_2:def 1
.= rng f by RELAT_1:113
.= the carrier of T by A1, FUNCT_2:def 3
.= Intersect Y by SETFAM_1:def 9;
hence W in L0 by B1,CANTOR_1:def 3;
end;
end;
then f.:K0 = L0 by FUNCT_2:def 10;
hence thesis by A1, Th47;
end;
:: compare TOPGEN_5:71 (the converse)
theorem Th49:
for S, T being TopSpace
st ex K being Basis of S, L being Basis of T st K = INTERSECTION(L,{[#]S})
holds S is SubSpace of T
proof
let S, T be TopSpace;
given K being Basis of S, L being Basis of T such that
A1: K = INTERSECTION(L,{[#]S});
A2: for A being Subset of S holds A in the topology of S iff
ex B being Subset of T st B in the topology of T & A = B /\ [#]S
proof
let A be Subset of S;
hereby
assume A in the topology of S;
then A in UniCl K by CANTOR_1:def 2, TARSKI:def 3;
then consider X being Subset-Family of S such that
A3: X c= K & A = union X by CANTOR_1:def 1;
set Y = { D where D is Subset of T :
D in L & ex C being Element of K st C in X & C = D /\ [#]S };
Y c= bool the carrier of T
proof
let x be object;
assume x in Y;
then ex D being Subset of T st
D = x & D in L &
ex C being Element of K st C in X & C = D /\ [#]S;
hence thesis;
end;
then reconsider Y as Subset-Family of T;
set B = union Y;
take B;
for x being Subset of T holds x in Y implies x is open
proof
let x be Subset of T;
assume x in Y;
then ex D being Subset of T st
D = x & D in L &
ex C being Element of K st C in X & C = D /\ [#]S;
hence thesis by TOPS_2:def 1;
end;
then Y is open by TOPS_2:def 1;
hence B in the topology of T by TOPS_2:19, PRE_TOPC:def 2;
for x being object holds x in A iff x in B /\ [#]S
proof
let x be object;
hereby
assume x in A;
then consider C being set such that
A6: x in C & C in X by A3, TARSKI:def 4;
reconsider C as Element of K by A3, A6;
consider D, S0 being set such that
A7: D in L & S0 in {[#]S} & C = D /\ S0
by A1, A3, A6, SETFAM_1:def 5;
reconsider D as Subset of T by A7;
C in X & C = D /\ [#]S by A6, A7, TARSKI:def 1;
then A8: D in Y by A7;
x in D by A6, A7, XBOOLE_0:def 4;
then A9: x in B by A8, TARSKI:def 4;
x in S0 by A6, A7, XBOOLE_0:def 4;
then x in [#]S by A7, TARSKI:def 1;
hence x in B /\ [#]S by A9, XBOOLE_0:def 4;
end;
assume A10: x in B /\ [#]S;
then x in B by XBOOLE_0:def 4;
then consider D0 being set such that
A11: x in D0 & D0 in Y by TARSKI:def 4;
consider D being Subset of T such that
A12: D = D0 & D in L and
A13: ex C being Element of K st C in X & C = D /\ [#]S by A11;
consider C being Element of K such that
A14: C in X & C = D /\ [#]S by A13;
x in [#]S by A10, XBOOLE_0:def 4;
then x in C by A11, A12, A14, XBOOLE_0:def 4;
hence thesis by A3, A14, TARSKI:def 4;
end;
hence A = B /\ [#]S by TARSKI:2;
end;
given B being Subset of T such that
A15: B in the topology of T & A = B /\ [#]S;
B in UniCl L by A15, CANTOR_1:def 2, TARSKI:def 3;
then consider Y being Subset-Family of T such that
A16: Y c= L & B = union Y by CANTOR_1:def 1;
set X = INTERSECTION(Y,{[#]S});
X c= bool the carrier of S
proof
let x be object;
reconsider x0 = x as set by TARSKI:1;
assume x in X;
then consider C, S0 being set such that
A17: C in Y & S0 in {[#]S} & x0 = C /\ S0 by SETFAM_1:def 5;
x0 c= S0 by A17, XBOOLE_1:17;
then x0 c= [#]S by A17, TARSKI:def 1;
then x0 c= the carrier of S by STRUCT_0:def 3;
hence thesis;
end;
then reconsider X as Subset-Family of S;
for x being Subset of S holds x in X implies x is open
proof
let x be Subset of S;
assume x in X;
then consider C, S0 being set such that
A18: C in Y & S0 in {[#]S} & x = C /\ S0 by SETFAM_1:def 5;
x in K by A1, A16, A18, SETFAM_1:def 5;
hence thesis by TOPS_2:def 1;
end;
then A19: X is open by TOPS_2:def 1;
A = union X by A15, A16, SETFAM_1:25;
hence thesis by A19, TOPS_2:19, PRE_TOPC:def 2;
end;
:: since we are only dealing with unions here, [#]S c= [#]T can be derived
the carrier of S in the topology of S by PRE_TOPC:def 1;
then consider B being Subset of T such that
A20: B in the topology of T & the carrier of S = B /\ [#]S
by A2;
[#]S = B /\ [#]S by A20, STRUCT_0:def 3;
then [#]S c= B by XBOOLE_1:17;
then [#]S c= the carrier of T by XBOOLE_1:1;
then [#]S c= [#]T by STRUCT_0:def 3;
hence thesis by A2, PRE_TOPC:def 4;
end;
theorem Th50:
for S, T being TopSpace
st [#]S c= [#]T & ex K being prebasis of S, L being prebasis of T
st K = INTERSECTION(L,{[#]S})
holds S is SubSpace of T
proof
let S, T be TopSpace;
assume A1: [#]S c= [#]T;
given K being prebasis of S, L being prebasis of T such that
A2: K = INTERSECTION(L,{[#]S});
:: the basic idea is to take the canonical bases from the prebases and
:: show the condition of the theorem above
reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;
reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;
for x being object holds x in K0 iff x in INTERSECTION(L0,{[#]S})
proof
let x be object;
hereby
assume A3: x in K0;
then reconsider A = x as Subset of S;
consider X being Subset-Family of S such that
A4: X c= K & X is finite & A = Intersect X by A3, CANTOR_1:def 3;
per cases;
suppose A5: X <> {};
then A6: A = meet X by A4, SETFAM_1:def 9;
defpred P[object,object] means ex D being Subset of T
st $1 = D /\ [#]S & $2 = D;
A7: for x being object st x in X ex y being object st y in L & P[x,y]
proof
let x be object;
assume x in X;
then consider D, S0 being set such that
A8: D in L & S0 in {[#]S} & x = D /\ S0 by A2, A4, SETFAM_1:def 5;
take D;
thus D in L by A8;
reconsider D0 = D as Subset of T by A8;
take D0;
thus thesis by A8, TARSKI:def 1;
end;
consider f being Function such that
A9: dom f = X & rng f c= L and
A10: for x being object st x in X holds P[x,f.x]
from FUNCT_1:sch 6(A7);
reconsider Y = rng f as Subset-Family of T by A9, XBOOLE_1:1;
set B = meet Y;
A11: Y is finite by A4, A9, FINSET_1:8;
A12: f <> {} by A5, A9;
then B = Intersect Y by SETFAM_1:def 9;
then A13: B in L0 by A9, A11, CANTOR_1:def 3;
for y being object holds y in A iff y in B /\ [#]S
proof
let y be object;
hereby
assume A14: y in A;
for D being set st D in Y holds y in D
proof
let D be set;
assume D in Y;
then consider C being object such that
A15: C in dom f & f.C = D by FUNCT_1:def 3;
reconsider C as set by TARSKI:1;
A16: ex D0 being Subset of T st
C = D0 /\ [#]S & D = D0 by A9, A10, A15;
y in C by A6, A9, A14, A15, SETFAM_1:def 1;
hence thesis by A16, TARSKI:def 3, XBOOLE_1:17;
end;
then A17: y in B by A12, SETFAM_1:def 1;
the carrier of S = [#]S by STRUCT_0:def 3;
hence y in B /\ [#]S by A14, A17, XBOOLE_0:def 4;
end;
assume y in B /\ [#]S;
then A18: y in B & y in [#]S by XBOOLE_0:def 4;
for C being set st C in X holds y in C
proof
let C be set;
assume A19: C in X;
then consider D being Subset of T such that
A20: C = D /\ [#]S & f.C = D by A10;
D in Y by A9, A19, A20, FUNCT_1:def 3;
then y in D by A18, SETFAM_1:def 1;
hence thesis by A18, A20, XBOOLE_0:def 4;
end;
hence thesis by A5, A6, SETFAM_1:def 1;
end;
then A21: A = B /\ [#]S by TARSKI:2;
[#]S in {[#]S} by TARSKI:def 1;
hence x in INTERSECTION(L0,{[#]S}) by A13, A21, SETFAM_1:def 5;
end;
suppose X = {};
then A22: A = the carrier of S by A4, SETFAM_1:def 9
.= [#]S by STRUCT_0:def 3;
ex B, S0 being set st B in L0 & S0 in {[#]S} & A = B /\ S0
proof
take [#]T, [#]S;
set Y = the empty Subset-Family of T;
A23: Y c= L & Y is finite by XBOOLE_1:2;
Intersect Y = the carrier of T by SETFAM_1:def 9
.= [#]T by STRUCT_0:def 3;
hence thesis by A1, A22, XBOOLE_1:28,TARSKI:def 1,A23,CANTOR_1:def 3;
end;
hence x in INTERSECTION(L0,{[#]S}) by SETFAM_1:def 5;
end;
end;
assume x in INTERSECTION(L0,{[#]S});
then consider B, S0 being set such that
A24: B in L0 & S0 in {[#]S} & x = B /\ S0 by SETFAM_1:def 5;
consider Y being Subset-Family of T such that
A25: Y c= L & Y is finite & B = Intersect Y by A24, CANTOR_1:def 3;
per cases;
suppose A26: Y <> {};
defpred P[object,object] means ex D being Subset of T
st $2 = D /\ [#]S & $1 = D;
A27: for x being object st x in Y ex y being object st y in K & P[x,y]
proof
let x be object;
assume A28: x in Y;
then reconsider D = x as Subset of T;
take D /\ [#]S;
[#]S in {[#]S} by TARSKI:def 1;
hence D /\ [#]S in K by A2, A25, A28, SETFAM_1:def 5;
take D;
thus thesis;
end;
consider f being Function such that
A29: dom f = Y & rng f c= K and
A30: for x being object st x in Y holds P[x,f.x]
from FUNCT_1:sch 6(A27);
reconsider X = rng f as Subset-Family of S by A29, XBOOLE_1:1;
A31: X is finite by A25, A29, FINSET_1:8;
a32:f <> {} by A26, A29;
reconsider A = x as set by TARSKI:1;
for y being object holds y in A iff
for M being set st M in X holds y in M
proof
let y be object;
hereby
assume A33: y in A;
let M be set;
assume M in X;
then consider D being object such that
A34: D in dom f & f.D = M by FUNCT_1:def 3;
consider D0 being Subset of T such that
A35: M = D0 /\ [#]S & D = D0 by A29, A30, A34;
y in B by A24, A33, XBOOLE_0:def 4;
then y in meet Y by A25, A26, SETFAM_1:def 9;
then A36: y in D0 by A29, A34, A35, SETFAM_1:def 1;
y in S0 by A24, A33, XBOOLE_0:def 4;
then y in [#]S by A24, TARSKI:def 1;
hence y in M by A36, A35, XBOOLE_0:def 4;
end;
assume A37: for M being set st M in X holds y in M;
for M being set st M in Y holds y in M
proof
let M be set;
assume A38: M in Y;
then consider D being Subset of T such that
A39: f.M = D /\ [#]S & M = D by A30;
M /\ [#]S in X by A29, A38, A39, FUNCT_1:3;
then y in M /\ [#]S by A37;
hence thesis by XBOOLE_1:17, TARSKI:def 3;
end;
then y in meet Y by A26, SETFAM_1:def 1;
then A40: y in B by A25, A26, SETFAM_1:def 9;
set M0 = the Element of Y;
consider D0 being Subset of T such that
A41: f.M0 = D0 /\ [#]S & M0 = D0 by A26, A30;
M0 /\ [#]S in X by A29, A26, A41, FUNCT_1:3;
then y in M0 /\ [#]S by A37;
then y in [#]S by XBOOLE_1:17, TARSKI:def 3;
then y in S0 by A24, TARSKI:def 1;
hence thesis by A24, A40, XBOOLE_0:def 4;
end;
then A = meet X by a32, SETFAM_1:def 1;
then x = Intersect X by a32, SETFAM_1:def 9;
hence thesis by A29, A31, CANTOR_1:def 3;
end;
suppose Y = {};
then A42: B = the carrier of T by A25, SETFAM_1:def 9
.= [#]T by STRUCT_0:def 3;
set X = the empty Subset-Family of S;
[#]S = the carrier of S by STRUCT_0:def 3;
then a43: X c= K & X is finite & [#]S = Intersect X
by XBOOLE_1:2, SETFAM_1:def 9;
x = B /\ [#]S by A24, TARSKI:def 1
.= [#]S by A1, A42, XBOOLE_1:28;
hence thesis by a43, CANTOR_1:def 3;
end;
end;
hence thesis by TARSKI:2, Th49;
end;
theorem Th51:
for S, T being TopSpace
st ex K being prebasis of S, L being prebasis of T
st [#]S in K & K = INTERSECTION(L,{[#]S})
holds S is SubSpace of T
proof
let S, T be TopSpace;
given K being prebasis of S, L being prebasis of T such that
A1: [#]S in K & K = INTERSECTION(L,{[#]S});
consider B, S0 being set such that
A2: B in L & S0 in {[#]S} & [#]S = B /\ S0 by A1, SETFAM_1:def 5;
B c= the carrier of T by A2;
then A3: B c= [#]T by STRUCT_0:def 3;
[#]S c= B by A2, XBOOLE_1:17;
hence thesis by A1, A3, Th50, XBOOLE_1:1;
end;
theorem Th52:
for I being non empty set
for J being TopStruct-yielding non-Empty ManySortedSet of I
for i being Element of I holds rng proj(J,i) = the carrier of J.i
proof
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let i be Element of I;
A1: dom Carrier J = I by PARTFUN1:def 2;
thus rng proj(J,i) = rng proj(Carrier J,i) by WAYBEL18:def 4
.= (Carrier J).i by A1, YELLOW17:3
.= [#](J.i) by PENCIL_3:7
.= the carrier of J.i by STRUCT_0:def 3;
end;
registration
let X be set, T be TopStruct;
cluster X --> T -> TopStruct-yielding;
coherence;
end;
definition
let F be Relation;
attr F is TopSpace-yielding means
:Def1:
for x being object st x in rng F holds x is TopSpace;
end;
registration
cluster TopSpace-yielding -> TopStruct-yielding for Relation;
coherence
proof
let F be Relation;
assume F is TopSpace-yielding;
then for x being object st x in rng F holds x is TopStruct;
hence thesis by WAYBEL18:def 1;
end;
end;
registration
cluster TopSpace-yielding -> 1-sorted-yielding for Function;
coherence;
end;
registration
let X be set, T be TopSpace;
cluster X --> T -> TopSpace-yielding;
coherence
proof
for x being set st x in rng(X --> T) holds x is TopSpace by TARSKI:def 1;
hence thesis;
end;
end;
registration
let I be set;
cluster TopSpace-yielding non-Empty for ManySortedSet of I;
existence
proof
take J = I --> the non empty TopSpace;
thus thesis;
end;
end;
definition
let I being non empty set;
let J being TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
redefine func J.i -> non empty TopSpace; :: redefines . (FUNCT_1, definition)
coherence
proof
dom J = I by PARTFUN1:def 2;
then J.i in rng J by FUNCT_1:def 3;
hence thesis by Def1;
end;
end;
definition
let f be Function;
func ProjMap f -> ManySortedFunction of dom f means
:Def2:
for x being object st x in dom f holds it.x = proj(f,x);
existence
proof
deffunc F(object) = proj(f,$1);
consider g being ManySortedSet of dom f such that
A1: for x being object st x in dom f holds g.x = F(x) from PBOOLE:sch 4;
now
let x be object;
assume x in dom g;
then g.x = proj(f,x) by A1;
hence g.x is Function;
end;
then reconsider g as ManySortedFunction of dom f by FUNCOP_1:def 6;
take g;
thus thesis by A1;
end;
uniqueness
proof
let g1, g2 be ManySortedFunction of dom f;
assume that
A2: for x being object st x in dom f holds g1.x = proj(f,x) and
A3: for x being object st x in dom f holds g2.x = proj(f,x);
now
let x be object;
assume A4: x in dom f;
hence g1.x = proj(f,x) by A2 .= g2.x by A3, A4;
end;
hence thesis by PBOOLE:3;
end;
end;
registration
let f be empty Function;
cluster ProjMap f -> empty;
coherence;
end;
registration
let f be non-empty Function;
cluster ProjMap f -> non-empty;
coherence
proof
now
let x be object;
assume x in dom ProjMap f;
then (ProjMap f).x = proj(f,x) by Def2;
hence (ProjMap f).x is non empty;
end;
hence thesis by FUNCT_1:def 9;
end;
end;
registration
let f be non non-empty Function;
cluster ProjMap f -> empty-yielding;
coherence
proof
{} in rng f by RELAT_1:def 9;
then A1: product f = {} by CARD_3:26;
now
let x be object;
assume x in dom ProjMap f;
then (ProjMap f).x = proj(f,x) by Def2;
hence (ProjMap f).x is empty by A1;
end;
hence thesis by FUNCT_1:def 8;
end;
end;
definition
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
func ProjMap J -> ManySortedSet of I equals
ProjMap Carrier J;
coherence
proof
dom Carrier J = I by PARTFUN1:def 2;
hence thesis;
end;
end;
registration
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
cluster ProjMap J -> Function-yielding non empty non-empty;
coherence;
end;
theorem Th53:
for I being non empty set
for J being TopStruct-yielding non-Empty ManySortedSet of I
for i being Element of I holds (ProjMap J).i = proj(J,i)
proof
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let i be Element of I;
dom Carrier J = I by PARTFUN1:def 2;
hence (ProjMap J).i = proj(Carrier J,i) by Def2
.= proj(J,i) by WAYBEL18:def 4;
end;
:: this functor will be used to express the notion of
:: "all but finitely many factors being the full factor space"
:: when considering the canonical base of the product topology
definition
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let f be one-to-one I-valued Function;
func product_basis_selector(J,f) -> ManySortedSet of rng f equals
((ProjMap J).:.:(I-indexing(f"))) | rng f;
coherence
proof
dom (((ProjMap J).:.:(I-indexing(f"))) |rng f)
= dom ((ProjMap J).:.:(I-indexing(f"))) /\ rng f by RELAT_1:61
.= I /\ rng f by PARTFUN1:def 2
.= rng f by XBOOLE_1:28;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let f be empty one-to-one I-valued Function;
cluster product_basis_selector(J,f) -> empty;
coherence;
end;
theorem Th54:
for I being non empty set
for J being TopStruct-yielding non-Empty ManySortedSet of I
for f being one-to-one I-valued Function
for i being Element of I st i in rng f
holds product_basis_selector(J,f).i = proj(J,i).:(f".i)
proof
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let f be one-to-one I-valued Function;
let i be Element of I;
assume A1: i in rng f;
then A2: i in dom(f") by FUNCT_1:33;
thus product_basis_selector(J,f).i
= ((ProjMap J).:.:(I-indexing(f"))).i by A1, FUNCT_1:49
.= ((ProjMap J).i).:((I-indexing(f")).i) by PBOOLE:def 20
.= proj(J,i).:((I-indexing(f")).i) by Th53
.= proj(J,i).:(f".i) by A2, ALGSPEC1:9;
end;
theorem Th55:
for I being non empty set
for J being TopStruct-yielding non-Empty ManySortedSet of I
for f being one-to-one I-valued Function
st f" is non-empty & dom f c= bool product Carrier J
holds product_basis_selector(J,f) is non-empty
proof
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let f be one-to-one I-valued Function;
assume A1: f" is non-empty & dom f c= bool product Carrier J;
assume product_basis_selector(J,f) is non non-empty;
then consider x being object such that
A2: x in dom product_basis_selector(J,f) and
A3: product_basis_selector(J,f).x is empty by FUNCT_1:def 9;
A4: x in rng f by A2;
then reconsider i = x as Element of I;
proj(J,i).:(f".i) is empty by A3, A2, Th54;
then dom proj(J,i) misses f".i by RELAT_1:118;
then dom proj(Carrier J,i) misses f".i by WAYBEL18:def 4;
then A5: product Carrier J misses f".i by CARD_3:def 16;
A6: rng(f") c= bool product Carrier J by A1, FUNCT_1:33;
i in dom(f") by A4, FUNCT_1:33;
then f".i in rng(f") by FUNCT_1:3;
hence contradiction by A1,A5, A6, XBOOLE_1:67;
end;
theorem Th56:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
holds {} in product_prebasis J
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
set P = the empty Subset of product Carrier J;
ex i being set, T being TopStruct, V being Subset of T
st i in I & V is open & T = J.i & P = product ((Carrier J) +* (i,V))
proof
set i = the Element of I;
set V = the empty Subset of J.i;
take i, J.i, V;
dom Carrier J = I by PARTFUN1:def 2;
hence thesis by Th36;
end;
hence thesis by WAYBEL18:def 2;
end;
:: compare YELLOW17:16
theorem Th57:
for I being non empty set
for J being TopStruct-yielding non-Empty ManySortedSet of I
for P being non empty Subset of product Carrier J st P in product_prebasis J
holds ex i being Element of I st proj(J,i).:P is open &
for j being Element of I st j <> i holds proj(J,j).:P = [#](J.j)
proof
let I being non empty set;
let J being TopStruct-yielding non-Empty ManySortedSet of I;
let P be non empty Subset of product Carrier J;
assume P in product_prebasis J;
then consider i being set, T being TopStruct, V being Subset of T such that
A1: i in I & V is open & T = J.i and
A2: P = product( (Carrier J) +* (i,V)) by WAYBEL18:def 2;
reconsider i as Element of I by A1;
reconsider V as Subset of J.i by A1;
take i;
A3: dom Carrier J = I by PARTFUN1:def 2;
a4: rng proj(J,i) = the carrier of J.i by Th52;
proj(J,i).:P = proj(J,i).:(proj(J,i)"V) by A2, WAYBEL18:4;
hence proj(J,i).:P is open by A1, a4, FUNCT_1:77;
let j be Element of I;
assume A5: j <> i;
for x being object holds x in proj(J,j).:P iff x in [#](J.j)
proof
let x be object;
hereby
assume x in proj(J,j).:P;
then consider y being object such that
A6: y in dom proj(J,j) & y in P & x = proj(J,j).y by FUNCT_1:def 6;
consider g being Function such that
A7: y = g & dom g = dom ((Carrier J) +* (i,V)) and
A8: for z being object st z in dom ((Carrier J) +* (i,V))
holds g.z in ((Carrier J) +* (i,V)).z by A2, A6, CARD_3:def 5;
j in dom Carrier J by A3;
then A9: j in dom ((Carrier J) +* (i,V)) by FUNCT_7:30;
x = g.j by A6, A7, YELLOW17:8;
then x in ((Carrier J) +* (i,V)).j by A8, A9;
then x in (Carrier J).j by A5, FUNCT_7:32;
hence x in [#](J.j) by PENCIL_3:7;
end;
assume x in [#](J.j);
then x in (Carrier J).j by PENCIL_3:7;
then A10: x in ((Carrier J) +* (i,V)).j by A5, FUNCT_7:32;
set g0 = the Element of product( (Carrier J) +* (i,V));
set g = g0 +* (j,x);
a11:(Carrier J).i = [#](J.i) by PENCIL_3:7
.= the carrier of J.i by STRUCT_0:def 3;
consider g00 being Function such that
A12: g0 = g00 & dom g00 = dom ((Carrier J) +* (i,V)) and
A13: for z being object st z in dom ((Carrier J) +* (i,V))
holds g00.z in ((Carrier J) +* (i,V)).z by A2, CARD_3:def 5;
ex f being Function st g = 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
proof
take g;
thus g=g & dom g = dom ((Carrier J) +* (i,V)) by A12, FUNCT_7:30;
let z be object;
assume A15: z in dom ((Carrier J) +* (i,V));
z <> j implies g.z = g0.z by FUNCT_7:32;
hence thesis by A10, A12,A13, A15, FUNCT_7:31;
end;
then A16: g in product( (Carrier J) +* (i,V)) by CARD_3:def 5;
a17: product( (Carrier J) +* (i,V)) c= product Carrier J by A3, a11, Th39;
then g in product Carrier J by A16;
then g in dom proj(Carrier J,j) by CARD_3:def 16;
then A18: g in dom proj(J,j) by WAYBEL18:def 4;
A19: j in dom Carrier J by A3;
A20: g is Element of product J by a17,A16, WAYBEL18:def 3;
j in dom g0 by A12, A19, FUNCT_7:30;
then x = g.j by FUNCT_7:31
.= proj(J,j).g by A20, YELLOW17:8;
hence thesis by A2, A16, A18, FUNCT_1:def 6;
end;
hence proj(J,j).:P = [#](J.j) by TARSKI:2;
end;
theorem Th58:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for P being non empty Subset of product Carrier J st P in product_prebasis J
holds (for j being Element of I holds proj(J,j).:P is open) &
ex i being Element of I
st for j being Element of I st j <> i holds proj(J,j).:P = [#](J.j)
proof
let I being non empty set;
let J being TopSpace-yielding non-Empty ManySortedSet of I;
let P be non empty Subset of product Carrier J;
assume P in product_prebasis J;
then consider i being Element of I such that
A1: proj(J,i).:P is open and
A2: for j being Element of I st j <> i holds proj(J,j).:P = [#](J.j)
by Th57;
hereby
let j be Element of I;
j<>i implies proj(J,j).:P = [#](J.j) by A2;
hence proj(J,j).:P is open by A1;
end;
take i;
thus thesis by A2;
end;
theorem Th59:
for I being non empty set
for J being TopStruct-yielding non-Empty ManySortedSet of I
for f being one-to-one I-valued Function
for X being Subset-Family of product Carrier J
st X c= product_prebasis J & dom f = X & f" is non-empty &
for A being Subset of product Carrier J st A in X
holds proj(J,f/.A).:A is open
holds for i being Element of I holds
(not i in rng f implies
proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) = [#](J.i))
& (i in rng f implies
proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) is open)
proof
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let f be one-to-one I-valued Function;
let X be Subset-Family of product Carrier J;
set g = product_basis_selector(J,f);
set P = product(Carrier J +* g);
assume that
A1: X c= product_prebasis J & dom f = X & f" is non-empty and
A2: for A being Subset of product Carrier J st A in X
holds proj(J,f/.A).:A is open;
let i be Element of I;
A3: dom Carrier J = I & dom g = rng f by PARTFUN1:def 2;
A4: g is non-empty by A1, Th55;
A6: now
let j be object;
assume a7: j in dom g;
then j in rng f;
then reconsider k = j as Element of I;
g.j = proj(J,k).:(f".k) by a7, Th54;
then g.j c= the carrier of J.k;
then g.j c= [#](J.k) by STRUCT_0:def 3;
hence g.j c= (Carrier J).j by PENCIL_3:7;
end;
thus not i in rng f implies proj(J,i).:P = [#](J.i)
proof
assume not i in rng f;
then A8: i in dom Carrier J \ dom g by A3, XBOOLE_0:def 5;
thus proj(J,i).:P = proj(Carrier J,i).:P by WAYBEL18:def 4
.= (Carrier J).i by A3, A4, A6, A8, Th24
.= [#](J.i) by PENCIL_3:7;
end;
assume A9: i in rng f;
A11: proj(J,i).:P = proj(Carrier J,i).:P by WAYBEL18:def 4
.= g.i by A4, A3, A6, A9, Th25
.= proj(J,i).:(f".i) by A9, Th54;
A12: f.(f".i) = i by A9, FUNCT_1:35;
i in dom(f") by A9, FUNCT_1:33;
then a13: f".i in rng(f") by FUNCT_1:3;
then A13: f".i in dom f by FUNCT_1:33;
f".i in X by A1,a13,FUNCT_1:33;
then reconsider A = f".i as Subset of product Carrier J;
f/.A = i by A12, A13, PARTFUN1:def 6;
hence thesis by A2, A11, A13,A1;
end;
theorem Th60:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for f being one-to-one I-valued Function
for X being Subset-Family of product Carrier J
st X c= product_prebasis J & dom f = X & f" is non-empty &
for A being Subset of product Carrier J st A in X
holds proj(J,f/.A).:A is open
holds for i being Element of I holds
proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) is open &
(not i in rng f implies
proj(J,i).:product(Carrier J +* product_basis_selector(J,f)) = [#](J.i))
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let f be one-to-one I-valued Function;
let X be Subset-Family of product Carrier J;
set g = product_basis_selector(J,f);
set P = product(Carrier J +* g);
assume that
A1: X c= product_prebasis J & dom f = X & f" is non-empty and
A2: for A being Subset of product Carrier J st A in X
holds proj(J,f/.A).:A is open;
let i be Element of I;
not i in rng f implies
proj(J,i).:P = [#](J.i) by A1, A2, Th59;
hence thesis by A1, A2, Th59;
end;
Lm3:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for P being Subset of product Carrier J
holds P in FinMeetCl product_prebasis J implies
ex X being Subset-Family of product Carrier J,
f being one-to-one I-valued Function
st X c= product_prebasis J & X is finite & P = Intersect X &
dom f = X & P = product(Carrier J +* product_basis_selector(J,f))
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let P be Subset of product Carrier J;
assume A1: P in FinMeetCl product_prebasis J;
consider Y being Subset-Family of product Carrier J such that
A2: Y c= product_prebasis J & Y is finite & P = Intersect Y
by A1, CANTOR_1:def 3;
:: the usual textbook Proof uses induction to prove this theorem.
:: Here, we take a more direct approach.
per cases;
:: the special cases of P = {} and P = product J are handled at the end
suppose A3: Y is non empty & meet Y <> {};
then A4: P = meet Y by A2, SETFAM_1:def 9;
:: P is an intersection of a set Y of prebasis elements (possibly infinite)
:: g maps these prebasis elements to their corresponding coordinate
defpred P[object,object] means
ex i being Element of I, B being Subset of J.i
st $2 = i & B is open & $1 = product(Carrier J +* (i,B));
A5: for x being object st x in Y ex i being object st i in I & P[x,i]
proof
let x be object;
assume x in Y;
then consider i being set, T being TopStruct, V being Subset of T
such that
A6: i in I & V is open & T = J.i & x = product ((Carrier J) +* (i,V))
by A2, WAYBEL18:def 2;
take i;
thus i in I by A6;
reconsider j=i as Element of I by A6;
reconsider V as Subset of J.j by A6;
take j,V;
thus thesis by A6;
end;
consider g being Function of Y, I such that
A7: for x being object st x in Y holds P[x,g.x] from FUNCT_2:sch 1(A5);
:: the set of all g"{i} partitions Y; taking the meet of each one
:: we get a set X of prebasis elements of which two always have a
:: different relevant coordinate (hence ensuring that f will be one-to-one)
set X = {meet (g"{i}) where i is Element of I : g"{i} <> {}};
X c= bool product Carrier J
proof
let x be object;
assume x in X;
then consider i being Element of I such that
A8: x = meet(g"{i}) & g"{i} <> {};
reconsider Z = g"{i} as Subset-Family of product Carrier J by XBOOLE_1:1;
meet Z is Subset of product Carrier J;
hence thesis by A8;
end;
then reconsider X as Subset-Family of product Carrier J;
take X;
:: f is designed to work like g: it maps the elements of X
:: to their corresponding coordinate.
defpred Q[object,object] means ex i being Element of I
st $2 = i & $1 = meet (g"{i}) & g"{i} <> {};
A9: for x being object st x in X ex i being object st i in I & Q[x,i]
proof
let x be object;
assume x in X;
then consider i being Element of I such that
A10: x = meet(g"{i}) & g"{i} <> {};
take i;
thus i in I;
take i;
thus thesis by A10;
end;
consider f being Function of X, I such that
A11: for x being object st x in X holds Q[x,f.x] from FUNCT_2:sch 1(A9);
A12: dom f = X & rng f c= I by FUNCT_2:def 1;
:: confirm the one-to-one property
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1, x2 being object;
assume A13: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then consider i1 being Element of I such that
A14: f.x1 = i1 & x1 = meet(g"{i1}) & g"{i1} <> {} by A11;
ex i2 being Element of I st
f.x2 = i2 & x2 = meet(g"{i2}) & g"{i2} <> {} by A11, A13;
hence thesis by A13, A14;
end;
then reconsider f as one-to-one I-valued Function by FUNCT_1:def 4;
take f;
:: needed for technical reasons
A16: for i being Element of I, S being non empty set
st g"{i} <> {} & S in g"{i}
ex V being non empty open Subset of J.i
st S = product (Carrier J +* (i,V))
proof
let i be Element of I;
let S be non empty set;
assume a17: g"{i} <> {} & S in g"{i};
then A17: S in Y & g.S in {i} by FUNCT_2:38;
then consider j being set, T being TopStruct, V being Subset of T
such that A18: j in I & V is open & T = J.j and
A19: S = product (Carrier J +* (j,V)) by A2, WAYBEL18:def 2;
a20:dom Carrier J = I by PARTFUN1:def 2;
per cases;
suppose A21: V <> (Carrier J).j;
A22: V is non empty by A19, a20, Th36,A18;
A23: i = j
proof
g.S = i by A17, TARSKI:def 1;
then consider k being Element of I, B being Subset of J.k such that
A24: i = k & B is open and
A25: S = product(Carrier J +* (k,B)) by A7, a17;
B is non empty by a20, A25, Th36;
hence thesis by A19, A18,a20, A21, A22, A24, A25, Th42;
end;
then reconsider V as non empty open Subset of J.i
by A19, a20, Th36, A18;
take V;
thus thesis by A19, A23;
end;
suppose V = (Carrier J).j;
then A26: S = product Carrier J by A19, FUNCT_7:35
.= product(Carrier J +* (i,(Carrier J).i)) by FUNCT_7:35;
take [#](J.i);
thus thesis by A26, PENCIL_3:7;
end;
end;
A27: X is non empty
proof
A28: ex i being Element of I st g"{i} <> {}
proof
set A = the Element of Y;
consider i being Element of I, B being Subset of J.i such that
A29: g.A = i & B is open & A = product(Carrier J +* (i,B)) by A3, A7;
take i;
g.A in {i} by A29, TARSKI:def 1;
hence g"{i} <> {} by A3, FUNCT_2:38;
end;
ex x being object st x in X
proof
consider i being Element of I such that
A30: g"{i} <> {} by A28;
meet(g"{i}) in X by A30;
hence thesis;
end;
hence thesis;
end;
:: this Lemma is basically asserting that
:: $\bigcap_{i\in g"\{k\}} \pi^{-1}_{k} (U_{i})
:: = \pi^{-1}_{k} (\bigcap_{i\in g"\{k\}} U_{i})$ holds for each $k$
A31: for x being Element of X
st x = meet (g"{f.x}) & g"{f.x} <> {} & x <> {}
ex Z being Subset-Family of J.(In(f.x, I))
st Z = {proj(J,In(f.x, I)).:V
where V is Subset of product Carrier J : V in g"{f.x}} &
Z is open & Z is finite & Z is non empty &
x = product (Carrier J +* (f.x, meet Z))
proof
let x be Element of X;
set i = In(f.x, I);
a32: f.x in rng f by A12, A27, FUNCT_1:3;
then A32: i = f.x by SUBSET_1:def 8;
assume A33: x = meet (g"{f.x}) & g"{f.x} <> {} & x <> {};
set Z = {proj(J,In(f.x, I)).:V
where V is Subset of product Carrier J : V in g"{f.x}};
Z c= bool the carrier of J.i
proof
let y be object;
assume y in Z;
then ex V being Subset of product Carrier J st
y = proj(J,i).:V & V in g"{f.x};
hence thesis;
end;
then reconsider Z as Subset-Family of J.i;
take Z;
thus Z = {proj(J,In(f.x, I)).:V
where V is Subset of product Carrier J : V in g"{f.x}};
for A being Subset of J.i holds A in Z implies A is open
proof
let A be Subset of J.i;
assume A in Z;
then consider V being Subset of product Carrier J such that
A35: A = proj(J,i).:V & V in g"{f.x};
V in Y & (V is empty or V is non empty) by A35;
hence thesis by A2, A35, Th58;
end;
hence Z is open by TOPS_2:def 1;
defpred R[object,object] means ex V being Subset of product Carrier J
st $1 = V & $2 = proj(J,i).:V;
A37: for y,z1,z2 being object st y in g"{i} & R[y,z1] & R[y,z2]
holds z1 = z2;
A38: for y being object st y in g"{i} ex z being object st R[y,z]
proof
let y be object;
assume y in g"{i};
then y in Y;
then reconsider V = y as Subset of product Carrier J;
take proj(J,i).:V,V;
thus thesis;
end;
consider h being Function such that
A39: dom h = g"{i} & for y being object st y in g"{i}
holds R[y,h.y] from FUNCT_1:sch 2(A37,A38);
a45: for y being object holds y in rng h iff y in Z
proof
let y be object;
hereby
assume y in rng h;
then consider z being object such that
A40: z in dom h & y = h.z by FUNCT_1:def 3;
ex V being Subset of product Carrier J st
z = V & h.z = proj(J,i).:V by A39, A40;
hence y in Z by A32, A39, A40;
end;
assume y in Z;
then consider V being Subset of product Carrier J such that
A42: y = proj(J,i).:V & V in g"{f.x};
A43: V in dom h by a32,SUBSET_1:def 8, A39, A42;
ex V0 being Subset of product Carrier J st
V = V0 & h.V = proj(J,i).:V0 by A32, A39, A42;
hence thesis by A42, A43, FUNCT_1:def 3;
end;
then rng h = Z by TARSKI:2;
hence Z is finite by A2, A39, FINSET_1:8;
h.the Element of g"{f.x} in rng h by A32, A33, A39, FUNCT_1:3;
hence A46: Z is non empty by a45;
a47: dom Carrier J = I by PARTFUN1:def 2;
then A47: i in dom Carrier J;
for y being object holds y in meet(g"{i}) iff
y in product (Carrier J +* (i,meet Z))
proof
let y be object;
hereby
assume A49: y in meet(g"{i});
set S0 = the Element of g"{i};
S0 is non empty by A32, A33, A49, SETFAM_1:def 1;
then consider V0 being non empty open Subset of J.i such that
A50: S0 = product (Carrier J +* (i,V0)) by A16, A32, A33;
y in product (Carrier J +* (i,V0))
by A32, A33, A49, A50, SETFAM_1: def 1;
then consider f0 being Function such that
A51: y = f0 & dom f0 = dom (Carrier J +* (i,V0)) and
A52: for z being object st z in dom (Carrier J +* (i,V0))
holds f0.z in (Carrier J +* (i,V0)).z by CARD_3:def 5;
now
take f0;
thus y = f0 by A51;
thus dom f0 = dom Carrier J by A51, FUNCT_7:30
.= dom (Carrier J +* (i,meet Z)) by FUNCT_7:30;
let z be object;
assume z in dom (Carrier J +* (i,meet Z));
then A53: z in dom Carrier J by FUNCT_7:30;
per cases;
suppose A54: z <> i;
then A55: (Carrier J +* (i,meet Z)).z
=(Carrier J).z by FUNCT_7:32
.= (Carrier J +* (i,V0)).z by A54, FUNCT_7:32;
z in dom (Carrier J +* (i,V0)) by A53, FUNCT_7:30;
hence f0.z in (Carrier J +* (i,meet Z)).z by A52, A55;
end;
suppose A56: z = i;
then A57: (Carrier J +* (i,meet Z)).z
= meet Z by A53, FUNCT_7:31;
for S being set st S in Z holds f0.z in S
proof
let S be set;
assume S in Z;
then consider S1 being Subset of product Carrier J
such that A58: S = proj(J,i).:S1 & S1 in g"{f.x};
S1 is non empty by A32, A49, A58, SETFAM_1:def 1;
then consider V1 being non empty open Subset of J.i
such that A59: S1 = product (Carrier J +* (i,V1))
by A16, A32, A58;
V1 c= the carrier of J.i;
then V1 c= [#](J.i) by STRUCT_0:def 3;
then A60: V1 c= (Carrier J).i by PENCIL_3:7;
proj(J,i) = proj(Carrier J,i) by WAYBEL18:def 4;
then A61: S = V1 by A58, A59, A60, a47, Th43;
y in S1 by A32, A49, A58, SETFAM_1:def 1;
then consider f1 being Function such that
A62: y = f1 & dom f1 = dom (Carrier J +* (i,V1)) and
A63: for a being object st a in dom (Carrier J +* (i,V1))
holds f1.a in (Carrier J +* (i,V1)).a by A59, CARD_3:def 5;
i in dom (Carrier J +* (i,V1)) by A47, FUNCT_7:30;
then f1.i in (Carrier J +* (i,V1)).i by A63;
hence f0.z in S by A51, A56, A61, A62, a47, FUNCT_7:31;
end;
hence f0.z in (Carrier J +* (i,meet Z)).z
by A57,A46,SETFAM_1:def 1;
end;
end;
hence y in product (Carrier J +* (i,meet Z)) by CARD_3:def 5;
end;
assume A64: y in product (Carrier J +* (i,meet Z));
for S being set st S in g"{i} holds y in S
proof
let S be set;
assume A65: S in g"{i};
S is non empty by A32, A33, A65, SETFAM_1:4;
then consider V being non empty open Subset of J.i such that
A66: S = product (Carrier J +* (i,V)) by A16, A65;
V c= the carrier of J.i;
then V c= [#](J.i) by STRUCT_0:def 3;
then A67: V c= (Carrier J).i by PENCIL_3:7;
proj(J,i) = proj(Carrier J,i) by WAYBEL18:def 4;
then A68: proj(J,i).:S = V by a47, A66, A67, Th43;
S in Y by A65;
then V in Z by A32, A65, A68;
then product (Carrier J +* (i,meet Z))
c= product (Carrier J +* (i,V)) by a47, Th38,SETFAM_1:3;
hence y in S by A64, A66;
end;
hence y in meet(g"{i}) by A32, A33, SETFAM_1:def 1;
end;
hence x = product (Carrier J +* (f.x, meet Z)) by A32, A33, TARSKI:2;
end;
:: this is proven easily with the Lemma
for x being object holds x in X implies x in product_prebasis J
proof
let x be object;
assume A69: x in X;
per cases;
suppose A70: x <> {};
ex i being set, T being TopStruct, V being Subset of T
st i in I & V is open & T = J.i & x = product (Carrier J +* (i,V))
proof
consider i being Element of I such that
A71: f.x = i & x = meet(g"{i}) & g"{i} <> {} by A11, A69;
consider Z being Subset-Family of J.(In(f.x, I)) such that
Z = {proj(J,In(f.x, I)).:V
where V is Subset of product Carrier J : V in g"{f.x}} and
A72: Z is open & Z is finite & Z is non empty and
A73: x = product (Carrier J +* (f.x, meet Z))
by A31, A69, A70, A71;
set W = meet Z;
take i, J.(In(f.x, I)), W;
thus thesis by A71, A73,A72, TOPS_2:20;
end;
hence thesis by A69, WAYBEL18:def 2;
end;
suppose x = {};
hence thesis by Th56;
end;
end;
hence X c= product_prebasis J by TARSKI:def 3;
:: we show that changing the order of intersections (as we grouped some
:: with meet g"{i}) doesn't change the set
for x being object holds x in meet X iff x in meet Y
proof
let x be object;
hereby
assume A74: x in meet X;
for Sy being set st Sy in Y holds x in Sy
proof
let Sy be set;
assume A75: Sy in Y;
then consider i being Element of I, B being Subset of J.i such that
A76: g.Sy = i & B is open & Sy = product(Carrier J +* (i,B)) by A7;
g.Sy in {i} by A76, TARSKI:def 1;
then A77: Sy in g"{i} by A75, FUNCT_2:38;
then meet(g"{i}) in X;
then A78: x in meet(g"{i}) by A74, SETFAM_1:def 1;
meet(g"{i}) c= Sy by A77, SETFAM_1:3;
hence x in Sy by A78;
end;
hence x in meet Y by A3, SETFAM_1:def 1;
end;
assume A79: x in meet Y;
for Sx being set st Sx in X holds x in Sx
proof
let Sx be set;
assume Sx in X;
then consider i being Element of I such that
A80: Sx = meet(g"{i}) & g"{i} <> {};
for A being set st A in g"{i} holds x in A by A79, SETFAM_1:def 1;
hence x in Sx by A80, SETFAM_1:def 1;
end;
hence x in meet X by A27, SETFAM_1:def 1;
end;
then A81: meet X = meet Y by TARSKI:2;
:: we map g"{i} to meet g"{i}; since the g"{i} partition Y and
:: Y is finite, X must be finite, too
thus X is finite
proof
set S = {g"{i} where i is Element of I : i in rng g};
a82: S is a_partition of Y by Th5;
defpred R[object,object] means ex M being set st $1 = M & $2 = meet M;
A83: for A being object st A in S ex B being object st B in X & R[A,B]
proof
let A be object;
assume A in S;
then consider i being Element of I such that
A84: A = g"{i} & i in rng g;
take meet(g"{i});
consider x being object such that
A85: x in Y & g.x = i by A84, FUNCT_2:11;
i in {i} by TARSKI:def 1;
then x in g"{i} by A85, FUNCT_2:38;
hence meet(g"{i}) in X;
take g"{i};
thus thesis by A84;
end;
consider h being Function of S,X such that
A86: for A being object st A in S holds R[A,h.A]
from FUNCT_2:sch 1(A83);
for B being object st B in X ex A being object st A in S & B = h.A
proof
let B be object;
assume B in X;
then consider i being Element of I such that
A87: B = meet(g"{i}) & g"{i} <> {};
take g"{i};
consider x being object such that
A88: x in g"{i} by A87, XBOOLE_0:def 1;
x in Y & g.x in {i} by A88, FUNCT_2:38;
then A90: g.x = i by TARSKI:def 1;
dom g = Y by FUNCT_2:def 1;
then i in rng g by A88, A90, FUNCT_1:def 3;
hence g"{i} in S;
then ex M being set st
g"{i} = M & h.(g"{i}) = meet M by A86;
hence thesis by A87;
end;
then rng h = X by FUNCT_2:10;
hence X is finite by a82,A2;
end;
thus P = Intersect X by A4, A27, A81, SETFAM_1:def 9;
thus dom f = X by FUNCT_2:def 1;
:: we show that if x has the form
:: $\pi_1^{-1}(U_1)\cap\ldots\cap\pi_n^{-1}(U_n)$ if and only if it has
:: the form $\prod_{i\in I} U_i$ with all but finitely many of the
:: factors being the whole factor space
set F = Carrier J +* product_basis_selector(J,f);
for x being object holds x in meet X iff x in product F
proof
let x be object;
A92: I = I \/ rng f by XBOOLE_1:12
.= dom Carrier J \/ rng f by PARTFUN1:def 2
.= dom Carrier J \/ dom product_basis_selector(J,f) by PARTFUN1:def 2
.= dom F by FUNCT_4:def 1;
hereby
assume A93: x in meet X;
consider A0 being object such that
A94: A0 in X by A27, XBOOLE_0:def 1;
reconsider A0 as set by TARSKI:1;
consider i0 being Element of I such that
A95: f.A0 = i0 & A0 = meet(g"{i0}) & g"{i0} <> {} by A11, A94;
A0 <> {} by A3, A81, A94, SETFAM_1:4;
then consider Z0 being Subset-Family of J.(In(f.A0, I)) such that
Z0 = {proj(J,In(f.A0, I)).:V
where V is Subset of product Carrier J : V in g"{f.A0}} and
Z0 is open & Z0 is finite & Z0 is non empty and
A96: A0 = product (Carrier J +* (f.A0, meet Z0)) by A31, A94, A95;
x in A0 by A93, A94, SETFAM_1:def 1;
then consider h being Function such that
A97: x = h & dom h = dom(Carrier J +* (f.A0, meet Z0)) and
A98: for y being object st y in dom(Carrier J +* (f.A0, meet Z0))
holds h.y in (Carrier J +* (f.A0, meet Z0)).y
by A96, CARD_3:def 5;
A99: dom h = I by A97, PARTFUN1:def 2;
A100: dom h = dom F by A92, A97, PARTFUN1:def 2;
for y being object st y in dom F holds h.y in F.y
proof
let y be object;
assume y in dom F;
then reconsider i = y as Element of I by A92;
i in dom h by A99;
then A101: i in dom Carrier J by A97, FUNCT_7:30;
per cases;
suppose A102: y in rng f;
then y in dom product_basis_selector(J,f) by PARTFUN1:def 2;
then F.y = product_basis_selector(J,f).i by FUNCT_4:13;
then A103: F.y = proj(J,i).:(f".i) by A102, Th54;
consider A being object such that
A104: A in X & f.A = i by A102, FUNCT_2:11;
reconsider A as set by TARSKI:1;
consider j being Element of I such that
A105: f.A = j & A = meet (g"{j}) & g"{j} <> {} by A11, A104;
A <> {} by A3, A81, A104, SETFAM_1:4;
then consider Z being Subset-Family of J.(In(f.A, I)) such that
Z = {proj(J,In(f.A, I)).:V
where V is Subset of product Carrier J : V in g"{f.A}} and
Z is open & Z is finite & Z is non empty and
A106: A = product(Carrier J +* (f.A, meet Z)) by A31, A104, A105;
reconsider Z as Subset-Family of J.i by A104;
a107: h in A by A93, A97, A104, SETFAM_1:def 1;
dom(Carrier J +* (f.A, meet Z)) = I by PARTFUN1:def 2;
then h.i in (Carrier J +* (f.A, meet Z)).i by a107,A106, CARD_3:9;
then A108: h.i in meet Z by A104, A101, FUNCT_7:31;
ex z being object st z in dom proj(J,i) &
z in meet(g"{i}) & proj(J,i).z = h.i
proof
set z0 = the Element of product Carrier J;
set z = z0 +* (i,h.i);
take z;
meet Z c= the carrier of J.i;
then meet Z c= [#](J.i) by STRUCT_0:def 3;
then A109: meet Z c= (Carrier J).i by PENCIL_3:7;
A110: z in product(Carrier J +* (i, meet Z)) by A101, A108, Th37;
product(Carrier J +* (i, meet Z)) c= product Carrier J
by A101, A109, Th39;
then z in product Carrier J by A110;
then A111: z in dom proj(Carrier J,i) by CARD_3:def 16;
hence z in dom proj(J,i) & z in meet(g"{i})
by A104, A105, A106, A101, A108, Th37,WAYBEL18:def 4;
A112: i in dom z0 by A101, CARD_3:9;
thus proj(J,i).z = proj(Carrier J,i).z by WAYBEL18:def 4
.= z.i by A111, CARD_3:def 16
.= h.i by A112, FUNCT_7:31;
end;
then h.i in proj(J,i).:meet(g"{i}) by FUNCT_1:def 6;
hence h.y in F.y by A103, A105, A12, A104, FUNCT_1:34;
end;
suppose not y in rng f;
then not y in dom product_basis_selector(J,f);
then A114: F.y = (Carrier J).y by FUNCT_4:11;
reconsider Z0 as Subset-Family of J.i0 by A95;
meet Z0 c= the carrier of J.i0;
then meet Z0 c= [#](J.i0) by STRUCT_0:def 3;
then A115: meet Z0 c= (Carrier J).i0 by PENCIL_3:7;
i0 in I;
then i0 in dom Carrier J by PARTFUN1:def 2;
then A116: product(Carrier J +* (i0, meet Z0)) c= product Carrier J
by A115, Th39;
h in product(Carrier J +* (i0, meet Z0))
by A95, A97, A98, CARD_3:9;
hence h.y in F.y by A114,A101,A116, CARD_3:9;
end;
end;
hence x in product F by A97, A100, CARD_3:def 5;
end;
assume x in product F;
then consider h being Function such that
A117: h = x & dom h = dom F and
A118: for y being object st y in dom F holds h.y in F.y
by CARD_3:def 5;
for A being set st A in X holds h in A
proof
let A be set;
assume A119: A in X;
then consider i being Element of I such that
A120: f.A = i & A = meet(g"{i}) & g"{i} <> {} by A11;
A121: f".i = A by A12, A119, A120, FUNCT_1:34;
A <> {} by A3, A81, A119, SETFAM_1:4;
then consider Z being Subset-Family of J.(In(f.A, I)) such that
A122: Z = {proj(J,In(f.A, I)).:V
where V is Subset of product Carrier J : V in g"{f.A}} and
Z is open & Z is finite & Z is non empty and
A124: A = product (Carrier J +* (f.A, meet Z)) by A31, A119, A120;
A125: dom h = dom(Carrier J +* (f.A, meet Z))
by A92, A117, PARTFUN1:def 2;
for y being object st y in dom(Carrier J +* (f.A, meet Z))
holds h.y in (Carrier J +* (f.A, meet Z)).y
proof
let y be object;
assume A126: y in dom(Carrier J +* (f.A, meet Z));
per cases;
suppose y <> i;
then A127: (Carrier J +* (f.A, meet Z)).y = (Carrier J).y
by A120, FUNCT_7:32;
A128: y in dom Carrier J by A126, FUNCT_7:30;
A129: h.y in F.y by A92, A118,A126;
per cases;
suppose A130: y in rng f;
then reconsider i0 = y as Element of I;
y in dom product_basis_selector(J,f) by A130, PARTFUN1:def 2;
then F.y = product_basis_selector(J,f).i0 by FUNCT_4:13
.= proj(J,i0).:(f".i0) by A130, Th54;
then F.y c= rng proj(J,i0) by RELAT_1:111;
then F.y c= rng proj(Carrier J,i0) by WAYBEL18:def 4;
then F.y c= (Carrier J).i0 by A128, YELLOW17:3;
hence thesis by A127, A129;
end;
suppose not y in rng f;
then not y in dom product_basis_selector(J,f);
hence thesis by A127, A129, FUNCT_4:11;
end;
end;
suppose A131: y = i;
i in I;
then a132: i in dom Carrier J by PARTFUN1:def 2;
A133: i in rng f by A12, A119, A120, FUNCT_1:def 3;
then i in dom product_basis_selector(J,f) by PARTFUN1:def 2;
then A134: F.i = product_basis_selector(J,f).i by FUNCT_4:13
.= proj(J,i).:meet(g"{i}) by A120, A121, A133, Th54;
reconsider G = g"{i} as Subset-Family of product Carrier J
by XBOOLE_1:1;
h.i in proj(J,i).:meet(g"{i}) by A92, A118, A134;
then h.i in meet {proj(J,i).:B
where B is Subset of product Carrier J : B in G}
by Th3, TARSKI:def 3;
hence thesis by A131, a132, FUNCT_7:31, A120, A122;
end;
end;
hence h in A by A124, A125, CARD_3:9;
end;
hence thesis by A27, A117, SETFAM_1:def 1;
end;
hence thesis by A4, A81, TARSKI:2;
end;
:: trivial cases
suppose A136: Y is empty;
reconsider f = the empty Function as one-to-one I-valued Function
by XBOOLE_1:2, RELAT_1:38, RELAT_1:def 19;
take Y, f;
thus Y c= product_prebasis J & Y is finite & P = Intersect Y by A2;
thus dom f = Y by A136;
product_basis_selector(J,f) is empty;
hence thesis by A2, A136, SETFAM_1:def 9;
end;
suppose Y is non empty & meet Y = {};
then A138: P = {} by A2, SETFAM_1:def 9;
set i = the Element of I;
set V = the empty Subset of J.i;
a139: dom Carrier J = I by PARTFUN1:def 2;
then A140: product (Carrier J +* (i,V)) = {} by Th36;
then product (Carrier J +* (i,V)) in product_prebasis J by Th56;
then reconsider A = product (Carrier J +* (i,V)) as
Subset of product Carrier J;
set X = {A};
set f = A .--> i;
take X, f;
thus X c= product_prebasis J & X is finite by A140,Th56, ZFMISC_1:31;
{} in X by A140, TARSKI:def 1;
then meet X = {} by SETFAM_1:4;
hence P = Intersect X by A138, SETFAM_1:def 9;
thus dom f = dom ({A} --> i) by FUNCOP_1:def 9
.= X;
set F = Carrier J +* product_basis_selector(J,f);
ex j being object st j in dom F & F.j = {}
proof
take i;
i in dom Carrier J \/ dom product_basis_selector(J,f)
by a139,XBOOLE_1:7, TARSKI:def 3;
hence i in dom F by FUNCT_4:def 1;
i in {i} by TARSKI:def 1;
then i in rng({A} --> i) by FUNCOP_1:8;
then A142: i in rng f by FUNCOP_1:def 9;
then i in dom product_basis_selector(J,f) by PARTFUN1:def 2;
hence F.i = product_basis_selector(J,f).i by FUNCT_4:13
.= proj(J,i).:(f".i) by A142, Th54
.= proj(J,i).:((i .--> A).i) by NECKLACE:9
.= proj(J,i).:A by FUNCOP_1:72
.= {} by A140;
end;
then {} in rng F by FUNCT_1:def 3;
hence thesis by A138,CARD_3:26;
end;
end;
:: Theorem of canonical product base characterization
theorem
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for P being Subset of product Carrier J
holds P in FinMeetCl product_prebasis J iff
ex X being Subset-Family of product Carrier J,
f being one-to-one I-valued Function
st X c= product_prebasis J & X is finite & P = Intersect X & dom f = X &
P = product(Carrier J +* product_basis_selector(J,f))
by Lm3, CANTOR_1:def 3;
theorem Th62:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for P being non empty Subset of product Carrier J
holds P in FinMeetCl product_prebasis J implies
ex X being Subset-Family of product Carrier J,
f being one-to-one I-valued Function
st X c= product_prebasis J & X is finite & P = Intersect X & dom f = X &
for i being Element of I holds proj(J,i).:P is open &
(not i in rng f implies proj(J,i).:P = [#](J.i))
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let P be non empty Subset of product Carrier J;
assume A1: P in FinMeetCl product_prebasis J;
consider X being Subset-Family of product Carrier J,
f being one-to-one I-valued Function such that
A2: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
A3: P = product(Carrier J +* product_basis_selector(J,f)) by A1, Lm3;
take X, f;
thus X c= product_prebasis J & X is finite & P = Intersect X & dom f = X
by A2;
A4: now
let A be Subset of product Carrier J;
assume A5: A in X;
A is empty implies proj(J,f/.A).:A = {}(J.(f/.A));
hence proj(J,f/.A).:A is open by A2, A5, Th58;
end;
f" is non-empty
proof
assume f" is non non-empty;
then {} in rng(f") by RELAT_1:def 9;
then {} in X by A2, FUNCT_1:33;
then X is non empty & meet X = {} by SETFAM_1:4;
hence contradiction by A2, SETFAM_1:def 9;
end;
hence thesis by A2, A3, A4, Th60;
end;
theorem Th63:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for P being non empty Subset of product Carrier J
holds P in FinMeetCl product_prebasis J implies
ex I0 being finite Subset of I st for i being Element of I holds
proj(J,i).:P is open & (not i in I0 implies proj(J,i).:P = [#](J.i))
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let P be non empty Subset of product Carrier J;
assume P in FinMeetCl product_prebasis J;
then consider X being Subset-Family of product Carrier J,
f being one-to-one I-valued Function such that
A1: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
A2: for i being Element of I holds proj(J,i).:P is open &
(not i in rng f implies proj(J,i).:P = [#](J.i)) by Th62;
reconsider I0 = rng f as finite Subset of I by A1, FINSET_1:8;
take I0;
thus thesis by A2;
end;
:: characterization of the canonical prebasis of
:: the product topology over one factor
theorem Th64:
for I being 1-element set
for J being TopStruct-yielding non-Empty ManySortedSet of I
for i being Element of I, P being Subset of product Carrier J
holds P in product_prebasis J iff ex V being Subset of J.i
st V is open & P = product ({i} --> V)
proof
let I be 1-element set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let i be Element of I;
card I = 1 by CARD_1:def 7;
then A1: I = {i} by ORDERS_5:2;
the carrier of J.i = [#](J.i) by STRUCT_0:def 3
.= (Carrier J).i by PENCIL_3:7;
then A2: Carrier J = {i} --> the carrier of J.i by A1, Th7;
let P be Subset of product Carrier J;
hereby
assume P in product_prebasis J;
then consider j being set, T being TopStruct, V being Subset of T such that
A3: j in I & V is open & T = J.j and
A4: P = product ((Carrier J) +* (j,V)) by WAYBEL18:def 2;
A5: i = j by A1, A3, TARSKI:def 1;
reconsider W=V as Subset of J.i by A1, A3, TARSKI:def 1;
take W;
thus W is open by A3, A5;
thus P = product ( (i .--> the carrier of J.i) +* (i,W))
by A2, A4, A5, FUNCOP_1:def 9
.= product (i .--> W) by Th44
.= product ({i} --> W) by FUNCOP_1:def 9;
end;
given V being Subset of J.i such that
A6: V is open & P = product ({i} --> V);
P = product (i .--> V) by A6, FUNCOP_1:def 9
.= product ( (i .--> the carrier of J.i) +* (i,V)) by Th44
.= product ((Carrier J) +* (i,V)) by A2, FUNCOP_1:def 9;
hence thesis by A6,WAYBEL18:def 2;
end;
:: before I used the Theorem of canonical product base characterization
:: the Proof of this theorem was 4 times as long.
Lm4:
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i being Element of I, P being Subset of product Carrier J
holds P in FinMeetCl product_prebasis J implies ex V being Subset of J.i
st V is open & P = product ({i} --> V)
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
card I = 1 by CARD_1:def 7;
then A1: I = {i} by ORDERS_5:2;
the carrier of J.i = [#](J.i) by STRUCT_0:def 3
.= (Carrier J).i by PENCIL_3:7;
then A2: Carrier J = {i} --> the carrier of J.i by A1, Th7;
let P be Subset of product Carrier J;
assume P in FinMeetCl product_prebasis J;
then consider X being Subset-Family of product Carrier J,
f being one-to-one I-valued Function such that
A3: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
A4: P = product(Carrier J +* product_basis_selector(J,f)) by Lm3;
set F = Carrier J +* product_basis_selector(J,f);
per cases by A1, ZFMISC_1:33;
suppose rng f = {};
then a5: product_basis_selector(J,f) = {};
take [#](J.i);
thus thesis by a5,A2, A4, STRUCT_0:def 3;
end;
suppose A6: rng f = {i};
then A7: dom f = {f".i} by Th1;
A8: i in rng f by A6, TARSKI:def 1;
A9: f".i in X by A3, A7, TARSKI:def 1;
then reconsider V0 = f".i as Subset of product Carrier J;
reconsider V = proj(J,i).:V0 as Subset of J.i;
take V;
V0 is empty or V0 is non empty;
hence V is open by A3, A9, Th58;
A10: product_basis_selector(J,f)
= {i} --> product_basis_selector(J,f).i by A6, Th7
.= {i} --> proj(J,i).:V0 by A8, Th54;
dom Carrier J = {i} by A1, PARTFUN1:def 2;
then dom Carrier J = dom product_basis_selector(J,f) by A6, PARTFUN1:def 2;
hence thesis by A4,A10, FUNCT_4:19;
end;
end;
Lm5:
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i being Element of I, P being Subset of product Carrier J
holds P in FinMeetCl product_prebasis J iff ex V being Subset of J.i
st V is open & P = product ({i} --> V)
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
let P be Subset of product Carrier J;
thus P in FinMeetCl product_prebasis J implies ex V being Subset of J.i
st V is open & P = product ({i} --> V) by Lm4;
given V being Subset of J.i such that
A2: V is open & P = product ({i} --> V);
P in product_prebasis J by A2, Th64;
hence thesis by TARSKI:def 3, CANTOR_1:4;
end;
Lm6:
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i being Element of I, P being Subset of product Carrier J
holds P in UniCl FinMeetCl product_prebasis J iff ex V being Subset of J.i
st V is open & P = product ({i} --> V)
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
card I = 1 by CARD_1:def 7;
then A1: I = {i} by ORDERS_5:2;
the carrier of J.i = [#](J.i) by STRUCT_0:def 3
.= (Carrier J).i by PENCIL_3:7;
then A2: Carrier J = {i} --> the carrier of J.i by A1, Th7;
let P be Subset of product Carrier J;
hereby
assume P in UniCl FinMeetCl product_prebasis J;
then consider Y being Subset-Family of product Carrier J such that
A3: Y c= FinMeetCl product_prebasis J & P = union Y by CANTOR_1:def 1;
:: each basis element points to an open set, we take the set
:: of all these open sets and show that (set) P points to their union
defpred P[object] means ex W being open Subset of J.i st
W = $1 & product({i} --> W) in Y;
consider Z being Subset of bool the carrier of J.i such that
A4: for x being set holds x in Z iff
x in bool the carrier of J.i & P[x] from SUBSET_1:sch 1;
reconsider Z as Subset-Family of J.i;
set V = union Z;
take V;
A5: for W being Subset of J.i holds W in Z iff W is open
& product({i} --> W) in Y
proof
let W be Subset of J.i;
hereby
assume W in Z;
then ex W2 being open Subset of J.i st
W2 = W & product({i} --> W2) in Y by A4;
hence W is open & product({i} --> W) in Y;
end;
assume W is open & product({i} --> W) in Y;
hence thesis by A4;
end;
then for W being Subset of J.i holds W in Z implies W is open;
hence V is open by TOPS_2:def 1, TOPS_2:19;
for x being object holds x in union Y iff x in product ({i} --> V)
proof
let x be object;
hereby
assume x in union Y;
then consider K being set such that
A7: x in K & K in Y by TARSKI:def 4;
reconsider K as Subset of product Carrier J by A7;
consider L being Subset of J.i such that
A8: L is open & K = product({i} --> L) by A3, A7, Lm5;
A9: L in Z by A5, A7, A8;
A10: L is non empty
proof
assume L is empty;
then dom({i} --> L) = {i} & rng({i} --> L) = {{}}
by FUNCOP_1:8;
hence contradiction by A7, A8, Lm1;
end;
then consider y being Element of L such that
A11: x = {i} --> y by A7, A8, Th16;
y in V by A9, A10, TARSKI:def 4;
hence x in product({i} --> V) by A11, Th16;
end;
assume A12: x in product({i} --> V);
A13: V is non empty
proof
assume V is empty;
then rng({i} --> V) = {{}} by FUNCOP_1:8;
hence contradiction by A12, Lm1;
end;
then consider y being Element of V such that
A14: x = {i} --> y by A12, Th16;
consider L being set such that
A15: y in L & L in Z by A13, TARSKI:def 4;
reconsider L as Subset of J.i by A15;
reconsider K= product({i} --> L) as Subset of product Carrier J
by A2, Th14;
A16: K in Y by A5, A15;
x in K by A14, A15, Th16;
hence thesis by A16, TARSKI:def 4;
end;
hence P = product ({i} --> V) by A3, TARSKI:2;
end;
assume ex V being Subset of J.i st V is open & P = product ({i} --> V);
then P in FinMeetCl product_prebasis J by Lm5;
hence thesis by CANTOR_1:1, TARSKI:def 3;
end;
Lm7:
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
holds UniCl FinMeetCl product_prebasis J = product_prebasis J
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
for x being object holds x in UniCl FinMeetCl product_prebasis J
iff x in product_prebasis J
proof
let x be object;
set i = the Element of I;
hereby
assume A1: x in UniCl FinMeetCl product_prebasis J;
then reconsider P=x as Subset of product Carrier J;
ex V being Subset of J.i st V is open & P = product({i} --> V)
by A1, Lm6;
hence x in product_prebasis J by Th64;
end;
assume A2: x in product_prebasis J;
then reconsider P=x as Subset of product Carrier J;
ex V being Subset of J.i st V is open & P = product({i} --> V)
by A2, Th64;
hence thesis by Lm6;
end;
hence thesis by TARSKI:2;
end;
theorem Th65:
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
holds the topology of product J = product_prebasis J
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
reconsider T = product J as TopSpace;
reconsider K = product_prebasis J as Subset-Family of T by WAYBEL18:def 3;
K is prebasis of T by WAYBEL18:def 3;
then A1: UniCl FinMeetCl K = the topology of T by YELLOW_9:22, YELLOW_9:23;
FinMeetCl K = FinMeetCl product_prebasis J by WAYBEL18:def 3;
then UniCl FinMeetCl K = UniCl FinMeetCl product_prebasis J
by WAYBEL18:def 3;
hence thesis by A1, Lm7;
end;
:: characterization of open sets in the product topology over one factor
theorem
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i being Element of I, P being Subset of product J
holds P is open iff ex V being Subset of J.i
st V is open & P = product ({i} --> V)
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
let P be Subset of product J;
hereby
assume P is open;
then P in the topology of product J by PRE_TOPC:def 2;
then P in product_prebasis J by Th65;
hence ex V being Subset of J.i st V is open & P = product ({i} --> V)
by Th64;
end;
A1: P is Subset of product Carrier J by WAYBEL18:def 3;
assume ex V being Subset of J.i st V is open & P = product ({i} --> V);
then P in product_prebasis J by A1, Th64;
then P in the topology of product J by Th65;
hence P is open by PRE_TOPC:def 2;
end;
registration
let I being non empty set;
let J being TopStruct-yielding non-Empty ManySortedSet of I;
let i be Element of I;
cluster proj(J,i) -> continuous onto;
coherence
proof
rng proj(J,i) = the carrier of J.i by Th52;
hence thesis by WAYBEL18:5, FUNCT_2:def 3;
end;
end;
registration
let I being non empty set;
let J being TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
cluster proj(J,i) -> open;
coherence
proof
A1: ex B being Basis of product J st
for P being Subset of product J st P in B holds proj(J,i).:P is open
proof
set B = FinMeetCl product_prebasis J;
set T = product J;
reconsider K = product_prebasis J as Subset-Family of T
by WAYBEL18:def 3;
FinMeetCl K is Basis of T by WAYBEL18:def 3, YELLOW_9:23;
then reconsider B as Basis of product J by WAYBEL18:def 3;
take B;
let P be Subset of product J;
assume A2: P in B;
per cases;
suppose P <> {};
then ex I0 being finite Subset of I st
for j being Element of I holds proj(J,j).:P is open &
(not j in I0 implies proj(J,j).:P = [#](J.j))
by A2, Th63;
hence thesis;
end;
suppose P = {};
then proj(J,i).:P is empty & proj(J,i).:P is Subset of J.i;
hence thesis;
end;
end;
product J is TopSpace & J.i is TopSpace;
hence thesis by A1, Th45;
end;
end;
theorem Th67:
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i being Element of I holds proj(J,i) is being_homeomorphism
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
card I = 1 by CARD_1:def 7;
then A1: I = {i} by ORDERS_5:2;
:: we already have all properties ready and just need to collect them
set f = proj(J,i);
A2: dom f = the carrier of product J by FUNCT_2:def 1
.= [#]product J by STRUCT_0:def 3;
the carrier of J.i = [#](J.i) by STRUCT_0:def 3
.= (Carrier J).i by PENCIL_3:7;
then A3: Carrier J = {i} --> the carrier of J.i by A1, Th7;
A4: rng f = the carrier of J.i by FUNCT_2:def 3
.= [#](J.i) by STRUCT_0:def 3;
a5: f = proj(Carrier J,i) by WAYBEL18:def 4
.= proj(i .--> the carrier of J.i,i) by A3, FUNCOP_1:def 9;
f" is continuous by a5, TOPREALA:14;
hence f is being_homeomorphism by A2, A4, a5, TOPS_2:def 5;
end;
:: the product topology over one factor is homeomorphic to that factor
theorem
for I being 1-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i being Element of I
holds product J, J.i are_homeomorphic
proof
let I be 1-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
proj(J,i) is being_homeomorphism by Th67;
hence thesis by T_0TOPSP:def 1;
end;
Lm8:
for I being 2-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I, P being Subset of product Carrier J st i <> j
holds P in product_prebasis J implies
(ex V being Subset of J.i st
V is open & P = product( (i,j) --> (V,[#](J.j)) ) ) or
(ex W being Subset of J.j st
W is open & P = product( (i,j) --> ([#](J.i),W) ) )
proof
let I be 2-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i, j be Element of I, P be Subset of product Carrier J;
assume A1: i <> j & P in product_prebasis J;
then consider k being set, T being TopStruct, U being Subset of T such that
A2: k in I & U is open & T = J.k & P = product ((Carrier J) +* (k,U))
by WAYBEL18:def 2;
k in {i,j} by A1, A2, Th8;
then per cases by TARSKI:def 2;
suppose A3: k = i;
then reconsider V = U as Subset of J.i by A2;
now
take V;
thus V is open by A2, A3;
(Carrier J).j = [#](J.j) by PENCIL_3:7;
hence P = product( (i,j) --> (V,[#](J.j)) ) by A2,A1, A3, Th34;
end;
hence thesis;
end;
suppose A4: k = j;
then reconsider W = U as Subset of J.j by A2;
now
take W;
thus W is open by A2, A4;
(Carrier J).i = [#](J.i) by PENCIL_3:7;
hence P = product( (i,j) --> ([#](J.i),W) ) by A2,A1, A4, Th34;
end;
hence thesis;
end;
end;
:: characterization of the canonical prebasis of
:: the product topology over two factors
theorem Th69:
for I being 2-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I, P being Subset of product Carrier J st i <> j
holds P in product_prebasis J iff
(ex V being Subset of J.i st
V is open & P = product((i,j) --> (V,[#](J.j)) ) ) or
(ex W being Subset of J.j st
W is open & P = product((i,j) --> ([#](J.i),W) ) )
proof
let I be 2-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i, j be Element of I, P be Subset of product Carrier J;
assume A1: i <> j;
hence P in product_prebasis J implies
(ex V being Subset of J.i st
V is open & P = product( (i,j) --> (V,[#](J.j)) ) ) or
(ex W being Subset of J.j st
W is open & P = product( (i,j) --> ([#](J.i),W) ) ) by Lm8;
assume
(ex V being Subset of J.i st
V is open & P = product( (i,j) --> (V,[#](J.j)) ) ) or
(ex W being Subset of J.j st
W is open & P = product( (i,j) --> ([#](J.i),W) ) );
then per cases;
suppose ex V being Subset of J.i st
V is open & P = product( (i,j) --> (V,[#](J.j)) );
then consider V being Subset of J.i such that
A2: V is open & P = product( (i,j) --> (V,[#](J.j)) );
(Carrier J).j = [#](J.j) by PENCIL_3:7;
then P = product ((Carrier J) +* (i,V)) by A1, A2, Th34;
hence P in product_prebasis J by A2,WAYBEL18:def 2;
end;
suppose ex W being Subset of J.j st
W is open & P = product( (i,j) --> ([#](J.i),W) );
then consider W being Subset of J.j such that
A3: W is open & P = product( (i,j) --> ([#](J.i),W) );
(Carrier J).i = [#](J.i) by PENCIL_3:7;
then P = product ((Carrier J) +* (j,W)) by A1, A3, Th34;
hence P in product_prebasis J by A3,WAYBEL18:def 2;
end;
end;
Lm9:
for I being 2-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I, P being Subset of product Carrier J st i <> j
holds P in FinMeetCl product_prebasis J implies
ex V being Subset of J.i, W being Subset of J.j
st V is open & W is open & P = product((i,j) --> (V,W))
proof
let I be 2-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i,j be Element of I, P be Subset of product Carrier J;
assume A1: i <> j & P in FinMeetCl product_prebasis J;
then consider X being Subset-Family of product Carrier J,
f being one-to-one I-valued Function such that
A2: X c= product_prebasis J & X is finite & P = Intersect X & dom f = X and
A3: P = product(Carrier J +* product_basis_selector(J,f)) by Lm3;
set F = Carrier J +* product_basis_selector(J,f);
i in I & j in I;
then A4: i in dom Carrier J & j in dom Carrier J by PARTFUN1:def 2;
rng f c= I;
then rng f c= {i,j} by A1, Th8;
then per cases by ZFMISC_1:36;
:: all cases are structured the same way and are very much alike
suppose rng f = {};
then product_basis_selector(J,f) = {};
then A5: P = product (i,j) --> ((Carrier J).i,(Carrier J).j)
by A1, A3, Th9
.= product (i,j) --> ([#](J.i),(Carrier J).j) by PENCIL_3:7
.= product (i,j) --> ([#](J.i),[#](J.j)) by PENCIL_3:7;
thus thesis by A5;
end;
suppose A6: rng f = {i};
then A7: dom f = {f".i} by Th1;
A8: i in rng f by A6, TARSKI:def 1;
A9: f".i in X by A2, A7, TARSKI:def 1;
then reconsider V0 = f".i as Subset of product Carrier J;
reconsider V = proj(J,i).:V0 as Subset of J.i;
take V, [#](J.j);
V0 is empty or V0 is non empty;
hence V is open & [#](J.j) is open by A2, A9, Th58;
product_basis_selector(J,f)
= {i} --> product_basis_selector(J,f).i by A6, Th7
.= {i} --> proj(J,i).:(f".i) by A8, Th54
.= i .--> V by FUNCOP_1:def 9;
then F = Carrier J +* (i,V) by A4, FUNCT_7:def 3
.= (i,j) --> (V,(Carrier J).j) by A1, Th34
.= (i,j) --> (V,[#](J.j)) by PENCIL_3:7;
hence thesis by A3;
end;
suppose A10: rng f = {j};
then A11: dom f = {f".j} by Th1;
A12: j in rng f by A10, TARSKI:def 1;
A13: f".j in X by A2, A11, TARSKI:def 1;
then reconsider W0 = f".j as Subset of product Carrier J;
reconsider W = proj(J,j).:W0 as Subset of J.j;
take [#](J.i), W;
thus [#](J.i) is open;
W0 is empty or W0 is non empty;
hence W is open by A2, A13, Th58;
product_basis_selector(J,f)
= {j} --> product_basis_selector(J,f).j by A10, Th7
.= {j} --> proj(J,j).:(f".j) by A12, Th54
.= j .--> W by FUNCOP_1:def 9;
then F = Carrier J +* (j,W) by A4, FUNCT_7:def 3
.= (i,j) --> ((Carrier J).i,W) by A1, Th34
.= (i,j) --> ([#](J.i),W) by PENCIL_3:7;
hence thesis by A3;
end;
suppose A14: rng f = {i,j};
then A15: dom f = {f".i, f".j} by Th2;
A16: i in rng f & j in rng f by A14, TARSKI:def 2;
A17: f".i in X & f".j in X by A2, A15, TARSKI:def 2;
then reconsider V0 = f".i as Subset of product Carrier J;
reconsider V = proj(J,i).:V0 as Subset of J.i;
reconsider W0 = f".j as Subset of product Carrier J by A17;
reconsider W = proj(J,j).:W0 as Subset of J.j;
take V, W;
V0 is empty or V0 is non empty;
hence V is open by A2, A17, Th58;
W0 is empty or W0 is non empty;
hence W is open by A2, A17, Th58;
rng f = I by A1, A14, Th8;
then A18: product_basis_selector(J,f) = (i,j)
--> (product_basis_selector(J,f).i,product_basis_selector(J,f).j)
by A1, Th9
.= (i,j) --> (product_basis_selector(J,f).i,proj(J,j).:(f".j))
by A16, Th54
.= (i,j) --> (V,W) by A16, Th54;
dom Carrier J = I by PARTFUN1:def 2
.= {i,j} by A1, Th8;
then dom Carrier J =dom product_basis_selector(J,f) by A14, PARTFUN1:def 2;
hence thesis by A3, A18, FUNCT_4:19;
end;
end;
:: characterization of the canonical basis of
:: the product topology over two factors
theorem
for I being 2-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I, P being Subset of product Carrier J st i <> j
holds P in FinMeetCl product_prebasis J iff
ex V being Subset of J.i, W being Subset of J.j
st V is open & W is open & P = product((i,j) --> (V,W))
proof
let I be 2-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i,j be Element of I, P be Subset of product Carrier J;
assume A1: i <> j;
hence P in FinMeetCl product_prebasis J implies
ex V being Subset of J.i, W being Subset of J.j
st V is open & W is open & P = product((i,j) --> (V,W)) by Lm9;
given V being Subset of J.i, W being Subset of J.j such that
A2: V is open & W is open & P = product((i,j) --> (V,W));
ex Y being Subset-Family of product Carrier J
st Y c= product_prebasis J & Y is finite & P = Intersect Y
proof
set V0 = product(Carrier J +* (i,V));
set W0 = product(Carrier J +* (j,W));
set Y = {V0,W0};
A3: dom Carrier J = I by PARTFUN1:def 2;
(Carrier J).i = [#](J.i) & (Carrier J).j = [#](J.j) by PENCIL_3:7;
then a4: (Carrier J).i = the carrier of J.i &
(Carrier J).j = the carrier of J.j by STRUCT_0:def 3;
A5: V0 c= product Carrier J & W0 c= product Carrier J by a4,A3, Th39;
then reconsider Y as Subset-Family of product Carrier J by ZFMISC_1:32;
take Y;
A6: V0 = product((i,j) --> (V,(Carrier J).j)) &
W0 = product((i,j) --> ((Carrier J).i,W)) by A1, Th34;
then V0 = product((i,j) --> (V,[#](J.j))) &
W0 = product((i,j) --> ([#](J.i),W)) by PENCIL_3:7;
then V0 in product_prebasis J & W0 in product_prebasis J
by A1, A2, A5, Th69;
hence Y c= product_prebasis J & Y is finite by ZFMISC_1:32;
P c= V0 & P c= W0 by A2, a4, A6, Th28;
then A7: P c= V0 /\ W0 by XBOOLE_1:19;
V0 /\ W0 c= P
proof
let x be object;
assume x in V0 /\ W0;
then A8: x in V0 & x in W0 by XBOOLE_0:def 4;
then consider g being Function such that
A9: g = x & dom g = dom (i,j) --> (V,(Carrier J).j) and
A10: for y being object st y in dom (i,j) --> (V,(Carrier J).j)
holds g.y in ((i,j) --> (V,(Carrier J).j)).y by A6, CARD_3:def 5;
A12: dom g = {i,j} by A9, FUNCT_4:62
.= dom (i,j) --> (V,W) by FUNCT_4:62;
for y being object st y in dom (i,j) --> (V,W)
holds g.y in ((i,j) --> (V,W)).y
proof
let y be object;
assume y in dom (i,j) --> (V,W);
then A13: y in {i,j} by FUNCT_4:62;
then per cases by TARSKI:def 2;
suppose A14: y = i;
then A15: ((i,j) --> (V,(Carrier J).j)).y = V by A1, FUNCT_4:63
.= ((i,j) --> (V,W)).y by A1, A14, FUNCT_4:63;
y in dom (i,j) --> (V,(Carrier J).j) by A13, FUNCT_4:62;
hence thesis by A10, A15;
end;
suppose A16: y = j;
then A17: ((i,j) --> ((Carrier J).i,W)).y = W by FUNCT_4:63
.= ((i,j) --> (V,W)).y by A16, FUNCT_4:63;
y in dom (i,j) --> ((Carrier J).i,W) by A13, FUNCT_4:62;
hence thesis by A6, A8, A9, CARD_3:9, A17;
end;
end;
hence x in P by A2, A9, A12, CARD_3:9;
end;
then P = V0 /\ W0 by A7, XBOOLE_0:def 10;
then P = meet Y by SETFAM_1:11;
hence P = Intersect Y by SETFAM_1:def 9;
end;
hence P in FinMeetCl product_prebasis J by CANTOR_1:def 3;
end;
theorem ::Th71:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I
holds <: proj(J,i), proj(J,j) :> is Function of product J, [: J.i, J.j :]
by BORSUK_1:def 2;
:: can be generalized: P only needs to contain the square F.i x F.j
:: at one point p, the Proof works the same
theorem Th72:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for P being Subset of product Carrier J
for i,j being Element of I st i <> j &
(ex F being ManySortedSet of I st P = product F &
for k being Element of I holds F.k c= (Carrier J).k)
holds <: proj(J,i), proj(J,j) :>.:P = [: proj(J,i).:P, proj(J,j).:P :]
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let P be Subset of product Carrier J;
let i,j be Element of I;
assume that A1: i <> j and
A2: ex F being ManySortedSet of I st P = product F &
for k being Element of I holds F.k c= (Carrier J).k;
consider F being ManySortedSet of I such that
A3: P = product F and
A4: for k being Element of I holds F.k c= (Carrier J).k by A2;
per cases;
suppose A5: F is non-empty;
for y being object holds y in [: proj(J,i).:P, proj(J,j).:P :]
implies y in <: proj(J,i), proj(J,j) :>.:P
proof
let y be object;
assume y in [: proj(J,i).:P, proj(J,j).:P :];
then consider y1, y2 being object such that
A6: y1 in proj(J,i).:P & y2 in proj(J,j).:P & y = [y1,y2]
by ZFMISC_1:def 2;
A7: dom F = I by PARTFUN1:def 2
.= dom Carrier J by PARTFUN1:def 2;
i in I & j in I;
then A8: i in dom F & j in dom F by PARTFUN1:def 2;
for k being object st k in dom F holds F.k c= (Carrier J).k by A4;
:: here is the square F.i x F.j I mentioned above
then proj(Carrier J,i).:P = F.i & proj(Carrier J,j).:P = F.j
by A3, A5, A7, A8, Th26;
then A9: proj(J,i).:P = F.i & proj(J,j).:P = F.j by WAYBEL18:def 4;
set p0 = the Element of product F;
set p = p0 +* (i,j) --> (y1,y2);
A10: dom <: proj(J,i), proj(J,j) :> = dom proj(J,i) /\ dom proj(J,j)
by FUNCT_3:def 7
.= dom proj(Carrier J,i) /\ dom proj(J,j) by WAYBEL18:def 4
.= dom proj(Carrier J,i) /\ dom proj(Carrier J,j) by WAYBEL18:def 4;
then A11: dom <: proj(J,i), proj(J,j) :>
= dom proj(Carrier J,i) /\ product Carrier J by CARD_3:def 16
.= product Carrier J /\ product Carrier J by CARD_3:def 16
.= product Carrier J;
p in product(F +* (i,j) --> (F.i,F.j)) by A1, A6, A5, A9, Th30;
then A12: p in P by A3, A8, Th11;
then A14: p in dom proj(Carrier J,i) & p in dom proj(Carrier J,j)
by A11,A10, XBOOLE_0:def 4;
A15: proj(J,i).p = proj(Carrier J,i).p by WAYBEL18:def 4
.= p.i by A14, CARD_3:def 16
.= y1 by A1, FUNCT_4:84;
A16: proj(J,j).p = proj(Carrier J,j).p by WAYBEL18:def 4
.= p.j by A14, CARD_3:def 16
.= y2 by A1, FUNCT_4:84;
<: proj(J,i), proj(J,j) :>.p = [y1,y2] by A11,A12,A15,A16, FUNCT_3:def 7;
hence thesis by A6, A12, A11, FUNCT_1:def 6;
end;
then A17: [: proj(J,i).:P, proj(J,j).:P :] c= <: proj(J,i), proj(J,j) :>.:P
by TARSKI:def 3;
<: proj(J,i), proj(J,j) :>.:P c= [: proj(J,i).:P, proj(J,j).:P :]
by FUNCT_3:56;
hence thesis by A17, XBOOLE_0:def 10;
end;
suppose not F is non-empty;
then {} in rng F by RELAT_1:def 9;
then P = {} by A3, CARD_3:26;
then <: proj(J,i), proj(J,j) :>.:P = {} & proj(J,i).:P = {};
hence thesis by ZFMISC_1:90;
end;
end;
theorem Th73:
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I, f being Function of product J, [: J.i, J.j :]
st i <> j & f = <: proj(J,i), proj(J,j) :>
holds f is onto open
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i,j be Element of I, f be Function of product J, [: J.i, J.j :];
assume A1: i <> j & f = <: proj(J,i), proj(J,j) :>;
:: onto is corrolary from previous theorem
a2: for k being Element of I holds Carrier J.k c= (Carrier J).k;
A3: for k being Element of I holds
proj(J,k).:[#]product Carrier J = the carrier of J.k
proof
let k be Element of I;
thus proj(J,k).:[#]product Carrier J
= proj(J,k).:product Carrier J by SUBSET_1:def 3
.= proj(J,k).:dom proj(Carrier J,k) by CARD_3:def 16
.= proj(J,k).:dom proj(J,k) by WAYBEL18:def 4
.= rng proj(J,k) by RELAT_1:113
.= the carrier of J.k by Th52;
end;
rng f = <: proj(J,i), proj(J,j) :>.:dom f by A1, RELAT_1:113
.= <: proj(J,i), proj(J,j) :>.:the carrier of product J by FUNCT_2:def 1
.= <: proj(J,i), proj(J,j) :>.:product Carrier J by WAYBEL18:def 3
.= <: proj(J,i), proj(J,j) :>.:[#]product Carrier J by SUBSET_1:def 3
.= [: proj(J,i).:[#]product Carrier J, proj(J,j).:[#]product Carrier J :]
by A1, SUBSET_1:def 3,a2, Th72
.= [: the carrier of J.i, proj(J,j).:[#]product Carrier J :] by A3
.= [: the carrier of J.i, the carrier of J.j :] by A3
.= the carrier of [: J.i, J.j :] by BORSUK_1:def 2;
hence f is onto by FUNCT_2:def 3;
:: openness will be shown using the canonical base of the product space,
:: the Theorem of canonical base characterisation and the previous theorem
ex B being Basis of product J st
for P being Subset of product J st P in B holds f.:P is open
proof
set B = FinMeetCl product_prebasis J;
set T = product J;
reconsider K = product_prebasis J as Subset-Family of T
by WAYBEL18:def 3;
FinMeetCl K is Basis of T by WAYBEL18:def 3, YELLOW_9:23;
then reconsider B as Basis of product J by WAYBEL18:def 3;
take B;
let P be Subset of product J;
assume A4: P in B;
A5: proj(J,i).:P is open & proj(J,j).:P is open
proof
per cases;
suppose P <> {};
then ex I0 being finite Subset of I st
for j being Element of I holds proj(J,j).:P is open &
(not j in I0 implies proj(J,j).:P = [#](J.j)) by A4, Th63;
hence thesis;
end;
suppose P = {};
then proj(J,i).:P is empty & proj(J,i).:P is Subset of J.i &
proj(J,j).:P is empty & proj(J,j).:P is Subset of J.j;
hence thesis;
end;
end;
A7: ex F being ManySortedSet of I st P = product F &
for k being Element of I holds F.k c= (Carrier J).k
proof
consider X being Subset-Family of product Carrier J,
g being one-to-one I-valued Function such that
X c= product_prebasis J & X is finite & P=Intersect X & dom g = X and
A8: P = product(Carrier J +* product_basis_selector(J,g))
by A4, Lm3;
set F = Carrier J +* product_basis_selector(J,g);
reconsider F as ManySortedSet of I;
take F;
thus P = product F by A8;
let k be Element of I;
per cases;
suppose A9: k in rng g;
then k in dom product_basis_selector(J,g) by PARTFUN1:def 2;
then a10: F.k = product_basis_selector(J,g).k by FUNCT_4:13
.= proj(J,k).:(g".k) by A9, Th54;
rng proj(J,k) = the carrier of J.k by Th52
.= [#](J.k) by STRUCT_0:def 3
.= (Carrier J).k by PENCIL_3:7;
hence thesis by a10,RELAT_1:111;
end;
suppose not k in rng g;
then not k in dom product_basis_selector(J,g);
hence thesis by FUNCT_4:11;
end;
end;
P is Subset of product Carrier J by WAYBEL18:def 3;
then f.:P = [: proj(J,i).:P, proj(J,j).:P :] by A1, A7, Th72;
hence f.:P is open by A5, BORSUK_1:6;
end;
hence f is open by Th45;
end;
theorem Th74:
for I being 2-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I, f being Function of product J, [: J.i, J.j :]
st i <> j & f = <: proj(J,i), proj(J,j) :>
holds f is being_homeomorphism
proof
let I be 2-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i,j be Element of I, f be Function of product J, [: J.i, J.j :];
:: we need to show the one-to-one property, the rest can simply be collected
assume A1: i <> j & f = <: proj(J,i), proj(J,j) :>;
A2: dom f = the carrier of product J by FUNCT_2:def 1
.= [#]product J by STRUCT_0:def 3;
A3: f is onto open by A1, Th73;
then rng f = the carrier of [: J.i, J.j :] by FUNCT_2:def 3;
then A4: rng f = [#][: J.i, J.j :] by STRUCT_0:def 3;
for x1, x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1, x2 be object;
assume A5: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then a6:f.x1 = [proj(J,i).x1, proj(J,j).x1] &
f.x2 = [proj(J,i).x2, proj(J,j).x2] by A1, FUNCT_3:def 7;
x1 in dom proj(J,i) /\ dom proj(J,j) &
x2 in dom proj(J,i) /\ dom proj(J,j) by A1, A5, FUNCT_3:def 7;
then x1 in dom proj(J,i) & x2 in dom proj(J,j) by XBOOLE_0:def 4;
then a7: x1 in dom proj(Carrier J,i) & x2 in dom proj(Carrier J,j)
by WAYBEL18:def 4;
reconsider g1 = x1, g2 = x2 as Element of product J by A5;
proj(J,i).x1 = g1.i & proj(J,i).x2 = g2.i &
proj(J,j).x1 = g1.j & proj(J,j).x2 = g2.j by YELLOW17:8;
then A8: g1.i = g2.i & g1.j = g2.j by a6,A5, XTUPLE_0:1;
A9: Carrier J = (i,j) --> ((Carrier J).i,(Carrier J).j) by A1, Th9;
then consider a1,b1 being object such that
a1 in (Carrier J).i & b1 in (Carrier J).j and
A10: g1 = (i,j) --> (a1,b1) by A1, a7, Th29;
consider a2,b2 being object such that
a2 in (Carrier J).i & b2 in (Carrier J).j and
A11: g2 = (i,j) --> (a2,b2) by A1, a7, A9, Th29;
g1.i = a1 & g2.i = a2 & g1.j = b1 & g2.j = b2 by A1, A10, A11, FUNCT_4:63;
hence thesis by A8, A10, A11;
end;
then A12: f is one-to-one by FUNCT_1:def 4;
A13: f is continuous by A1, YELLOW12:41;
f" is continuous by A3, A12, TOPREALA:14;
hence f is being_homeomorphism by A2, A4, A12, A13, TOPS_2:def 5;
end;
:: the product topology over two factors is
:: homeomorphic to the cartesian product of these two factors
:: ( [: S,T :], [: T,S :] are_homeomorphic is a corrolary,
:: but it is already in the MML)
theorem
for I being 2-element set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for i,j being Element of I st i <> j
holds product J, [: J.i,J.j :] are_homeomorphic
proof
let I be 2-element set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i,j be Element of I;
assume A1: i <> j;
reconsider f = <: proj(J,i), proj(J,j) :>
as Function of product J, [: J.i, J.j :] by BORSUK_1:def 2;
f is being_homeomorphism by A1,Th74;
hence thesis by T_0TOPSP:def 1;
end;
registration
let I1, I2 be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I2;
let f be Function of I1, I2;
cluster J*f -> TopSpace-yielding non-Empty;
coherence
proof
hereby
let y be object;
assume y in rng(J*f);
then y in rng J by RELAT_1:26, TARSKI:def 3;
hence y is TopSpace by Def1;
end;
for S being 1-sorted st S in rng(J*f) holds S is non empty
proof
let S be 1-sorted;
assume S in rng (J*f);
then S in rng J by RELAT_1:26, TARSKI:def 3;
hence thesis by WAYBEL_3:def 7;
end;
hence thesis by WAYBEL_3:def 7;
end;
end;
definition
let I1, I2 be non empty set;
let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
let p be Function of I1, I2;
assume that A1: p is bijective and
A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
mode ProductHomeo of J1, J2, p -> Function of product J1, product J2 means
:Def5:
ex F being ManySortedFunction of I1 st
(for i being Element of I1 ex f being Function of J1.i, (J2*p).i
st F.i = f & f is being_homeomorphism) &
for g being Element of product J1, i being Element of I1 holds
(it.g).(p.i) = (F.i).(g.i); :: H(g)_{p_i} = F_i(g_i)
existence
proof
defpred P[object,object] means
ex i being Element of I1, f being Function of J1.i, (J2*p).i
st $1 = i & $2 = f & f is being_homeomorphism;
A3: for x being object st x in I1 ex y being object st P[x,y]
proof
let x be object;
assume x in I1;
then reconsider i = x as Element of I1;
consider f being Function of J1.i, (J2*p).i such that
A4: f is being_homeomorphism by A2, T_0TOPSP:def 1;
take f,i,f;
thus thesis by A4;
end;
consider F being ManySortedSet of I1 such that
A5: for x being object st x in I1 holds P[x,F.x] from PBOOLE:sch 3(A3);
A6: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
st F.i = f & f is being_homeomorphism
proof
let i be Element of I1;
consider j being Element of I1, f being Function of J1.j, (J2*p).j
such that A7: i = j & F.i = f & f is being_homeomorphism by A5;
reconsider f as Function of J1.i, (J2*p).i by A7;
take f;
thus thesis by A7;
end;
for x being object st x in dom F holds F.x is Function
proof
let x be object;
assume x in dom F;
then reconsider i = x as Element of I1;
ex f being Function of J1.i, (J2*p).i st
F.i = f & f is being_homeomorphism by A6;
hence thesis;
end;
then reconsider F as ManySortedFunction of I1 by FUNCOP_1:def 6;
defpred Q[object,object] means
ex g being Element of product J1, h being Element of product J2
st $1 = g & $2 = h &
for i being Element of I1 holds h.(p.i) = (F.i).(g.i);
A9: for x being object st x in the carrier of product J1
ex y being object st y in the carrier of product J2 & Q[x,y]
proof
let x be object;
assume x in the carrier of product J1;
then reconsider g = x as Element of product J1;
:: since Q is a little bit sophisticated, we need to
:: construct the RHS using another scheme
deffunc H(object) = (F.$1).(g.$1);
consider h0 being ManySortedSet of I1 such that
A10: for i being Element of I1 holds h0.i = H(i) from PBOOLE:sch 5;
reconsider p9 = p as one-to-one Function by A1;
rng(p9") = dom p9 by FUNCT_1:33
.= I1 by FUNCT_2:def 1
.= dom h0 by PARTFUN1:def 2;
then dom(h0*(p9")) = dom(p9") by RELAT_1:27
.= rng p9 by FUNCT_1:33
.= I2 by A1, FUNCT_2:def 3;
then reconsider h = h0*(p9") as ManySortedSet of I2
by PARTFUN1:def 2, RELAT_1:def 18;
take h;
A11: dom h = I2 by PARTFUN1:def 2
.= dom Carrier J2 by PARTFUN1:def 2;
for x being object st x in dom Carrier J2 holds h.x in (Carrier J2).x
proof
let x be object;
assume x in dom Carrier J2;
then reconsider j = x as Element of I2;
j in I2;
then A12: j in rng p9 by A1, FUNCT_2:def 3;
then A13: j in dom(p9") by FUNCT_1:33;
then p9".j in rng(p9") by FUNCT_1:3;
then p9".j in dom p9 by FUNCT_1:33;
then reconsider i = p9".j as Element of I1 by FUNCT_2:def 1;
A14: (F.i).(g.i) = h0.i by A10
.= h.j by A13, FUNCT_1:13;
consider f being Function of J1.i, (J2*p).i such that
A15: F.i = f & f is being_homeomorphism by A6;
A16: f.(g.i) in the carrier of (J2*p).i;
i in I1;
then i in dom p by FUNCT_2:def 1;
then (J2*p).i = J2.(p.i) by FUNCT_1:13
.= J2.j by A12, FUNCT_1:35;
then h.j in [#](J2.j) by A14, A15, A16, STRUCT_0:def 3;
hence thesis by PENCIL_3:7;
end;
then H: h in product Carrier J2 by A11, CARD_3:9;
hence h in the carrier of product J2 by WAYBEL18:def 3;
reconsider h as Element of product J2 by H,WAYBEL18:def 3;
take g, h;
now
let i be Element of I1;
i in I1;
then A17: i in dom p by PARTFUN1:def 2;
then p9.i in rng p9 by FUNCT_1:3;
then A18: p9.i in dom(p9") by FUNCT_1:33;
thus h.(p.i) = h0.(p9".(p9.i)) by A18, FUNCT_1:13
.= h0.i by A17, FUNCT_1:34
.= (F.i).(g.i) by A10;
end;
hence thesis;
end;
consider IT being Function
of the carrier of product J1, the carrier of product J2 such that
A19: for x being object st x in the carrier of product J1 holds Q[x,IT.x]
from FUNCT_2:sch 1(A9);
reconsider IT as Function of product J1, product J2;
take IT, F;
now
let g be Element of product J1;
A20: ex g0 being Element of product J1,
h being Element of product J2 st
g = g0 & IT.g = h &
for i being Element of I1 holds h.(p.i) = (F.i).(g0.i) by A19;
let i be Element of I1;
thus (IT.g).(p.i) = (F.i).(g.i) by A20;
end;
hence thesis by A6;
end;
end;
:: characterization of images of certain subsets under product homeomorphism
theorem Th76:
for I1, I2 being non empty set
for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
for p being Function of I1, I2, H being ProductHomeo of J1, J2, p
for F being ManySortedFunction of I1
st p is bijective &
(for i being Element of I1 ex f being Function of J1.i, (J2*p).i
st F.i = f & f is being_homeomorphism) &
(for g being Element of product J1, i being Element of I1 holds
(H.g).(p.i) = (F.i).(g.i))
holds for i being Element of I1, U being Subset of J1.i holds
H.:product(Carrier J1 +* (i,U)) = product(Carrier J2 +* (p.i,(F.i).:U))
proof
let I1, I2 be non empty set;
let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;
let F be ManySortedFunction of I1;
assume that
A1: p is bijective and
A2: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
st F.i = f & f is being_homeomorphism and
A3: for g being Element of product J1, i being Element of I1 holds
(H.g).(p.i) = (F.i).(g.i);
let i be Element of I1, U be Subset of J1.i;
reconsider j = p.i as Element of I2;
i in I1;
then A4: i in dom p by FUNCT_2:def 1;
consider f being Function of J1.i, (J2*p).i such that
A5: F.i = f & f is being_homeomorphism by A2;
A6: rng f = [#]((J2*p).i) by A5, TOPS_2:def 5
.= [#](J2.j) by A4, FUNCT_1:13
.= the carrier of J2.j by STRUCT_0:def 3;
:: the rest of the Proof is so sophisticated because of the sophisticated
:: definition of H
for y being object holds y in H.:product(Carrier J1 +* (i,U))
iff y in product(Carrier J2 +* (j,(F.i).:U))
proof
let y be object;
thus y in H.:product(Carrier J1 +* (i,U))
implies y in product(Carrier J2 +* (j,(F.i).:U))
proof
assume y in H.:product(Carrier J1 +* (i,U));
then consider x being object such that
A8: x in dom H & x in product(Carrier J1 +* (i,U)) & y = H.x
by FUNCT_1:def 6;
reconsider g = x as Element of product J1 by A8;
y in rng H by A8, FUNCT_1:3;
then reconsider h = y as Element of product J2;
h in the carrier of product J2;
then A9: h in product Carrier J2 by WAYBEL18:def 3;
then A10: dom h = dom Carrier J2 by CARD_3:9
.= dom(Carrier J2 +* (j,(F.i).:U)) by FUNCT_7:30;
for z being object st z in dom(Carrier J2 +* (j,(F.i).:U))
holds h.z in (Carrier J2 +* (j,(F.i).:U)).z
proof
let z be object;
assume a11: z in dom(Carrier J2 +* (j,(F.i).:U));
then A11: z in dom Carrier J2 by FUNCT_7:30;
reconsider j0 = z as Element of I2 by a11;
I2 = rng p by A1, FUNCT_2:def 3;
then consider i0 being object such that
A12: i0 in I1 & p.i0 = j0 by FUNCT_2:11;
reconsider i0 as Element of I1 by A12;
consider f0 being Function of J1.i0, (J2*p).i0 such that
A13: F.i0 = f0 & f0 is being_homeomorphism by A2;
A14: h.j0 = f0.(g.i0) by A3, A8, A12, A13;
per cases;
suppose A15: j0 = j;
then A16: (Carrier J2 +* (j,(F.i).:U)).z = (F.i).:U
by A11, FUNCT_7:31;
A17: i0 = i by A1, A12, A15, FUNCT_2:19;
a18: I1 = dom Carrier J1 by PARTFUN1:def 2;
then i in dom Carrier J1;
then i in dom(Carrier J1 +* (i,U)) by FUNCT_7:30;
then g.i in (Carrier J1 +* (i,U)).i by A8, CARD_3:9;
then g.i in U by a18, FUNCT_7:31;
hence thesis by A14, A16, A17, A13, FUNCT_2:35;
end;
suppose j0 <> j;
then (Carrier J2 +* (j,(F.i).:U)).z = (Carrier J2).z by FUNCT_7:32;
hence thesis by A9, A11, CARD_3:9;
end;
end;
hence y in product(Carrier J2 +* (j,(F.i).:U)) by A10, CARD_3:9;
end;
assume A20: y in product(Carrier J2 +* (j,(F.i).:U));
then reconsider h = y as Element of product (Carrier J2 +* (j,(F.i).:U));
A21: the carrier of J1.i = [#](J1.i) by STRUCT_0:def 3
.= (Carrier J1).i by PENCIL_3:7;
i in I1;
then A22: i in dom Carrier J1 by PARTFUN1:def 2;
then A23: product(Carrier J1 +* (i,U)) c= product Carrier J1
by A21, Th39;
A24: (Carrier J2).j = [#](J2.j) by PENCIL_3:7
.= the carrier of J2.j by STRUCT_0:def 3;
a25: j in I2 & (F.i).:U c= the carrier of J2.j by A6, A5, RELAT_1:111;
then A25: j in dom Carrier J2 & (F.i).:U c= (Carrier J2).j
by A24, PARTFUN1:def 2;
then A26: product(Carrier J2 +* (j,(F.i).:U)) c= product Carrier J2
by Th39;
ex x being object
st x in dom H & x in product(Carrier J1 +* (i,U)) & H.x = y
proof
:: some parts of this Proof were copied from the onto Proof of H
defpred P[object,object] means ex f being one-to-one Function
st F.$1 = f & $2 = f".(h.(p.$1));
A28: for i0 being Element of I1 ex y being object st P[i0,y]
proof
let i0 be Element of I1;
consider f0 being Function of J1.i0, (J2*p).i0 such that
A29: F.i0 = f0 & f0 is being_homeomorphism by A2;
reconsider f0 as one-to-one Function by A29;
take f0".(h.(p.i0)), f0;
thus thesis by A29;
end;
consider g being ManySortedSet of I1 such that
A30: for i being Element of I1 holds P[i,g.i]
from PBOOLE:sch 6(A28);
take g;
A31: dom g = I1 by PARTFUN1:def 2
.= dom(Carrier J1 +* (i,U)) by PARTFUN1:def 2;
a36: for z being object st z in dom(Carrier J1 +* (i,U))
holds g.z in (Carrier J1 +* (i,U)).z
proof
let z be object;
assume z in dom(Carrier J1 +* (i,U));
then reconsider i0 = z as Element of I1;
consider f0 being one-to-one Function such that
A32: F.i0 = f0 & g.i0 = f0".(h.(p.i0)) by A30;
p.i0 in I2;
then p.i0 in dom Carrier J2 by PARTFUN1: def 2;
then h.(p.i0) in (Carrier J2).(p.i0) by A20, A26, CARD_3:9;
then h.(p.i0) in [#](J2.(p.i0)) by PENCIL_3:7;
then A33: h.(p.i0) in [#]((J2*p).i0) by FUNCT_2:15;
per cases;
suppose A35: i = i0;
then A36: (Carrier J1 +* (i,U)).z = U by A22, FUNCT_7:31;
j in dom(Carrier J2 +* (j,(F.i).:U))
by a25,PARTFUN1:def 2;
then h.j in (Carrier J2 +* (j,(F.i).:U)).j by A20, CARD_3:9;
then A37: h.j in (F.i).:U by A25, FUNCT_7:31;
A38: f" = f0" by A5, A32, A35, TOPS_2:def 4;
[#]((J2*p).i0) = rng f by A5, A35, TOPS_2:def 5
.= dom(f0") by A5, A32, A35, FUNCT_1:33;
then g.i0 in rng(f0") by A32, A33, FUNCT_1:3;
then A39:g.i0 in dom f by A5, A32, A35, FUNCT_1:33;
h.j in (Carrier J2).j by A20, A26, A25, CARD_3:9;
then h.j in [#](J2.j) by PENCIL_3:7;
then a40: h.j in [#]((J2*p).i) by A4, FUNCT_1:13;
a41: dom f = the carrier of J1.i by FUNCT_2:def 1;
reconsider f1 = f as one-to-one Function by A5;
A43: h.j in rng f1 by a40,A5, TOPS_2:def 5;
f.(f".(h.j)) = f1.(f1".(h.j)) by A5, TOPS_2:def 4
.= h.j by A43, FUNCT_1:35;
then g.i0 in f0"(f0.:U) by A5, A32, A35, A38,A39,A37, FUNCT_1:def 7;
hence thesis by A36, a41,A5, A32, A35, FUNCT_1:94;
end;
suppose i <> i0;
then A44: (Carrier J1 +* (i,U)).z = (Carrier J1).z
by FUNCT_7:32;
consider f9 being Function of J1.i0, (J2*p).i0 such that
A45: F.i0 = f9 & f9 is being_homeomorphism by A2;
dom(f0") = rng f0 by FUNCT_1:33
.= [#]((J2*p).i0) by A32, A45, TOPS_2:def 5
.= the carrier of (J2*p).i0 by STRUCT_0:def 3;
then f0".(h.(p.i0)) in rng(f0") by A33, FUNCT_1:3;
then g.i0 in dom f0 by A32, FUNCT_1:33;
then g.i0 in [#](J1.i0) by A32, A45, TOPS_2:def 5;
hence thesis by A44, PENCIL_3:7;
end;
end;
then g in product(Carrier J1 +* (i,U)) by A31, CARD_3:9;
then g in product Carrier J1 by A23;
then A47: g in the carrier of product J1 by WAYBEL18:def 3;
hence g in dom H & g in product(Carrier J1 +* (i,U))
by a36,A31, CARD_3:9, FUNCT_2:def 1;
reconsider h0 = H.g as Element of product J2
by A47,FUNCT_2:5;
h0 in the carrier of product J2;
then h0 in product Carrier J2 by WAYBEL18:def 3;
then A48: dom h0 = dom Carrier J2 by CARD_3:9
.= dom h by A20, A26, CARD_3:9;
for z being object st z in dom h holds h.z = h0.z
proof
let z be object;
assume z in dom h;
then z in dom Carrier J2 by A20, A26, CARD_3:9;
then reconsider j0 = z as Element of I2;
reconsider p9 = p as one-to-one Function by A1;
j0 in I2;
then A49: j0 in rng p9 by A1, FUNCT_2:def 3;
then j0 in dom(p9") by FUNCT_1:33;
then p9".j0 in rng(p9") by FUNCT_1:3;
then A50: p9".j0 in dom p9 by FUNCT_1:33;
then reconsider i0 = p9".j0 as Element of I1 by FUNCT_2:def 1;
consider f9 being one-to-one Function such that
A51: F.i0 = f9 & g.i0 = f9".(h.(p.i0)) by A30;
consider f0 being Function of J1.i0, (J2*p).i0 such that
A52: F.i0 = f0 & f0 is being_homeomorphism by A2;
A53: rng f9 = [#]((J2*p).i0) by A51, A52, TOPS_2:def 5
.= the carrier of (J2*p).i0 by STRUCT_0:def 3;
A54: p.i0 = j0 by A49, FUNCT_1:35;
A55: (Carrier J2).(p.i0) = [#](J2.(p.i0)) by PENCIL_3:7
.= [#]((J2*p).i0) by A50, FUNCT_1:13
.= the carrier of (J2*p).i0 by STRUCT_0:def 3;
p.i0 in I2;
then p.i0 in dom Carrier J2 by PARTFUN1:def 2;
then A56: h.(p.i0) in (Carrier J2).(p.i0) by A20, A26, CARD_3:9;
h.j0 = f9.(f9".(h.(p.i0))) by A53, A54, A55, A56, FUNCT_1:35
.= h0.j0 by A3, A47, A51, A54;
hence thesis;
end;
hence H.g = y by A48, FUNCT_1:2;
end;
hence thesis by FUNCT_1:def 6;
end;
hence thesis by TARSKI:2;
end;
theorem Th77:
for I1, I2 being non empty set
for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
for p being Function of I1, I2, H being ProductHomeo of J1, J2, p
st p is bijective &
for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic
holds H is bijective
proof
let I1, I2 be non empty set;
let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;
assume that A1: p is bijective and
A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
consider F being ManySortedFunction of I1 such that
A3: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
st F.i = f & f is being_homeomorphism and
A4: for g being Element of product J1, i being Element of I1 holds
(H.g).(p.i) = (F.i).(g.i) by A1, A2, Def5;
for x1,x2 being object st x1 in dom H & x2 in dom H & H.x1 = H.x2
holds x1 = x2
proof
let x1,x2 be object;
assume A5: x1 in dom H & x2 in dom H & H.x1 = H.x2;
then reconsider g1 = x1, g2 = x2 as Element of product J1;
A6: g1 is Element of product Carrier J1 &
g2 is Element of product Carrier J1 by WAYBEL18:def 3;
A7: dom g1 = dom Carrier J1 by A6, CARD_3:9
.= dom g2 by A6, CARD_3:9;
for z being object st z in dom g1 holds g1.z = g2.z
proof
let z be object;
assume z in dom g1;
then z in dom Carrier J1 by A6, CARD_3:9;
then reconsider i = z as Element of I1;
a8: (H.g1).(p.i) = (F.i).(g1.i) & (H.g2).(p.i) = (F.i).(g2.i) by A4;
consider f being Function of J1.i, (J2*p).i such that
A9: F.i = f & f is being_homeomorphism by A3;
A12: (Carrier J1).i = [#](J1.i) by PENCIL_3:7
.= the carrier of J1.i by STRUCT_0:def 3
.= dom f by FUNCT_2:def 1;
i in I1;
then i in dom Carrier J1 by PARTFUN1:def 2;
then g1.i in (Carrier J1).i & g2.i in (Carrier J1).i by A6, CARD_3:9;
hence thesis by a8,A5, A9, A12, FUNCT_1:def 4;
end;
hence thesis by A7, FUNCT_1:2;
end;
then A13: H is one-to-one by FUNCT_1:def 4;
set i0 = the Element of I1;
consider f0 being Function of J1.i0, (J2*p).i0 such that
A14: F.i0 = f0 & f0 is being_homeomorphism by A3;
i0 in I1;
then A15: i0 in dom p by FUNCT_2:def 1;
rng H = H.:dom H by RELAT_1:113
.= H.:the carrier of product J1 by FUNCT_2:def 1
.= H.:product Carrier J1 by WAYBEL18:def 3
.= H.:product(Carrier J1 +* (i0,(Carrier J1).i0)) by FUNCT_7:35
.= H.:product(Carrier J1 +* (i0,[#](J1.i0))) by PENCIL_3:7
.= product(Carrier J2 +* (p.i0,(F.i0).:[#](J1.i0))) by A1, A3, A4, Th76
.= product(Carrier J2 +* (p.i0,f0.:dom f0)) by A14, TOPS_2:def 5
.= product(Carrier J2 +* (p.i0,rng f0)) by RELAT_1:113
.= product(Carrier J2 +* (p.i0,[#]((J2*p).i0))) by A14, TOPS_2:def 5
.= product(Carrier J2 +* (p.i0,[#](J2.(p.i0)))) by A15, FUNCT_1:13
.= product(Carrier J2 +* (p.i0,(Carrier J2).(p.i0))) by PENCIL_3:7
.= product Carrier J2 by FUNCT_7:35
.= the carrier of product J2 by WAYBEL18:def 3;
then H is onto by FUNCT_2:def 3;
hence thesis by A13;
end;
theorem Th78:
for I1, I2 being non empty set
for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
for p being Function of I1, I2, H being ProductHomeo of J1, J2, p
st p is bijective &
for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic
holds H is being_homeomorphism
proof
let I1, I2 be non empty set;
let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
let p be Function of I1, I2, H be ProductHomeo of J1, J2, p;
assume that
A1: p is bijective and
A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
consider F being ManySortedFunction of I1 such that
A3: for i being Element of I1 ex f being Function of J1.i, (J2*p).i
st F.i = f & f is being_homeomorphism and
A4: for g being Element of product J1, i being Element of I1 holds
(H.g).(p.i) = (F.i).(g.i) by A1, A2, Def5;
A5: H is bijective by A1, A2, Th77;
:: using the canonical product prebasis for both J1 and J2
:: and showing that H maps one to the other, we are already done
:: with the bijectivity of H
ex K being prebasis of product J1, L being prebasis of product J2 st H.:K = L
proof
reconsider K = product_prebasis J1 as prebasis of product J1
by WAYBEL18:def 3;
reconsider L = product_prebasis J2 as prebasis of product J2
by WAYBEL18:def 3;
take K, L;
:: we use the characterization of images under H above to show the equality
for W being Subset of product J2 holds W in L iff
ex V being Subset of product J1 st V in K & H.:V = W
proof
let W be Subset of product J2;
thus W in L implies ex V being Subset of product J1 st V in K & H.:V = W
proof
assume W in L;
then consider j being set, T being TopStruct, W0j being Subset of T
such that A6: j in I2 & W0j is open & T = J2.j and
A7: W = product (Carrier J2 +* (j,W0j)) by WAYBEL18:def 2;
reconsider j as Element of I2 by A6;
reconsider Wj = W0j as Subset of J2.j by A6;
j in I2;
then j in rng p by A1, FUNCT_2:def 3;
then consider i being object such that
A8: i in I1 & p.i = j by FUNCT_2:11;
A9: i in dom p by A8, FUNCT_2:def 1;
reconsider i as Element of I1 by A8;
consider f being Function of J1.i, (J2*p).i such that
A10: F.i = f & f is being_homeomorphism by A3;
reconsider Vi = f"Wj as Subset of J1.i;
A11: the carrier of J1.i = [#](J1.i) by STRUCT_0:def 3
.= (Carrier J1).i by PENCIL_3:7;
i in dom Carrier J1 by A8, PARTFUN1:def 2;
then product(Carrier J1 +* (i,Vi)) c= product Carrier J1 by A11, Th39;
then reconsider V = product(Carrier J1 +* (i,Vi))
as Subset of product J1 by WAYBEL18:def 3;
take V;
A12: V is Subset of product Carrier J1 by WAYBEL18:def 3;
ex k being set, S being TopStruct, U being Subset of S
st k in I1 & U is open & S = J1.k & V = product(Carrier J1 +* (k,U))
proof
take i, J1.i, Vi;
reconsider W1j = Wj as Subset of (J2*p).i by A8, A9, FUNCT_1:13;
W0j in the topology of J2.j by A6, PRE_TOPC:def 2;
then W1j in the topology of (J2*p).i by A8, A9, FUNCT_1:13;
then A14: W1j is open by PRE_TOPC:def 2;
[#]((J2*p).i) = {} implies [#](J1.i) = {};
hence thesis by A10, A14, TOPS_2:43;
end;
hence V in K by A12, WAYBEL18:def 2;
reconsider f0 = f as one-to-one Function by A10;
rng f0 = [#]((J2*p).i) by A10, TOPS_2:def 5
.= [#](J2.j) by A9, A8, FUNCT_1:13
.= the carrier of J2.j by STRUCT_0:def 3;
then f.:(f"Wj) = Wj by FUNCT_1:77;
hence H.:V = W by A1, A3, A4, A7, A8, Th76,A10;
end;
given V being Subset of product J1 such that
A16: V in K & H.:V = W;
consider i being set, S being TopStruct, Vi being Subset of S such that
A17: i in I1 & Vi is open & S = J1.i and
A18: V = product ((Carrier J1) +* (i,Vi))
by A16, WAYBEL18:def 2;
reconsider i as Element of I1 by A17;
reconsider Vi as Subset of J1.i by A17;
A19: W is Subset of product Carrier J2 by WAYBEL18:def 3;
ex j being set, T being TopStruct, U being Subset of T
st j in I2 & U is open & T = J2.j & W = product(Carrier J2 +* (j,U))
proof
reconsider j = p.i as Element of I2;
consider f being Function of J1.i, (J2*p).i such that
A20: F.i = f & f is being_homeomorphism by A3;
a21: i in dom p by A17, FUNCT_2:def 1;
then A21: (J2*p).i = J2.j by FUNCT_1:13;
reconsider Wj = f.:Vi as Subset of J2.j by a21,FUNCT_1:13;
take j, J2.j, Wj;
thus j in I2 & Wj is open & J2.j = J2.j
by A21,A17, A20, T_0TOPSP:def 2;
thus W = product(Carrier J2 +* (j,Wj))
by A16,A1, A3, A4, A18, A20, Th76;
end;
hence W in L by A19, WAYBEL18:def 2;
end;
hence H.:K = L by FUNCT_2:def 10;
end;
hence thesis by A5, Th48;
end;
:: pairwise homeomorphic factors lead to homeomorphic products
theorem Th79:
for I1, I2 being non empty set
for J1 being TopSpace-yielding non-Empty ManySortedSet of I1
for J2 being TopSpace-yielding non-Empty ManySortedSet of I2
for p being Function of I1, I2
st p is bijective &
for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic
holds product J1, product J2 are_homeomorphic
proof
let I1, I2 be non empty set;
let J1 be TopSpace-yielding non-Empty ManySortedSet of I1;
let J2 be TopSpace-yielding non-Empty ManySortedSet of I2;
let p be Function of I1, I2;
assume that
A1: p is bijective and
A2: for i being Element of I1 holds J1.i, (J2*p).i are_homeomorphic;
set H = the ProductHomeo of J1, J2, p;
H is being_homeomorphism by A1, A2, Th78;
hence thesis by T_0TOPSP:def 1;
end;
theorem
for I being non empty set
for J1, J2 being TopSpace-yielding non-Empty ManySortedSet of I
for p being Permutation of I
st for i being Element of I holds J1.i, (J2*p).i are_homeomorphic
holds product J1, product J2 are_homeomorphic by Th79;
:: permutations of the underlying set family lead to a homeomorphic copy of
:: the original product
:: (the following one could also be done with TopStruct-yielding
:: but then the theorems before couldn't be used and the long argumentation
:: would have to be repeated for most parts)
theorem
for I being non empty set
for J being TopSpace-yielding non-Empty ManySortedSet of I
for p being Permutation of I
holds product J, product(J*p) are_homeomorphic
proof
let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let p be Permutation of I;
reconsider q = p" as Permutation of I;
now
let i be Element of I;
A1: J = J*id dom J by RELAT_1:52
.= J*id I by PARTFUN1:def 2
.= J*(p*q) by FUNCT_2:61
.= (J*p)*q by RELAT_1:36;
thus J.i, ((J*p)*q).i are_homeomorphic by A1;
end;
hence product J, product(J*p) are_homeomorphic by Th79;
end;
:: if each factor of the first product is a subspace of a corresponding
:: factor of the second product, the first product is a subspae of the second
theorem
for I being non empty set
for J1, J2 being TopSpace-yielding non-Empty ManySortedSet of I
st for i being Element of I holds J1.i is SubSpace of J2.i
holds product J1 is SubSpace of product J2
proof
let I be non empty set;
let J1 be TopSpace-yielding non-Empty ManySortedSet of I;
let J2 be TopSpace-yielding non-Empty ManySortedSet of I;
assume A1: for i being Element of I holds J1.i is SubSpace of J2.i;
ex K1 being prebasis of product J1, K2 being prebasis of product J2
st [#]product J1 in K1 & K1 = INTERSECTION(K2,{[#]product J1})
proof
reconsider K1 = product_prebasis J1 as prebasis of product J1
by WAYBEL18:def 3;
reconsider K2 = product_prebasis J2 as prebasis of product J2
by WAYBEL18:def 3;
take K1, K2;
A2: [#]product J1 = the carrier of product J1 by STRUCT_0:def 3
.= product Carrier J1 by WAYBEL18:def 3;
then [#]product J1 = [#]product Carrier J1 by SUBSET_1:def 3;
then reconsider P = [#]product J1 as Subset of product Carrier J1;
ex i being set, T being TopStruct, V being Subset of T
st i in I & V is open & T = J1.i & P = product(Carrier J1 +* (i,V))
proof
set i = the Element of I;
take i, J1.i, [#](J1.i);
thus i in I & [#](J1.i) is open & J1.i = J1.i;
thus P = product(Carrier J1 +* (i,(Carrier J1).i)) by A2, FUNCT_7:35
.= product(Carrier J1 +* (i,[#](J1.i))) by PENCIL_3:7;
end;
hence [#]product J1 in K1 by WAYBEL18:def 2;
for U being set holds U in K1 iff
ex A, P0 being set st A in K2 & P0 in {[#]product J1} & U = A /\ P0
proof
let U be set;
A3: for i being Element of I, V being Subset of J1.i,
W being Subset of J2.i st V = W /\ [#](J1.i)
holds Carrier J1 +* (i,V) = (Carrier J2 +* (i,W)) (/\) Carrier J1
proof
let i be Element of I, V be Subset of J1.i, W be Subset of J2.i;
assume A4: V = W /\ [#](J1.i);
A5: dom(Carrier J1 +* (i,V)) = I by PARTFUN1:def 2
.= dom((Carrier J2 +* (i,W)) (/\) Carrier J1) by PARTFUN1:def 2;
for x being object st x in dom(Carrier J1 +* (i,V))
holds (Carrier J1 +* (i,V)).x =
((Carrier J2 +* (i,W)) (/\) Carrier J1).x
proof
let x be object;
assume a6: x in dom(Carrier J1 +* (i,V));
then A6: x in dom Carrier J1 by FUNCT_7:30;
A7: x in I by a6;
reconsider j = x as Element of I by a6;
A8: x in dom Carrier J2 by A7, PARTFUN1:def 2;
per cases;
suppose A9: x = i;
hence (Carrier J1 +* (i,V)).x = V by A6, FUNCT_7:31
.= (Carrier J2 +* (i,W)).x /\ [#](J1.i)
by A4, A8, A9, FUNCT_7:31
.= (Carrier J2 +* (i,W)).x /\ (Carrier J1).i by PENCIL_3:7
.= ((Carrier J2 +*(i,W)) (/\) Carrier J1).x
by A9, PBOOLE:def 5;
end;
suppose A10: x <> i;
A11: (Carrier J1).j = [#](J1.j) & (Carrier J2).j = [#](J2.j)
by PENCIL_3:7;
a12: J1.j is SubSpace of J2.j by A1;
thus (Carrier J1 +* (i,V)).x = (Carrier J1).x by A10, FUNCT_7:32
.= (Carrier J2).x /\ (Carrier J1).x
by a12, XBOOLE_1:28,A11, PRE_TOPC:def 4
.= (Carrier J2 +* (i,W)).x /\ (Carrier J1).x by A10, FUNCT_7:32
.= ((Carrier J2 +*(i,W)) (/\) Carrier J1).x
by a6, PBOOLE:def 5;
end;
end;
hence Carrier J1 +* (i,V) = (Carrier J2 +* (i,W)) (/\) Carrier J1
by A5, FUNCT_1:2;
end;
thus U in K1 implies ex A, P0 being set
st A in K2 & P0 in {[#]product J1} & U = A /\ P0
proof
assume U in K1;
then consider i being set, T being TopStruct, V being Subset of T
such that A13: i in I & V is open & T = J1.i and
A14: U = product(Carrier J1 +* (i,V)) by WAYBEL18:def 2;
reconsider i as Element of I by A13;
A15: V in the topology of J1.i by A13, PRE_TOPC:def 2;
reconsider V as Subset of J1.i by A13;
J1.i is SubSpace of J2.i by A1;
then consider W being Subset of J2.i such that
A16: W in the topology of J2.i & V = W /\ [#](J1.i)
by A15, PRE_TOPC:def 4;
set A = product(Carrier J2 +* (i,W));
take A, P;
(Carrier J2).i = [#](J2.i) by PENCIL_3:7
.= the carrier of J2.i by STRUCT_0:def 3;
then i in dom Carrier J2 & W c= (Carrier J2).i by A13, PARTFUN1:def 2;
then A17: A is Subset of product Carrier J2 by Th39;
ex i9 being set, T9 being TopStruct, V9 being Subset of T9 st i9 in I &
V9 is open & T9 = J2.i9 & A = product(Carrier J2 +* (i9,V9))
by A16, PRE_TOPC:def 2;
hence A in K2 by A17, WAYBEL18:def 2;
thus P in {[#]product J1} by TARSKI:def 1;
thus U = product((Carrier J2 +* (i,W)) (/\) Carrier J1) by A14, A16, A3
.= A /\ P by A2, Th33;
end;
given A, P0 being set such that
A18: A in K2 & P0 in {[#]product J1} & U = A /\ P0;
consider i being set, T being TopStruct, W being Subset of T such that
A19: i in I & W is open & T = J2.i and
A20: A = product(Carrier J2 +* (i,W)) by A18, WAYBEL18:def 2;
reconsider i as Element of I by A19;
A21: W in the topology of J2.i by A19, PRE_TOPC:def 2;
reconsider W as Subset of J2.i by A19;
set V = W /\ [#](J1.i);
A22: V c= [#](J1.i) by XBOOLE_1:17;
reconsider V as Subset of J1.i;
P0 = product Carrier J1 by A2, A18, TARSKI:def 1;
then A23: U
= product((Carrier J2 +* (i,W)) (/\) Carrier J1) by A18, A20, Th33
.= product(Carrier J1 +* (i,V)) by A3;
A24: i in dom Carrier J1 by A19, PARTFUN1:def 2;
V c= (Carrier J1).i by A22, PENCIL_3:7;
then A25: U c= product Carrier J1 by A23, A24, Th39;
ex i9 being set, T9 being TopStruct, V9 being Subset of T9
st i9 in I & V9 is open & T9 = J1.i9 &
U = product(Carrier J1 +* (i9,V9))
proof
take i, J1.i, V;
thus i in I;
J1.i is SubSpace of J2.i by A1;
then V in the topology of J1.i by A21, PRE_TOPC:def 4;
hence thesis by A23, PRE_TOPC:def 2;
end;
hence U in K1 by A25, WAYBEL18:def 2;
end;
hence thesis by SETFAM_1:def 5;
end;
hence thesis by Th51;
end;