Copyright (c) 1998 Association of Mizar Users
environ
vocabulary BOOLE, FUNCT_1, RELAT_1, SETFAM_1, CANTOR_1, TARSKI, PRE_TOPC,
PRALG_1, PBOOLE, FUNCOP_1, WAYBEL_3, CARD_3, RLVECT_2, FUNCT_4, BORSUK_1,
ORDINAL2, FUNCTOR0, PARTFUN1, FUNCT_6, FUNCT_3, GROUP_6, SUBSET_1,
WAYBEL_1, SGRAPH1, T_0TOPSP, TOPS_2, METRIC_1, RELAT_2, ORDERS_1,
WAYBEL11, YELLOW_9, YELLOW_1, LATTICE3, FILTER_1, WAYBEL_0, QUANTAL1,
YELLOW_0, FINSET_1, BHSP_3, WAYBEL_8, LATTICES, CAT_1, WAYBEL_9,
COMPTS_1, WAYBEL18, RLVECT_3;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
T_0TOPSP, STRUCT_0, FUNCT_1, FUNCT_2, PRE_TOPC, FUNCT_3, FUNCT_6,
FUNCT_7, PBOOLE, CARD_3, PRALG_1, ORDERS_1, LATTICE3, YELLOW_1, PRE_CIRC,
CANTOR_1, FINSET_1, PRALG_3, TOPS_2, BORSUK_1, TMAP_1, GRCAT_1, YELLOW_0,
YELLOW_2, YELLOW_9, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11;
constructors PRALG_3, CANTOR_1, WAYBEL_1, WAYBEL_3, ENUMSET1, T_0TOPSP,
GRCAT_1, TOPS_2, FUNCT_7, WAYBEL_8, WAYBEL11, TMAP_1, WAYBEL_5, YELLOW_9,
LATTICE3, BORSUK_1;
clusters STRUCT_0, PRE_TOPC, FUNCT_1, LATTICE3, YELLOW_1, WAYBEL_0, WAYBEL_3,
WAYBEL_8, WAYBEL11, YELLOW_9, FUNCOP_1, RELSET_1, SUBSET_1, BORSUK_1,
XBOOLE_0;
requirements SUBSET, BOOLE;
definitions STRUCT_0, TARSKI, PRE_TOPC, PRALG_1, WAYBEL_1, WAYBEL_3, 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, PBOOLE,
CANTOR_1, LATTICE3, ORDERS_1, MSSUBFAM, COMPTS_1, PRALG_1, CARD_3,
CARD_5, STRUCT_0, WAYBEL_3, PRALG_3, FUNCT_6, FUNCT_7, EXTENS_1, TMAP_1,
GRCAT_1, YELLOW_9, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1, WAYBEL_7,
WAYBEL_8, WAYBEL11, WAYBEL13, WAYBEL14, RELSET_1, SETFAM_1, XBOOLE_0,
XBOOLE_1;
schemes SETFAM_1, ZFREFLE1, FUNCT_1, FRAENKEL;
begin :: Preliminaries
theorem Th1:
for x,y,z,Z being set holds
Z c= {x,y,z} iff Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or
Z = {y,z} or Z = {x,z} or Z = {x,y,z}
proof
let x,y,z,Z be set; hereby assume that
A1: Z c= {x,y,z} and A2: Z <> {} and A3: Z <> {x} and A4: Z <> {y} and
A5: Z <> {z} and A6: Z <> {x,y} and A7: Z <> {y,z} and A8: Z <> {x,z};
{x,y,z} c= Z
proof
let a be set; assume
A9: a in {x,y,z};
A10: now assume not x in Z;
then A11: Z c= {x,y,z} \ {x} by A1,ZFMISC_1:40;
{x,y,z} \ {x} = ({x} \/ {y,z}) \ {x} by ENUMSET1:42
.= {y,z} \ {x} by XBOOLE_1:40;
then {x,y,z} \ {x} c= {y,z} by XBOOLE_1:36;
then Z c= {y,z} by A11,XBOOLE_1:1;
hence contradiction by A2,A4,A5,A7,ZFMISC_1:42;
end;
A12: now assume not y in Z;
then A13: Z c= {x,y,z} \ {y} by A1,ZFMISC_1:40;
{x,y,z} \ {y} = ({x,y} \/ {z}) \ {y} by ENUMSET1:43
.= ({x} \/ {y} \/ {z}) \ {y} by ENUMSET1:41
.= ({x} \/ {z} \/ {y}) \ {y} by XBOOLE_1:4
.= ({x,z} \/ {y}) \ {y} by ENUMSET1:41
.= {x,z} \ {y} by XBOOLE_1:40;
then {x,y,z} \ {y} c= {x,z} by XBOOLE_1:36;
then Z c= {x,z} by A13,XBOOLE_1:1;
hence contradiction by A2,A3,A5,A8,ZFMISC_1:42;
end;
now assume not z in Z;
then A14: Z c= {x,y,z} \ {z} by A1,ZFMISC_1:40;
{x,y,z} \ {z} = ({x,y} \/ {z}) \ {z} by ENUMSET1:43
.= {x,y} \ {z} by XBOOLE_1:40;
then {x,y,z} \ {z} c= {x,y} by XBOOLE_1:36;
then Z c= {x,y} by A14,XBOOLE_1:1;
hence contradiction by A2,A3,A4,A6,ZFMISC_1:42;
end;
hence thesis by A9,A10,A12,ENUMSET1:13;
end;
hence Z = {x,y,z} by A1,XBOOLE_0:def 10;
end;
assume A15: Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or
Z = {y,z} or Z = {x,z} or Z = {x,y,z};
per cases by A15;
suppose Z = {}; hence Z c= {x,y,z} by XBOOLE_1:2;
suppose Z = {x}; then Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:42;
suppose Z = {y}; then A16: Z c= {x,y} by ZFMISC_1:12;
{x,y} c= {x,y} \/ {z} by XBOOLE_1:7; then {x,y} c= {x,y,z} by ENUMSET1:
43
;
hence Z c= {x,y,z} by A16,XBOOLE_1:1;
suppose Z = {z}; then Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:43;
suppose Z = {x,y}; then Z c= {x,y} \/ {z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:43;
suppose Z = {y,z}; then Z c= {x} \/ {y,z} by XBOOLE_1:7;
hence Z c= {x,y,z} by ENUMSET1:42;
suppose Z = {x,z}; then A17: Z c= {x,z} \/ {y} by XBOOLE_1:7
; {x,z} \/ {y} =
{x} \/ {z} \/ {y} by ENUMSET1:41 .=
{x} \/ ({y} \/ {z}) by XBOOLE_1:4 .= {x} \/ {y,z} by ENUMSET1:41;
hence Z c= {x,y,z} by A17,ENUMSET1:42;
suppose Z = {x,y,z}; hence Z c= {x,y,z};
end;
Lm1:
for X being set for f,g being Function holds f"(g"X) = (g*f)"X
proof let X be set; let f,g be Function;
A1: f"(g"X) c= (g*f)"X
proof let x be set; assume
A2: x in f"(g"X);
then A3: x in dom f by FUNCT_1:def 13;
A4: f.x in g"X by A2,FUNCT_1:def 13;
then A5: f.x in dom g by FUNCT_1:def 13;
A6: g.(f.x) in X by A4,FUNCT_1:def 13;
A7: x in dom (g*f) by A3,A5,FUNCT_1:21;
(g*f).x in X by A3,A6,FUNCT_1:23;
hence x in (g*f)"X by A7,FUNCT_1:def 13;
end;
(g*f)"X c= f"(g"X)
proof let x be set; assume
A8: x in (g*f)"X;
then A9: x in dom (g*f) by FUNCT_1:def 13;
(g*f).x in X by A8,FUNCT_1:def 13;
then A10: g.(f.x) in X by A9,FUNCT_1:22;
f.x in dom g by A9,FUNCT_1:21;
then A11: f.x in g"X by A10,FUNCT_1:def 13;
dom (g*f) c= dom f by RELAT_1:44;
hence x in f"(g"X) by A9,A11,FUNCT_1:def 13;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th2:
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 \/ {{}};
then B c= A by XBOOLE_1:7,36;
then A2: UniCl B c= UniCl A by CANTOR_1:9;
UniCl A c= UniCl B
proof let x be set; 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 set; assume
A6: w in Y \ {{}};
per cases by A1;
suppose A7: B = A \ {{}};
w in Y & not w in {{}} by A6,XBOOLE_0:def 4;
hence w in B by A3,A7,XBOOLE_0:def 4;
suppose A8: A = B \/ {{}};
w in Y & not w in {{}} by A6,XBOOLE_0:def 4;
hence w in B by A3,A8,XBOOLE_0:def 2;
end;
then Y \ {{}} c= bool X by XBOOLE_1:1;
then reconsider Z = Y \ {{}} as Subset-Family of X by SETFAM_1:def 7;
Z \/ {{}} = Y \/ {{}} by XBOOLE_1:39;
then union (Z \/ {{}}) =
union Y \/ union {{}} by ZFMISC_1:96 .= union Y \/ {} by ZFMISC_1:31
.= union Y;
then x = union Z \/ union {{}} by A4,ZFMISC_1:96
.= union Z \/ {} by ZFMISC_1:31 .= union Z;
hence x in UniCl B by A5,CANTOR_1:def 1;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th3:
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;
A1: K \ {{}} c= K by XBOOLE_1:36;
then reconsider K' = K \ {{}} as Subset-Family of T by TOPS_2:3;
hereby assume
A2: K is Basis of T;
then A3: K c= the topology of T by CANTOR_1:def 2;
A4: the topology of T c= UniCl K by A2,CANTOR_1:def 2;
A5: K \ {{}} c= the topology of T by A1,A3,XBOOLE_1:1;
the topology of T c= UniCl K' by A4,Th2;
hence K \ {{}} is Basis of T by A5,CANTOR_1:def 2;
end; assume
A6: K \ {{}} is Basis of T;
then A7: K' c= the topology of T by CANTOR_1:def 2;
A8: the topology of T c= UniCl K' by A6,CANTOR_1:def 2;
A9: K c= the topology of T
proof let x be set; assume
A10: x in K;
per cases;
suppose x = {};
hence x in the topology of T by PRE_TOPC:5;
suppose x <> {};
then not x in {{}} by TARSKI:def 1;
then x in K' by A10,XBOOLE_0:def 4;
hence x in the topology of T by A7;
end;
UniCl K' c= UniCl K by A1,CANTOR_1:9;
then the topology of T c= UniCl K by A8,XBOOLE_1:1;
hence K is Basis of T by A9,CANTOR_1:def 2;
end;
definition let F be Relation;
attr F is TopSpace-yielding means :Def1:
for x being set st x in rng F holds x is TopStruct;
end;
definition
cluster TopSpace-yielding -> 1-sorted-yielding Function;
coherence
proof let F be Function such that
A1: F is TopSpace-yielding;
let x be set;
assume x in dom F;
then F.x in rng F by FUNCT_1:def 5;
hence F.x is 1-sorted by A1,Def1;
end;
end;
definition let I be set;
cluster TopSpace-yielding ManySortedSet of I;
existence
proof consider T being TopSpace;
take I --> T;
let v be set;
A1: rng(I --> T) c= {T} by FUNCOP_1:19;
assume v in rng(I --> T);
hence thesis by A1,TARSKI:def 1;
end;
end;
definition let I be set;
cluster TopSpace-yielding non-Empty ManySortedSet of I;
existence
proof consider R being non empty TopSpace;
take J = I --> R;
A1: dom J = I & rng J c= {R} by FUNCOP_1:19;
thus J is TopSpace-yielding
proof let x be set; assume
x in rng J;
hence x is TopStruct by A1,TARSKI:def 1;
end;
thus J is non-Empty
proof let S be 1-sorted; assume
S in rng J;
hence thesis by A1,TARSKI:def 1;
end;
end;
end;
definition let J be non empty set;
let A be TopSpace-yielding ManySortedSet of J;
let j be Element of J;
redefine func A.j -> TopStruct;
coherence
proof
dom A = J by PBOOLE:def 3;
then A.j in rng A by FUNCT_1:def 5;
hence thesis by Def1;
end;
end;
definition let I be set; let J be TopSpace-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 SubFamEx;
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:P1 c= P2
proof let x be set; assume A4: x in P1;
then reconsider x' = 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 &
x' = product ((Carrier J) +* (i,V)) by A1,A4;
hence x in P2 by A2;
end;
P2 c= P1
proof let x be set; assume A5: x in P2;
then reconsider x' = 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 &
x' = product ((Carrier J) +* (i,V)) by A2,A5;
hence x in P1 by A1;
end;
hence P1 = P2 by A3,XBOOLE_0:def 10;
end;
end;
theorem Th4:
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#);
A2: the carrier of T in FinMeetCl A by CANTOR_1:8;
FinMeetCl A c= UniCl FinMeetCl A by CANTOR_1:1;
hence A3: the carrier of T in the topology of T by A2;
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,XBOOLE_1:3;
thus for a,b being Subset of T st
a in the topology of T & b in the topology of T
holds a /\ b in the topology of T by A1,A3,XBOOLE_1:3;
suppose X <> {};
hence TopStruct (#X,UniCl FinMeetCl A#) is TopSpace-like by CANTOR_1:17;
end;
definition let I be set;
let J be TopSpace-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,Th4;
take T;
thus the carrier of T = product Carrier J by A1;
now assume {} in rng Carrier J;
then consider i being set such that
A2: i in dom Carrier J & {} = (Carrier J).i by FUNCT_1:def 5;
A3: dom Carrier J = I & dom J = I by PBOOLE:def 3;
then consider R being 1-sorted such that
A4: R = J.i & {} = the carrier of R by A2,PRALG_1:def 13;
R in rng J by A2,A3,A4,FUNCT_1:def 5;
then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A4;
hence contradiction;
end;
then X is non empty by CARD_3:37;
hence product_prebasis J is prebasis of T by A1,CANTOR_1:20;
end;
uniqueness
proof let T1,T2 be strict TopSpace such that
A5: the carrier of T1 = product Carrier J and
A6: product_prebasis J is prebasis of T1 and
A7: the carrier of T2 = product Carrier J and
A8: product_prebasis J is prebasis of T2;
now assume {} in rng Carrier J;
then consider i being set such that
A9: i in dom Carrier J & {} = (Carrier J).i by FUNCT_1:def 5;
A10: dom Carrier J = I & dom J = I by PBOOLE:def 3;
then consider R being 1-sorted such that
A11: R = J.i & {} = the carrier of R by A9,PRALG_1:def 13;
R in rng J by A9,A10,A11,FUNCT_1:def 5;
then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A11;
hence contradiction;
end;
then product Carrier J <> {} by CARD_3:37;
then reconsider t1 = T1, t2 = T2 as non empty TopSpace by A5,A7,STRUCT_0:def
1;
t1 = t2 by A5,A6,A7,A8,CANTOR_1:19;
hence T1 = T2;
end;
end;
definition let I be set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
cluster product J -> non empty;
coherence
proof
A1: the carrier of product J = product Carrier J by Def3;
now assume {} in rng Carrier J;
then consider i being set such that
A2: i in dom Carrier J & {} = (Carrier J).i by FUNCT_1:def 5;
A3: dom Carrier J = I & dom J = I by PBOOLE:def 3;
then consider R being 1-sorted such that
A4: R = J.i & {} = the carrier of R by A2,PRALG_1:def 13;
R in rng J by A2,A3,A4,FUNCT_1:def 5;
then reconsider R as non empty 1-sorted by WAYBEL_3:def 7;
the carrier of R = {} by A4;
hence contradiction;
end;
then the carrier of product J <> {} by A1,CARD_3:37;
hence thesis by STRUCT_0:def 1;
end;
end;
definition let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
redefine func J.i -> non empty TopStruct;
coherence
proof dom J = I by PBOOLE:def 3;
then J.i in rng J by FUNCT_1:def 5;
hence thesis by WAYBEL_3:def 7;
end;
end;
definition let I be set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
cluster -> Function-like Relation-like Element of product J;
coherence
proof let x be Element of product J;
the carrier of product J = product Carrier J by Def3;
then ex g being Function st x = g & dom g = dom Carrier J &
for x being set st x in dom Carrier J holds g.x in (Carrier J).x
by CARD_3:def 5;
hence thesis;
end;
end;
definition
let I be non empty set;
let J be TopSpace-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;
coherence
proof
A1: ex R being 1-sorted st R = J.i & (Carrier J).i = the carrier of R
by PRALG_1:def 13;
the carrier of product J = product Carrier J &
dom Carrier J = I by Def3,PBOOLE:def 3;
then x.i in (Carrier J).i by CARD_3:18;
hence thesis by A1;
end;
end;
definition let I be non empty set;
let J be TopSpace-yielding non-Empty ManySortedSet of I;
let i be Element of I;
func proj(J,i) -> map of product J, J.i equals :Def4:
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,PRALG_3:def 2
.= the carrier of product J by Def3;
rng f c= the carrier of J.i
proof
let y be set; assume y in rng f;
then consider x be set such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 5;
reconsider x as Element of product J by A2,A3;
f.x = x.i by A1,A3,PRALG_3:def 2;
hence y in the carrier of J.i by A4;
end;
then f is Function of the carrier of product J, the carrier of J.i
by A2,FUNCT_2:def 1,RELSET_1:11;
hence thesis by A1;
end;
end;
theorem Th5:
for I being non empty set,
J being TopSpace-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 TopSpace-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 f = dom Carrier J by FUNCT_7:32 .= I by PBOOLE:def 3;
A2: dom Carrier J = I by PBOOLE:def 3;
A3:product f c= proj(J,i)"P
proof let x be set; 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 set st y in dom f holds g.y in f.y by CARD_3:def 5;
f.i = P by A2,FUNCT_7:33;
then A7: g.i in P by A1,A6;
A8: dom g = dom Carrier J by A5,FUNCT_7:32;
for j being set st j in dom Carrier J holds g.j in (Carrier J).j
proof let j be set; assume
j in dom Carrier J;
then A9: j in I by PBOOLE:def 3;
then consider R being 1-sorted such that
A10: R = J.j and
A11: (Carrier J).j = the carrier of R by PRALG_1:def 13;
per cases;
suppose A12: j = i;
f.i = P by A2,FUNCT_7:33;
then g.j in P by A1,A6,A12;
hence g.j in (Carrier J).j by A10,A11,A12;
suppose j <> i;
then f.j = (Carrier J).j by FUNCT_7:34;
hence g.j in (Carrier J).j by A1,A6,A9;
end;
then g in product Carrier J by A8,CARD_3:18;
then A13: g in dom proj(Carrier J,i) by PRALG_3:def 2;
then A14: g in dom proj(J,i) by Def4;
proj(Carrier J,i).g in P by A7,A13,PRALG_3:def 2;
then proj(J,i).g in P by Def4;
hence x in proj(J,i)"P by A4,A14,FUNCT_1:def 13;
end;
proj(J,i)"P c= product f
proof let x be set; assume
x in proj(J,i)"P;
then A15: x in proj(Carrier J,i)"P by Def4;
then A16: x in dom proj(Carrier J,i) by FUNCT_1:def 13;
then x in product Carrier J by PRALG_3:def 2;
then consider g being Function such that
A17: x = g and
A18: dom g = dom Carrier J and
A19: for y being set st y in dom Carrier J holds
g.y in (Carrier J).y by CARD_3:def 5;
A20: dom g = dom f by A18,FUNCT_7:32;
for j being set st j in dom f holds g.j in f.j
proof let j be set; assume
j in dom f;
then A21: g.j in (Carrier J).j by A18,A19,A20;
per cases;
suppose A22: i = j;
proj(Carrier J,i).x = g.i by A16,A17,PRALG_3:def 2;
then g.i in P by A15,FUNCT_1:def 13;
hence g.j in f.j by A2,A22,FUNCT_7:33;
suppose i <> j;
hence g.j in f.j by A21,FUNCT_7:34;
end;
hence x in product f by A17,A20,CARD_3:def 5;
end;
hence proj(J,i)"P = product ((Carrier J) +* (i,P)) by A3,XBOOLE_0:def 10;
end;
theorem Th6:
for I being non empty set,
J being TopSpace-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 TopSpace-yielding non-Empty ManySortedSet of I, i be Element of I;
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
A1: P is open;
proj(J,i)"P c= product Carrier J
proof let x be set; assume
x in proj(J,i)"P;
then x in proj(Carrier J,i)"P by Def4;
then x in dom proj(Carrier J,i) by FUNCT_1:def 13;
hence x in product Carrier J by PRALG_3:def 2;
end;
then reconsider x = proj(J,i)"P as Subset of product Carrier J;
x = product ((Carrier J) +* (i,P)) by Th5;
then A2: proj(J,i)"P in product_prebasis J by A1,Def2;
product_prebasis J is prebasis of product J by Def3;
then product_prebasis J c= the topology of product J by CANTOR_1:def 5;
hence proj(J,i)"P is open by A2,PRE_TOPC:def 5;
end;
hence proj(J,i) is continuous by TOPS_2:55;
end;
theorem Th7:
for X being non empty TopSpace, I being non empty set,
J being TopSpace-yielding non-Empty ManySortedSet of I,
f being map 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 TopSpace-yielding non-Empty ManySortedSet of I,
f be map of X, product J;
hereby assume
A1:f is continuous;
let i be Element of I;
proj(J,i) is continuous by Th6;
hence proj(J,i)*f is continuous by A1,TOPS_2:58;
end;
assume
A2:for i being Element of I holds proj(J,i)*f is continuous;
set B = product_prebasis J;
A3: B is prebasis of product J by Def3;
for P being Subset of product J st P in B holds f"P is open
proof let P be Subset of product J; assume
A4: P in B;
reconsider p = P as Subset of product Carrier J by Def3;
consider i being set, T being TopStruct,
V being Subset of T such that
A5: i in I and
A6: V is open and
A7: T = J.i and
A8: p = product ((Carrier J) +* (i,V)) by A4,Def2;
reconsider j = i as Element of I by A5;
A9: proj(J,j)*f is continuous by A2;
reconsider V as Subset of J.j by A7;
A10: proj(J,j)"V = p by A8,Th5;
(proj(J,j)*f)"V is open by A6,A7,A9,TOPS_2:55;
hence f"P is open by A10,Lm1;
end;
hence f is continuous by A3,YELLOW_9:36;
end;
begin :: Main Part
definition let Z be TopStruct;
attr Z is injective means :Def5: ::p.121 definition 3.1.
for X being non empty TopSpace
for f being map of X, Z st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y
ex g being map of Y,Z st g is continuous & g|(the carrier of X) = f;
end;
theorem Th8: ::p.121 lemma 3.2.(i)
for I being non empty set, J being TopSpace-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 TopSpace-yielding non-Empty ManySortedSet of I;
assume
A1: for i being Element of I holds J.i is injective;
let X be non empty TopSpace;
let f be map of X, product J; assume
A2: f is continuous;
let Y be non empty TopSpace; assume
A3: X is SubSpace of Y;
defpred P[set,set] means
ex i1 being Element of I st i1 = $1 &
ex g being map of Y, J.i1 st g is continuous &
g|(the carrier of X) = proj(J,i1)*f & $2 = g;
A4: for i being set st i in I ex u being set st P[i,u]
proof let i be set; assume i in I;
then reconsider i1 = i as Element of I;
A5: J.i1 is injective by A1;
proj(J,i1)*f is continuous by A2,Th7;
then consider g being map of Y, J.i1 such that
A6: g is continuous and
A7: g|(the carrier of X) = proj(J,i1)*f by A3,A5,Def5;
take g, i1;
thus thesis by A6,A7;
end;
consider G being Function such that
A8:dom G = I and
A9:for i being set st i in I holds P[i,G.i] from NonUniqFuncEx(A4);
A10: dom <:G:> c= the carrier of Y
proof let x be set; assume
A11: x in dom <:G:>;
consider j being set such that
A12: j in I by XBOOLE_0:def 1;
consider i being Element of I such that
i = j and
A13: ex g being map of Y, J.i st g is continuous &
g|(the carrier of X) = proj(J,i)*f & G.j = g by A9,A12;
consider g being map of Y, J.i such that
g is continuous & g|(the carrier of X) = proj(J,i)*f and
A14: G.j = g by A13;
g in rng G by A8,A12,A14,FUNCT_1:def 5;
then x in dom g by A11,FUNCT_6:52;
hence x in the carrier of Y by FUNCT_2:def 1;
end;
the carrier of Y c= dom <:G:>
proof let x be set; assume
A15: x in the carrier of Y;
consider i being set such that
A16: i in I by XBOOLE_0:def 1;
consider j being Element of I such that
j = i and
A17: ex g being map of Y, J.j st g is continuous &
g|(the carrier of X) = proj(J,j)*f & G.i = g by A9,A16;
consider g being map of Y, J.j such that
g is continuous and g|(the carrier of X) = proj(J,j)*f and
A18: G.i = g by A17;
A19: g in rng G by A8,A16,A18,FUNCT_1:def 5;
for f' being Function st f' in rng G holds x in dom f'
proof let f' be Function; assume
f' in rng G;
then consider k being set such that
A20: k in dom G and
A21: f' = G.k by FUNCT_1:def 5;
consider i1 being Element of I such that
i1 = k and
A22: ex ff being map of Y, J.i1 st ff is continuous &
ff|(the carrier of X) = proj(J,i1)*f & G.k = ff by A8,A9,A20;
consider ff being map of Y, J.i1 such that
ff is continuous and ff|(the carrier of X) = proj(J,i1)*f and
A23: G.k = ff by A22;
thus x in dom f' by A15,A21,A23,FUNCT_2:def 1;
end;
hence x in dom <:G:> by A19,FUNCT_6:53;
end;
then A24:dom <:G:> = the carrier of Y by A10,XBOOLE_0:def 10;
A25:G is Function-yielding
proof let j be set; assume j in dom G;
then consider i being Element of I such that
i = j and
A26: ex g being map of Y, J.i st g is continuous &
g|(the carrier of X) = proj(J,i)*f & G.j = g by A8,A9;
consider g being map of Y, J.i such that
g is continuous & g|(the carrier of X) = proj(J,i)*f and
A27: G.j = g by A26;
thus G.j is Function by A27;
end;
A28:product rngs G c= product Carrier J
proof let y be set; assume
y in product rngs G;
then consider h being Function such that
A29: y = h and
A30: dom h = dom rngs G and
A31: for x being set st x in dom rngs G holds h.x in (rngs G).x
by CARD_3:def 5;
A32: dom h = I by A8,A25,A30,EXTENS_1:4
.= dom Carrier J by PBOOLE:def 3;
for x being set st x in dom Carrier J holds h.x in (Carrier J).x
proof let x be set; assume
A33: x in dom Carrier J;
then A34: h.x in (rngs G).x by A30,A31,A32;
A35: x in I by A33,PBOOLE:def 3;
then consider i being Element of I such that
A36: i = x and
A37: ex g being map of Y, J.i st g is continuous &
g|(the carrier of X) = proj(J,i)*f & G.x = g by A9;
consider g being map of Y, J.i such that
g is continuous & g|(the carrier of X) = proj(J,i)*f and
A38: G.x = g by A37;
x in dom G by A8,A33,PBOOLE:def 3;
then A39: (rngs G).x = rng g by A38,FUNCT_6:31;
consider R being 1-sorted such that
A40: R = J.x and
A41: (Carrier J).x = the carrier of R by A35,PRALG_1:def 13;
thus h.x in (Carrier J).x by A34,A36,A39,A40,A41;
end;
hence y in product Carrier J by A29,A32,CARD_3:def 5;
end;
rng <:G:> c= product rngs G by FUNCT_6:49;
then A42:rng <:G:> c= product Carrier J by A28,XBOOLE_1:1;
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 A24,FUNCT_2:def 1,RELSET_1:11;
A43: the carrier of X c= the carrier of Y by A3,BORSUK_1:35;
A44: dom (h|(the carrier of X)) = dom h /\ the carrier of X by RELAT_1:90
.= (the carrier of Y) /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X by A43,XBOOLE_1:28
.= dom f by FUNCT_2:def 1;
A45: for x being set st x in dom (h|(the carrier of X)) holds
(h|(the carrier of X)).x = f.x
proof let x be set; assume
A46: x in dom (h|(the carrier of X));
then A47: x in the carrier of X by A44,FUNCT_2:def 1;
then A48: x in the carrier of Y by A43;
f.x in rng f by A44,A46,FUNCT_1:def 5;
then f.x in the carrier of product J;
then A49: f.x in product Carrier J by Def3;
then consider y being Function such that
A50: f.x = y and
A51: dom y = dom Carrier J and
for i being set st i in dom Carrier J holds
y.i in (Carrier J).i by CARD_3:def 5;
A52: rng (h|(the carrier of X)) c= rng h by FUNCT_1:76;
(h|(the carrier of X)).x in rng (h|(the carrier of X)) by A46,FUNCT_1
:def 5;
then (h|
(the carrier of X)).x in rng h by A52;
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
A53: (h|(the carrier of X)).x = z and
A54: dom z = dom Carrier J and
for i being set st i in dom Carrier J holds
z.i in (Carrier J).i by CARD_3:def 5;
for j being set st j in dom y holds y.j = z.j
proof let j be set; assume
j in dom y;
then A55: j in I by A51,PBOOLE:def 3;
then consider i being Element of I such that
A56: i = j and
A57: ex g being map of Y, J.i st g is continuous &
g|(the carrier of X) = proj(J,i)*f & G.j = g by A9;
consider g being map of Y, J.i such that
g is continuous and
A58: g|(the carrier of X) = proj(J,i)*f and
A59: G.j = g by A57;
A60: x in dom h by A48,FUNCT_2:def 1;
A61: y in dom proj(Carrier J,i) by A49,A50,PRALG_3:def 2;
z = <:G:>.x by A47,A53,FUNCT_1:72;
hence z.j = g.x by A8,A55,A59,A60,FUNCT_6:54
.= (proj(J,i)*f).x by A47,A58,FUNCT_1:72
.= proj(J,i).y by A47,A50,FUNCT_2:21
.= proj(Carrier J,i).y by Def4 .= y.j by A56,A61,PRALG_3:def
2;
end;
hence (h|(the carrier of X)).x = f.x by A50,A51,A53,A54,FUNCT_1:9;
end;
reconsider h as map of Y, product J ;
take h;
set B = product_prebasis J;
A62: B is prebasis of product J by Def3;
for P being Subset of product J st P in B holds h"P is open
proof let P be Subset of product J; assume
A63: P in B;
reconsider p = P as Subset of product Carrier J by Def3;
consider i being set, T being TopStruct,
V being Subset of T such that
A64: i in I and
A65: V is open and
A66: T = J.i and
A67: p = product ((Carrier J) +* (i,V)) by A63,Def2;
consider j being Element of I such that
A68: j = i and
A69: ex g being map of Y, J.j st g is continuous &
g|(the carrier of X) = proj(J,j)*f & G.i = g by A9,A64;
consider g being map of Y, J.j such that
A70: g is continuous and
g|(the carrier of X) = proj(J,j)*f and
A71: G.i = g by A69;
reconsider V as Subset of J.j by A66,A68;
A72: proj(J,j)"V = p by A67,A68,Th5;
A73: g"V is open by A65,A66,A68,A70,TOPS_2:55;
A74: dom g = the carrier of Y by FUNCT_2:def 1 .= dom h by FUNCT_2:def 1;
A75: dom proj(J,j) = dom proj(Carrier J,j) by Def4
.= product Carrier J by PRALG_3:def 2;
A76: h"P c= g"V
proof let x be set; assume
A77: x in h"P;
then A78: x in dom h & h.x in P by FUNCT_1:def 13;
A79: x in dom g by A74,A77,FUNCT_1:def 13;
A80: h.x in proj(J,j)"V by A72,A77,FUNCT_1:def 13;
then A81: h.x in dom proj(J,j) by FUNCT_1:def 13;
h.x in product Carrier J by A75,A80,FUNCT_1:def 13;
then consider y being Function such that
A82: h.x = y and
dom y = dom Carrier J and
for i being set st i in dom Carrier J holds
y.i in (Carrier J).i by CARD_3:def 5;
A83: y in dom proj(Carrier J,j) by A75,A81,A82,PRALG_3:def 2;
proj(J,j).(h.x) = proj(Carrier J,j).y by A82,Def4
.= y.j by A83,PRALG_3:def 2;
then A84: y.j in V by A80,FUNCT_1:def 13;
g.x = y.j by A8,A68,A71,A78,A82,FUNCT_6:54;
hence x in g"V by A79,A84,FUNCT_1:def 13;
end;
g"V c= h"P
proof let x be set; assume
A85: x in g"V;
then A86: x in dom h by A74,FUNCT_1:def 13;
then A87: h.x in rng h by FUNCT_1:def 5;
then A88: h.x in product Carrier J by A42;
consider y being Function such that
A89: h.x = y and
dom y = dom Carrier J and
for i being set st i in dom Carrier J holds
y.i in
(Carrier J).i by A42,A87,CARD_3:def 5;
A90: y in dom proj(Carrier J,j) by A88,A89,PRALG_3:def 2;
A91: proj(J,j).(h.x) = proj(Carrier J,j).y by A89,Def4
.= y.j by A90,PRALG_3:def 2;
g.x = y.j by A8,A68,A71,A86,A89,FUNCT_6:54;
then proj(J,j).(h.x) in V by A85,A91,FUNCT_1:def 13;
then h.x in proj(J,j)"V by A42,A75,A87,FUNCT_1:def 13;
hence x in h"P by A72,A86,FUNCT_1:def 13;
end;
hence h"P is open by A73,A76,XBOOLE_0:def 10;
end;
hence h is continuous by A62,YELLOW_9:36;
thus h|(the carrier of X) = f by A44,A45,FUNCT_1:9;
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; assume
S is_a_retract_of T;
then consider r being continuous map of T,S such that
A2: r is being_a_retraction by BORSUK_1:def 20;
set p = incl S;
A3: p is continuous by TMAP_1:98;
let X be non empty TopSpace, F be map of X, S; assume
A4: F is continuous;
let Y be non empty TopSpace; assume
A5: X is SubSpace of Y;
reconsider f = p*F as map of X,T;
f is continuous by A3,A4,TOPS_2:58;
then consider g be map of Y,T such that
A6: g is continuous and
A7: g|(the carrier of X) = f by A1,A5,Def5;
take G = r*g;
thus G is continuous by A6,TOPS_2:58;
A8: the carrier of X c= the carrier of Y by A5,BORSUK_1:35;
A9: the carrier of S c= the carrier of T by BORSUK_1:35;
A10: dom G /\ the carrier of X
= (the carrier of Y) /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X by A8,XBOOLE_1:28;
A11: dom F = the carrier of X by FUNCT_2:def 1;
for x being set st x in dom F holds F.x = G.x
proof let x be set; assume
A12: x in dom F;
then A13: x in the carrier of X by FUNCT_2:def 1;
A14: F.x in rng F by A12,FUNCT_1:def 5;
then F.x in the carrier of S;
then reconsider y = F.x as Point of T by A9;
A15: F.x = r.y by A2,A14,BORSUK_1:def 19;
A16: f.x = p.y by A13,FUNCT_2:21 .= F.x by A14,TMAP_1:95;
g.x = f.x by A7,A13,FUNCT_1:72;
hence G.x = F.x by A8,A13,A15,A16,FUNCT_2:21;
end;
hence G|(the carrier of X) = F by A10,A11,FUNCT_1:68;
end;
definition let X be 1-sorted, Y be TopStruct, f be map of X,Y;
func Image f -> SubSpace of Y equals :Def6:
Y|(rng f);
coherence;
end;
definition let X be non empty 1-sorted,
Y be non empty TopStruct,
f be map of X,Y;
cluster Image f -> non empty;
coherence
proof
A1:dom f = the carrier of X by FUNCT_2:def 1;
consider x being Element of dom f;
f.x in rng f by A1,FUNCT_1:def 5;
then reconsider A = rng f as non empty Subset of Y;
A2:Image f = Y|A by Def6;
the carrier of Image f = [#]Image f by PRE_TOPC:12
.= A by A2,PRE_TOPC:def 10;
hence the carrier of Image f is non empty;
end;
end;
theorem Th10:
for X being 1-sorted, Y being TopStruct,
f being map of X,Y holds
the carrier of Image f = rng f
proof let X be 1-sorted,Y be TopStruct, f be map of X,Y;
thus the carrier of Image f = [#]Image f by PRE_TOPC:12
.= [#](Y|(rng f)) by Def6 .= rng f by PRE_TOPC:def 10;
end;
definition let X be 1-sorted, Y be non empty TopStruct,
f be map of X,Y;
func corestr(f) -> map of X,Image f equals :Def7:
f;
coherence
proof
A1: the carrier of Image f = rng f by Th10;
then A2: (the carrier of Image f)|f = f & the carrier of X = dom f
by FUNCT_2:def 1,RELAT_1:125;
then (the carrier of Image f)|f
is Function of the carrier of X, the carrier of Image f by A1,FUNCT_2:3;
hence thesis by A2;
end;
end;
theorem Th11:
for X, Y being non empty TopSpace, f being map of X,Y st
f is continuous holds
corestr f is continuous
proof let X, Y be non empty TopSpace; let f be map of X,Y; assume
A1:f is continuous;
A2:f is Function of dom f ,rng f by FUNCT_2:3;
for R being Subset of Image f st R is open holds (corestr f)"R is open
proof let R be Subset of Image f; assume
R is open;
then R in the topology of Image f by PRE_TOPC:def 5;
then consider Q being Subset of Y such that
A3: Q in the topology of Y and
A4: R = Q /\ [#](Image f) by PRE_TOPC:def 9;
reconsider Q as Subset of Y;
Q is open by A3,PRE_TOPC:def 5;
then A5: f"Q is open by A1,TOPS_2:55;
[#](Image f) = the carrier of Image f by PRE_TOPC:12
.= rng f by Th10;
then A6: f"([#](Image f)) = dom f by A2,FUNCT_2:48
.= the carrier of X by FUNCT_2:def 1;
the carrier of X in the topology of X by PRE_TOPC:def 1;
then A7: f"([#](Image f)) is open by A6,PRE_TOPC:def 5;
f"Q /\ f"([#](Image f)) = f"(Q /\ [#](Image f)) by FUNCT_1:137;
then f"(Q /\ [#](Image f)) is open by A5,A7,TOPS_1:38;
hence (corestr f)"R is open by A4,Def7;
end;
hence corestr f is continuous by TOPS_2:55;
end;
definition let X be 1-sorted,Y be non empty TopStruct; let f be map of X,Y;
cluster corestr f -> onto;
coherence
proof
the carrier of Image f = rng f by Th10 .= rng corestr f by Def7;
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 map of Y,Y st f is continuous & f*f = f &
Image f, X are_homeomorphic;
end;
theorem Th12: ::p.121 lemma 3.2.(iii)
for T,S being non empty TopSpace st T is injective
for f being map of T,S st corestr(f) is_homeomorphism holds
T is_Retract_of S
proof let T,S be non empty TopSpace; assume
A1:T is injective;
let f be map of T,S; assume
A2:corestr(f) is_homeomorphism;
then A3:corestr(f) is continuous by TOPS_2:def 5;
consider g being map of Image f, T such that
A4:g = (corestr f)";
g is continuous by A2,A4,TOPS_2:def 5;
then consider h being map of S,T such that
A5:h is continuous and
A6:h|(the carrier of Image f) = g by A1,Def5;
g is_homeomorphism by A2,A4,TOPS_2:70;
then A7:g is one-to-one by TOPS_2:def 5;
reconsider p = incl(Image f) as map of Image f,S;
p is continuous by TMAP_1:98;
then A8:p*(corestr f) is continuous by A3,TOPS_2:58;
A9:dom (p*(corestr f)) = the carrier of T by FUNCT_2:def 1
.= dom f by FUNCT_2:def 1;
take F = f*h;
A10:the carrier of Image f = rng f by Th10;
dom h = the carrier of S & rng h c= the carrier of T by FUNCT_2:def 1;
then A11:rng h c= dom f by FUNCT_2:def 1;
A12:for P being Subset of S holds f"P = (p*(corestr f))"P
proof let P be Subset of S;
hereby let x be set; assume
x in f"P;
then A13: x in dom f & f.x in P by FUNCT_1:def 13;
then f.x in rng f by FUNCT_1:def 5;
then A14: f.x in the carrier of Image f by Th10;
reconsider y = f.x as Point of S by A13;
(p*(corestr f)).x = (p*f).x by Def7 .= p.(f.x) by A13,FUNCT_1:23
.= y by A14,TMAP_1:95;
hence x in (p*(corestr f))"P by A9,A13,FUNCT_1:def 13;
end; let x be set; assume
x in (p*(corestr f))"P;
then A15: x in dom(p*(corestr f)) & (p*(corestr f)).x in P by FUNCT_1:def 13
;
then A16: f.x in rng f by A9,FUNCT_1:def 5;
then A17: f.x in the carrier of Image f by Th10;
reconsider y = f.x as Point of S by A16;
(p*(corestr f)).x = (p*f).x by Def7 .= p.(f.x) by A9,A15,FUNCT_1:23
.= y by A17,TMAP_1:95;
hence x in f"P by A9,A15,FUNCT_1:def 13;
end;
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 A8,TOPS_2:55;
then f"P is open by A12; then h"(f"P) is open by A5,TOPS_2:55;
hence F"P is open by RELAT_1:181;
end;
hence F is continuous by TOPS_2:55;
A18:dom (h*f) = the carrier of T by FUNCT_2:def 1;
for x being set st x in the carrier of T holds (h*f).x = x
proof let x be set; assume
A19: x in the carrier of T;
then A20: x in dom f by FUNCT_2:def 1;
A21: x in dom (corestr f) by A19,FUNCT_2:def 1;
A22: corestr f is one-to-one by A2,TOPS_2:def 5;
A23: rng (corestr f) = the carrier of Image f by FUNCT_2:def 3
.= [#](Image f) by PRE_TOPC:12;
A24: f.x in rng f by A20,FUNCT_1:def 5;
thus (h*f).x = h.(f.x) by A20,FUNCT_1:23
.= ((corestr f)").(f.x) by A4,A6,A10,A24,FUNCT_1:72
.= ((corestr f)").((corestr f).x) by Def7
.= ((corestr f qua Function)").((corestr f).x)
by A22,A23,TOPS_2:def 4
.= x by A21,A22,FUNCT_1:56;
end;
then A25:h*f = id (the carrier of T) by A18,FUNCT_1:34;
thus F*F = (f*h*f)*h by RELAT_1:55 .= f*(h*f)*h by RELAT_1:55
.= f*(id T)*h by A25,GRCAT_1:def 11 .= F by GRCAT_1:12;
A26: rng F c= rng f
proof let y be set; assume
y in rng F;
then consider x being set such that
A27: x in dom F and
A28: y = F.x by FUNCT_1:def 5;
x in the carrier of S by A27,FUNCT_2:def 1;
then A29: x in dom h by FUNCT_2:def 1;
then A30: h.x in rng h by FUNCT_1:def 5;
f.(h.x) = y by A28,A29,FUNCT_1:23;
hence y in rng f by A11,A30,FUNCT_1:def 5;
end;
set H = h*(incl Image F);
A31:dom incl Image F = the carrier of Image F by FUNCT_2:def 1;
A32:dom H = the carrier of Image F by FUNCT_2:def 1
.= [#](Image F) by PRE_TOPC:12;
A33:rng H = [#](T)
proof
hereby
rng H c= the carrier of T;
hence rng H c= [#](T) by PRE_TOPC:12;
end; let y be set; assume
A34: y in [#](T);
then A35: y in the carrier of T;
A36: dom H = the carrier of Image F by A32,PRE_TOPC:12
.= rng F by Th10;
A37: y in dom f by A35,FUNCT_2:def 1;
then A38: f.y in rng f by FUNCT_1:def 5;
then f.y in the carrier of S;
then A39: f.y in dom F by FUNCT_2:def 1;
A40: F.(f.y) = ((f*h)*f).y by A37,FUNCT_1:23 .= (f*(h*f)).y by RELAT_1:55
.= (f*id T).y by A25,GRCAT_1:def 11 .= f.y by GRCAT_1:12;
then A41: f.y in dom H by A36,A39,FUNCT_1:def 5;
reconsider pp = f.y as Point of S by A38;
F.(f.y) in rng F by A39,FUNCT_1:def 5;
then A42: f.y in the carrier of Image F by A40,Th10;
then A43: y in dom((incl Image F)*f) by A31,A37,FUNCT_1:21;
H.(f.y) = ((h*(incl Image F))*f).y by A37,FUNCT_1:23
.= (h*((incl Image F)*f)).y by RELAT_1:55
.= h.(((incl Image F)*f).y) by A43,FUNCT_1:23
.= h.((incl Image F).pp) by A37,FUNCT_1:23
.= h.(f.y) by A42,TMAP_1:95 .= (h*f).y by A37,FUNCT_1:23
.= (id T).y by A25,GRCAT_1:def 11 .= y by A34,GRCAT_1:11;
hence y in rng H by A41,FUNCT_1:def 5;
end;
A44:H is one-to-one
proof let x,y be Element of Image F; assume
A45: H.x = H.y;
A46: x in the carrier of Image F;
then A47: x in rng F by Th10;
A48: x in dom (incl Image F) by A46,FUNCT_2:def 1;
x in rng f by A26,A47;
then A49: x in the carrier of Image f by Th10;
A50: y in the carrier of Image F;
then A51: y in rng F by Th10;
then y in rng f by A26;
then A52: y in the carrier of Image f by Th10;
A53: y in dom (incl Image F) by A50,FUNCT_2:def 1;
reconsider a = x, b = y as Point of S by A47,A51;
reconsider x' = x, y' = y as Element of Image f by A49,A52;
g.x' = h.x by A6,FUNCT_1:72
.= h.((incl Image F).a) by TMAP_1:95
.= (h*(incl Image F)).b by A45,A48,FUNCT_1:23
.= h.((incl Image F).b) by A53,FUNCT_1:23
.= h.y by TMAP_1:95
.= g.y' by A6,FUNCT_1:72;
hence x = y by A7,WAYBEL_1:def 1;
end;
incl Image F is continuous by TMAP_1:98;
then A54:H is continuous by A5,TOPS_2:58;
for P being Subset of Image F st P is open holds (H")"P is open
proof let P be Subset of Image F; assume
P is open;
then P in the topology of Image F by PRE_TOPC:def 5;
then consider Q being Subset of S such that
A55: Q in the topology of S and
A56: P = Q /\ [#](Image F) by PRE_TOPC:def 9;
reconsider Q as Subset of S;
A57: Q is open by A55,PRE_TOPC:def 5;
p is continuous by TMAP_1:98;
then p*(corestr f) is continuous by A3,TOPS_2:58;
then (p*(corestr f))"Q is open by A57,TOPS_2:55;
then A58: f"Q is open by A12;
A59: (incl Image F).:P = P
proof
hereby let y be set; assume
y in (incl Image F).:P;
then consider x being set such that
A60: x in dom (incl Image F) and
A61: x in P and
A62: y = (incl Image F).x by FUNCT_1:def 12;
A63: x in the carrier of Image F by A60,FUNCT_2:def 1;
then x in rng F by Th10;
then reconsider xx = x as Point of S;
(incl Image F).xx = x by A63,TMAP_1:95;
hence y in P by A61,A62;
end; let y be set; assume
A64: y in P;
then A65: y in the carrier of Image F;
then A66: y in dom (incl Image F) by FUNCT_2:def 1;
y in rng F by A65,Th10;
then reconsider yy = y as Point of S;
yy = (incl Image F).y by A64,TMAP_1:95;
hence y in (incl Image F).:P by A64,A66,FUNCT_1:def 12;
end;
A67: f"Q = h.:P
proof
hereby let x be set; assume
A68: x in f"Q;
then A69: x in dom f by FUNCT_1:def 13;
A70: f.x in Q by A68,FUNCT_1:def 13;
f.x in rng f by A69,FUNCT_1:def 5;
then A71: f.x in the carrier of S;
then A72: f.x in dom h by FUNCT_2:def 1;
A73: f.x in dom F by A71,FUNCT_2:def 1;
F.(f.x) = f.(h.(f.x)) by A72,FUNCT_1:23
.= f.((h*f).x) by A69,FUNCT_1:23
.= f.((id T).x) by A25,GRCAT_1:def 11
.= f.x by A68,GRCAT_1:11;
then f.x in rng F by A73,FUNCT_1:def 5;
then f.x in the carrier of Image F by Th10;
then f.x in [#](Image F) by PRE_TOPC:12;
then A74: f.x in P by A56,A70,XBOOLE_0:def 3;
h.(f.x) = (h*f).x by A69,FUNCT_1:23
.= (id T).x by A25,GRCAT_1:def 11 .= x by A68,GRCAT_1:11;
hence x in h.:P by A72,A74,FUNCT_1:def 12;
end; let x be set; assume
x in h.:P;
then consider y being set such that
A75: y in dom h and
A76: y in P and
A77: x = h.y by FUNCT_1:def 12;
A78: x in rng h by A75,A77,FUNCT_1:def 5;
A79: y in Q by A56,A76,XBOOLE_0:def 3;
y in the carrier of Image F by A76;
then y in rng F by Th10;
then y in rng f by A26;
then A80: y in the carrier of Image f by Th10;
f.x in rng f by A11,A78,FUNCT_1:def 5;
then f.x in the carrier of Image f by Th10;
then reconsider a = f.x, b = y as Element of Image f by A80;
g.a = h.(f.x) by A6,FUNCT_1:72
.= (h*f).x by A11,A78,FUNCT_1:23
.= (id T).x by A25,GRCAT_1:def 11 .= h.y by A77,A78,GRCAT_1:11 .= g
.b by A6,FUNCT_1:72;
then f.x in Q by A7,A79,WAYBEL_1:def 1;
hence x in f"Q by A11,A78,FUNCT_1:def 13;
end;
H.:P = h.:P by A59,RELAT_1:159;
hence (H")"P is open by A33,A44,A58,A67,TOPS_2:67;
end;
then H" is continuous by TOPS_2:55;
then H is_homeomorphism by A32,A33,A44,A54,TOPS_2:def 5;
hence Image F,T are_homeomorphic 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 set; assume A1: x in t;
per cases by A1,ENUMSET1:def 1;
suppose
A2: x = {};
{} c= c by XBOOLE_1:2;
hence thesis by A2;
suppose x = {1}; then x c= c by ZFMISC_1:12; hence x in bool c;
thus thesis;
suppose x = {0,1}; then x c= c;
hence thesis;
end;
then reconsider t as Subset-Family of c by SETFAM_1:def 7;
take s = TopStruct (# c, t #);
thus the carrier of s = {0,1};
thus the topology of s = {{}, {1}, {0,1} };
end;
uniqueness;
end;
definition
cluster Sierpinski_Space -> non empty TopSpace-like;
coherence
proof
set IT = Sierpinski_Space;
thus IT is non empty
proof
thus the carrier of IT is non empty by Def9;
end;
{0,1} in {{}, {1}, {0,1} } by ENUMSET1:14;
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,Th1;
suppose a = {};
then union a in {{}, {1}, {0,1} } by ENUMSET1:14,ZFMISC_1:2;
hence union a in the topology of IT by Def9;
suppose a = {{}}; then union a = {} by ZFMISC_1:31;
then union a in {{}, {1}, {0,1} } by ENUMSET1:14;
hence union a in the topology of IT by Def9;
suppose a = {{1}}; then union a = {1} by ZFMISC_1:31;
then union a in {{}, {1}, {0,1} } by ENUMSET1:14;
hence union a in the topology of IT by Def9;
suppose a = {{0,1}}; then union a = {0,1} by ZFMISC_1:31;
then union a in {{}, {1}, {0,1} } by ENUMSET1:14;
hence union a in the topology of IT by Def9;
suppose a = {{},{1}}; then union a = {} \/ {1} by ZFMISC_1:93;
then union a in {{}, {1}, {0,1} } by ENUMSET1:14;
hence union a in the topology of IT by Def9;
suppose a = {{1},{0,1}}; then union a = {1} \/ {0,1} by ZFMISC_1:93
.= {0,1} by ZFMISC_1:14; then union a in {{}
, {1}, {0,1}} by ENUMSET1:14;
hence union a in the topology of IT by Def9;
suppose a = {{},{0,1}}; then union a = {} \/ {0,1} by ZFMISC_1:93;
then union a in {{}, {1}, {0,1} } by ENUMSET1:14;
hence union a in the topology of IT by Def9;
suppose a = {{},{1},{0,1}}; then a = {{}
} \/ {{1},{0,1}} by ENUMSET1:42;
then union a = union {{}} \/ union {{1},{0,1}} by ZFMISC_1:96
.= {} \/ union {{1},{0,1}} by ZFMISC_1:31
.= {1} \/ {0,1} by ZFMISC_1:93 .= {0,1} by ZFMISC_1:14;
then union a in {{}, {1}, {0,1} } by ENUMSET1:14;
hence union a in the topology of IT by Def9;
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:13;
suppose a = {} & b = {};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14; hence thesis by Def9;
suppose a = {} & b = {1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14;
hence thesis by Def9;
suppose a = {} & b = {0,1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14;
hence thesis by Def9;
suppose a = {1} & b = {};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14;
hence thesis by Def9;
suppose a = {1} & b = {1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14; hence thesis by Def9;
suppose a = {1} & b = {0,1}; then a /\ b = {1} by ZFMISC_1:19;
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14; hence thesis by Def9;
suppose a = {0,1} & b = {};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14;
hence thesis by Def9;
suppose a = {0,1} & b = {1}; then a /\ b = {1} by ZFMISC_1:19;
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14; hence thesis by Def9;
suppose a = {0,1} & b = {0,1};
then a /\ b in {{}, {1}, {0,1} } by ENUMSET1:14; hence thesis by Def9;
end;
end;
Lm2:
Sierpinski_Space is discerning
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
let x,y be Point of S; assume
A1: x <> y; x in the carrier of S & y in the carrier of S;
then x in {0,1} & y in {0,1} by Def9;
then A2: (x = 0 or x = 1) & (y = 0 or y = 1) by TARSKI:def 2;
set V = {1};
{1} c= {0,1} by ZFMISC_1:12;
then V is Subset of S by Def9;
then reconsider V as Subset of S;
{1} in {{}, {1}, {0,1} } by ENUMSET1:14;
then {1} in the topology of S by Def9;
then A3: V is open by PRE_TOPC:def 5;
per cases by A1,A2;
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 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)) by A3;
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 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)) by A3;
end;
hence thesis by T_0TOPSP:def 7;
end;
definition
cluster Sierpinski_Space -> discerning;
coherence by Lm2;
end;
definition ::p.122 lemma 3.3.
cluster Sierpinski_Space -> injective;
coherence
proof
set S = Sierpinski_Space;
let X be non empty TopSpace; let f be map of X, S; assume
A1: f is continuous;
let Y be non empty TopSpace; assume
A2: X is SubSpace of Y;
then A3: the carrier of X c= the carrier of Y by BORSUK_1:35;
{1} c= {0,1} by ZFMISC_1:12;
then {1} is Subset of S by Def9;
then reconsider u = {1} as Subset of S;
u in {{}, {1}, {0,1} } by ENUMSET1:14;
then u in the topology of S by Def9;
then u is open by PRE_TOPC:def 5;
then f"u is open by A1,TOPS_2:55;
then f"u in the topology of X by PRE_TOPC:def 5;
then consider V being Subset of Y such that
A4: V in the topology of Y and
A5: f"u = V /\ [#](X) by A2,PRE_TOPC:def 9;
reconsider V as Subset of Y;
A6: V is open by A4,PRE_TOPC:def 5;
A7: f"u = V /\ (the carrier of X) by A5,PRE_TOPC:12;
set g = chi(V,the carrier of Y);
A8: dom g = the carrier of Y by FUNCT_3:def 3;
the carrier of S = {0,1} by Def9;
then reconsider g as map of Y,S ;
take g;
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 by PRE_TOPC:def 5;
then A9: P in {{}, {1}, {0,1} } by Def9;
per cases by A9,ENUMSET1:13;
suppose P = {}; then g"P = {} by RELAT_1:171; then g"P in the topology
of Y
by PRE_TOPC:5; hence g"P is open by PRE_TOPC:def 5;
suppose A10: P = {1};
A11: g"P c= V
proof let x be set; assume
A12: x in g"P;
then x in dom g & g.x in {1} by A10,FUNCT_1:def 13;
then g.x = 1 by TARSKI:def 1;
hence x in V by A12,FUNCT_3:def 3;
end;
V c= g"P
proof let x be set; assume
A13: x in V; then g.x = 1 by FUNCT_3:def 3;
then x in dom g & g.x in {1} by A8,A13,TARSKI:def 1;
hence x in g"P by A10,FUNCT_1:def 13;
end;
hence g"P is open by A6,A11,XBOOLE_0:def 10;
suppose P = {0,1};
then g"P = the carrier of Y by FUNCT_2:48;
then g"P in the topology of Y by PRE_TOPC:def 1;
hence g"P is open by PRE_TOPC:def 5;
end;
hence g is continuous by TOPS_2:55;
A14: dom g /\ (the carrier of X) = (the carrier of Y) /\ (the carrier of X)
by FUNCT_3:def 3 .= the carrier of X by A3,XBOOLE_1:28
.= dom f by FUNCT_2:def 1;
for x being set st x in dom f holds f.x = g.x
proof
let x be set; assume
A15: x in dom f;
then A16: x in the carrier of X by FUNCT_2:def 1;
per cases;
suppose A17: x in V;
then A18: g.x = 1 by FUNCT_3:def 3;
x in f"u by A7,A16,A17,XBOOLE_0:def 3;
then x in dom f & f.x in {1} by FUNCT_1:def 13;
hence f.x = g.x by A18,TARSKI:def 1;
suppose A19: not x in V;
f.x in rng f by A15,FUNCT_1:def 5;
then f.x in the carrier of S;
then f.x in {0,1} by Def9;
then A20: f.x = 0 or f.x = 1 by TARSKI:def 2;
not x in f"{1} by A5,A19,XBOOLE_0:def 3;
then not x in dom f or not f.x in {1} by FUNCT_1:def 13;
hence f.x = g.x by A3,A15,A16,A19,A20,FUNCT_3:def 3,TARSKI:def 1;
end;
hence g|(the carrier of X) = f by A14,FUNCT_1:68;
end;
end;
definition let I be set; let S be non empty 1-sorted;
cluster I --> S -> non-Empty;
coherence
proof let s be 1-sorted; assume
A1: s in rng (I --> S);
rng (I --> S) c= {S} by FUNCOP_1:19;
hence s is non empty by A1,TARSKI:def 1;
end;
end;
definition let I be set; let T be TopStruct;
cluster I --> T -> TopSpace-yielding;
coherence
proof let x be set; assume
A1: x in rng (I --> T);
rng (I --> T) c= {T} by FUNCOP_1:19;
hence x is TopStruct by A1,TARSKI:def 1;
end;
end;
definition let I be set; let L be reflexive RelStr;
cluster I --> L -> reflexive-yielding;
coherence
proof let S be RelStr; assume
A1: S in rng (I --> L);
rng (I --> L) c= {L} by FUNCOP_1:19;
hence S is reflexive by A1,TARSKI:def 1;
end;
end;
definition 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
by FUNCOP_1:13;
hence product (I --> L) is antisymmetric by WAYBEL_3:30;
end;
end;
definition 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 by FUNCOP_1:13;
hence product (I --> L) is transitive by WAYBEL_3:29;
end;
end;
theorem
for T being Scott TopAugmentation of BoolePoset 1
holds the topology of T = the topology of Sierpinski_Space
proof
let T be Scott TopAugmentation of BoolePoset 1;
A1: the RelStr of T = BoolePoset 1 by YELLOW_9:def 4;
A2: LattPOSet BooleLatt 1 = RelStr(#the carrier of BooleLatt 1,
LattRel(BooleLatt 1)#) by LATTICE3:def 2;
A3: the carrier of T = the carrier of LattPOSet BooleLatt 1 by A1,YELLOW_1:def
2
.= bool 1 by A2,LATTICE3:def 1
.= {0,1} by CARD_5:1,ZFMISC_1:30;
then 0 in the carrier of BoolePoset 1 &
1 in the carrier of BoolePoset 1 by A1,TARSKI:def 2;
then reconsider j = 1, z = 0 as Element of BoolePoset 1;
reconsider c = {z} as Subset of T by A1;
A4: now let y be set; assume
A5: y in the topology of T;
then reconsider x = y as Subset of T;
A6: x = {} or x = {0} or x = {1} or x = {0,1} by A3,ZFMISC_1:42;
set a = 0, b = 1;
A7: a c= b by XBOOLE_1:2;
A8: a in {z} by TARSKI:def 1;
not b in {z} by TARSKI:def 1;
then not {z} is upper by A7,A8,WAYBEL_7:11;
then not c is upper by A1,WAYBEL_0:25;
then not c is open by WAYBEL11:def 4;
then y in {{}, {1}, {0,1} } by A5,A6,ENUMSET1:14,PRE_TOPC:def 5;
hence y in the topology of Sierpinski_Space by Def9;
end;
now let x be set; assume
x in the topology of Sierpinski_Space;
then A9: x in {{}, {1}, {0,1} } by Def9;
per cases by A9,ENUMSET1:13;
suppose x = {};
hence x in the topology of T by PRE_TOPC:5;
suppose A10: x = {1}; {1} c= {0,1} by ZFMISC_1:12;
then reconsider x' = x as Subset of T by A3,A10;
for a,b being Element of T st a in x' & a <= b holds b in x'
proof let a,b be Element of T; assume that
A11: a in x' and
A12: a <= b;
A13: a = 1 by A10,A11,TARSKI:def 1;
A14: b = 0 or b = 1 by A3,TARSKI:def 2;
b <> 0
proof
assume A15: b = 0;
[a, b] in the InternalRel of T by A12,ORDERS_1:def 9;
then j <= z by A1,A13,A15,ORDERS_1:def 9;
then A16: 1 c= 0 by YELLOW_1:2;
0 c= 1 by XBOOLE_1:2; hence thesis by A16,XBOOLE_0:def 10;
end;
hence b in x' by A10,A14,TARSKI:def 1;
end;
then A17: x' is upper by WAYBEL_0:def 20;
for D being non empty directed Subset of T st sup D in x'
holds D meets x'
proof let D be non empty directed Subset of T; assume
A18: sup D in x';
D <> {0}
proof assume
A19: D = {0};
ex_sup_of D, BoolePoset 1 by YELLOW_0:17;
then sup D = sup {z} by A1,A19,YELLOW_0:26 .= 0 by YELLOW_0:39
;
hence thesis by A10,A18,TARSKI:def 1;
end;
then D = {1} or D = {0,1} by A3,ZFMISC_1:42;
then A20: 1 in D by TARSKI:def 1,def 2;
1 in x' by A10,TARSKI:def 1;
hence D meets x' by A20,XBOOLE_0:3;
end;
then x' is inaccessible by WAYBEL11:def 1;
then x' is open by A17,WAYBEL11:def 4;
hence x in the topology of T by PRE_TOPC:def 5;
suppose x = {0,1};
hence x in the topology of T by A3,PRE_TOPC:def 1;
end; hence thesis by A4,TARSKI:2;
end;
theorem Th14:
for I being non empty set holds
{product ((Carrier (I --> Sierpinski_Space))+*(i,{1}))
where i is Element of I: not contradiction }
is prebasis of product (I --> Sierpinski_Space)
proof let I be non empty set;
set IS = I --> Sierpinski_Space,
pB = { product ((Carrier IS)+*(i,{1}))
where i is Element of I: not contradiction },
P = product_prebasis IS;
pB c= bool the carrier of product IS
proof let x be set; assume
x in pB;
then consider i being Element of I such that
A1: x = product ((Carrier IS)+*(i,{1}));
product ((Carrier IS)+*(i,{1})) c= product Carrier IS
proof let y be set; assume
y in product ((Carrier IS)+*(i,{1}));
then consider g being Function such that
A2: y = g and
A3: dom g = dom ((Carrier IS)+*(i,{1})) and
A4: for z being set st z in dom ((Carrier IS)+*(i,{1}))
holds g.z in ((Carrier IS)+*(i,{1})).z by CARD_3:def 5;
A5: dom g = dom Carrier IS by A3,FUNCT_7:32;
for z being set st z in dom (Carrier IS) holds g.z in (Carrier IS)
.
z
proof let z be set; assume
A6: z in dom (Carrier IS);
then z in dom ((Carrier IS)+*(i,{1})) by FUNCT_7:32;
then A7: g.z in ((Carrier IS)+*(i,{1})).z by A4;
A8: z in I by A6,PBOOLE:def 3;
then consider R being 1-sorted such that
A9: R = IS.z and
A10: (Carrier IS).z = the carrier of R by PRALG_1:def 13;
A11: the carrier of R = the carrier of Sierpinski_Space
by A8,A9,FUNCOP_1:13 .= {0,1} by Def9;
per cases;
suppose z = i;
then ((Carrier IS)+*(i,{1})).z = {1} by A6,FUNCT_7:33;
then g.z = 1 by A7,TARSKI:def 1;
hence g.z in (Carrier IS).z by A10,A11,TARSKI:def 2;
suppose z <> i;
hence g.z in (Carrier IS).z by A7,FUNCT_7:34;
end;
hence y in product Carrier IS by A2,A5,CARD_3:def 5;
end;
then x c= the carrier of product IS by A1,Def3;
hence x in bool the carrier of product IS;
end;
then reconsider B = pB as Subset-Family of product IS
by SETFAM_1:def 7;
reconsider B as Subset-Family of product IS;
A12:B c= P
proof let x be set; assume
A13: x in B;
then consider i being Element of I such that
A14: x = product ((Carrier IS)+*(i,{1}));
reconsider y = x as Subset of product Carrier IS by A13,Def3;
{1} c= {0,1} by ZFMISC_1:12;
then {1} is Subset of Sierpinski_Space by Def9;
then reconsider V = {1} as Subset of Sierpinski_Space;
{1} in {{}, {1}, {0,1} } by ENUMSET1:14;
then {1} in the topology of Sierpinski_Space by Def9;
then A15: V is open by PRE_TOPC:def 5;
A16: Sierpinski_Space = IS.i by FUNCOP_1:13;
y = product ((Carrier IS) +* (i,V)) by A14;
hence x in P by A15,A16,Def2;
end;
A17: P is prebasis of product IS by Def3;
then A18: P c= the topology of product IS by CANTOR_1:def 5;
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 A17,YELLOW_9:23;
then reconsider F = (FinMeetCl P) \ {{}} as Basis of product IS by Th3;
A19: F c= FinMeetCl B
proof let x be set; assume
A20: x in F;
then reconsider y = x as Subset of product IS;
A21: not x in {{}} by A20,XBOOLE_0:def 4;
x in FinMeetCl P by A20,XBOOLE_0:def 4;
then consider Y1 being Subset-Family of product IS such
that
A22: Y1 c= P and
A23: Y1 is finite and
A24: y = Intersect Y1 by CANTOR_1:def 4;
A25: the carrier of product IS = product Carrier IS by Def3;
reconsider Y2 = Y1 /\ B as Subset-Family of product IS;
A26: Y2 c= B by XBOOLE_1:17;
A27: Y2 c= Y1 by XBOOLE_1:17;
then A28: Y2 is finite by A23,FINSET_1:13;
A29: Intersect Y1 c= Intersect Y2 by A27,CANTOR_1:11;
Intersect Y2 c= Intersect Y1
proof let z be set; assume
A30: z in Intersect Y2;
then A31: z in product Carrier IS by A25;
for Y being set st Y in Y1 holds z in Y
proof let Y be set; assume
A32: Y in Y1;
then reconsider Y' = Y as Subset of product Carrier IS by Def3;
consider i being set, S being TopStruct,
V being Subset of S such that
A33: i in I and
A34: V is open and
A35: S = IS.i and
A36: Y' = product ((Carrier IS) +* (i,V)) by A22,A32,Def2;
consider RR being 1-sorted such that
A37: RR = IS.i and
A38: (Carrier IS).i = the carrier of RR by A33,PRALG_1:def 13;
A39: i in dom (Carrier IS) by A33,PBOOLE:def 3;
reconsider V' = V as Subset of Sierpinski_Space
by A33,A35,FUNCOP_1:13;
V in the topology of S by A34,PRE_TOPC:def 5;
then V' in the topology of Sierpinski_Space
by A33,A35,FUNCOP_1:13;
then A40: V' in {{}, {1}, {0,1} } by Def9;
A41: V' <> {}
proof assume
A42: V' = {};
A43: ((Carrier IS)+*(i,{})).i = {} by A39,FUNCT_7:33;
i in dom ((Carrier IS)+*(i,{})) by A39,FUNCT_7:32;
then {} in rng ((Carrier IS)+*(i,{})) by A43,FUNCT_1:def 5
;
then Y' = {} by A36,A42,CARD_3:37;
then y = {} by A24,A32,MSSUBFAM:3;
hence thesis by A21,TARSKI:def 1;
end;
reconsider i' = i as Element of I by A33;
per cases by A40,A41,ENUMSET1:13;
suppose V' = {1};
then Y' = product ((Carrier IS)+*(i',{1})) by A36;
then Y in B;
then Y in Y2 by A32,XBOOLE_0:def 3;
hence z in Y by A30,CANTOR_1:10;
suppose V' = {0,1};
then V' = the carrier of Sierpinski_Space by Def9
.= (Carrier IS).i by A33,A37,A38,FUNCOP_1:13;
hence z in Y by A31,A36,FUNCT_7:37;
end;
hence z in Intersect Y1 by A30,CANTOR_1:10;
end;
then y = Intersect Y2 by A24,A29,XBOOLE_0:def 10;
hence x in FinMeetCl B by A26,A28,CANTOR_1:def 4;
end;
pB c= the topology of product IS by A12,A18,XBOOLE_1:1;
hence pB is prebasis of product (I --> Sierpinski_Space)
by A19,CANTOR_1:def 5;
end;
definition 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
by FUNCOP_1:13;
hence product (I --> L) is with_suprema complete by WAYBEL_3:31;
end;
end;
definition 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
by FUNCOP_1:13;
hence product (I --> X) is algebraic by WAYBEL13:25;
end;
end;
theorem Th15:
for X being non empty set
ex f being map of BoolePoset X, product (X --> BoolePoset 1) 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 1;
LattPOSet BooleLatt X = RelStr(#the carrier of BooleLatt X,
LattRel(BooleLatt X)#) by LATTICE3:def 2;
then A1: the carrier of BoolePoset X = the carrier of BooleLatt X by YELLOW_1:
def 2
.= bool X by LATTICE3:def 1;
LattPOSet BooleLatt 1 = RelStr(#the carrier of BooleLatt 1,
LattRel(BooleLatt 1)#) by LATTICE3:def 2;
then A2: the carrier of BoolePoset 1 = the carrier of BooleLatt 1 by YELLOW_1:
def 2
.= bool {{}} by CARD_5:1,LATTICE3:def 1
.= {0,1} by CARD_5:1,ZFMISC_1:30;
A3: the carrier of product XB = product Carrier XB by YELLOW_1:def 4;
deffunc F(set) = chi($1,X);
consider f being Function such that
A4: dom f = bool X and
A5: for Y being set st Y in bool X holds f.Y = F(Y) from Lambda;
rng f c= product Carrier XB
proof let y be set; assume
y in rng f;
then consider x being set such that
A6: x in dom f and
A7: y = f.x by FUNCT_1:def 5;
A8: chi(x,X) = y by A4,A5,A6,A7;
A9: dom chi(x,X) = X by FUNCT_3:def 3 .= dom (Carrier XB) by PBOOLE:def 3;
for z being set st z in dom (Carrier XB) holds
chi(x,X).z in (Carrier XB).z
proof let z be set; assume
z in dom (Carrier XB);
then A10: z in X by PBOOLE:def 3;
then consider R being 1-sorted such that
A11: R = XB.z and
A12: (Carrier XB).z = the carrier of R by PRALG_1:def 13;
A13: (Carrier XB).z = {0,1} by A2,A10,A11,A12,FUNCOP_1:13;
per cases;
suppose z in x;
then chi(x,X).z = 1 by A10,FUNCT_3:def 3;
hence chi(x,X).z in (Carrier XB).z by A13,TARSKI:def 2;
suppose not z in x;
then chi(x,X).z = 0 by A10,FUNCT_3:def 3;
hence chi(x,X).z in (Carrier XB).z by A13,TARSKI:def 2;
end;
hence y in product Carrier XB by A8,A9,CARD_3:def 5;
end;
then f is Function of the carrier of BoolePoset X,
the carrier of product XB
by A1,A3,A4,FUNCT_2:def 1,RELSET_1:11;
then reconsider f as map of BoolePoset X, product (X --> BoolePoset 1)
;
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
A14: f.A = f.B;
f.A = chi(A,X) & f.B = chi(B,X) by A1,A5;
hence A = B by A1,A14,FUNCT_3:47;
end;
then A15: f is one-to-one by WAYBEL_1:def 1;
product Carrier XB c= rng f
proof let z be set; assume
z in product Carrier XB;
then consider g being Function such that
A16: z = g and
A17: dom g = dom (Carrier XB) and
A18: for y being set st y in dom (Carrier XB) holds
g.y in (Carrier XB).y by CARD_3:def 5;
set A = g"{1};
A19: A c= X
proof let a be set; assume
a in A;
then a in dom g by FUNCT_1:def 13;
hence a in X by A17,PBOOLE:def 3;
end;
A20: dom chi(A,X) = X by FUNCT_3:def 3 .= dom g by A17,PBOOLE:def 3;
for a being set st a in dom chi(A,X) holds chi(A,X).a = g.a
proof let a be set; assume
A21: a in dom chi(A,X);
then A22: a in X by FUNCT_3:def 3;
then consider R being 1-sorted such that
A23: R = XB.a and
A24: (Carrier XB).a = the carrier of R by PRALG_1:def 13;
A25: (Carrier XB).a = {0,1} by A2,A22,A23,A24,FUNCOP_1:13;
a in dom (Carrier XB) by A22,PBOOLE:def 3;
then g.a in (Carrier XB).a by A18;
then A26: g.a = 0 or g.a = 1 by A25,TARSKI:def 2;
per cases;
suppose a in A;
then chi(A,X).a = 1 & g.a in {1} by A22,FUNCT_1:def 13,FUNCT_3:def
3;
hence chi(A,X).a = g.a by TARSKI:def 1;
suppose A27: not a in A;
g.a <> 1
proof assume
g.a = 1;
then g.a in {1} by TARSKI:def 1;
hence thesis by A20,A21,A27,FUNCT_1:def 13;
end;
hence chi(A,X).a = g.a by A22,A26,A27,FUNCT_3:def 3;
end;
then z = chi(A,X) by A16,A20,FUNCT_1:9 .= f.A by A5,A19;
hence z in rng f by A4,A19,FUNCT_1:def 5;
end;
then A28: rng f = the carrier of product XB by A3,XBOOLE_0:def 10;
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;
A29: f.A = chi(A,X) & f.B = chi(B,X) by A1,A5;
hereby assume
A <= B;
then A30: A c= B by YELLOW_1:2;
for i being set 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 set; assume
A31: i in X;
take R = BoolePoset 1;
A32: 0 in the carrier of R & 1 in the carrier of R by A2,TARSKI:def 2;
per cases;
suppose
A33: i in A;
reconsider xi = 1, yi = 1 as Element of R by A32;
take xi,yi;
thus R = XB.i by A31,FUNCOP_1:13;
thus xi = chi(A,X).i by A31,A33,FUNCT_3:def 3;
thus yi = chi(B,X).i by A30,A31,A33,FUNCT_3:def 3;
thus xi <= yi;
suppose
A34: not i in A;
thus thesis
proof
per cases;
suppose
A35: i in B;
reconsider xi = 0, yi = 1 as Element of R by A32;
take xi,yi;
thus R = XB.i by A31,FUNCOP_1:13;
thus xi = chi(A,X).i by A31,A34,FUNCT_3:def 3;
thus yi = chi(B,X).i by A31,A35,FUNCT_3:def 3;
xi c= yi by XBOOLE_1:2;
hence xi <= yi by YELLOW_1:2;
suppose
A36: not i in B;
reconsider xi = 0, yi = 0 as Element of R by A32;
take xi,yi;
thus R = XB.i by A31,FUNCOP_1:13;
thus xi = chi(A,X).i by A31,A34,FUNCT_3:def 3;
thus yi = chi(B,X).i by A31,A36,FUNCT_3:def 3;
thus xi <= yi;
end;
end;
hence f.A <= f.B by A3,A29,YELLOW_1:def 4;
end; assume
f.A <= f.B;
then consider h1,h2 being Function such that
A37: h1 = f.A and
A38: h2 = f.B and
A39: for i be set 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 A3,YELLOW_1:def 4;
A c= B
proof let i be set; assume
A40: i in A;
then consider R being RelStr, xi,yi being Element of R such that
A41: R = XB.i and
A42: xi = h1.i and
A43: yi = h2.i and
A44: xi <= yi by A1,A39;
A45: R = BoolePoset 1 by A1,A40,A41,FUNCOP_1:13;
A46: xi = chi(A,X).i by A1,A5,A37,A42
.= 1 by A1,A40,FUNCT_3:def 3;
reconsider a = xi, b = yi as Element of BoolePoset 1
by A1,A40,A41,FUNCOP_1:13;
A47: a <= b by A1,A40,A41,A44,FUNCOP_1:13;
A48: yi <> 0
proof assume
yi = 0;
then A49: 1 c= 0 by A46,A47,YELLOW_1:2;
0 c= 1 by XBOOLE_1:2; hence thesis by A49,XBOOLE_0:def 10;
end;
chi(B,X).i = h2.i by A1,A5,A38 .= 1 by A2,A43,A45,A48,TARSKI:def
2
;
hence i in B by FUNCT_3:42;
end;
hence A <= B by YELLOW_1:2;
end;
hence f is isomorphic by A15,A28,WAYBEL_0:66;
thus for Y being Subset of X holds f.Y = chi(Y,X) by A5;
end;
theorem Th16: ::p.122 lemma 3.4.(i)
for I being non empty set
for T being Scott TopAugmentation of product (I --> BoolePoset 1) holds
the topology of T = the topology of product (I --> Sierpinski_Space)
proof
let I be non empty set;
let T be Scott TopAugmentation of product (I --> BoolePoset 1);
A1: the RelStr of T = product (I --> BoolePoset 1) by YELLOW_9:def 4;
set IB = I --> BoolePoset 1,
IS = I --> Sierpinski_Space;
LattPOSet BooleLatt 1 = RelStr(#the carrier of BooleLatt 1,
LattRel(BooleLatt 1)#) by LATTICE3:def 2;
then A2: the carrier of BoolePoset 1 = the carrier of BooleLatt 1 by YELLOW_1:
def 2 .= bool {{}} by CARD_5:1,LATTICE3:def 1 .= {0,1} by CARD_5:1,ZFMISC_1:30
;
A3: dom Carrier IB = I by PBOOLE:def 3 .= dom Carrier IS by PBOOLE:def 3;
A4: for i being set st i in
dom Carrier IB holds (Carrier IB).i = (Carrier IS).i
proof let i be set; assume i in dom Carrier IB;
then A5: i in I by PBOOLE:def 3;
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 13;
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 13;
the carrier of R1 = {0,1} by A2,A5,A6,FUNCOP_1:13
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A5,A8,FUNCOP_1:13;
hence (Carrier IB).i = (Carrier IS).i by A7,A9;
end;
then A10: Carrier IB = Carrier IS by A3,FUNCT_1:9;
A11: the carrier of T = product Carrier (I --> BoolePoset 1) by A1,YELLOW_1:def
4
.= product Carrier (I --> Sierpinski_Space) by A3,A4,FUNCT_1:9
.= the carrier of product (I --> Sierpinski_Space) by Def3;
A12: the carrier of product IB = product Carrier IB by YELLOW_1:def 4;
reconsider P = {product ((Carrier IS)+*(ii,{1}))
where ii is Element of I: not contradiction }
as prebasis of product (I --> Sierpinski_Space) by Th14;
reconsider T' = T as complete Scott TopLattice;
T' is algebraic by A1,WAYBEL_8:17;
then consider R being Basis of T' such that
A13: R = {uparrow yy where yy is Element of T' :
yy in the carrier of CompactSublatt T'} by WAYBEL14:42;
consider f being map of BoolePoset I, product IB such that
A14: f is isomorphic and
A15: for Y being Subset of I holds f.Y = chi(Y,I) by Th15;
A16: dom f = the carrier of BoolePoset I by FUNCT_2:def 1;
A17: rng f = the carrier of product IB by A14,WAYBEL_0:66;
A18: R c= FinMeetCl P
proof let X be set; assume
A19: X in R;
then consider Y being Element of T' such that
A20: X = uparrow Y and
A21: Y in the carrier of CompactSublatt T' by A13;
A22: Y is compact by A21,WAYBEL_8:def 1;
reconsider X' = X as Subset of product IS by A11,A19;
reconsider y = Y as Element of product IB by A1;
A23: y is compact by A1,A22,WAYBEL_8:9;
consider x being set such that
A24: x in dom f and
A25: y = f.x by A17,FUNCT_1:def 5;
reconsider x as Element of BoolePoset I by A16,A24;
reconsider x' = x as Subset of I by WAYBEL_8:28;
deffunc F(Element of I) = product ((Carrier IS)+*($1,{1}));
x is compact by A14,A23,A25,WAYBEL13:28;
then
A26: x is finite by WAYBEL_8:30;
A27: uparrow Y = uparrow {Y} by WAYBEL_0:def 18
.= uparrow {y} by A1,WAYBEL_0:13 .= uparrow y by WAYBEL_0:def 18;
set ZZ = {product ((Carrier IS)+*(jj,{1}))
where jj is Element of I: jj in x };
A28: ZZ c= P
proof let z be set; assume
z in ZZ;
then consider j being Element of I such that
A29: z = product ((Carrier IS)+*(j,{1})) and j in x';
thus z in P by A29;
end;
then ZZ c= bool the carrier of product IS by XBOOLE_1:1;
then reconsider ZZ as Subset-Family of product IS
by SETFAM_1:def 7;
A30: {F(jj) where jj is Element of I: jj in x} is finite
from FraenkelFin(A26);
A31: X' c= Intersect ZZ
proof let z be set; assume
A32: z in X';
then A33: z in the carrier of product IB by A1,A11;
reconsider z' = z as
Element of product IB by A1,A11,A32;
z in product Carrier IB by A33,YELLOW_1:def 4;
then consider gg being Function such that
A34: z = gg and
A35: dom gg = dom (Carrier IB) and
A36: for w being set st w in dom (Carrier IB)
holds gg.w in (Carrier IB).w by CARD_3:def 5;
y <= z' by A20,A27,A32,WAYBEL_0:18;
then consider h1,h2 being Function such that
A37: h1 = y and
A38: h2 = z' and
A39: for i be set 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 A12,YELLOW_1:def 4;
A40: h1 = f.x' by A25,A37 .= chi(x,I) by A15;
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;
A43: dom ((Carrier IS)+*(j,{1})) = dom (Carrier IS) by FUNCT_7:32
.= I by PBOOLE:def 3;
consider RS being RelStr, xj,yj being Element of RS such that
A44: RS = IB.j and
A45: xj = h1.j and
A46: yj = h2.j and
A47: xj <= yj by A39;
A48: xj = 1 by A40,A42,A45,FUNCT_3:def 3;
reconsider a = xj, b = yj
as Element of BoolePoset 1 by A44,FUNCOP_1:13;
A49: a <= b by A44,A47,FUNCOP_1:13;
A50: b in the carrier of BoolePoset 1;
A51: yj <> 0
proof assume
yj = 0;
then A52: 1 c= 0 by A48,A49,YELLOW_1:2;
0 c= 1 by XBOOLE_1:2; hence thesis by A52,XBOOLE_0:def 10
;
end;
A53: dom h2 = dom ((Carrier IS)+*(j,{1})) by A34,A35,A38,A43,PBOOLE
:def 3;
for w being set st w in dom ((Carrier IS)+*(j,{1}))
holds h2.w in ((Carrier IS)+*(j,{1})).w
proof let w be set; assume
w in dom ((Carrier IS)+*(j,{1}));
then A54: w in dom Carrier IS by A43,PBOOLE:def 3;
per cases;
suppose
A55: w = j;
then A56: ((Carrier IS)+*(j,{1})).w = {1} by A54,FUNCT_7:33;
h2.w = 1 by A2,A46,A50,A51,A55,TARSKI:def 2;
hence h2.w in ((Carrier IS)+*(j,{1})).w by A56,TARSKI:def 1;
suppose w <> j;
then ((Carrier IS)+*(j,{1})).w =(Carrier IS).w by FUNCT_7:34;
hence h2.w in ((Carrier IS)+*(j,{1})).w
by A10,A34,A36,A38,A54;
end;
hence z in Z by A38,A41,A53,CARD_3:def 5;
end;
hence z in Intersect ZZ by A32,CANTOR_1:10;
end;
Intersect ZZ c= X'
proof let z be set; assume
A57: z in Intersect ZZ;
then A58: z in the carrier of product IB by A1,A11;
reconsider z' = z
as Element of product IB by A1,A11,A57;
set h1 = chi(x,I);
A59: h1 = f.x' by A15 .= y by A25;
z in product Carrier IB by A58,YELLOW_1:def 4;
then consider h2 being Function such that
A60: z = h2 and
dom h2 = dom (Carrier IB) and
A61: for w being set st w in dom (Carrier IB) holds
h2.w in (Carrier IB).w by CARD_3:def 5;
for i be set 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 set; assume
A62: i in I;
then reconsider i' = i as Element of I;
take RS = BoolePoset 1;
A63: 0 in the carrier of RS & 1 in the carrier of RS
by A2,TARSKI:def 2;
consider RB being 1-sorted such that
A64: RB = IB.i and
A65: (Carrier IB).i = the carrier of RB by A62,PRALG_1:def 13;
A66: (Carrier IB).i = {0,1} by A2,A62,A64,A65,FUNCOP_1:13;
A67: i in dom (Carrier IB) by A62,PBOOLE:def 3;
then A68: h2.i in (Carrier IB).i by A61;
per cases;
suppose
A69: i in x;
then product ((Carrier IS)+*(i',{1})) in ZZ;
then z in product ((Carrier IS)+*(i',{1})) by A57,CANTOR_1:10;
then consider h2' being Function such that
A70: z = h2' and
dom h2' = dom ((Carrier IS)+*(i',{1})) and
A71: for w being set st w in dom ((Carrier IS)+*(i',{1})) holds
h2'.w in ((Carrier IS)+*(i',{1})).w by CARD_3:def 5;
i' in dom ((Carrier IS)+*(i',{1})) by A3,A67,FUNCT_7:32;
then A72: h2'.i' in ((Carrier IS)+*(i',{1})).i' by A71;
A73: ((Carrier IS)+*(i',{1})).i' = {1} by A3,A67,FUNCT_7:33;
reconsider xi = 1, yi = 1 as Element of RS by A63;
take xi,yi;
thus RS = IB.i by A62,FUNCOP_1:13;
thus xi = h1.i by A62,A69,FUNCT_3:def 3;
thus yi = h2.i by A60,A70,A72,A73,TARSKI:def 1;
thus xi <= yi;
suppose A74: not i in x;
thus thesis
proof
per cases by A66,A68,TARSKI:def 2;
suppose
A75: h2.i = 0;
reconsider xi = 0, yi = 0
as Element of RS by A63;
take xi,yi;
thus RS = IB.i by A62,FUNCOP_1:13;
thus xi = h1.i by A62,A74,FUNCT_3:def 3;
thus yi = h2.i by A75;
thus xi <= yi;
suppose
A76: h2.i = 1;
reconsider xi = 0, yi = 1
as Element of RS by A63;
take xi,yi;
thus RS = IB.i by A62,FUNCOP_1:13;
thus xi = h1.i by A62,A74,FUNCT_3:def 3;
thus yi = h2.i by A76;
xi c= yi by XBOOLE_1:2;
hence xi <= yi by YELLOW_1:2;
end;
end;
then y <= z' by A12,A59,A60,YELLOW_1:def 4;
hence z in X' by A20,A27,WAYBEL_0:18;
end;
then X' = Intersect ZZ by A31,XBOOLE_0:def 10;
hence X in FinMeetCl P by A28,A30,CANTOR_1:def 4;
end;
FinMeetCl P c= R
proof let X be set; assume
A77: X in FinMeetCl P;
then reconsider X' = X as Subset of product IS;
consider ZZ being Subset-Family of product IS such that
A78: ZZ c= P and
A79: ZZ is finite and
A80: X = Intersect ZZ by A77,CANTOR_1:def 4;
deffunc F(set) = product ((Carrier IS)+*($1,{1}));
consider F being Function such that
A81: dom F = I and
A82: for e being set st e in I holds F.e = F(e) from Lambda;
P c= rng F
proof let w be set; assume
w in P;
then consider e being Element of I such that
A83: w = product ((Carrier IS)+*(e,{1}));
w = F.e by A82,A83;
hence w in rng F by A81,FUNCT_1:def 5;
end;
then ZZ c= rng F by A78,XBOOLE_1:1;
then consider x' being set such that
A84: x' c= dom F and
A85: x' is finite and
A86: F.:x' = ZZ by A79,COMPTS_1:1;
reconsider x' as Subset of I by A81,A84;
set PP = {product ((Carrier IS)+*(i,{1}))
where i is Element of I: i in x'};
A87: ZZ c= PP
proof let w be set; assume
w in ZZ;
then consider e being set such that
A88: e in dom F and
A89: e in x' and
A90: w = F.e by A86,FUNCT_1:def 12;
reconsider e as Element of I by A81,A88;
w = product ((Carrier IS)+*(e,{1})) by A82,A90;
hence w in PP by A89;
end;
PP c= ZZ
proof let w be set; assume
w in PP;
then consider e being Element of I such that
A91: w = product ((Carrier IS)+*(e,{1})) and
A92: e in x';
w = F.e by A82,A91;
hence w in ZZ by A81,A86,A92,FUNCT_1:def 12;
end;
then A93: ZZ = PP by A87,XBOOLE_0:def 10;
reconsider x = x' as Element of BoolePoset I by WAYBEL_8:28;
A94: x is compact by A85,WAYBEL_8:30;
reconsider y = f.x as Element of product IB;
A95: y is compact by A14,A94,WAYBEL13:28;
reconsider Y = y as Element of T' by A1;
A96: uparrow Y = uparrow {Y} by WAYBEL_0:def 18
.= uparrow {y} by A1,WAYBEL_0:13 .= uparrow y by WAYBEL_0:def 18;
A97: X' c= uparrow y
proof let z be set; assume
A98: z in X';
then A99: z in the carrier of product IB by A1,A11;
reconsider z' = z
as Element of product IB by A1,A11,A98;
set h1 = chi(x,I);
A100: h1 = y by A15;
z in product Carrier IB by A99,YELLOW_1:def 4;
then consider h2 being Function such that
A101: z = h2 and
dom h2 = dom (Carrier IB) and
A102: for w being set st w in dom (Carrier IB) holds
h2.w in (Carrier IB).w by CARD_3:def 5;
for i be set 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 set; assume
A103: i in I;
then reconsider i' = i as Element of I;
take RS = BoolePoset 1;
A104: 0 in the carrier of RS & 1 in the carrier of RS
by A2,TARSKI:def 2;
consider RB being 1-sorted such that
A105: RB = IB.i and
A106: (Carrier IB).i = the carrier of RB by A103,PRALG_1:def 13;
A107: (Carrier IB).i = {0,1} by A2,A103,A105,A106,FUNCOP_1:13;
A108: i in dom (Carrier IB) by A103,PBOOLE:def 3;
then A109: h2.i in (Carrier IB).i by A102;
per cases;
suppose
A110: i in x;
then product ((Carrier IS)+*(i',{1})) in ZZ by A93;
then z in product ((Carrier IS)+*(i',{1})) by A80,A98,CANTOR_1:
10;
then
consider h2' being Function such that
A111: z = h2' and
dom h2' = dom ((Carrier IS)+*(i',{1})) and
A112: for w being set st w in dom ((Carrier IS)+*(i',{1})) holds
h2'.w in ((Carrier IS)+*(i',{1})).w by CARD_3:def 5;
i' in dom ((Carrier IS)+*(i',{1})) by A3,A108,FUNCT_7:32;
then A113: h2'.i' in ((Carrier IS)+*(i',{1})).i' by A112;
A114: ((Carrier IS)+*(i',{1})).i' = {1} by A3,A108,FUNCT_7:33;
reconsider xi = 1, yi = 1 as Element of RS by A104
;
take xi,yi;
thus RS = IB.i by A103,FUNCOP_1:13;
thus xi = h1.i by A110,FUNCT_3:def 3;
thus yi = h2.i by A101,A111,A113,A114,TARSKI:def 1;
thus xi <= yi;
suppose A115:not i in x;
thus thesis
proof
per cases by A107,A109,TARSKI:def 2;
suppose
A116: h2.i = 0;
reconsider xi = 0, yi = 0
as Element of RS by A104;
take xi,yi;
thus RS = IB.i by A103,FUNCOP_1:13;
thus xi = h1.i by A103,A115,FUNCT_3:def 3;
thus yi = h2.i by A116;
thus xi <= yi;
suppose
A117: h2.i = 1;
reconsider xi = 0, yi = 1
as Element of RS by A104;
take xi,yi;
thus RS = IB.i by A103,FUNCOP_1:13;
thus xi = h1.i by A103,A115,FUNCT_3:def 3;
thus yi = h2.i by A117;
xi c= yi by XBOOLE_1:2;
hence xi <= yi by YELLOW_1:2;
end;
end;
then y <= z' by A12,A100,A101,YELLOW_1:def 4;
hence z in uparrow y by WAYBEL_0:18;
end;
uparrow y c= X'
proof let z be set; assume
A118: z in uparrow y;
then A119: z in the carrier of product IB;
reconsider z' = z as Element of product IB by A118;
z in product Carrier IB by A119,YELLOW_1:def 4;
then consider gg being Function such that
A120: z = gg and
A121: dom gg = dom (Carrier IB) and
A122: for w being set st w in dom (Carrier IB)
holds gg.w in (Carrier IB).w by CARD_3:def 5;
y <= z' by A118,WAYBEL_0:18;
then consider h1,h2 being Function such that
A123: h1 = y and
A124: h2 = z' and
A125: for i be set 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 A12,YELLOW_1:def 4;
A126: h1 = chi(x,I) by A15,A123;
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
A127: Z = product ((Carrier IS)+*(j,{1})) and
A128: j in x by A93;
A129: dom ((Carrier IS)+*(j,{1})) = dom (Carrier IS) by FUNCT_7:32
.= I by PBOOLE:def 3;
consider RS being RelStr, xj,yj being Element of RS such that
A130: RS = IB.j and
A131: xj = h1.j and
A132: yj = h2.j and
A133: xj <= yj by A125;
A134: xj = 1 by A126,A128,A131,FUNCT_3:def 3;
A135: RS = BoolePoset 1 by A130,FUNCOP_1:13;
reconsider b = yj as Element of BoolePoset 1 by A130,FUNCOP_1:13;
A136: b in the carrier of BoolePoset 1;
A137: yj <> 0
proof assume
yj = 0;
then A138: 1 c= 0 by A133,A134,A135,YELLOW_1:2;
0 c= 1 by XBOOLE_1:2; hence thesis by A138,XBOOLE_0:def
10;
end;
A139: dom h2 = dom ((Carrier IS)+*(j,{1})) by A120,A121,A124,A129,
PBOOLE:def 3;
for w being set st w in dom ((Carrier IS)+*(j,{1}))
holds h2.w in ((Carrier IS)+*(j,{1})).w
proof let w be set; assume
w in dom ((Carrier IS)+*(j,{1}));
then A140: w in dom Carrier IS by A129,PBOOLE:def 3;
per cases;
suppose
A141: w = j;
then A142: ((Carrier IS)+*(j,{1})).w = {1} by A140,FUNCT_7:33;
h2.w = 1 by A2,A132,A136,A137,A141,TARSKI:def 2;
hence h2.w in ((Carrier IS)+*(j,{1})).w by A142,TARSKI:def 1
;
suppose w <> j;
then ((Carrier IS)+*(j,{1})).w =(Carrier IS).w by FUNCT_7:34
;
hence h2.w in ((Carrier IS)+*(j,{1})).w
by A10,A120,A122,A124,A140;
end;
hence z in Z by A124,A127,A139,CARD_3:def 5;
end;
hence z in X' by A1,A11,A80,A118,CANTOR_1:10;
end;
then A143: X = uparrow Y by A96,A97,XBOOLE_0:def 10;
Y is compact by A1,A95,WAYBEL_8:9;
then Y in the carrier of CompactSublatt T' by WAYBEL_8:def 1;
hence X in R by A13,A143;
end;
then A144: R = FinMeetCl P by A18,XBOOLE_0:def 10;
reconsider P' = P as Subset-Family of T by A11;
P' is prebasis of T by A11,A144,YELLOW_9:23;
hence thesis by A11,YELLOW_9:26;
end;
theorem Th17:
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 map of X,S; assume
A4: f is continuous;
reconsider f' = f as map of X,T by A1;
for P being Subset of T st P is open holds (f')"P is open
proof let P be Subset of T; assume
A5: P is open;
reconsider P' = P as Subset of S by A1;
P' in the topology of S by A2,A5,PRE_TOPC:def 5;
then P' is open by PRE_TOPC:def 5;
hence f'"P is open by A4,TOPS_2:55;
end;
then A6: f' is continuous by TOPS_2:55;
let Y be non empty TopSpace; assume
X is SubSpace of Y;
then consider h being map of Y,T such that
A7: h is continuous and
A8: h|(the carrier of X) = f' by A3,A6,Def5;
reconsider g = h as map 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; assume
A9: P is open;
reconsider P' = P as Subset of T by A1;
P' in the topology of T by A2,A9,PRE_TOPC:def 5;
then P' is open by PRE_TOPC:def 5;
hence g"P is open by A7,TOPS_2:55;
end;
hence g is continuous by TOPS_2:55;
thus g|(the carrier of X) = f by A8;
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 1)
holds T is injective
proof
let I be non empty set,
T be Scott TopAugmentation of product (I --> BoolePoset 1);
A1:the RelStr of T = product (I --> BoolePoset 1) by YELLOW_9:def 4;
A2: the topology of T = the topology of product (I --> Sierpinski_Space) by
Th16;
set IB = I --> BoolePoset 1,
IS = I --> Sierpinski_Space;
LattPOSet BooleLatt 1 = RelStr(#the carrier of BooleLatt 1,
LattRel(BooleLatt 1)#) by LATTICE3:def 2;
then A3: the carrier of BoolePoset 1 = the carrier of BooleLatt 1 by YELLOW_1:
def 2 .= bool {{}} by CARD_5:1,LATTICE3:def 1 .= {0,1} by CARD_5:1,ZFMISC_1:30
;
A4: dom Carrier IB = I by PBOOLE:def 3 .= dom Carrier IS by PBOOLE:def 3;
A5: for i being set st i in
dom Carrier IB holds (Carrier IB).i = (Carrier IS).i
proof let i be set; assume i in dom Carrier IB;
then A6: i in I by PBOOLE:def 3;
then consider R1 being 1-sorted such that
A7: R1 = IB.i and
A8: (Carrier IB).i = the carrier of R1 by PRALG_1:def 13;
consider R2 being 1-sorted such that
A9: R2 = IS.i and
A10: (Carrier IS).i = the carrier of R2 by A6,PRALG_1:def 13;
the carrier of R1 = {0,1} by A3,A6,A7,FUNCOP_1:13
.= the carrier of Sierpinski_Space by Def9
.= the carrier of R2 by A6,A9,FUNCOP_1:13;
hence (Carrier IB).i = (Carrier IS).i by A8,A10;
end;
A11: the carrier of T = product Carrier (I --> BoolePoset 1) by A1,YELLOW_1:def
4
.= product Carrier (I --> Sierpinski_Space) by A4,A5,FUNCT_1:9
.= the carrier of product (I --> Sierpinski_Space) by Def3;
for i being Element of I holds (I --> Sierpinski_Space).i is injective
by FUNCOP_1:13;
then product (I --> Sierpinski_Space) is injective by Th8;
hence T is injective by A2,A11,Th17;
end;
theorem Th19: ::p.122 lemma 3.4.(ii)
for T being T_0-TopSpace ex M being non empty set,
f being map of T, product (M --> Sierpinski_Space) st
corestr(f) is_homeomorphism
proof let T be T_0-TopSpace;
take M = the carrier of (InclPoset the topology of T);
set J = M --> Sierpinski_Space;
deffunc F(set) = 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 set st x in the carrier of T holds f.x = F(x) from Lambda;
rng f c= the carrier of product J
proof let y be set; assume
y in rng f;
then consider x being set such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 5;
set ch = chi({u where u is Subset of T: x in u & u is open},
the topology of T);
A5: y = ch by A1,A2,A3,A4;
A6: dom ch = the topology of T by FUNCT_3:def 3
.= M by YELLOW_1:1
.= dom (Carrier J) by PBOOLE:def 3;
for z being set st z in dom (Carrier J) holds ch.z in (Carrier J).z
proof let z be set; assume
z in dom (Carrier J);
then A7: z in M by PBOOLE:def 3;
then A8: z in the topology of T by YELLOW_1:1;
consider R being 1-sorted such that
A9: R = J.z and
A10: (Carrier J).z = the carrier of R by A7,PRALG_1:def 13;
A11: (Carrier J).z = the carrier of Sierpinski_Space by A7,A9,A10,
FUNCOP_1:13 .= {0,1} by Def9;
z in dom ch by A8,FUNCT_3:def 3;
then A12: ch.z in rng ch by FUNCT_1:def 5;
rng ch c= {0,1} by FUNCT_3:48;
hence ch.z in (Carrier J).z by A11,A12;
end;
then y in product Carrier J by A5,A6,CARD_3:def 5;
hence y in the carrier of product J by Def3;
end;
then f is Function of the carrier of T, the carrier of product J
by A1,FUNCT_2:def 1,RELSET_1:11;
then reconsider f as map of T, product J ;
reconsider PP = {product((Carrier J)+*(m,{1})) where m is Element of M:
not contradiction } as prebasis of product J by Th14;
for A being Subset of product J st A in PP holds f"A is open
proof let A be Subset of product J; assume
A13: A in PP;
reconsider a = A as Subset of product Carrier J by Def3;
consider i being Element of M such that
A14: a = product ((Carrier J) +* (i,{1})) by A13;
A15: i in M;
then A16: i in the topology of T by YELLOW_1:1;
then reconsider i' = i as Subset of T;
A17: i in dom (Carrier J) by A15,PBOOLE:def 3;
{1} c= {0,1} by ZFMISC_1:12;
then {1} c= the carrier of Sierpinski_Space by Def9;
then reconsider V = {1} as Subset of Sierpinski_Space;
A18: ((Carrier J)+*(i,V)).i = {1} by A17,FUNCT_7:33;
A19: f"A c= i
proof let z be set; assume
A20: z in f"A;
then A21: f.z in a by FUNCT_1:def 13;
set W = {u where u is Subset of T: z in u & u is open};
f.z = chi(W,the topology of T) by A2,A20;
then consider g being Function such that
A22: chi(W,the topology of T) = g and
dom g = dom ((Carrier J) +* (i,V)) and
A23: for w being set st w in dom ((Carrier J) +* (i,V)) holds
g.w in ((Carrier J) +* (i,V)).w by A14,A21,CARD_3:def 5;
i in dom ((Carrier J) +* (i,V)) by A17,FUNCT_7:32;
then g.i in ((Carrier J) +* (i,V)).i by A23;
then chi(W,the topology of T).i = 1 by A18,A22,TARSKI:def 1;
then i in W by FUNCT_3:42;
then ex uu being Subset of T st i = uu & z in uu & uu is open;
hence z in i;
end;
i c= f"A
proof let z be set; assume
A24: z in i;
set W = {u where u is Subset of T: z in u & u is open};
i' is open by A16,PRE_TOPC:def 5;
then A25: i in W by A24;
A26: z in i' by A24;
then A27: f.z = chi(W,the topology of T) by A2;
A28: 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 PBOOLE:def 3
.= dom ((Carrier J) +* (i,V)) by FUNCT_7:32;
for w being set 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 set; assume
w in dom ((Carrier J) +* (i,V));
then w in dom (Carrier J) by FUNCT_7:32;
then A29: w in M by PBOOLE:def 3;
then w in the topology of T by YELLOW_1:1;
then A30: w in dom chi(W,the topology of T) by FUNCT_3:def 3;
per cases;
suppose
A31: w = i;
then A32: ((Carrier J) +* (i,V)).w = {1} by A17,FUNCT_7:33;
chi(W,the topology of T).w = 1 by A16,A25,A31,FUNCT_3:def 3;
hence chi(W,the topology of T).w in ((Carrier J) +* (i,V)).w
by A32,TARSKI:def 1;
suppose
w <> i;
then A33: ((Carrier J) +* (i,V)).w = (Carrier J).w by FUNCT_7:34;
consider r being 1-sorted such that
A34: r = J.w and
A35: (Carrier J).w = the carrier of r by A29,PRALG_1:def 13;
A36: (Carrier J).w = the carrier of Sierpinski_Space by A29,A34,A35
,FUNCOP_1:13 .= {0,1} by Def9;
A37: rng chi(W,the topology of T) c= {0,1} by FUNCT_3:48;
chi(W,the topology of T).w in rng chi(W,the topology of T)
by A30,FUNCT_1:def 5;
hence chi(W,the topology of T).w in ((Carrier J) +* (i,V)).w
by A33,A36,A37;
end;
then f.z in A by A14,A27,A28,CARD_3:def 5;
hence z in f"A by A1,A26,FUNCT_1:def 13;
end;
then f"A = i by A19,XBOOLE_0:def 10;
hence f"A is open by A16,PRE_TOPC:def 5;
end;
then A38:f is continuous by YELLOW_9:36;
take f;
A39:dom (corestr f) = the carrier of T by FUNCT_2:def 1 .= [#]T by PRE_TOPC:12;
A40:rng (corestr f) = the carrier of Image f by FUNCT_2:def 3
.= [#](Image f) by PRE_TOPC:12;
A41:corestr f is one-to-one
proof let x,y be Element of T; assume
(corestr f).x = (corestr f).y;
then A42: f.x = (corestr f).y by Def7 .= f.y by Def7;
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};
thus x = y
proof assume not thesis;
then consider V being Subset of T such that
A43: V is open and
A44: ((x in V & not y in V) or (y in V & not x in V)) by T_0TOPSP:def 7;
A45: f.x = chi(U1,the topology of T) by A2;
A46: f.y = chi(U2,the topology of T) by A2;
A47: V in the topology of T by A43,PRE_TOPC:def 5;
per cases by A44;
suppose
A48: x in V & not y in V;
reconsider v = V as Subset of T;
A49: 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 A48;
end;
v in U1 by A43,A48;
then chi(U1,the topology of T).v = 1 by A47,FUNCT_3:def 3;
hence thesis by A42,A45,A46,A47,A49,FUNCT_3:def 3;
suppose
A50: y in V & not x in V;
reconsider v = V as Subset of T;
A51: 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 A50;
end;
v in U2 by A43,A50;
then chi(U2,the topology of T).v = 1 by A47,FUNCT_3:def 3;
hence thesis by A42,A45,A46,A47,A51,FUNCT_3:def 3;
end;
end;
A52:corestr f is continuous by A38,Th11;
A53: 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
A54: V is open;
hereby let y be set; assume
y in f.:V;
then consider x being set such that
A55: x in dom f and
A56: x in V and
A57: y = f.x by FUNCT_1:def 12;
set Q = {u where u is Subset of T: x in u & u is open};
A58: V in Q by A54,A56;
A59: y = chi(Q,the topology of T) by A1,A2,A55,A57;
A60: 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 PBOOLE:def 3
.= dom ((Carrier J) +* (V,{1})) by FUNCT_7:32;
for W being set 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 set; assume
W in dom ((Carrier J) +* (V,{1}));
then A61: W in dom (Carrier J) by FUNCT_7:32;
then A62: W in M by PBOOLE:def 3;
then A63: W in the topology of T by YELLOW_1:1;
then A64: W in dom chi(Q,the topology of T) by FUNCT_3:def 3;
per cases;
suppose
A65: W = V;
then A66: ((Carrier J) +* (V,{1})).W = {1} by A61,FUNCT_7:33;
chi(Q,the topology of T).W = 1 by A58,A63,A65,FUNCT_3:def 3;
hence chi(Q,the topology of T).W in ((Carrier J) +* (V,{1})).W
by A66,TARSKI:def 1;
suppose
W <> V;
then A67: ((Carrier J) +* (V,{1})).W = (Carrier J).W by FUNCT_7:34;
consider r being 1-sorted such that
A68: r = J.W and
A69: (Carrier J).W = the carrier of r by A62,PRALG_1:def 13;
A70: (Carrier J).W = the carrier of Sierpinski_Space by A62,A68,A69,
FUNCOP_1:13 .= {0,1} by Def9;
A71: rng chi(Q,the topology of T) c= {0,1} by FUNCT_3:48;
chi(Q,the topology of T).W in rng chi(Q,the topology of T)
by A64,FUNCT_1:def 5;
hence chi(Q,the topology of T).W in ((Carrier J) +* (V,{1})).W
by A67,A70,A71;
end;
then A72: y in product ((Carrier J) +* (V,{1})) by A59,A60,CARD_3:def 5;
y in rng f by A55,A57,FUNCT_1:def 5;
then y in the carrier of Image f by Th10;
hence y in product ((Carrier J) +* (V,{1})) /\ the carrier of Image f
by A72,XBOOLE_0:def 3;
end; let y be set; assume
A73: y in product ((Carrier J) +* (V,{1})) /\ the carrier of Image f;
rng f = the carrier of Image f by Th10;
then y in rng f by A73,XBOOLE_0:def 3;
then consider x being set such that
A74: x in dom f and
A75: y = f.x by FUNCT_1:def 5;
set Q = {u where u is Subset of T: x in u & u is open};
A76: y = chi(Q,the topology of T) by A1,A2,A74,A75;
y in product ((Carrier J) +* (V,{1})) by A73,XBOOLE_0:def 3;
then consider g being Function such that
A77: y = g and
dom g = dom ((Carrier J) +* (V,{1})) and
A78: for W being set st W in dom ((Carrier J) +* (V,{1}))
holds g.W in ((Carrier J) +* (V,{1})).W by CARD_3:def 5;
V in the topology of T by A54,PRE_TOPC:def 5;
then V in M by YELLOW_1:1;
then A79: V in dom (Carrier J) by PBOOLE:def 3;
then V in dom ((Carrier J) +* (V,{1})) by FUNCT_7:32;
then g.V in ((Carrier J) +* (V,{1})).V by A78;
then g.V in {1} by A79,FUNCT_7:33;
then chi(Q,the topology of T).V = 1 by A76,A77,TARSKI:def 1;
then V in Q by FUNCT_3:42;
then ex u being Subset of T st u = V & x in u & u is open;
hence y in f.:V by A74,A75,FUNCT_1:def 12;
end;
for V being Subset of T st V is open holds
((corestr f)")"V is open
proof let V be Subset of T; assume
A80: V is open;
then V in the topology of T by PRE_TOPC:def 5;
then reconsider W = V as Element of M by YELLOW_1:1;
A81: product((Carrier J)+*(W,{1})) in PP;
then reconsider Q = product((Carrier J)+*(V,{1})) as
Subset of product J;
A82: (corestr f).:V = f.:V by Def7
.= product((Carrier J)+*(V,{1})) /\ the carrier of Image f by A53,A80
.= Q /\ [#](Image f) by PRE_TOPC:12;
PP c= the topology of product J by CANTOR_1:def 5;
then (corestr f).:
V in the topology of Image f by A81,A82,PRE_TOPC:def 9;
then (corestr f).:V is open by PRE_TOPC:def 5;
hence ((corestr f)")"V is open by A40,A41,TOPS_2:67;
end;
then (corestr f)" is continuous by TOPS_2:55;
hence corestr(f) is_homeomorphism by A39,A40,A41,A52,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;
consider M being non empty set,
f being map of T, product (M --> Sierpinski_Space) such that
A2: corestr(f) is_homeomorphism by Th19;
T is_Retract_of product (M --> Sierpinski_Space) by A1,A2,Th12;
hence thesis;
end;