:: Injective Spaces
:: by Jaros{\l}aw Gryko
::
:: Received April 17, 1998
:: Copyright (c) 1998-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 SETFAM_1, XBOOLE_0, CANTOR_1, TARSKI, PRE_TOPC, RLVECT_3,
RELAT_1, PRALG_1, FUNCT_1, PBOOLE, FUNCOP_1, WAYBEL_3, STRUCT_0,
SUBSET_1, CARD_3, RLVECT_2, RCOMP_1, FUNCT_4, MONOID_0, ORDINAL2,
FUNCTOR0, PARTFUN1, FUNCT_6, BORSUK_1, FUNCT_3, GROUP_6, WAYBEL_1,
FUNCT_2, T_0TOPSP, TOPS_2, CARD_1, ZFMISC_1, RELAT_2, ORDERS_2, WAYBEL11,
YELLOW_9, YELLOW_1, LATTICE3, FILTER_1, XXREAL_0, WAYBEL_0, CARD_FIL,
FINSET_1, REWRITE1, WAYBEL_8, LATTICES, CAT_1, WAYBEL_9, WAYBEL18;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, RELAT_1, PBOOLE,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, ORDINAL1, NUMBERS,
STRUCT_0, PRE_TOPC, T_0TOPSP, FUNCT_3, FUNCT_6, FUNCT_7, CARD_3,
FUNCOP_1, MONOID_0, PRALG_1, ORDERS_2, LATTICE3, YELLOW_1, CANTOR_1,
FINSET_1, TOPS_2, BORSUK_1, TMAP_1, YELLOW_0, YELLOW_9, WAYBEL_0,
WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11;
constructors FUNCT_3, FUNCT_7, TOPS_2, BORSUK_1, LATTICE3, TMAP_1, T_0TOPSP,
CANTOR_1, MONOID_0, PRALG_1, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL11,
YELLOW_9, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3,
STRUCT_0, PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0,
YELLOW_1, WAYBEL_3, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL17, RELAT_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, PRE_TOPC, FUNCOP_1, WAYBEL_1, WAYBEL_3, XBOOLE_0, PRALG_1;
equalities STRUCT_0, ORDINAL1;
expansions TARSKI, PRE_TOPC, WAYBEL_1, XBOOLE_0;
theorems TARSKI, PRE_TOPC, ENUMSET1, ZFMISC_1, T_0TOPSP, TOPS_1, TOPS_2,
FINSET_1, FUNCT_2, FUNCT_3, RELAT_1, FUNCT_1, BORSUK_1, FUNCOP_1,
CANTOR_1, LATTICE3, ORDERS_2, MSSUBFAM, PRALG_1, CARD_3, WAYBEL_3,
FUNCT_6, FUNCT_7, TMAP_1, YELLOW_9, YELLOW_0, YELLOW_1, WAYBEL_0,
WAYBEL_7, WAYBEL_8, WAYBEL11, WAYBEL13, WAYBEL14, RELSET_1, SETFAM_1,
XBOOLE_0, XBOOLE_1, ORDERS_1, MONOID_0, CARD_1, PARTFUN1;
schemes SUBSET_1, CLASSES1, FUNCT_1, FRAENKEL;
begin :: Preliminaries
theorem Th1:
for X being set, A,B being Subset-Family of X st B = A \ {{}} or
A = B \/ {{}} holds UniCl A = UniCl B
proof
let X be set;
let A,B be Subset-Family of X;
assume
A1: B = A \ {{}} or A = B \/ {{}};
A2: UniCl A c= UniCl B
proof
let x be object;
assume x in UniCl A;
then consider Y being Subset-Family of X such that
A3: Y c= A and
A4: x = union Y by CANTOR_1:def 1;
A5: Y \ {{}} c= B
proof
let w be object;
assume
A6: w in Y \ {{}};
per cases by A1;
suppose
A7: B = A \ {{}};
w in Y & not w in {{}} by A6,XBOOLE_0:def 5;
hence thesis by A3,A7,XBOOLE_0:def 5;
end;
suppose
A8: A = B \/ {{}};
w in Y & not w in {{}} by A6,XBOOLE_0:def 5;
hence thesis by A3,A8,XBOOLE_0:def 3;
end;
end;
reconsider Z = Y \ {{}} as Subset-Family of X;
Z \/ {{}} = Y \/ {{}} by XBOOLE_1:39;
then union (Z \/ {{}}) = union Y \/ union {{}} by ZFMISC_1:78
.= union Y \/ {} by ZFMISC_1:25
.= union Y;
then x = union Z \/ union {{}} by A4,ZFMISC_1:78
.= union Z \/ {} by ZFMISC_1:25
.= union Z;
hence thesis by A5,CANTOR_1:def 1;
end;
UniCl B c= UniCl A by A1,CANTOR_1:9,XBOOLE_1:7,36;
hence thesis by A2;
end;
theorem Th2:
for T being TopSpace, K being Subset-Family of T holds K is Basis
of T iff K \ {{}} is Basis of T
proof
let T be TopSpace, K be Subset-Family of T;
reconsider K9 = K \ {{}} as Subset-Family of T;
A1: UniCl K9 c= UniCl K by CANTOR_1:9,XBOOLE_1:36;
A2: K \ {{}} c= K by XBOOLE_1:36;
hereby
assume
A3: K is Basis of T;
then the topology of T c= UniCl K by CANTOR_1:def 2;
then
A4: the topology of T c= UniCl K9 by Th1;
K c= the topology of T by A3,TOPS_2:64;
then K \ {{}} c= the topology of T by A2;
hence K \ {{}} is Basis of T by A4,CANTOR_1:def 2,TOPS_2:64;
end;
assume
A5: K \ {{}} is Basis of T;
then
A6: K9 c= the topology of T by TOPS_2:64;
A7: K c= the topology of T
proof
let x be object;
assume
A8: x in K;
per cases;
suppose
x = {};
hence thesis by PRE_TOPC:1;
end;
suppose
x <> {};
then not x in {{}} by TARSKI:def 1;
then x in K9 by A8,XBOOLE_0:def 5;
hence thesis by A6;
end;
end;
the topology of T c= UniCl K9 by A5,CANTOR_1:def 2;
then the topology of T c= UniCl K by A1;
hence thesis by A7,CANTOR_1:def 2,TOPS_2:64;
end;
definition
let F be Relation;
attr F is TopStruct-yielding means
:Def1:
for x being object st x in rng F holds x is TopStruct;
end;
registration
cluster TopStruct-yielding -> 1-sorted-yielding for Function;
coherence
proof
let F be Function such that
A1: F is TopStruct-yielding;
let x be object;
assume x in dom F;
then F.x in rng F by FUNCT_1:def 3;
hence thesis by A1;
end;
end;
registration
let I be set;
cluster TopStruct-yielding for ManySortedSet of I;
existence
proof
take f = I --> the TopSpace;
let v be object;
assume v in rng(f);
hence thesis by TARSKI:def 1;
end;
end;
registration
let I be set;
cluster TopStruct-yielding non-Empty for ManySortedSet of I;
existence
proof
set R = the non empty TopSpace;
take J = I --> R;
thus J is TopStruct-yielding
proof
let x be object;
assume x in rng J;
hence thesis by TARSKI:def 1;
end;
thus J is non-Empty
proof
let S be 1-sorted;
assume S in rng J;
hence thesis by TARSKI:def 1;
end;
end;
end;
definition
let J be non empty set;
let A be TopStruct-yielding ManySortedSet of J;
let j be Element of J;
redefine func A.j -> TopStruct; :: redefines . (FUNCT_1, definition)
coherence
proof
dom A = J by PARTFUN1:def 2;
then A.j in rng A by FUNCT_1:def 3;
hence thesis by Def1;
end;
end;
definition
let I be set;
let J be TopStruct-yielding ManySortedSet of I;
func product_prebasis J -> Subset-Family of product Carrier J means
:Def2:
for x being Subset of product Carrier J holds x in it iff 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));
existence
proof
defpred P[Subset of product Carrier J] means ex i being set, T being
TopStruct, V being Subset of T st i in I & V is open & T = J.i & $1 = product (
(Carrier J) +* (i,V));
thus ex F being Subset-Family of product Carrier J st for x being Subset
of product Carrier J holds x in F iff P[x] from SUBSET_1:sch 3;
end;
uniqueness
proof
let P1,P2 be Subset-Family of product Carrier J such that
A1: for x being Subset of product Carrier J holds x in P1 iff 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)) and
A2: for x being Subset of product Carrier J holds x in P2 iff 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));
A3: P2 c= P1
proof
let x be object;
assume
A4: x in P2;
then reconsider x9 = x as 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 & x9 = product ((Carrier J) +* (i,V)) by A2,A4;
hence thesis by A1;
end;
P1 c= P2
proof
let x be object;
assume
A5: x in P1;
then reconsider x9 = x as 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 & x9 = product ((Carrier J) +* (i,V)) by A1,A5;
hence thesis by A2;
end;
hence thesis by A3;
end;
end;
theorem Th3:
for X be set, A be Subset-Family of X holds TopStruct (#X,UniCl
FinMeetCl A#) is TopSpace-like
proof
let X be set;
let A be Subset-Family of X;
per cases;
suppose
A1: X = {};
set T = TopStruct (#X, UniCl FinMeetCl A#);
the carrier of T in FinMeetCl A & FinMeetCl A c= UniCl FinMeetCl A by
CANTOR_1:1,8;
hence the carrier of T in the topology of T;
hence for a being Subset-Family of T st a c= the topology of T holds union
a in the topology of T by A1;
thus thesis by A1;
end;
suppose
X <> {};
hence thesis by CANTOR_1:15;
end;
end;
definition
let I be set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
func product J -> strict TopSpace means
:Def3:
the carrier of it = product Carrier J & product_prebasis J is prebasis of it;
existence
proof
set X = product Carrier J;
reconsider A = product_prebasis J as Subset-Family of X;
consider T being strict TopStruct such that
A1: T = TopStruct (# X, UniCl FinMeetCl A #);
reconsider T as strict TopSpace by A1,Th3;
take T;
thus the carrier of T = product Carrier J by A1;
now
assume {} in rng Carrier J;
then consider i being object such that
A2: i in dom Carrier J and
A3: {} = (Carrier J).i by FUNCT_1:def 3;
consider R being 1-sorted such that
A4: R = J.i and
A5: {} = the carrier of R by A2,A3,PRALG_1:def 15;
dom J = I by PARTFUN1:def 2;
then R in rng J by A2,A4,FUNCT_1:def 3;
then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A5;
hence contradiction;
end;
then X is non empty by CARD_3:26;
hence thesis by A1,CANTOR_1:18;
end;
uniqueness
proof
let T1,T2 be strict TopSpace such that
A6: the carrier of T1 = product Carrier J and
A7: product_prebasis J is prebasis of T1 and
A8: the carrier of T2 = product Carrier J and
A9: product_prebasis J is prebasis of T2;
now
assume {} in rng Carrier J;
then consider i being object such that
A10: i in dom Carrier J and
A11: {} = (Carrier J).i by FUNCT_1:def 3;
consider R being 1-sorted such that
A12: R = J.i and
A13: {} = the carrier of R by A10,A11,PRALG_1:def 15;
dom J = I by PARTFUN1:def 2;
then R in rng J by A10,A12,FUNCT_1:def 3;
then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A13;
hence contradiction;
end;
then product Carrier J <> {} by CARD_3:26;
then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A6,A8;
t1 = t2 by A6,A7,A8,A9,CANTOR_1:17;
hence thesis;
end;
end;
registration
let I be set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
cluster product J -> non empty;
coherence
proof
A1: now
assume {} in rng Carrier J;
then consider i being object such that
A2: i in dom Carrier J and
A3: {} = (Carrier J).i by FUNCT_1:def 3;
consider R being 1-sorted such that
A4: R = J.i and
A5: {} = the carrier of R by A2,A3,PRALG_1:def 15;
dom J = I by PARTFUN1:def 2;
then R in rng J by A2,A4,FUNCT_1:def 3;
then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A5;
hence contradiction;
end;
the carrier of product J = product Carrier J by Def3;
then the carrier of product J <> {} by A1,CARD_3:26;
hence thesis;
end;
end;
definition
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let i be Element of I;
redefine func J.i -> non empty TopStruct; :: 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 WAYBEL_3:def 7;
end;
end;
registration
let I be set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
cluster product J -> constituted-Functions;
coherence
proof
the carrier of product J = product Carrier J by Def3;
hence thesis by MONOID_0:80;
end;
end;
definition
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let x be Element of product J;
let i be Element of I;
redefine func x.i -> Element of J.i; :: redefines . (FUNCT_1, definition)
coherence
proof
A1: dom Carrier J = I by PARTFUN1:def 2;
( ex R being 1-sorted st R = J.i & (Carrier J).i = the carrier of R)&
the carrier of product J = product Carrier J by Def3,PRALG_1:def 15;
hence thesis by A1,CARD_3:9;
end;
end;
definition
let I be non empty set;
let J be TopStruct-yielding non-Empty ManySortedSet of I;
let i be Element of I;
func proj(J,i) -> Function of product J, J.i equals
proj(Carrier J,i);
coherence
proof
consider f being Function such that
A1: f = proj (Carrier J,i);
A2: dom f = product Carrier J by A1,CARD_3:def 16
.= the carrier of product J by Def3;
rng f c= the carrier of J.i
proof
let y be object;
assume y in rng f;
then consider x be object such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 3;
reconsider x as Element of product J by A2,A3;
f.x = x.i by A1,A3,CARD_3:def 16;
hence thesis by A4;
end;
hence thesis by A1,A2,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem Th4:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I, P being Subset of J.i holds proj(J,i)
"P = product ((Carrier J) +* (i,P))
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I, P be Subset of J.i;
set f = (Carrier J) +* (i,P);
A1: dom Carrier J = I by PARTFUN1:def 2;
A2: dom f = dom Carrier J by FUNCT_7:30
.= I by PARTFUN1:def 2;
A3: product f c= proj(J,i)"P
proof
let x be object;
assume x in product f;
then consider g being Function such that
A4: x = g and
A5: dom g = dom f and
A6: for y being object st y in dom f holds g.y in f.y by CARD_3:def 5;
A7: for j being object st j in dom Carrier J holds g.j in (Carrier J).j
proof
let j be object;
assume j in dom Carrier J;
then
A8: j in I;
then
A9: ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R by
PRALG_1:def 15;
per cases;
suppose
A10: j = i;
f.i = P by A1,FUNCT_7:31;
then g.j in P by A2,A6,A10;
hence thesis by A9,A10;
end;
suppose
j <> i;
then f.j = (Carrier J).j by FUNCT_7:32;
hence thesis by A2,A6,A8;
end;
end;
dom g = dom Carrier J by A5,FUNCT_7:30;
then
A11: g in product Carrier J by A7,CARD_3:9;
then
A12: g in dom proj(Carrier J,i) by CARD_3:def 16;
f.i = P by A1,FUNCT_7:31;
then g.i in P by A2,A6;
then
A13: proj(Carrier J,i).g in P by A12,CARD_3:def 16;
g in dom proj(J,i) by A11,CARD_3:def 16;
hence thesis by A4,A13,FUNCT_1:def 7;
end;
proj(J,i)"P c= product f
proof
let x be object;
assume
A14: x in proj(J,i)"P;
then
A15: x in dom proj(Carrier J,i) by FUNCT_1:def 7;
then x in product Carrier J;
then consider g being Function such that
A16: x = g and
A17: dom g = dom Carrier J and
A18: for y being object st y in dom Carrier J holds g.y in (Carrier J).y
by CARD_3:def 5;
A19: dom g = dom f by A17,FUNCT_7:30;
for j being object st j in dom f holds g.j in f.j
proof
let j be object;
assume j in dom f;
then
A20: g.j in (Carrier J).j by A17,A18,A19;
per cases;
suppose
A21: i = j;
proj(Carrier J,i).x = g.i by A15,A16,CARD_3:def 16;
then g.i in P by A14,FUNCT_1:def 7;
hence thesis by A1,A21,FUNCT_7:31;
end;
suppose
i <> j;
hence thesis by A20,FUNCT_7:32;
end;
end;
hence thesis by A16,A19,CARD_3:def 5;
end;
hence thesis by A3;
end;
theorem Th5:
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I, i being Element of I holds proj(J,i) is continuous
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I,
i be Element of I;
A1: for P being Subset of J.i st P is open holds proj(J,i)"P is open
proof
let P be Subset of J.i;
assume
A2: P is open;
proj(J,i)"P c= product Carrier J
proof
let x be object;
assume x in proj(J,i)"P;
then x in dom proj(Carrier J,i) by FUNCT_1:def 7;
hence thesis;
end;
then reconsider x = proj(J,i)"P as Subset of product Carrier J;
product_prebasis J is prebasis of product J by Def3;
then
A3: product_prebasis J c= the topology of product J by TOPS_2:64;
x = product ((Carrier J) +* (i,P)) by Th4;
then proj(J,i)"P in product_prebasis J by A2,Def2;
hence thesis by A3;
end;
[#](J.i) <> {};
hence thesis by A1,TOPS_2:43;
end;
theorem Th6:
for X being non empty TopSpace, I being non empty set, J being
TopStruct-yielding non-Empty ManySortedSet of I, f being Function of X, product
J holds f is continuous iff for i being Element of I holds proj(J,i)*f is
continuous
proof
let X be non empty TopSpace, I be non empty set, J be TopStruct-yielding
non-Empty ManySortedSet of I, f be Function of X, product J;
set B = product_prebasis J;
hereby
assume
A1: f is continuous;
let i be Element of I;
proj(J,i) is continuous by Th5;
hence proj(J,i)*f is continuous by A1,TOPS_2:46;
end;
assume
A2: for i being Element of I holds proj(J,i)*f is continuous;
A3: for P being Subset of product J st P in B holds f"P is open
proof
let P be Subset of product J;
reconsider p = P as Subset of product Carrier J by Def3;
assume P in B;
then consider
i being set, T being TopStruct, V being Subset of T such that
A4: i in I and
A5: V is open and
A6: T = J.i and
A7: p = product ((Carrier J) +* (i,V)) by Def2;
reconsider j = i as Element of I by A4;
reconsider V as Subset of J.j by A6;
proj(J,j)*f is continuous & [#](J.j) <> {} by A2;
then
A8: (proj(J,j)*f)"V is open by A5,A6,TOPS_2:43;
proj(J,j)"V = p by A7,Th4;
hence thesis by A8,RELAT_1:146;
end;
B is prebasis of product J by Def3;
hence thesis by A3,YELLOW_9:36;
end;
begin :: Main Part
definition
let Z be TopStruct;
attr Z is injective means ::p.121 definition 3.1.
for X being non empty TopSpace for f being
Function of X, Z st f is continuous holds for Y being non empty TopSpace st X
is SubSpace of Y ex g being Function of Y,Z st g is continuous & g|(the carrier
of X) = f;
end;
theorem Th7: ::p.121 lemma 3.2.(i)
for I being non empty set, J being TopStruct-yielding non-Empty
ManySortedSet of I st for i being Element of I holds J.i is injective holds
product J is injective
proof
let I be non empty set, J be TopStruct-yielding non-Empty ManySortedSet of I;
assume
A1: for i being Element of I holds J.i is injective;
set B = product_prebasis J;
let X be non empty TopSpace;
let f be Function of X, product J;
assume
A2: f is continuous;
let Y be non empty TopSpace;
defpred P[object,object] means
ex i1 being Element of I st i1 = $1 & ex g being
Function of Y, J.i1 st g is continuous & g|(the carrier of X) = proj(J,i1)*f &
$2 = g;
assume
A3: X is SubSpace of Y;
A4: for i being object st i in I ex u being object st P[i,u]
proof
let i be object;
assume i in I;
then reconsider i1 = i as Element of I;
J.i1 is injective & proj(J,i1)*f is continuous by A1,A2,Th6;
then consider g being Function of Y, J.i1 such that
A5: g is continuous & g|(the carrier of X) = proj(J,i1)*f by A3;
take g, i1;
thus thesis by A5;
end;
consider G being Function such that
A6: dom G = I and
A7: for i being object st i in I holds P[i,G.i] from CLASSES1:sch 1(A4);
G is Function-yielding
proof
let j be object;
assume j in dom G;
then ex i being Element of I st i = j & ex g being Function of Y, J.i st g
is continuous & g|(the carrier of X) = proj(J,i)*f & G.j = g by A6,A7;
hence thesis;
end;
then reconsider G as Function-yielding Function;
A8: the carrier of Y c= dom <:G:>
proof
let x be object;
consider i being object such that
A9: i in I by XBOOLE_0:def 1;
assume
A10: x in the carrier of Y;
A11: for f9 being Function st f9 in rng G holds x in dom f9
proof
let f9 be Function;
assume f9 in rng G;
then consider k being object such that
A12: k in dom G and
A13: f9 = G.k by FUNCT_1:def 3;
ex i1 being Element of I st i1 = k & ex ff being Function of Y, J.i1
st ff is continuous & ff|(the carrier of X) = proj(J,i1)*f & G.k = ff by A6,A7
,A12;
hence thesis by A10,A13,FUNCT_2:def 1;
end;
consider j being Element of I such that
j = i and
A14: ex g being Function of Y, J.j st g is continuous & g|(the carrier
of X) = proj(J,j)*f & G.i = g by A7,A9;
consider g being Function of Y, J.j such that
g is continuous and
g|(the carrier of X) = proj(J,j)*f and
A15: G.i = g by A14;
g in rng G by A6,A9,A15,FUNCT_1:def 3;
hence thesis by A11,FUNCT_6:33;
end;
A16: product rngs G c= product Carrier J
proof
let y be object;
assume y in product rngs G;
then consider h being Function such that
A17: y = h and
A18: dom h = dom rngs G and
A19: for x being object st x in dom rngs G holds h.x in (rngs G).x
by CARD_3:def 5;
A20: dom h = I by A6,A18,FUNCT_6:60
.= dom Carrier J by PARTFUN1:def 2;
for x being object st x in dom Carrier J holds h.x in (Carrier J).x
proof
let x be object;
assume
A21: x in dom Carrier J;
then
A22: x in I;
then consider i being Element of I such that
A23: i = x and
A24: ex g being Function of Y, J.i st g is continuous & g|(the
carrier of X) = proj(J,i)*f & G.x = g by A7;
A25: ex R being 1-sorted st R = J.x & (Carrier J).x = the carrier of R by A22,
PRALG_1:def 15;
consider g being Function of Y, J.i such that
g is continuous and
g|(the carrier of X) = proj(J,i)*f and
A26: G.x = g by A24;
x in dom G by A6,A21;
then
A27: (rngs G).x = rng g by A26,FUNCT_6:22;
h.x in (rngs G).x by A18,A19,A20,A21;
hence thesis by A23,A27,A25;
end;
hence thesis by A17,A20,CARD_3:def 5;
end;
dom <:G:> c= the carrier of Y
proof
let x be object;
assume
A28: x in dom <:G:>;
consider j being object such that
A29: j in I by XBOOLE_0:def 1;
consider i being Element of I such that
i = j and
A30: ex g being Function of Y, J.i st g is continuous & g|(the carrier
of X) = proj(J,i)*f & G.j = g by A7,A29;
consider g being Function of Y, J.i such that
g is continuous and
g|(the carrier of X) = proj(J,i)*f and
A31: G.j = g by A30;
g in rng G by A6,A29,A31,FUNCT_1:def 3;
then x in dom g by A28,FUNCT_6:32;
hence thesis;
end;
then
A32: dom <:G:> = the carrier of Y by A8;
rng <:G:> c= product rngs G by FUNCT_6:29;
then
A33: rng <:G:> c= product Carrier J by A16;
then rng <:G:> c= the carrier of product J by Def3;
then reconsider
h = <:G:> as Function of the carrier of Y, the carrier of product
J by A32,FUNCT_2:def 1,RELSET_1:4;
A34: dom (h|(the carrier of X)) = dom h /\ the carrier of X by RELAT_1:61
.= (the carrier of Y) /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X by A3,BORSUK_1:1,XBOOLE_1:28
.= dom f by FUNCT_2:def 1;
A35: for x being object st x in dom (h|(the carrier of X)) holds (h|(the
carrier of X)).x = f.x
proof
let x be object;
assume
A36: x in dom (h|(the carrier of X));
then
A37: x in dom h by RELAT_1:57;
(h|(the carrier of X)).x in rng (h|(the carrier of X)) by A36,FUNCT_1:def 3
;
then (h|(the carrier of X)).x in the carrier of product J;
then (h|(the carrier of X)).x in product Carrier J by Def3;
then consider z being Function such that
A38: (h|(the carrier of X)).x = z and
A39: dom z = dom Carrier J and
for i being object st i in dom Carrier J holds z.i in (Carrier J).i by
CARD_3:def 5;
f.x in rng f by A34,A36,FUNCT_1:def 3;
then f.x in the carrier of product J;
then
A40: f.x in product Carrier J by Def3;
then consider y being Function such that
A41: f.x = y and
A42: dom y = dom Carrier J and
for i being object st i in dom Carrier J holds y.i in (Carrier J).i by
CARD_3:def 5;
A43: x in the carrier of Y by A37;
for j being object st j in dom y holds y.j = z.j
proof
let j be object;
assume j in dom y;
then
A44: j in I by A42;
then consider i being Element of I such that
A45: i = j and
A46: ex g being Function of Y, J.i st g is continuous & g|(the
carrier of X) = proj(J,i)*f & G.j = g by A7;
A47: y in dom proj(Carrier J,i) by A40,A41,CARD_3:def 16;
consider g being Function of Y, J.i such that
g is continuous and
A48: g|(the carrier of X) = proj(J,i)*f and
A49: G.j = g by A46;
x in dom h & z = <:G:>.x by A36,A43,A38,FUNCT_1:49,FUNCT_2:def 1;
hence z.j = g.x by A6,A44,A49,FUNCT_6:34
.= (proj(J,i)*f).x by A36,A48,FUNCT_1:49
.= proj(Carrier J,i).y by A36,A41,FUNCT_2:15
.= y.j by A45,A47,CARD_3:def 16;
end;
hence thesis by A41,A42,A38,A39,FUNCT_1:2;
end;
reconsider h as Function of Y, product J;
A50: for P being Subset of product J st P in B holds h"P is open
proof
let P be Subset of product J;
reconsider p = P as Subset of product Carrier J by Def3;
assume P in B;
then consider
i being set, T being TopStruct, V being Subset of T such that
A51: i in I and
A52: V is open and
A53: T = J.i and
A54: p = product ((Carrier J) +* (i,V)) by Def2;
consider j being Element of I such that
A55: j = i and
A56: ex g being Function of Y, J.j st g is continuous & g|(the carrier
of X) = proj(J,j)*f & G.i = g by A7,A51;
reconsider V as Subset of J.j by A53,A55;
A57: dom proj(J,j) = product Carrier J by CARD_3:def 16;
consider g being Function of Y, J.j such that
A58: g is continuous and
g|(the carrier of X) = proj(J,j)*f and
A59: G.i = g by A56;
A60: dom g = the carrier of Y by FUNCT_2:def 1
.= dom h by FUNCT_2:def 1;
A61: proj(J,j)"V = p by A54,A55,Th4;
A62: h"P c= g"V
proof
let x be object;
assume
A63: x in h"P;
then
A64: h.x in proj(J,j)"V by A61,FUNCT_1:def 7;
then h.x in product Carrier J by A57,FUNCT_1:def 7;
then consider y being Function such that
A65: h.x = y and
dom y = dom Carrier J and
for i being object st i in dom Carrier J holds y.i in (Carrier J).i by
CARD_3:def 5;
h.x in dom proj(J,j) by A64,FUNCT_1:def 7;
then proj(J,j).(h.x) = y.j by A65,CARD_3:def 16;
then
A66: y.j in V by A64,FUNCT_1:def 7;
x in dom h by A63,FUNCT_1:def 7;
then
A67: g.x = y.j by A6,A55,A59,A65,FUNCT_6:34;
x in dom g by A60,A63,FUNCT_1:def 7;
hence thesis by A66,A67,FUNCT_1:def 7;
end;
A68: g"V c= h"P
proof
let x be object;
assume
A69: x in g"V;
then
A70: x in dom h by A60,FUNCT_1:def 7;
then
A71: h.x in rng h by FUNCT_1:def 3;
then consider y being Function such that
A72: h.x = y and
dom y = dom Carrier J and
for i being object st i in dom Carrier J holds y.i in (Carrier J).i
by A33,
CARD_3:def 5;
h.x in product Carrier J by A33,A71;
then y in dom proj(Carrier J,j) by A72,CARD_3:def 16;
then
A73: proj(J,j).(h.x) = y.j by A72,CARD_3:def 16;
g.x = y.j by A6,A55,A59,A70,A72,FUNCT_6:34;
then proj(J,j).(h.x) in V by A69,A73,FUNCT_1:def 7;
then h.x in proj(J,j)"V by A33,A57,A71,FUNCT_1:def 7;
hence thesis by A61,A70,FUNCT_1:def 7;
end;
[#](J.j) <> {};
then g"V is open by A52,A53,A55,A58,TOPS_2:43;
hence thesis by A62,A68,XBOOLE_0:def 10;
end;
take h;
B is prebasis of product J by Def3;
hence h is continuous by A50,YELLOW_9:36;
thus thesis by A34,A35,FUNCT_1:2;
end;
theorem ::p.121 lemma 3.2.(ii)
for T being non empty TopSpace st T is injective for S being non empty
SubSpace of T st S is_a_retract_of T holds S is injective
proof
let T be non empty TopSpace;
assume
A1: T is injective;
let S be non empty SubSpace of T;
set p = incl S;
assume S is_a_retract_of T;
then consider r being continuous Function of T,S such that
A2: r is being_a_retraction by BORSUK_1:def 17;
let X be non empty TopSpace, F be Function of X, S;
assume
A3: F is continuous;
reconsider f = p*F as Function of X,T;
let Y be non empty TopSpace;
assume
A4: X is SubSpace of Y;
p is continuous by TMAP_1:87;
then consider g be Function of Y,T such that
A5: g is continuous and
A6: g|(the carrier of X) = f by A1,A3,A4;
take G = r*g;
A7: the carrier of S c= the carrier of T by BORSUK_1:1;
A8: the carrier of X c= the carrier of Y by A4,BORSUK_1:1;
A9: for x being object st x in dom F holds F.x = G.x
proof
let x be object;
assume
A10: x in dom F;
then
A11: x in the carrier of X & g.x = f.x by A6,FUNCT_1:49;
A12: F.x in rng F by A10,FUNCT_1:def 3;
then F.x in the carrier of S;
then reconsider y = F.x as Point of T by A7;
A13: f.x = p.y by A10,FUNCT_2:15
.= F.x by A12,TMAP_1:84;
F.x = r.y by A2,A12,BORSUK_1:def 16;
hence thesis by A8,A13,A11,FUNCT_2:15;
end;
thus G is continuous by A5;
A14: dom F = the carrier of X by FUNCT_2:def 1;
dom G /\ the carrier of X = (the carrier of Y) /\ the carrier of X by
FUNCT_2:def 1
.= the carrier of X by A4,BORSUK_1:1,XBOOLE_1:28;
hence thesis by A14,A9,FUNCT_1:46;
end;
definition
let X be 1-sorted, Y be TopStruct, f be Function of X,Y;
func Image f -> SubSpace of Y equals
Y|(rng f);
coherence;
end;
registration
let X be non empty 1-sorted, Y be non empty TopStruct, f be Function of X,Y;
cluster Image f -> non empty;
coherence;
end;
theorem Th9:
for X being 1-sorted, Y being TopStruct, f being Function of X,Y
holds the carrier of Image f = rng f
proof
let X be 1-sorted,Y be TopStruct, f be Function of X,Y;
thus the carrier of Image f = [#](Y|(rng f)) .= rng f by PRE_TOPC:def 5;
end;
definition
let X be 1-sorted, Y be non empty TopStruct, f be Function of X,Y;
func corestr(f) -> Function of X,Image f equals
f;
coherence
proof
the carrier of Image f = rng f & the carrier of X = dom f by Th9,
FUNCT_2:def 1;
hence thesis by FUNCT_2:1;
end;
end;
theorem Th10:
for X, Y being non empty TopSpace, f being Function of X,Y st f
is continuous holds corestr f is continuous
proof
let X, Y be non empty TopSpace;
let f be Function of X,Y;
A1: f is Function of dom f,rng f by FUNCT_2:1;
A2: [#]Y <> {};
assume
A3: f is continuous;
A4: for R being Subset of Image f st R is open holds (corestr f)"R is open
proof
[#](Image f) = rng f by Th9;
then
A5: f"([#](Image f)) = dom f by A1,FUNCT_2:40
.= the carrier of X by FUNCT_2:def 1;
the carrier of X in the topology of X by PRE_TOPC:def 1;
then
A6: f"([#](Image f)) is open by A5;
let R be Subset of Image f;
assume R is open;
then R in the topology of Image f;
then consider Q being Subset of Y such that
A7: Q in the topology of Y and
A8: R = Q /\ [#](Image f) by PRE_TOPC:def 4;
reconsider Q as Subset of Y;
Q is open by A7;
then
A9: f"Q is open by A3,A2,TOPS_2:43;
f"Q /\ f"([#](Image f)) = f"(Q /\ [#](Image f)) by FUNCT_1:68;
hence thesis by A8,A9,A6,TOPS_1:11;
end;
[#]Image f <> {};
hence thesis by A4,TOPS_2:43;
end;
registration
let X be 1-sorted,Y be non empty TopStruct;
let f be Function of X,Y;
cluster corestr f -> onto;
coherence
proof
the carrier of Image f = rng corestr f by Th9;
hence thesis by FUNCT_2:def 3;
end;
end;
definition
let X,Y be TopStruct;
pred X is_Retract_of Y means
ex f being Function of Y,Y st f is continuous &
f*f = f & Image f, X are_homeomorphic;
end;
theorem Th11: ::p.121 lemma 3.2.(iii)
for T,S being non empty TopSpace st T is injective for f being
Function of T,S st corestr(f) is being_homeomorphism holds T is_Retract_of S
proof
let T,S be non empty TopSpace;
assume
A1: T is injective;
let f be Function of T,S;
consider g being Function of Image f, T such that
A2: g = (corestr f)";
assume
A3: corestr(f) is being_homeomorphism;
then g is continuous by A2,TOPS_2:def 5;
then consider h being Function of S,T such that
A4: h is continuous and
A5: h|(the carrier of Image f) = g by A1;
g is being_homeomorphism by A3,A2,TOPS_2:56;
then
A6: g is one-to-one by TOPS_2:def 5;
A7: the carrier of Image f = rng f by Th9;
A8: for x being object st x in the carrier of T holds (h*f).x = x
proof
let x be object;
assume
A9: x in the carrier of T;
then
A10: x in dom (corestr f) by FUNCT_2:def 1;
A11: x in dom f by A9,FUNCT_2:def 1;
then
A12: f.x in rng f by FUNCT_1:def 3;
A13: corestr f is one-to-one by A3,TOPS_2:def 5;
thus (h*f).x = h.(f.x) by A11,FUNCT_1:13
.= ((corestr f)").((corestr f).x) by A2,A5,A7,A12,FUNCT_1:49
.= ((corestr f qua Function)").((corestr f).x) by A13,TOPS_2:def 4
.= x by A10,A13,FUNCT_1:34;
end;
dom (h*f) = the carrier of T by FUNCT_2:def 1;
then
A14: h*f = id (the carrier of T) by A8,FUNCT_1:17;
take F = f*h;
set H = h*(incl Image F);
A15: dom H = [#](Image F) by FUNCT_2:def 1;
rng h c= the carrier of T;
then
A16: rng h c= dom f by FUNCT_2:def 1;
A17: rng F c= rng f
proof
let y be object;
assume y in rng F;
then consider x being object such that
A18: x in dom F and
A19: y = F.x by FUNCT_1:def 3;
x in the carrier of S by A18;
then
A20: x in dom h by FUNCT_2:def 1;
then
A21: h.x in rng h by FUNCT_1:def 3;
f.(h.x) = y by A19,A20,FUNCT_1:13;
hence thesis by A16,A21,FUNCT_1:def 3;
end;
A22: H is one-to-one
proof
let x,y be Element of Image F;
assume
A23: H.x = H.y;
A24: x in the carrier of Image F;
then
A25: x in dom (incl Image F) by FUNCT_2:def 1;
A26: y in the carrier of Image F;
then
A27: y in dom (incl Image F) by FUNCT_2:def 1;
A28: y in rng F by A26,Th9;
A29: x in rng F by A24,Th9;
then reconsider a = x, b = y as Point of S by A28;
reconsider x9 = x, y9 = y as Element of Image f by A17,A29,A28,Th9;
g.x9 = h.x by A5,FUNCT_1:49
.= h.((incl Image F).a) by TMAP_1:84
.= (h*(incl Image F)).b by A23,A25,FUNCT_1:13
.= h.((incl Image F).b) by A27,FUNCT_1:13
.= h.y by TMAP_1:84
.= g.y9 by A5,FUNCT_1:49;
hence thesis by A6;
end;
A30: dom incl Image F = the carrier of Image F by FUNCT_2:def 1;
A31: rng H = [#]T
proof
thus rng H c= [#](T);
let y be object;
assume
A32: y in [#](T);
then
A33: y in dom f by FUNCT_2:def 1;
then
A34: F.(f.y) = ((f*h)*f).y by FUNCT_1:13
.= (f*id T).y by A14,RELAT_1:36
.= f.y by FUNCT_2:17;
A35: f.y in rng f by A33,FUNCT_1:def 3;
then reconsider pp = f.y as Point of S;
f.y in the carrier of S by A35;
then
A36: f.y in dom F by FUNCT_2:def 1;
then F.(f.y) in rng F by FUNCT_1:def 3;
then
A37: f.y in the carrier of Image F by A34,Th9;
then
A38: y in dom((incl Image F)*f) by A30,A33,FUNCT_1:11;
dom H = rng F by A15,Th9;
then
A39: f.y in dom H by A36,A34,FUNCT_1:def 3;
H.(f.y) = ((h*(incl Image F))*f).y by A33,FUNCT_1:13
.= (h*((incl Image F)*f)).y by RELAT_1:36
.= h.(((incl Image F)*f).y) by A38,FUNCT_1:13
.= h.((incl Image F).pp) by A33,FUNCT_1:13
.= h.(f.y) by A37,TMAP_1:84
.= (id T).y by A14,A33,FUNCT_1:13
.= y by A32,FUNCT_1:18;
hence thesis by A39,FUNCT_1:def 3;
end;
reconsider p = incl(Image f) as Function of Image f,S;
A40: [#]S <> {};
A41: dom (p*(corestr f)) = the carrier of T by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
A42: for P being Subset of S holds f"P = (p*(corestr f))"P
proof
let P be Subset of S;
hereby
let x be object;
assume
A43: x in f"P;
then
A44: x in dom f by FUNCT_1:def 7;
then f.x in rng f by FUNCT_1:def 3;
then
A45: f.x in the carrier of Image f by Th9;
A46: f.x in P by A43,FUNCT_1:def 7;
then reconsider y = f.x as Point of S;
(p*(corestr f)).x = p.(f.x) by A44,FUNCT_1:13
.= y by A45,TMAP_1:84;
hence x in (p*(corestr f))"P by A41,A44,A46,FUNCT_1:def 7;
end;
let x be object;
assume
A47: x in (p*(corestr f))"P;
then
A48: x in dom(p*(corestr f)) by FUNCT_1:def 7;
then
A49: f.x in rng f by A41,FUNCT_1:def 3;
then reconsider y = f.x as Point of S;
A50: (p*(corestr f)).x in P by A47,FUNCT_1:def 7;
A51: f.x in the carrier of Image f by A49,Th9;
(p*(corestr f)).x = p.(f.x) by A41,A48,FUNCT_1:13
.= y by A51,TMAP_1:84;
hence thesis by A41,A48,A50,FUNCT_1:def 7;
end;
A52: corestr(f) is continuous by A3,TOPS_2:def 5;
A53: for P being Subset of Image F st P is open holds (H")"P is open
proof
let P be Subset of Image F;
A54: p is continuous by TMAP_1:87;
(incl Image F).:P = P
proof
hereby
let y be object;
assume y in (incl Image F).:P;
then consider x being object such that
A55: x in dom (incl Image F) and
A56: x in P & y = (incl Image F).x by FUNCT_1:def 6;
x in the carrier of Image F by A55;
then x in rng F by Th9;
then reconsider xx = x as Point of S;
(incl Image F).xx = x by A55,TMAP_1:84;
hence y in P by A56;
end;
let y be object;
assume
A57: y in P;
then
A58: y in the carrier of Image F;
then y in rng F by Th9;
then reconsider yy = y as Point of S;
A59: yy = (incl Image F).y by A57,TMAP_1:84;
y in dom (incl Image F) by A58,FUNCT_2:def 1;
hence thesis by A57,A59,FUNCT_1:def 6;
end;
then
A60: H.:P = h.:P by RELAT_1:126;
assume P is open;
then P in the topology of Image F;
then consider Q being Subset of S such that
A61: Q in the topology of S and
A62: P = Q /\ [#](Image F) by PRE_TOPC:def 4;
reconsider Q as Subset of S;
A63: f"Q = h.:P
proof
hereby
let x be object;
assume
A64: x in f"Q;
then
A65: x in dom f by FUNCT_1:def 7;
then
A66: h.(f.x) = (id T).x by A14,FUNCT_1:13
.= x by A64,FUNCT_1:18;
f.x in rng f by A65,FUNCT_1:def 3;
then
A67: f.x in the carrier of S;
then
A68: f.x in dom h by FUNCT_2:def 1;
A69: f.x in dom F by A67,FUNCT_2:def 1;
F.(f.x) = f.(h.(f.x)) by A68,FUNCT_1:13
.= f.((id T).x) by A14,A65,FUNCT_1:13
.= f.x by A64,FUNCT_1:18;
then f.x in rng F by A69,FUNCT_1:def 3;
then
A70: f.x in the carrier of Image F by Th9;
f.x in Q by A64,FUNCT_1:def 7;
then f.x in P by A62,A70,XBOOLE_0:def 4;
hence x in h.:P by A68,A66,FUNCT_1:def 6;
end;
let x be object;
assume x in h.:P;
then consider y being object such that
A71: y in dom h and
A72: y in P and
A73: x = h.y by FUNCT_1:def 6;
A74: y in Q by A62,A72,XBOOLE_0:def 4;
y in the carrier of Image F by A72;
then
A75: y in rng F by Th9;
A76: x in rng h by A71,A73,FUNCT_1:def 3;
then f.x in rng f by A16,FUNCT_1:def 3;
then reconsider a = f.x, b = y as Element of Image f by A17,A75,Th9;
g.a = h.(f.x) by A5,FUNCT_1:49
.= (id T).x by A16,A14,A76,FUNCT_1:13
.= h.y by A73,A76,FUNCT_1:18
.= g .b by A5,FUNCT_1:49;
then f.x in Q by A6,A74;
hence thesis by A16,A76,FUNCT_1:def 7;
end;
Q is open by A61;
then (p*(corestr f))"Q is open by A40,A52,A54,TOPS_2:43;
then f"Q is open by A42;
hence thesis by A31,A22,A63,A60,TOPS_2:54;
end;
A77: p is continuous by TMAP_1:87;
A78: [#]T <> {};
for P being Subset of S st P is open holds F"P is open
proof
let P be Subset of S;
assume P is open;
then (p*(corestr f))"P is open by A40,A52,A77,TOPS_2:43;
then f"P is open by A42;
then h"(f"P) is open by A78,A4,TOPS_2:43;
hence thesis by RELAT_1:146;
end;
hence F is continuous by A40,TOPS_2:43;
thus F*F = (f*h*f)*h by RELAT_1:36
.= f*(id T)*h by A14,RELAT_1:36
.= F by FUNCT_2:17;
[#]Image F <> {};
then incl Image F is continuous & H" is continuous by A53,TMAP_1:87,TOPS_2:43
;
then H is being_homeomorphism by A4,A15,A31,A22,TOPS_2:def 5;
hence thesis by T_0TOPSP:def 1;
end;
definition
func Sierpinski_Space -> strict TopStruct means
:Def9:
the carrier of it = {0,1} & the topology of it = {{}, {1}, {0,1}};
existence
proof
set c = {0,1}, t = {{}, {1}, {0,1} };
t c= bool c
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A1: x in t;
per cases by A1,ENUMSET1:def 1;
suppose
A2: x = {};
{} c= c;
hence thesis by A2;
end;
suppose
x = {1};
then xx c= c by ZFMISC_1:7;
hence thesis;
end;
suppose
x = {0,1};
then xx c= c;
hence thesis;
end;
end;
then reconsider t as Subset-Family of c;
take s = TopStruct (# c, t #);
thus the carrier of s = {0,1};
thus thesis;
end;
uniqueness;
end;
registration
cluster Sierpinski_Space -> non empty TopSpace-like;
coherence
proof
set IT = Sierpinski_Space;
thus IT is non empty by Def9;
{0,1} in {{}, {1}, {0,1} } by ENUMSET1:def 1;
then the carrier of IT in {{}, {1}, {0,1} } by Def9;
hence the carrier of IT in the topology of IT by Def9;
thus for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT
proof
let a be Subset-Family of IT;
assume a c= the topology of IT;
then
A1: a c= {{}, {1}, {0,1} } by Def9;
per cases by A1,ZFMISC_1:118;
suppose
a = {};
then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1,ZFMISC_1:2;
hence thesis by Def9;
end;
suppose
a = {{}};
then union a = {} by ZFMISC_1:25;
then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {{1}};
then union a = {1} by ZFMISC_1:25;
then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {{0,1}};
then union a = {0,1} by ZFMISC_1:25;
then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {{},{1}};
then union a = {} \/ {1} by ZFMISC_1:75;
then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {{1},{0,1}};
then union a = {1} \/ {0,1} by ZFMISC_1:75
.= {0,1} by ZFMISC_1:9;
then union a in {{} , {1}, {0,1}} by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {{},{0,1}};
then union a = {} \/ {0,1} by ZFMISC_1:75;
then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {{},{1},{0,1}};
then a = {{} } \/ {{1},{0,1}} by ENUMSET1:2;
then union a = union {{}} \/ union {{1},{0,1}} by ZFMISC_1:78
.= {} \/ union {{1},{0,1}} by ZFMISC_1:25
.= {1} \/ {0,1} by ZFMISC_1:75
.= {0,1} by ZFMISC_1:9;
then union a in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
end;
let a,b be Subset of IT;
assume a in the topology of IT & b in the topology of IT;
then
A2: a in {{}, {1}, {0,1} } & b in {{}, {1}, {0,1} } by Def9;
per cases by A2,ENUMSET1:def 1;
suppose
a = {} & b = {};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {} & b = {1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {} & b = {0,1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {1} & b = {};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {1} & b = {1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {1} & b = {0,1};
then a /\ b = {1} by ZFMISC_1:13;
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {0,1} & b = {};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {0,1} & b = {1};
then a /\ b = {1} by ZFMISC_1:13;
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
suppose
a = {0,1} & b = {0,1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:def 1;
hence thesis by Def9;
end;
end;
end;
Lm1: Sierpinski_Space is T_0
proof
set S = Sierpinski_Space;
for x,y being Point of S st x <> y holds ex V being Subset of S st V is
open & ( x in V & not y in V or y in V & not x in V )
proof
set V = {1};
let x,y be Point of S;
y in the carrier of S;
then
A1: y in {0,1} by Def9;
{1} c= {0,1} by ZFMISC_1:7;
then reconsider V as Subset of S by Def9;
x in the carrier of S;
then x in {0,1} by Def9;
then
A2: x = 0 or x = 1 by TARSKI:def 2;
{1} in {{}, {1}, {0,1} } by ENUMSET1:def 1;
then {1} in the topology of S by Def9;
then
A3: V is open;
assume
A4: x <> y;
per cases by A4,A1,A2,TARSKI:def 2;
suppose
x = 0 & y = 1;
then x in V & not y in V or y in V & not x in V by TARSKI:def 1;
hence thesis by A3;
end;
suppose
x = 1 & y = 0;
then x in V & not y in V or y in V & not x in V by TARSKI:def 1;
hence thesis by A3;
end;
end;
hence thesis;
end;
registration
cluster Sierpinski_Space -> T_0;
coherence by Lm1;
end;
registration ::p.122 lemma 3.3.
cluster Sierpinski_Space -> injective;
coherence
proof
let X be non empty TopSpace;
set S = Sierpinski_Space;
let f be Function of X, S;
A1: [#]S <> {};
{1} c= {0,1} by ZFMISC_1:7;
then reconsider u = {1} as Subset of S by Def9;
u in {{}, {1}, {0,1}} by ENUMSET1:def 1;
then u in the topology of S by Def9;
then
A2: u is open;
assume f is continuous;
then f"u is open by A1,A2,TOPS_2:43;
then
A3: f"u in the topology of X;
let Y be non empty TopSpace;
assume
A4: X is SubSpace of Y;
then consider V being Subset of Y such that
A5: V in the topology of Y and
A6: f"u = V /\ [#](X) by A3,PRE_TOPC:def 4;
reconsider V as Subset of Y;
set g = chi(V,the carrier of Y);
A7: dom g = the carrier of Y by FUNCT_3:def 3;
reconsider g as Function of Y,S by Def9;
A8: the carrier of X c= the carrier of Y by A4,BORSUK_1:1;
A9: for x being object st x in dom f holds f.x = g.x
proof
let x be object;
assume
A10: x in dom f;
then
A11: x in the carrier of X;
per cases;
suppose
A12: x in V;
then x in f"u by A6,A10,XBOOLE_0:def 4;
then
A13: f.x in {1} by FUNCT_1:def 7;
g.x = 1 by A12,FUNCT_3:def 3;
hence thesis by A13,TARSKI:def 1;
end;
suppose
A14: not x in V;
f.x in rng f by A10,FUNCT_1:def 3;
then f.x in the carrier of S;
then f.x in {0,1} by Def9;
then
A15: f.x = 0 or f.x = 1 by TARSKI:def 2;
not x in f"{1} by A6,A14,XBOOLE_0:def 4;
then not x in dom f or not f.x in {1} by FUNCT_1:def 7;
hence thesis by A8,A10,A11,A14,A15,FUNCT_3:def 3,TARSKI:def 1;
end;
end;
take g;
A16: V is open by A5;
for P being Subset of S st P is open holds g"P is open
proof
let P be Subset of S;
assume P is open;
then P in the topology of S;
then
A17: P in {{}, {1}, {0,1} } by Def9;
per cases by A17,ENUMSET1:def 1;
suppose
P = {};
then g"P = {};
then g"P in the topology of Y by PRE_TOPC:1;
hence thesis;
end;
suppose
A18: P = {1};
A19: g"P c= V
proof
let x be object;
assume
A20: x in g"P;
then g.x in {1} by A18,FUNCT_1:def 7;
then g.x = 1 by TARSKI:def 1;
hence thesis by A20,FUNCT_3:def 3;
end;
V c= g"P
proof
let x be object;
assume
A21: x in V;
then g.x = 1 by FUNCT_3:def 3;
then g.x in {1} by TARSKI:def 1;
hence thesis by A7,A18,A21,FUNCT_1:def 7;
end;
hence thesis by A16,A19,XBOOLE_0:def 10;
end;
suppose
P = {0,1};
then g"P = the carrier of Y by FUNCT_2:40;
then g"P in the topology of Y by PRE_TOPC:def 1;
hence thesis;
end;
end;
hence g is continuous by A1,TOPS_2:43;
dom g /\ (the carrier of X) = (the carrier of Y) /\ (the carrier of X
) by FUNCT_3:def 3
.= the carrier of X by A4,BORSUK_1:1,XBOOLE_1:28
.= dom f by FUNCT_2:def 1;
hence thesis by A9,FUNCT_1:46;
end;
end;
registration
let I be set;
let S be non empty 1-sorted;
cluster I --> S -> non-Empty;
coherence
proof
let s be 1-sorted;
assume s in rng (I --> S);
hence thesis by TARSKI:def 1;
end;
end;
registration
let I be set;
let T be TopStruct;
cluster I --> T -> TopStruct-yielding;
coherence
proof
let x be object;
assume x in rng (I --> T);
hence thesis by TARSKI:def 1;
end;
end;
registration
let I be non empty set;
let L be non empty antisymmetric RelStr;
cluster product (I --> L) -> antisymmetric;
coherence
proof
for i being Element of I holds (I --> L).i is antisymmetric;
hence thesis by WAYBEL_3:30;
end;
end;
registration
let I be non empty set;
let L be non empty transitive RelStr;
cluster product (I --> L) -> transitive;
coherence
proof
for i being Element of I holds (I --> L).i is transitive;
hence thesis by WAYBEL_3:29;
end;
end;
theorem
for T being Scott TopAugmentation of BoolePoset {0} holds the topology
of T = the topology of Sierpinski_Space
proof
let T be Scott TopAugmentation of BoolePoset {0};
A1: LattPOSet BooleLatt {0} =
RelStr(#the carrier of BooleLatt {0}, LattRel( BooleLatt {0})#)
by LATTICE3:def 2;
A2: the RelStr of T = BoolePoset {0} by YELLOW_9:def 4;
then
A3: the carrier of T = the carrier of LattPOSet BooleLatt {0}
by YELLOW_1:def 2
.= bool {0} by A1,LATTICE3:def 1
.= {0,1} by CARD_1:49,ZFMISC_1:24;
then reconsider j = {0}, z = 0 as Element of BoolePoset {0}
by A2,TARSKI:def 2,CARD_1:49;
A4: now
let x be object;
assume x in the topology of Sierpinski_Space;
then
A5: x in {{}, {{0}}, {0,{0}} } by Def9,CARD_1:49;
per cases by A5,ENUMSET1:def 1,CARD_1:49;
suppose
x = {};
hence x in the topology of T by PRE_TOPC:1;
end;
suppose
A6: x = {{0}};
then reconsider x9 = x as Subset of T by A3,ZFMISC_1:7,CARD_1:49;
for a,b being Element of T st a in x9 & a <= b holds b in x9
proof
let a,b be Element of T;
assume that
A7: a in x9 and
A8: a <= b;
A9: a = {0} by A6,A7,TARSKI:def 1;
A10: b <> 0
proof
assume
A11: b = 0;
[a, b] in the InternalRel of T by A8,ORDERS_2:def 5;
then j <= z by A2,A9,A11,ORDERS_2:def 5;
then {0} c= {} by YELLOW_1:2;
hence thesis;
end;
b = 0 or b = 1 by A3,TARSKI:def 2;
hence thesis by A6,A10,TARSKI:def 1,CARD_1:49;
end;
then
A12: x9 is upper by WAYBEL_0:def 20;
for D being non empty directed Subset of T st sup D in x9 holds D
meets x9
proof
let D be non empty directed Subset of T;
assume
A13: sup D in x9;
D <> {0}
proof
assume D = {0};
then sup D = sup {z} by A2,YELLOW_0:17,26
.= 0 by YELLOW_0:39;
hence thesis by A6,A13,TARSKI:def 1;
end;
then D = {1} or D = {0,1} by A3,ZFMISC_1:36;
then
A14: 1 in D by TARSKI:def 1,def 2;
1 in x9 by A6,TARSKI:def 1,CARD_1:49;
hence thesis by A14,XBOOLE_0:3;
end;
then x9 is inaccessible by WAYBEL11:def 1;
then x9 is open by A12,WAYBEL11:def 4;
hence x in the topology of T;
end;
suppose
x = {0,1};
hence x in the topology of T by A3,PRE_TOPC:def 1;
end;
end;
reconsider c = {z} as Subset of T by A2;
now
set a = 0, b = {0};
let y be object;
A15: not b in {z};
a c= b & a in {z} by TARSKI:def 1;
then not {z} is upper by A15,WAYBEL_7:7;
then not c is upper by A2,WAYBEL_0:25;
then
A16: not c is open by WAYBEL11:def 4;
assume
A17: y in the topology of T;
then reconsider x = y as Subset of T;
x = {} or x = {0} or x = {1} or x = {0,1} by A3,ZFMISC_1:36;
then y in {{}, {1}, {0,1} } by A17,A16,ENUMSET1:def 1;
hence y in the topology of Sierpinski_Space by Def9;
end;
hence thesis by A4,TARSKI:2;
end;
theorem Th13:
for I being non empty set holds the set of all product ((Carrier (I -->
Sierpinski_Space))+*(i,{1})) where i is Element of I is
prebasis of product (I --> Sierpinski_Space)
proof
let I be non empty set;
set IS = I --> Sierpinski_Space, pB = the set of all
product ((Carrier IS)+*(i,{1})) where i is Element of I;
set P = product_prebasis IS;
A1: P is prebasis of product IS by Def3;
then
A2: P c= the topology of product IS by TOPS_2:64;
pB c= bool the carrier of product IS
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in pB;
then consider i being Element of I such that
A3: x = product ((Carrier IS)+*(i,{1}));
product ((Carrier IS)+*(i,{1})) c= product Carrier IS
proof
let y be object;
assume y in product ((Carrier IS)+*(i,{1}));
then consider g being Function such that
A4: y = g and
A5: dom g = dom ((Carrier IS)+*(i,{1})) and
A6: for z being object st z in dom ((Carrier IS)+*(i,{1})) holds g.z in
((Carrier IS)+*(i,{1})).z by CARD_3:def 5;
A7: for z being object st z in dom Carrier IS
holds g.z in ( Carrier IS ) . z
proof
let z be object;
assume
A8: z in dom (Carrier IS);
then
A9: z in I;
then consider R being 1-sorted such that
A10: R = IS.z and
A11: (Carrier IS).z = the carrier of R by PRALG_1:def 15;
A12: the carrier of R = the carrier of Sierpinski_Space by A9,A10,FUNCOP_1:7
.= {0,1} by Def9;
z in dom ((Carrier IS)+*(i,{1})) by A8,FUNCT_7:30;
then
A13: g.z in ((Carrier IS)+*(i,{1})).z by A6;
per cases;
suppose
z = i;
then ((Carrier IS)+*(i,{1})).z = {1} by A8,FUNCT_7:31;
then g.z = 1 by A13,TARSKI:def 1;
hence thesis by A11,A12,TARSKI:def 2;
end;
suppose
z <> i;
hence thesis by A13,FUNCT_7:32;
end;
end;
dom g = dom Carrier IS by A5,FUNCT_7:30;
hence thesis by A4,A7,CARD_3:def 5;
end;
then xx c= the carrier of product IS by A3,Def3;
hence thesis;
end;
then reconsider B = pB as Subset-Family of product IS;
reconsider B as Subset-Family of product IS;
A14: B c= P
proof
{1} c= {0,1} by ZFMISC_1:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
let x be object;
assume
A15: x in B;
then consider i being Element of I such that
A16: x = product ((Carrier IS)+*(i,{1}));
reconsider y = x as Subset of product Carrier IS by A15,Def3;
{1} in {{}, {1}, {0,1} } by ENUMSET1:def 1;
then {1} in the topology of Sierpinski_Space by Def9;
then
A17: V is open;
Sierpinski_Space = IS.i & y = product ((Carrier IS) +* (i,V)) by A16;
hence thesis by A17,Def2;
end;
reconsider P as Subset-Family of product IS by Def3;
reconsider P as Subset-Family of product IS;
FinMeetCl P is Basis of product IS by A1,YELLOW_9:23;
then reconsider F = (FinMeetCl P) \ {{}} as Basis of product IS by Th2;
A18: F c= FinMeetCl B
proof
let x be object;
assume
A19: x in F;
then reconsider y = x as Subset of product IS;
x in FinMeetCl P by A19,XBOOLE_0:def 5;
then consider Y1 being Subset-Family of product IS such that
A20: Y1 c= P and
A21: Y1 is finite and
A22: y = Intersect Y1 by CANTOR_1:def 3;
reconsider Y2 = Y1 /\ B as Subset-Family of product IS;
A23: Y2 c= B & Y2 is finite by A21,FINSET_1:1,XBOOLE_1:17;
A24: the carrier of product IS = product Carrier IS by Def3;
A25: not x in {{}} by A19,XBOOLE_0:def 5;
A26: Intersect Y2 c= Intersect Y1
proof
let z be object;
assume
A27: z in Intersect Y2;
then
A28: z in product Carrier IS by A24;
for Y being set st Y in Y1 holds z in Y
proof
let Y be set;
assume
A29: Y in Y1;
then reconsider Y9 = Y as Subset of product Carrier IS by Def3;
consider i being set, S being TopStruct, V being Subset of S such that
A30: i in I and
A31: V is open and
A32: S = IS.i and
A33: Y9 = product ((Carrier IS) +* (i,V)) by A20,A29,Def2;
reconsider V9 = V as Subset of Sierpinski_Space by A30,A32,FUNCOP_1:7;
V in the topology of S by A31;
then V9 in the topology of Sierpinski_Space by A30,A32,FUNCOP_1:7;
then
A34: V9 in {{}, {1}, {0,1} } by Def9;
A35: i in dom (Carrier IS) by A30,PARTFUN1:def 2;
A36: V9 <> {}
proof
((Carrier IS)+*(i,{})).i = {} & i in dom ((Carrier IS)+*(i,{}))
by A35,FUNCT_7:30,31;
then
A37: {} in rng ((Carrier IS)+*(i,{})) by FUNCT_1:def 3;
assume V9 = {};
then Y9 = {} by A33,A37,CARD_3:26;
then y = {} by A22,A29,MSSUBFAM:3;
hence thesis by A25,TARSKI:def 1;
end;
reconsider i9 = i as Element of I by A30;
A38: ex RR being 1-sorted st RR = IS.i & (Carrier IS).i = the carrier
of RR by A30,PRALG_1:def 15;
per cases by A34,A36,ENUMSET1:def 1;
suppose
V9 = {1};
then Y9 = product ((Carrier IS)+*(i9,{1})) by A33;
then Y in B;
then Y in Y2 by A29,XBOOLE_0:def 4;
hence thesis by A27,SETFAM_1:43;
end;
suppose
V9 = {0,1};
then V9 = the carrier of Sierpinski_Space by Def9
.= (Carrier IS).i by A30,A38,FUNCOP_1:7;
hence thesis by A28,A33,FUNCT_7:35;
end;
end;
hence thesis by A27,SETFAM_1:43;
end;
Intersect Y1 c= Intersect Y2 by SETFAM_1:44,XBOOLE_1:17;
then y = Intersect Y2 by A22,A26;
hence thesis by A23,CANTOR_1:def 3;
end;
pB c= the topology of product IS by A14,A2;
hence thesis by A18,CANTOR_1:def 4,TOPS_2:64;
end;
registration
let I be non empty set;
let L be complete LATTICE;
cluster product (I --> L) -> with_suprema complete;
coherence
proof
reconsider IB = I --> L as RelStr-yielding non-Empty reflexive-yielding
ManySortedSet of I;
for i being Element of I holds IB.i is complete LATTICE;
hence thesis by WAYBEL_3:31;
end;
end;
registration
let I be non empty set;
let X be algebraic lower-bounded LATTICE;
cluster product (I --> X) -> algebraic;
coherence
proof
set IB = I --> X;
for i being Element of I holds IB.i is algebraic lower-bounded LATTICE;
hence thesis by WAYBEL13:25;
end;
end;
theorem Th14:
for X being non empty set ex f being Function of BoolePoset X,
product (X --> BoolePoset {0}) st f is isomorphic & for Y being Subset of X
holds
f.Y = chi(Y,X)
proof
let X be non empty set;
set XB = X --> BoolePoset {0};
deffunc F(set) = chi($1,X);
consider f being Function such that
A1: dom f = bool X and
A2: for Y being set st Y in bool X holds f.Y = F(Y) from FUNCT_1:sch 5;
LattPOSet BooleLatt {0} = RelStr(#the carrier of BooleLatt {0}, LattRel(
BooleLatt {0})#) by LATTICE3:def 2;
then
A3: the carrier of BoolePoset{0} = the carrier of BooleLatt{0}
by YELLOW_1:def 2
.= bool {{}} by LATTICE3:def 1
.= {0,1} by CARD_1:49,ZFMISC_1:24;
A4: rng f c= product Carrier XB
proof
let y be object;
assume y in rng f;
then consider x being object such that
A5: x in dom f & y = f.x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
A6: dom chi(x,X) = X by FUNCT_3:def 3
.= dom (Carrier XB) by PARTFUN1:def 2;
A7: for z being object st z in dom Carrier XB
holds chi(x,X).z in (Carrier XB).z
proof
let z be object;
assume z in dom (Carrier XB);
then
A8: z in X;
then ex R being 1-sorted st R = XB.z & (Carrier XB).z = the carrier of R
by PRALG_1:def 15;
then
A9: (Carrier XB).z = {0,1} by A3,A8,FUNCOP_1:7;
per cases;
suppose
z in x;
then chi(x,X).z = 1 by A8,FUNCT_3:def 3;
hence thesis by A9,TARSKI:def 2;
end;
suppose
not z in x;
then chi(x,X).z = 0 by A8,FUNCT_3:def 3;
hence thesis by A9,TARSKI:def 2;
end;
end;
chi(x,X) = y by A1,A2,A5;
hence thesis by A6,A7,CARD_3:def 5;
end;
LattPOSet BooleLatt X = RelStr(#the carrier of BooleLatt X, LattRel(
BooleLatt X)#) by LATTICE3:def 2;
then
A10: the carrier of BoolePoset X = the carrier of BooleLatt X by YELLOW_1:def 2
.= bool X by LATTICE3:def 1;
A11: the carrier of product XB = product Carrier XB by YELLOW_1:def 4;
then reconsider
f as Function of BoolePoset X, product (X --> BoolePoset {0}) by A10,A1,A4,
FUNCT_2:def 1,RELSET_1:4;
A12: for A,B being Element of BoolePoset X holds A <= B iff f.A <= f.B
proof
let A,B be Element of BoolePoset X;
A13: f.A = chi(A,X) & f.B = chi(B,X) by A10,A2;
hereby
assume A <= B;
then
A14: A c= B by YELLOW_1:2;
for i being object st i in X ex R being RelStr, xi,yi being Element of
R st R = XB.i & xi = chi(A,X).i & yi = chi(B,X).i & xi <= yi
proof
let i be object;
assume
A15: i in X;
take R = BoolePoset {0};
per cases;
suppose
A16: i in A;
reconsider xi = 1, yi = 1 as Element of R by A3,TARSKI:def 2;
take xi,yi;
thus R = XB.i by A15,FUNCOP_1:7;
thus xi = chi(A,X).i by A15,A16,FUNCT_3:def 3;
thus yi = chi(B,X).i by A14,A15,A16,FUNCT_3:def 3;
thus xi <= yi;
end;
suppose
A17: not i in A;
thus thesis
proof
per cases;
suppose
A18: i in B;
reconsider xi = 0, yi = 1 as Element of R by A3,TARSKI:def 2;
take xi,yi;
thus R = XB.i by A15,FUNCOP_1:7;
thus xi = chi(A,X).i by A15,A17,FUNCT_3:def 3;
thus yi = chi(B,X).i by A15,A18,FUNCT_3:def 3;
xi c= yi;
hence xi <= yi by YELLOW_1:2;
end;
suppose
A19: not i in B;
reconsider xi = 0, yi = 0 as Element of R by A3,TARSKI:def 2;
take xi,yi;
thus R = XB.i by A15,FUNCOP_1:7;
thus xi = chi(A,X).i by A15,A17,FUNCT_3:def 3;
thus yi = chi(B,X).i by A15,A19,FUNCT_3:def 3;
thus xi <= yi;
end;
end;
end;
end;
hence f.A <= f.B by A11,A13,YELLOW_1:def 4;
end;
assume f.A <= f.B;
then consider h1,h2 being Function such that
A20: h1 = f.A and
A21: h2 = f.B and
A22: for i be object st i in X ex R being RelStr, xi,yi being Element of
R st R = XB.i & xi = h1.i & yi = h2.i & xi <= yi by A11,YELLOW_1:def 4;
A c= B
proof
let i be object;
assume
A23: i in A;
then consider R being RelStr, xi,yi being Element of R such that
A24: R = XB.i and
A25: xi = h1.i and
A26: yi = h2.i and
A27: xi <= yi by A10,A22;
reconsider a = xi, b = yi as Element of BoolePoset {0} by A10,A23,A24,
FUNCOP_1:7;
A28: a <= b by A10,A23,A24,A27,FUNCOP_1:7;
A29: xi = chi(A,X).i by A10,A2,A20,A25
.= 1 by A10,A23,FUNCT_3:def 3;
A30: yi <> 0
proof
assume yi = 0;
then {0} c= 0 by A29,A28,YELLOW_1:2,CARD_1:49;
hence thesis;
end;
A31: R = BoolePoset {0} by A10,A23,A24,FUNCOP_1:7;
chi(B,X).i = h2.i by A10,A2,A21
.= 1 by A3,A26,A31,A30,TARSKI:def 2;
hence thesis by FUNCT_3:36;
end;
hence thesis by YELLOW_1:2;
end;
product Carrier XB c= rng f
proof
let z be object;
assume z in product Carrier XB;
then consider g being Function such that
A32: z = g and
A33: dom g = dom (Carrier XB) and
A34: for y being object st y in dom (Carrier XB) holds g.y in (Carrier XB
).y by CARD_3:def 5;
set A = g"{1};
A35: A c= X
proof
let a be object;
assume a in A;
then a in dom g by FUNCT_1:def 7;
hence thesis by A33;
end;
A36: dom chi(A,X) = X by FUNCT_3:def 3
.= dom g by A33,PARTFUN1:def 2;
for a being object st a in dom chi(A,X) holds chi(A,X).a = g.a
proof
let a be object;
assume
A37: a in dom chi(A,X);
then a in X;
then a in dom (Carrier XB) by PARTFUN1:def 2;
then
A38: g.a in (Carrier XB).a by A34;
ex R being 1-sorted st R = XB.a & (Carrier XB).a = the carrier of R
by A37,PRALG_1:def 15;
then (Carrier XB).a = {0,1} by A3,A37,FUNCOP_1:7;
then
A39: g.a = 0 or g.a = 1 by A38,TARSKI:def 2;
per cases;
suppose
a in A;
then chi(A,X).a = 1 & g.a in {1} by A37,FUNCT_1:def 7,FUNCT_3:def 3;
hence thesis by TARSKI:def 1;
end;
suppose
A40: not a in A;
g.a <> 1
proof
assume g.a = 1;
then g.a in {1} by TARSKI:def 1;
hence thesis by A36,A37,A40,FUNCT_1:def 7;
end;
hence thesis by A37,A39,A40,FUNCT_3:def 3;
end;
end;
then z = chi(A,X) by A32,A36,FUNCT_1:2
.= f.A by A2,A35;
hence thesis by A1,A35,FUNCT_1:def 3;
end;
then
A41: rng f = the carrier of product XB by A11;
take f;
for A,B being Element of BoolePoset X st f.A = f.B holds A = B
proof
let A, B be Element of BoolePoset X;
assume
A42: f.A = f.B;
f.A = chi(A,X) & f.B = chi(B,X) by A10,A2;
hence thesis by A10,A42,FUNCT_3:38;
end;
then f is one-to-one;
hence f is isomorphic by A41,A12,WAYBEL_0:66;
thus thesis by A2;
end;
theorem Th15: ::p.122 lemma 3.4.(i)
for I being non empty set for T being Scott TopAugmentation of
product (I --> BoolePoset {0})
holds the topology of T = the topology of product
(I --> Sierpinski_Space)
proof
let I be non empty set;
set IB = I --> BoolePoset {0}, IS = I --> Sierpinski_Space;
A1: the carrier of product IB = product Carrier IB by YELLOW_1:def 4;
LattPOSet BooleLatt{0} = RelStr(#the carrier of BooleLatt{0}, LattRel(
BooleLatt{0})#) by LATTICE3:def 2;
then
A2: the carrier of BoolePoset{0} = the carrier of BooleLatt{0}
by YELLOW_1:def 2
.= bool {{}} by LATTICE3:def 1
.= {0,1} by CARD_1:49,ZFMISC_1:24;
A3: for i being object st i in dom Carrier IB holds (Carrier IB).i = (Carrier
IS).i
proof
let i be object;
assume i in dom Carrier IB;
then
A4: i in I;
then consider R1 being 1-sorted such that
A5: R1 = IB.i and
A6: (Carrier IB).i = the carrier of R1 by PRALG_1:def 15;
consider R2 being 1-sorted such that
A7: R2 = IS.i and
A8: (Carrier IS).i = the carrier of R2 by A4,PRALG_1:def 15;
the carrier of R1 = {0,1} by A2,A4,A5,FUNCOP_1:7
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A4,A7,FUNCOP_1:7;
hence thesis by A6,A8;
end;
reconsider P = the set of all
product ((Carrier IS)+*(ii,{1})) where ii is Element of I
as prebasis of product (I --> Sierpinski_Space) by Th13;
let T be Scott TopAugmentation of product (I --> BoolePoset {0});
A9: dom Carrier IB = I by PARTFUN1:def 2
.= dom Carrier IS by PARTFUN1:def 2;
reconsider T9 = T as complete Scott TopLattice;
A10: the RelStr of T = product (I --> BoolePoset {0}) by YELLOW_9:def 4;
then T9 is algebraic by WAYBEL_8:17;
then consider R being Basis of T9 such that
A11: R = {uparrow yy where yy is Element of T9 : yy in the carrier of
CompactSublatt T9} by WAYBEL14:42;
A12: the carrier of T = product Carrier (I --> BoolePoset {0}) by A10,
YELLOW_1:def 4
.= product Carrier (I --> Sierpinski_Space) by A9,A3,FUNCT_1:2
.= the carrier of product (I --> Sierpinski_Space) by Def3;
then reconsider P9 = P as Subset-Family of T;
consider f being Function of BoolePoset I, product IB such that
A13: f is isomorphic and
A14: for Y being Subset of I holds f.Y = chi(Y,I) by Th14;
A15: Carrier IB = Carrier IS by A9,A3,FUNCT_1:2;
A16: FinMeetCl P c= R
proof
deffunc F(object) = product ((Carrier IS)+*($1,{1}));
let X be object;
consider F being Function such that
A17: dom F = I and
A18: for e being object st e in I holds F.e = F(e) from FUNCT_1:sch 3;
assume
A19: X in FinMeetCl P;
then reconsider X9 = X as Subset of product IS;
consider ZZ being Subset-Family of product IS such that
A20: ZZ c= P and
A21: ZZ is finite and
A22: X = Intersect ZZ by A19,CANTOR_1:def 3;
P c= rng F
proof
let w be object;
assume w in P;
then consider e being Element of I such that
A23: w = product ((Carrier IS)+*(e,{1}));
w = F.e by A18,A23;
hence thesis by A17,FUNCT_1:def 3;
end;
then ZZ c= rng F by A20;
then consider x9 being set such that
A24: x9 c= dom F and
A25: x9 is finite and
A26: F.:x9 = ZZ by A21,ORDERS_1:85;
reconsider x9 as Subset of I by A17,A24;
reconsider x = x9 as Element of BoolePoset I by WAYBEL_8:26;
reconsider y = f.x as Element of product IB;
set PP = {product ((Carrier IS)+*(i,{1})) where i is Element of I: i in x9
};
A27: ZZ c= PP
proof
let w be object;
assume w in ZZ;
then consider e being object such that
A28: e in dom F and
A29: e in x9 and
A30: w = F.e by A26,FUNCT_1:def 6;
reconsider e as Element of I by A17,A28;
w = product ((Carrier IS)+*(e,{1})) by A18,A30;
hence thesis by A29;
end;
PP c= ZZ
proof
let w be object;
assume w in PP;
then consider e being Element of I such that
A31: w = product ((Carrier IS)+*(e,{1})) and
A32: e in x9;
w = F.e by A18,A31;
hence thesis by A17,A26,A32,FUNCT_1:def 6;
end;
then
A33: ZZ = PP by A27;
A34: uparrow y c= X9
proof
let z be object;
assume
A35: z in uparrow y;
then reconsider z9 = z as Element of product IB;
y <= z9 by A35,WAYBEL_0:18;
then consider h1,h2 being Function such that
A36: h1 = y and
A37: h2 = z9 and
A38: for i be object st i in I ex R being RelStr, xi,yi being Element
of R st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi by A1,YELLOW_1:def 4;
z in the carrier of product IB by A35;
then z in product Carrier IB by YELLOW_1:def 4;
then
A39: ex gg being Function st z = gg & dom gg = dom (Carrier IB) & for w
being object st w in dom (Carrier IB) holds gg.w in (Carrier IB).w
by CARD_3:def 5;
A40: h1 = chi(x,I) by A14,A36;
for Z being set st Z in ZZ holds z in Z
proof
let Z be set;
assume Z in ZZ;
then consider j being Element of I such that
A41: Z = product ((Carrier IS)+*(j,{1})) and
A42: j in x by A33;
consider RS being RelStr, xj,yj being Element of RS such that
A43: RS = IB.j and
A44: xj = h1.j and
A45: yj = h2.j and
A46: xj <= yj by A38;
A47: RS = BoolePoset {0} by A43;
A48: xj = 1 by A40,A42,A44,FUNCT_3:def 3;
A49: yj <> 0
proof
assume yj = 0;
then {0} c= 0 by A46,A48,A47,YELLOW_1:2,CARD_1:49;
hence thesis;
end;
reconsider b = yj as Element of BoolePoset {0} by A43;
A50: dom ((Carrier IS)+*(j,{1})) = dom (Carrier IS) by FUNCT_7:30
.= I by PARTFUN1:def 2;
A51: b in the carrier of BoolePoset {0};
A52: for w being object st w in dom ((Carrier IS)+*(j,{1})) holds h2.w
in ((Carrier IS)+*(j,{1})).w
proof
let w be object;
assume w in dom ((Carrier IS)+*(j,{1}));
then
A53: w in dom Carrier IS by A50,PARTFUN1:def 2;
per cases;
suppose
w = j;
then ((Carrier IS)+*(j,{1})).w = {1} & h2.w = 1 by A2,A45,A51,A49
,A53,FUNCT_7:31,TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
suppose
w <> j;
then ((Carrier IS)+*(j,{1})).w =(Carrier IS).w by FUNCT_7:32;
hence thesis by A15,A39,A37,A53;
end;
end;
dom h2 = dom ((Carrier IS)+*(j,{1})) by A39,A37,A50,PARTFUN1:def 2;
hence thesis by A37,A41,A52,CARD_3:def 5;
end;
hence thesis by A10,A12,A22,A35,SETFAM_1:43;
end;
A54: X9 c= uparrow y
proof
set h1 = chi(x,I);
let z be object;
assume
A55: z in X9;
then reconsider z9 = z as Element of product IB by A10,A12;
z in the carrier of product IB by A10,A12,A55;
then z in product Carrier IB by YELLOW_1:def 4;
then consider h2 being Function such that
A56: z = h2 and
dom h2 = dom (Carrier IB) and
A57: for w being object st w in dom (Carrier IB) holds h2.w in (
Carrier IB).w by CARD_3:def 5;
A58: for i be object st i in I ex R being RelStr, xi,yi being Element of R
st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi
proof
let i be object;
assume
A59: i in I;
then reconsider i9 = i as Element of I;
ex RB being 1-sorted st RB = IB.i & (Carrier IB).i = the carrier
of RB by A59,PRALG_1:def 15;
then
A60: (Carrier IB).i = {0,1} by A2,A59,FUNCOP_1:7;
take RS = BoolePoset {0};
A61: i in dom (Carrier IB) by A59,PARTFUN1:def 2;
then
A62: h2.i in (Carrier IB).i by A57;
per cases;
suppose
A63: i in x;
reconsider xi = 1, yi = 1 as Element of RS by A2,TARSKI:def 2;
take xi,yi;
thus RS = IB.i by A59,FUNCOP_1:7;
thus xi = h1.i by A63,FUNCT_3:def 3;
A64: ((Carrier IS)+*(i9,{1})).i9 = {1} by A9,A61,FUNCT_7:31;
product ((Carrier IS)+*(i9,{1})) in ZZ by A33,A63;
then z in product ((Carrier IS)+*(i9,{1})) by A22,A55,SETFAM_1:43;
then consider h29 being Function such that
A65: z = h29 and
dom h29 = dom ((Carrier IS)+*(i9,{1})) and
A66: for w being object st w in dom ((Carrier IS)+*(i9,{1})) holds
h29.w in ((Carrier IS)+*(i9,{1})).w by CARD_3:def 5;
i9 in dom ((Carrier IS)+*(i9,{1})) by A9,A61,FUNCT_7:30;
then h29.i9 in ((Carrier IS)+*(i9,{1})).i9 by A66;
hence yi = h2.i by A56,A65,A64,TARSKI:def 1;
thus xi <= yi;
end;
suppose
A67: not i in x;
thus thesis
proof
per cases by A60,A62,TARSKI:def 2;
suppose
A68: h2.i = 0;
reconsider xi = 0, yi = 0 as Element of RS by A2,TARSKI:def 2;
take xi,yi;
thus RS = IB.i by A59,FUNCOP_1:7;
thus xi = h1.i by A59,A67,FUNCT_3:def 3;
thus yi = h2.i by A68;
thus xi <= yi;
end;
suppose
A69: h2.i = 1;
reconsider xi = 0, yi = 1 as Element of RS by A2,TARSKI:def 2;
take xi,yi;
thus RS = IB.i by A59,FUNCOP_1:7;
thus xi = h1.i by A59,A67,FUNCT_3:def 3;
thus yi = h2.i by A69;
xi c= yi;
hence xi <= yi by YELLOW_1:2;
end;
end;
end;
end;
h1 = y by A14;
then y <= z9 by A1,A56,A58,YELLOW_1:def 4;
hence thesis by WAYBEL_0:18;
end;
reconsider Y = y as Element of T9 by A10;
x is compact by A25,WAYBEL_8:28;
then y is compact by A13,WAYBEL13:28;
then Y is compact by A10,WAYBEL_8:9;
then
A70: Y in the carrier of CompactSublatt T9 by WAYBEL_8:def 1;
uparrow Y = uparrow {Y} by WAYBEL_0:def 18
.= uparrow {y} by A10,WAYBEL_0:13
.= uparrow y by WAYBEL_0:def 18;
then X = uparrow Y by A54,A34,XBOOLE_0:def 10;
hence thesis by A11,A70;
end;
A71: rng f = the carrier of product IB by A13,WAYBEL_0:66;
R c= FinMeetCl P
proof
deffunc F(Element of I) = product ((Carrier IS)+*($1,{1}));
let X be object;
assume
A72: X in R;
then consider Y being Element of T9 such that
A73: X = uparrow Y and
A74: Y in the carrier of CompactSublatt T9 by A11;
reconsider X9 = X as Subset of product IS by A12,A72;
reconsider y = Y as Element of product IB by A10;
consider x being object such that
A75: x in dom f and
A76: y = f.x by A71,FUNCT_1:def 3;
reconsider x as Element of BoolePoset I by A75;
Y is compact by A74,WAYBEL_8:def 1;
then y is compact by A10,WAYBEL_8:9;
then x is compact by A13,A76,WAYBEL13:28;
then
A77: x is finite by WAYBEL_8:28;
A78: {F(jj) where jj is Element of I: jj in x} is finite from FRAENKEL:sch
21(A77);
set ZZ = {product ((Carrier IS)+*(jj,{1})) where jj is Element of I: jj in
x };
reconsider x9 = x as Subset of I by WAYBEL_8:26;
A79: ZZ c= P
proof
let z be object;
assume z in ZZ;
then ex j being Element of I st z = product ((Carrier IS)+*(j, {1})) & j
in x9;
hence thesis;
end;
then reconsider ZZ as Subset-Family of product IS by XBOOLE_1:1;
A80: uparrow Y = uparrow {Y} by WAYBEL_0:def 18
.= uparrow {y} by A10,WAYBEL_0:13
.= uparrow y by WAYBEL_0:def 18;
A81: Intersect ZZ c= X9
proof
set h1 = chi(x,I);
let z be object;
assume
A82: z in Intersect ZZ;
then reconsider z9 = z as Element of product IB by A10,A12;
z in the carrier of product IB by A10,A12,A82;
then z in product Carrier IB by YELLOW_1:def 4;
then consider h2 being Function such that
A83: z = h2 and
dom h2 = dom (Carrier IB) and
A84: for w being object st w in dom (Carrier IB) holds h2.w in (Carrier
IB).w by CARD_3:def 5;
A85: for i be object st i in I ex R being RelStr, xi,yi being Element of R
st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi
proof
let i be object;
assume
A86: i in I;
then reconsider i9 = i as Element of I;
ex RB being 1-sorted st RB = IB.i & (Carrier IB).i = the carrier
of RB by A86,PRALG_1:def 15;
then
A87: (Carrier IB).i = {0,1} by A2,A86,FUNCOP_1:7;
take RS = BoolePoset {0};
A88: i in dom (Carrier IB) by A86,PARTFUN1:def 2;
then
A89: h2.i in (Carrier IB).i by A84;
per cases;
suppose
A90: i in x;
reconsider xi = 1, yi = 1 as Element of RS by A2,TARSKI:def 2;
take xi,yi;
thus RS = IB.i by A86,FUNCOP_1:7;
thus xi = h1.i by A86,A90,FUNCT_3:def 3;
A91: ((Carrier IS)+*(i9,{1})).i9 = {1} by A9,A88,FUNCT_7:31;
product ((Carrier IS)+*(i9,{1})) in ZZ by A90;
then z in product ((Carrier IS)+*(i9,{1})) by A82,SETFAM_1:43;
then consider h29 being Function such that
A92: z = h29 and
dom h29 = dom ((Carrier IS)+*(i9,{1})) and
A93: for w being object st w in dom ((Carrier IS)+*(i9,{1})) holds
h29.w in ((Carrier IS)+*(i9,{1})).w by CARD_3:def 5;
i9 in dom ((Carrier IS)+*(i9,{1})) by A9,A88,FUNCT_7:30;
then h29.i9 in ((Carrier IS)+*(i9,{1})).i9 by A93;
hence yi = h2.i by A83,A92,A91,TARSKI:def 1;
thus xi <= yi;
end;
suppose
A94: not i in x;
thus thesis
proof
per cases by A87,A89,TARSKI:def 2;
suppose
A95: h2.i = 0;
reconsider xi = 0, yi = 0 as Element of RS by A2,TARSKI:def 2;
take xi,yi;
thus RS = IB.i by A86,FUNCOP_1:7;
thus xi = h1.i by A86,A94,FUNCT_3:def 3;
thus yi = h2.i by A95;
thus xi <= yi;
end;
suppose
A96: h2.i = 1;
reconsider xi = 0, yi = 1 as Element of RS by A2,TARSKI:def 2;
take xi,yi;
thus RS = IB.i by A86,FUNCOP_1:7;
thus xi = h1.i by A86,A94,FUNCT_3:def 3;
thus yi = h2.i by A96;
xi c= yi;
hence xi <= yi by YELLOW_1:2;
end;
end;
end;
end;
h1 = f.x9 by A14
.= y by A76;
then y <= z9 by A1,A83,A85,YELLOW_1:def 4;
hence thesis by A73,A80,WAYBEL_0:18;
end;
X9 c= Intersect ZZ
proof
let z be object;
assume
A97: z in X9;
then reconsider z9 = z as Element of product IB by A10,A12;
y <= z9 by A73,A80,A97,WAYBEL_0:18;
then consider h1,h2 being Function such that
A98: h1 = y and
A99: h2 = z9 and
A100: for i be object st i in I ex R being RelStr, xi,yi being Element
of R st R = IB.i & xi = h1.i & yi = h2.i & xi <= yi by A1,YELLOW_1:def 4;
z in the carrier of product IB by A10,A12,A97;
then z in product Carrier IB by YELLOW_1:def 4;
then
A101: ex gg being Function st z = gg & dom gg = dom (Carrier IB) & for w
being object st w in dom (Carrier IB) holds gg.w in (Carrier IB).w
by CARD_3:def 5;
A102: h1 = f.x9 by A76,A98
.= chi(x,I) by A14;
for Z being set st Z in ZZ holds z in Z
proof
let Z be set;
assume Z in ZZ;
then consider j being Element of I such that
A103: Z = product ((Carrier IS)+*(j,{1})) and
A104: j in x;
consider RS being RelStr, xj,yj being Element of RS such that
A105: RS = IB.j and
A106: xj = h1.j and
A107: yj = h2.j and
A108: xj <= yj by A100;
reconsider a = xj, b = yj as Element of BoolePoset{0}
by A105;
A109: a <= b by A105,A108;
A110: xj = 1 by A102,A104,A106,FUNCT_3:def 3;
A111: yj <> 0
proof
assume yj = 0;
then {0} c= 0 by A110,A109,YELLOW_1:2,CARD_1:49;
hence thesis;
end;
A112: dom ((Carrier IS)+*(j,{1})) = dom (Carrier IS) by FUNCT_7:30
.= I by PARTFUN1:def 2;
A113: b in the carrier of BoolePoset{0};
A114: for w being object st w in dom ((Carrier IS)+*(j,{1})) holds h2.w in
((Carrier IS)+*(j,{1})).w
proof
let w be object;
assume w in dom ((Carrier IS)+*(j,{1}));
then
A115: w in dom Carrier IS by A112,PARTFUN1:def 2;
per cases;
suppose
w = j;
then
((Carrier IS)+*(j,{1})).w = {1} & h2.w = 1 by A2,A107,A113,A111
,A115,FUNCT_7:31,TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
suppose
w <> j;
then ((Carrier IS)+*(j,{1})).w =(Carrier IS).w by FUNCT_7:32;
hence thesis by A15,A101,A99,A115;
end;
end;
dom h2 = dom ((Carrier IS)+*(j,{1})) by A101,A99,A112,PARTFUN1:def 2;
hence thesis by A99,A103,A114,CARD_3:def 5;
end;
hence thesis by A97,SETFAM_1:43;
end;
then X9 = Intersect ZZ by A81;
hence thesis by A79,A78,CANTOR_1:def 3;
end;
then R = FinMeetCl P by A16;
then P9 is prebasis of T by A12,YELLOW_9:23;
hence thesis by A12,YELLOW_9:26;
end;
theorem Th16:
for T,S being non empty TopSpace st the carrier of T = the
carrier of S & the topology of T = the topology of S & T is injective holds S
is injective
proof
let T,S be non empty TopSpace;
assume that
A1: the carrier of T = the carrier of S and
A2: the topology of T = the topology of S and
A3: T is injective;
let X be non empty TopSpace;
let f be Function of X,S;
reconsider f9 = f as Function of X,T by A1;
A4: [#]S <> {};
assume
A5: f is continuous;
A6: for P being Subset of T st P is open holds (f9)"P is open
proof
let P be Subset of T;
reconsider P9 = P as Subset of S by A1;
assume P is open;
then P9 in the topology of S by A2;
then P9 is open;
hence thesis by A4,A5,TOPS_2:43;
end;
let Y be non empty TopSpace;
assume
A7: X is SubSpace of Y;
A8: [#]T <> {};
then f9 is continuous by A6,TOPS_2:43;
then consider h being Function of Y,T such that
A9: h is continuous and
A10: h|(the carrier of X) = f9 by A3,A7;
reconsider g = h as Function of Y,S by A1;
take g;
for P being Subset of S st P is open holds g"P is open
proof
let P be Subset of S;
reconsider P9 = P as Subset of T by A1;
assume P is open;
then P9 in the topology of T by A2;
then P9 is open;
hence thesis by A8,A9,TOPS_2:43;
end;
hence g is continuous by A4,TOPS_2:43;
thus thesis by A10;
end;
theorem ::p.122 lemma 3.4.(i) part II
for I being non empty set for T being Scott TopAugmentation of product
(I --> BoolePoset{0}) holds T is injective
proof
let I be non empty set, T be Scott TopAugmentation of product (I -->
BoolePoset{0});
set IB = I --> BoolePoset{0}, IS = I --> Sierpinski_Space;
A1: dom Carrier IB = I by PARTFUN1:def 2
.= dom Carrier IS by PARTFUN1:def 2;
A2: the topology of T = the topology of product (I --> Sierpinski_Space) by
Th15;
LattPOSet BooleLatt{0} = RelStr(#the carrier of BooleLatt{0}, LattRel(
BooleLatt{0})#) by LATTICE3:def 2;
then
A3: the carrier of BoolePoset{0} = the carrier of BooleLatt{0}
by YELLOW_1:def 2
.= bool {{}} by LATTICE3:def 1
.= {0,1} by CARD_1:49,ZFMISC_1:24;
A4: for i being object st i in dom Carrier IB holds (Carrier IB).i = (Carrier
IS).i
proof
let i be object;
assume i in dom Carrier IB;
then
A5: i in I;
then consider R1 being 1-sorted such that
A6: R1 = IB.i and
A7: (Carrier IB).i = the carrier of R1 by PRALG_1:def 15;
consider R2 being 1-sorted such that
A8: R2 = IS.i and
A9: (Carrier IS).i = the carrier of R2 by A5,PRALG_1:def 15;
the carrier of R1 = {0,1} by A3,A5,A6,FUNCOP_1:7
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A5,A8,FUNCOP_1:7;
hence thesis by A7,A9;
end;
for i being Element of I holds (I --> Sierpinski_Space).i is injective;
then
A10: product (I --> Sierpinski_Space) is injective by Th7;
the RelStr of T = product (I --> BoolePoset{0}) by YELLOW_9:def 4;
then the carrier of T = product Carrier (I --> BoolePoset{0}) by
YELLOW_1:def 4
.= product Carrier (I --> Sierpinski_Space) by A1,A4,FUNCT_1:2
.= the carrier of product (I --> Sierpinski_Space) by Def3;
hence thesis by A2,A10,Th16;
end;
theorem Th18: ::p.122 lemma 3.4.(ii)
for T being T_0-TopSpace ex M being non empty set, f being
Function of T, product (M --> Sierpinski_Space) st corestr(f) is
being_homeomorphism
proof
let T be T_0-TopSpace;
take M = the carrier of (InclPoset the topology of T);
set J = M --> Sierpinski_Space;
reconsider PP = the set of all
product((Carrier J)+*(m,{1})) where m is Element of M
as prebasis of product J by Th13;
deffunc F(object) =
chi({u where u is Subset of T: $1 in u & u is open}, the topology of T);
consider f being Function such that
A1: dom f = the carrier of T and
A2: for x being object st x in the carrier of T holds f.x = F(x) from
FUNCT_1:sch 3;
rng f c= the carrier of product J
proof
let y be object;
assume y in rng f;
then consider x being object such that
A3: x in dom f & y = f.x by FUNCT_1:def 3;
set ch = chi({u where u is Subset of T: x in u & u is open}, the topology
of T);
A4: dom ch = the topology of T by FUNCT_3:def 3
.= M by YELLOW_1:1
.= dom (Carrier J) by PARTFUN1:def 2;
A5: for z being object st z in dom (Carrier J) holds ch.z in (Carrier J).z
proof
let z be object;
assume z in dom (Carrier J);
then
A6: z in M;
then z in the topology of T by YELLOW_1:1;
then z in dom ch by FUNCT_3:def 3;
then
A7: ch.z in rng ch by FUNCT_1:def 3;
ex R being 1-sorted st R = J.z & (Carrier J).z = the carrier of R by A6,
PRALG_1:def 15;
then (Carrier J).z = the carrier of Sierpinski_Space by A6,FUNCOP_1:7
.= {0,1} by Def9;
hence thesis by A7;
end;
y = ch by A1,A2,A3;
then y in product Carrier J by A4,A5,CARD_3:def 5;
hence thesis by Def3;
end;
then reconsider f as Function of T, product J by A1,FUNCT_2:def 1,RELSET_1:4;
take f;
A8: rng (corestr f) = [#](Image f) by FUNCT_2:def 3;
for A being Subset of product J st A in PP holds f"A is open
proof
{1} c= {0,1} by ZFMISC_1:7;
then reconsider V = {1} as Subset of Sierpinski_Space by Def9;
let A be Subset of product J;
reconsider a = A as Subset of product Carrier J by Def3;
assume A in PP;
then consider i being Element of M such that
A9: a = product ((Carrier J) +* (i,{1}));
A10: i in M;
then
A11: i in the topology of T by YELLOW_1:1;
then reconsider i9 = i as Subset of T;
A12: i in dom (Carrier J) by A10,PARTFUN1:def 2;
A13: i c= f"A
proof
let z be object;
assume
A14: z in i;
set W = {u where u is Subset of T: z in u & u is open};
i9 is open by A11;
then
A15: i in W by A14;
A16: for w being object st w in dom ((Carrier J) +* (i,V)) holds chi(W,the
topology of T).w in ((Carrier J) +* (i,V)).w
proof
let w be object;
assume w in dom ((Carrier J) +* (i,V));
then w in dom (Carrier J) by FUNCT_7:30;
then
A17: w in M;
then w in the topology of T by YELLOW_1:1;
then
A18: w in dom chi(W,the topology of T) by FUNCT_3:def 3;
per cases;
suppose
w = i;
then
((Carrier J) +* (i,V)).w = {1} & chi(W,the topology of T).w = 1
by A11,A12,A15,FUNCT_3:def 3,FUNCT_7:31;
hence thesis by TARSKI:def 1;
end;
suppose
A19: w <> i;
A20: chi(W,the topology of T).w in rng chi(W,the topology of T ) by A18,
FUNCT_1:def 3;
ex r being 1-sorted st r = J.w & (Carrier J).w = the carrier of
r by A17,PRALG_1:def 15;
then
A21: (Carrier J).w = the carrier of Sierpinski_Space by A17,FUNCOP_1:7
.= {0,1} by Def9;
((Carrier J) +* (i,V)).w = (Carrier J).w by A19,FUNCT_7:32;
hence thesis by A21,A20;
end;
end;
A22: dom chi(W,the topology of T) = the topology of T by FUNCT_3:def 3
.= M by YELLOW_1:1
.= dom (Carrier J) by PARTFUN1:def 2
.= dom ((Carrier J) +* (i,V)) by FUNCT_7:30;
A23: z in i9 by A14;
then f.z = chi(W,the topology of T) by A2;
then f.z in A by A9,A22,A16,CARD_3:def 5;
hence thesis by A1,A23,FUNCT_1:def 7;
end;
A24: ((Carrier J)+*(i,V)).i = {1} by A12,FUNCT_7:31;
f"A c= i
proof
let z be object;
set W = {u where u is Subset of T: z in u & u is open};
assume z in f"A;
then f.z in a & f.z = chi(W,the topology of T) by A2,FUNCT_1:def 7;
then consider g being Function such that
A25: chi(W,the topology of T) = g and
dom g = dom ((Carrier J) +* (i,V)) and
A26: for w being object st w in dom ((Carrier J) +* (i,V)) holds g.w in
((Carrier J) +* (i,V)).w by A9,CARD_3:def 5;
i in dom ((Carrier J) +* (i,V)) by A12,FUNCT_7:30;
then g.i in ((Carrier J) +* (i,V)).i by A26;
then chi(W,the topology of T).i = 1 by A24,A25,TARSKI:def 1;
then i in W by FUNCT_3:36;
then ex uu being Subset of T st i = uu & z in uu & uu is open;
hence thesis;
end;
then f"A = i by A13;
hence thesis by A11;
end;
then f is continuous by YELLOW_9:36;
then
A27: dom (corestr f) = [#]T & corestr f is continuous by Th10,FUNCT_2:def 1;
A28: corestr f is one-to-one
proof
let x,y be Element of T;
set U1 = {u where u is Subset of T: x in u & u is open};
set U2 = {u where u is Subset of T: y in u & u is open};
assume
A29: (corestr f).x = (corestr f).y;
thus x = y
proof
A30: f.x = chi(U1,the topology of T) & f.y = chi(U2,the topology of T) by A2;
assume not thesis;
then consider V being Subset of T such that
A31: V is open and
A32: x in V & not y in V or y in V & not x in V by T_0TOPSP:def 7;
A33: V in the topology of T by A31;
per cases by A32;
suppose
A34: x in V & not y in V;
reconsider v = V as Subset of T;
A35: not v in U2
proof
assume not thesis;
then ex u being Subset of T st u = v & y in u & u is open;
hence thesis by A34;
end;
v in U1 by A31,A34;
then chi(U1,the topology of T).v = 1 by A33,FUNCT_3:def 3;
hence thesis by A29,A30,A33,A35,FUNCT_3:def 3;
end;
suppose
A36: y in V & not x in V;
reconsider v = V as Subset of T;
A37: not v in U1
proof
assume not thesis;
then ex u being Subset of T st u = v & x in u & u is open;
hence thesis by A36;
end;
v in U2 by A31,A36;
then chi(U2,the topology of T).v = 1 by A33,FUNCT_3:def 3;
hence thesis by A29,A30,A33,A37,FUNCT_3:def 3;
end;
end;
end;
A38: for V being Subset of T st V is open holds f.:V = product ((Carrier J)
+* (V,{1})) /\ the carrier of Image f
proof
let V be Subset of T;
assume
A39: V is open;
hereby
let y be object;
assume y in f.:V;
then consider x being object such that
A40: x in dom f and
A41: x in V and
A42: y = f.x by FUNCT_1:def 6;
y in rng f by A40,A42,FUNCT_1:def 3;
then
A43: y in the carrier of Image f by Th9;
set Q = {u where u is Subset of T: x in u & u is open};
A44: V in Q by A39,A41;
A45: for W being object st W in dom ((Carrier J) +* (V,{1})) holds chi(Q,
the topology of T).W in ((Carrier J) +* (V,{1})).W
proof
let W be object;
assume W in dom ((Carrier J) +* (V,{1}));
then
A46: W in dom (Carrier J) by FUNCT_7:30;
then
A47: W in M;
then
A48: W in the topology of T by YELLOW_1:1;
then
A49: W in dom chi(Q,the topology of T) by FUNCT_3:def 3;
per cases;
suppose
W = V;
then
((Carrier J) +* (V,{1})).W = {1} & chi(Q,the topology of T).W =
1 by A44,A46,A48,FUNCT_3:def 3,FUNCT_7:31;
hence thesis by TARSKI:def 1;
end;
suppose
A50: W <> V;
A51: chi(Q,the topology of T).W in rng chi(Q,the topology of T) by A49,
FUNCT_1:def 3;
ex r being 1-sorted st r = J.W & (Carrier J).W = the carrier of
r by A47,PRALG_1:def 15;
then
A52: (Carrier J).W = the carrier of Sierpinski_Space by A47,FUNCOP_1:7
.= {0,1} by Def9;
((Carrier J) +* (V,{1})).W = (Carrier J).W by A50,FUNCT_7:32;
hence thesis by A52,A51;
end;
end;
A53: dom chi(Q,the topology of T) = the topology of T by FUNCT_3:def 3
.= M by YELLOW_1:1
.= dom Carrier J by PARTFUN1:def 2
.= dom ((Carrier J) +* (V,{1})) by FUNCT_7:30;
y = chi(Q,the topology of T) by A2,A40,A42;
then y in product ((Carrier J) +* (V,{1})) by A53,A45,CARD_3:def 5;
hence y in product ((Carrier J) +* (V,{1})) /\ the carrier of Image f by
A43,XBOOLE_0:def 4;
end;
let y be object;
assume
A54: y in product ((Carrier J) +* (V,{1})) /\ the carrier of Image f;
then y in product ((Carrier J) +* (V,{1})) by XBOOLE_0:def 4;
then consider g being Function such that
A55: y = g and
dom g = dom ((Carrier J) +* (V,{1})) and
A56: for W being object st W in dom ((Carrier J) +* (V,{1})) holds g.W
in ((Carrier J) +* (V,{1})).W by CARD_3:def 5;
rng f = the carrier of Image f by Th9;
then y in rng f by A54,XBOOLE_0:def 4;
then consider x being object such that
A57: x in dom f & y = f.x by FUNCT_1:def 3;
V in the topology of T by A39;
then V in M by YELLOW_1:1;
then
A58: V in dom (Carrier J) by PARTFUN1:def 2;
then V in dom ((Carrier J) +* (V,{1})) by FUNCT_7:30;
then g.V in ((Carrier J) +* (V,{1})).V by A56;
then
A59: g.V in {1} by A58,FUNCT_7:31;
set Q = {u where u is Subset of T: x in u & u is open};
y = chi(Q,the topology of T) by A2,A57;
then chi(Q,the topology of T).V = 1 by A55,A59,TARSKI:def 1;
then V in Q by FUNCT_3:36;
then ex u being Subset of T st u = V & x in u & u is open;
hence thesis by A57,FUNCT_1:def 6;
end;
A60: for V being Subset of T st V is open holds ((corestr f)")"V is open
proof
let V be Subset of T;
A61: PP c= the topology of product J by TOPS_2:64;
assume
A62: V is open;
then V in the topology of T;
then reconsider W = V as Element of M by YELLOW_1:1;
A63: product((Carrier J)+*(W,{1})) in PP;
then reconsider Q = product((Carrier J)+*(V,{1})) as Subset of product J;
(corestr f).:V = Q /\ [#](Image f) by A38,A62;
then (corestr f).: V in the topology of Image f by A63,A61,PRE_TOPC:def 4;
then (corestr f).:V is open;
hence thesis by A8,A28,TOPS_2:54;
end;
[#]T <> {};
then (corestr f)" is continuous by A60,TOPS_2:43;
hence thesis by A8,A28,A27,TOPS_2:def 5;
end;
theorem ::p.122 lemma 3.4.(iii)
for T being T_0-TopSpace st T is injective ex M being non empty set st
T is_Retract_of product (M --> Sierpinski_Space)
proof
let T be T_0-TopSpace;
assume
A1: T is injective;
ex M being non empty set, f being Function of T, product (M -->
Sierpinski_Space) st corestr(f) is being_homeomorphism by Th18;
hence thesis by A1,Th11;
end;