:: The Characterization of Continuity of Topologies
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received January 6, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ORDERS_2, YELLOW_0, NEWTON, ZFMISC_1, FUNCT_1,
WAYBEL27, FUNCT_2, RELAT_1, STRUCT_0, SUBSET_1, FUNCOP_1, FUNCT_5,
TARSKI, CAT_1, SEQM_3, XXREAL_0, PRE_TOPC, SETFAM_1, WAYBEL11, WAYBEL_0,
WAYBEL19, WAYBEL24, EQREL_1, ORDINAL2, RCOMP_1, WAYBEL26, XBOOLEAN,
CARD_3, LATTICE3, WAYBEL_9, FUNCTOR0, REWRITE1, YELLOW_9, YELLOW16,
WAYBEL_3, PBOOLE, LATTICES, FINSET_1, FUNCT_4, RELAT_2, WAYBEL25,
PRELAMB, CARD_FIL, YELLOW_1, T_0TOPSP, CONNSP_2, WELLORD1, LATTICE5,
WAYBEL18, CARD_1, FUNCT_3, PROB_1, FUNCT_6, RLVECT_2, WELLORD2, RLVECT_3,
TOPS_1, YELLOW_6, WAYBEL29;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1,
RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3,
FINSET_1, CARD_3, ORDINAL1, NUMBERS, FUNCT_6, FUNCOP_1, ORDERS_1,
STRUCT_0, PRE_TOPC, TOPS_1, T_0TOPSP, CONNSP_2, CANTOR_1, FUNCT_4,
FUNCT_5, FUNCT_7, PRALG_1, WELLORD1, ORDERS_2, LATTICE3, TOPS_2,
YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_5,
WAYBEL_9, YELLOW_6, WAYBEL11, YELLOW_9, BORSUK_1, WAYBEL18, WAYBEL19,
WAYBEL24, WAYBEL25, YELLOW16, WAYBEL26, WAYBEL27;
constructors TOLER_1, FUNCT_7, TOPS_1, TOPS_2, BORSUK_1, T_0TOPSP, CANTOR_1,
MONOID_0, ORDERS_3, WAYBEL_5, WAYBEL11, YELLOW_9, WAYBEL18, WAYBEL24,
YELLOW16, WAYBEL26, WAYBEL27, WAYBEL20, XTUPLE_0;
registrations SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, STRUCT_0,
PRE_TOPC, TOPS_1, BORSUK_1, LATTICE3, YELLOW_0, BORSUK_2, WAYBEL_0,
YELLOW_1, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL10, WAYBEL11, WAYBEL14,
YELLOW_9, WAYBEL18, WAYBEL19, TOPGRP_1, WAYBEL24, YELLOW14, WAYBEL25,
YELLOW16, WAYBEL26, WAYBEL27, RELSET_1, FUNCT_5;
requirements BOOLE, SUBSET;
definitions TARSKI, RELAT_1, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_3,
PRE_TOPC, WAYBEL11, WAYBEL27, XBOOLE_0;
equalities RELAT_1, WAYBEL_3, WAYBEL11, XBOOLE_0, BINOP_1, STRUCT_0;
expansions TARSKI, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_3, PRE_TOPC, WAYBEL11,
WAYBEL27, XBOOLE_0;
theorems TARSKI, ZFMISC_1, GRCAT_1, WELLORD2, SETFAM_1, ENUMSET1, RELAT_1,
FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_5, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_2,
CANTOR_1, FUNCT_4, FUNCT_7, FINSET_1, BORSUK_1, FUNCOP_1, CARD_3,
ORDERS_2, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_9, YELLOW12,
YELLOW14, YELLOW16, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL11, WAYBEL13,
WAYBEL15, WAYBEL17, WAYBEL18, WAYBEL20, WAYBEL21, WAYBEL24, WAYBEL25,
WAYBEL26, WAYBEL27, XBOOLE_0, XBOOLE_1, FUNCT_6, PARTFUN1, XTUPLE_0;
schemes FUNCT_1, PBOOLE;
begin
theorem Th1:
for X,Y being non empty set, Z being non empty RelStr for S being
non empty SubRelStr of Z|^[:X,Y:] for T being non empty SubRelStr of (Z|^Y)|^X
for f being Function of S, T st f is currying one-to-one onto holds f" is
uncurrying
proof
let X,Y be non empty set, Z be non empty RelStr;
let S be non empty SubRelStr of Z|^[:X,Y:];
let T be non empty SubRelStr of (Z|^Y)|^X;
let f be Function of S, T;
assume
A1: f is currying one-to-one onto;
then
A2: rng f = the carrier of T by FUNCT_2:def 3;
A3: f" = f qua Function" by A1,TOPS_2:def 4;
A4: Funcs(X, the carrier of Z|^Y) = the carrier of (Z|^Y)|^X & Funcs(Y, the
carrier of Z) = the carrier of Z|^Y by YELLOW_1:28;
hereby
let x be set;
assume x in dom (f");
then x is Element of (Z|^Y)|^X by YELLOW_0:58;
then x is Function of X, Funcs(Y,the carrier of Z) by A4,FUNCT_2:66;
hence x is Function-yielding Function;
end;
let g be Function;
assume g in dom (f");
then consider h being object such that
A5: h in dom f and
A6: g = f.h by A2,FUNCT_1:def 3;
reconsider h as Function by A5;
Funcs([:X,Y:], the carrier of Z) = the carrier of Z|^[:X,Y:] & h is
Element of Z|^[:X,Y:] by A5,YELLOW_0:58,YELLOW_1:28;
then h is Function of [:X,Y:], the carrier of Z by FUNCT_2:66;
then
A7: dom h = [:X,Y:] by FUNCT_2:def 1;
g = curry h by A1,A5,A6;
then uncurry g = h by A7,FUNCT_5:49;
hence thesis by A1,A3,A5,A6,FUNCT_1:32;
end;
theorem Th2:
for X,Y being non empty set, Z being non empty RelStr for S being
non empty SubRelStr of Z|^[:X,Y:] for T being non empty SubRelStr of (Z|^Y)|^X
for f being Function of T, S st f is uncurrying one-to-one onto holds f" is
currying
proof
let X,Y be non empty set, Z be non empty RelStr;
let S be non empty SubRelStr of Z|^[:X,Y:];
let T be non empty SubRelStr of (Z|^Y)|^X;
let f be Function of T, S;
A1: Funcs(X, the carrier of Z|^Y) = the carrier of (Z|^Y)|^X & Funcs(Y, the
carrier of Z) = the carrier of Z|^Y by YELLOW_1:28;
assume
A2: f is uncurrying one-to-one onto;
then
A3: rng f = the carrier of S by FUNCT_2:def 3;
A4: f" = f qua Function" by A2,TOPS_2:def 4;
A5: Funcs([:X,Y:], the carrier of Z) = the carrier of Z|^[:X,Y:] by YELLOW_1:28
;
hereby
let x be set;
assume x in dom (f");
then x is Element of Z|^[:X,Y:] by YELLOW_0:58;
then reconsider g = x as Function of [:X,Y:], the carrier of Z by A5,
FUNCT_2:66;
dom g = proj1 g;
hence x is Function & proj1 x is Relation;
end;
let g be Function;
assume g in dom (f");
then consider h being object such that
A6: h in dom f and
A7: g = f.h by A3,FUNCT_1:def 3;
reconsider h as Function by A6;
h is Element of (Z|^Y)|^X by A6,YELLOW_0:58;
then h is Function of X, Funcs(Y, the carrier of Z) by A1,FUNCT_2:66;
then
A8: rng h c= Funcs(Y, the carrier of Z) by RELAT_1:def 19;
g = uncurry h by A2,A6,A7;
then curry g = h by A8,FUNCT_5:48;
hence thesis by A2,A4,A6,A7,FUNCT_1:32;
end;
theorem
for X,Y being non empty set, Z being non empty Poset for S being non
empty full SubRelStr of Z|^[:X,Y:] for T being non empty full SubRelStr of (Z|^
Y)|^X for f being Function of S, T st f is currying one-to-one onto holds f is
isomorphic
proof
let X,Y be non empty set, Z be non empty Poset;
let S be non empty full SubRelStr of Z|^[:X,Y:];
let T be non empty full SubRelStr of (Z|^Y)|^X;
let f be Function of S, T;
assume
A1: f is currying one-to-one onto;
then
A2: f*f" = id T & f"*f = id S by GRCAT_1:41;
f is monotone & f" is monotone by A1,Th1,WAYBEL27:20,21;
hence thesis by A2,YELLOW16:15;
end;
theorem
for X,Y being non empty set, Z being non empty Poset for T being non
empty full SubRelStr of Z|^[:X,Y:] for S being non empty full SubRelStr of (Z|^
Y)|^X for f being Function of S, T st f is uncurrying one-to-one onto holds f
is isomorphic
proof
let X,Y be non empty set, Z be non empty Poset;
let T be non empty full SubRelStr of Z|^[:X,Y:];
let S be non empty full SubRelStr of (Z|^Y)|^X;
let f be Function of S, T;
assume
A1: f is uncurrying one-to-one onto;
then
A2: f*f" = id T & f"*f = id S by GRCAT_1:41;
f is monotone & f" is monotone by A1,Th2,WAYBEL27:20,21;
hence thesis by A2,YELLOW16:15;
end;
theorem Th5:
for S1, S2, T1, T2 being RelStr st the RelStr of S1 = the RelStr
of S2 & the RelStr of T1 = the RelStr of T2 for f being Function of S1, T1 st f
is isomorphic for g being Function of S2, T2 st g = f holds g is isomorphic
proof
let S1, S2, T1, T2 be RelStr such that
A1: the RelStr of S1 = the RelStr of S2 and
A2: the RelStr of T1 = the RelStr of T2;
let f be Function of S1, T1 such that
A3: f is isomorphic;
let g be Function of S2, T2 such that
A4: g = f;
per cases;
suppose
A5: S1 is empty;
then T1 is empty by A3,WAYBEL_0:def 38;
then
A6: T2 is empty by A2;
S2 is empty by A1,A5;
hence thesis by A6,WAYBEL_0:def 38;
end;
suppose
S1 is non empty;
then reconsider S1, T1 as non empty RelStr by A3,WAYBEL_0:def 38;
reconsider f as Function of S1, T1;
the carrier of S1 <> {} & the carrier of T1 <> {};
then reconsider S2, T2 as non empty RelStr by A1,A2;
reconsider g as Function of S2, T2;
A7: now
let x,y be Element of S2;
reconsider a = x, b = y as Element of S1 by A1;
A8: x <= y iff a <= b by A1,YELLOW_0:1;
g.x <= g.y iff f.a <= f.b by A2,A4,YELLOW_0:1;
hence x <= y iff g.x <= g.y by A3,A8,WAYBEL_0:66;
end;
rng f = the carrier of T1 by A3,WAYBEL_0:66;
hence thesis by A2,A3,A4,A7,WAYBEL_0:66;
end;
end;
:: Przywlaszczone
theorem Th6: :: stolen from WAYBEL_1:8
for R, S, T being RelStr for f being Function of R, S st f is
isomorphic for g being Function of S, T st g is isomorphic for h being Function
of R, T st h = g*f holds h is isomorphic
proof
let L1,L2,L3 be RelStr;
let f1 be Function of L1,L2 such that
A1: f1 is isomorphic;
let f2 be Function of L2,L3 such that
A2: f2 is isomorphic;
let h be Function of L1,L3 such that
A3: h = f2*f1;
per cases;
suppose
L1 is non empty & L2 is non empty & L3 is non empty;
then reconsider L1,L2,L3 as non empty RelStr;
reconsider f1 as Function of L1,L2;
reconsider f2 as Function of L2,L3;
consider g1 being Function of L2,L1 such that
A4: g1 = (f1 qua Function)" & g1 is monotone by A1,WAYBEL_0:def 38;
consider g2 being Function of L3,L2 such that
A5: g2 = (f2 qua Function)" & g2 is monotone by A2,WAYBEL_0:def 38;
A6: f2*f1 is monotone by A1,A2,YELLOW_2:12;
g1*g2 is monotone & g1*g2 = ((f2*f1) qua Function)" by A1,A2,A4,A5,
FUNCT_1:44,YELLOW_2:12;
hence thesis by A1,A2,A3,A6,WAYBEL_0:def 38;
end;
suppose
A7: L1 is empty;
then L2 is empty by A1,WAYBEL_0:def 38;
then L3 is empty by A2,WAYBEL_0:def 38;
hence thesis by A7,WAYBEL_0:def 38;
end;
suppose
L2 is empty;
then L1 is empty & L3 is empty by A1,A2,WAYBEL_0:def 38;
hence thesis by WAYBEL_0:def 38;
end;
suppose
A8: L3 is empty;
then L2 is empty by A2,WAYBEL_0:def 38;
then L1 is empty by A1,WAYBEL_0:def 38;
hence thesis by A8,WAYBEL_0:def 38;
end;
end;
theorem Th7:
for X,Y,X1,Y1 being TopSpace st the TopStruct of X = the
TopStruct of X1 & the TopStruct of Y = the TopStruct of Y1 holds [:X,Y:] = [:X1
,Y1:]
proof
let X,Y,X1,Y1 be TopSpace;
assume
A1: the TopStruct of X = the TopStruct of X1 & the TopStruct of Y = the
TopStruct of Y1;
set U2 = {union A where A is Subset-Family of [:X1,Y1:]: A c= { [:X2,Y2:]
where X2 is Subset of X1, Y2 is Subset of Y1 : X2 in the topology of X1 & Y2 in
the topology of Y1}};
A2: the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by
BORSUK_1:def 2
.= the carrier of [:X1,Y1:] by A1,BORSUK_1:def 2;
then the topology of [:X,Y:] = U2 by A1,BORSUK_1:def 2
.= the topology of [:X1,Y1:] by BORSUK_1:def 2;
hence thesis by A2;
end;
theorem Th8:
for X being non empty TopSpace for L being Scott up-complete
non empty TopPoset for F being non empty directed Subset of ContMaps(X, L)
holds "\/"(F, L|^the carrier of X) is continuous Function of X, L
proof
let X be non empty TopSpace;
let L be Scott up-complete non empty TopPoset;
let F be non empty directed Subset of ContMaps(X, L);
set sF = "\/"(F, L|^the carrier of X);
Funcs(the carrier of X, the carrier of L) = the carrier of L|^the
carrier of X by YELLOW_1:28;
then reconsider sF as Function of X, L by FUNCT_2:66;
ContMaps(X, L) is full SubRelStr of L|^the carrier of X by WAYBEL24:def 3;
then reconsider
aF = F as non empty directed Subset of L|^the carrier of X by YELLOW_2:7;
A1: now
let A be Subset of L;
assume
A2: A is open;
now
let x be set;
hereby
assume
A3: x in sF"A;
then
A4: sF.x in A by FUNCT_1:def 7;
reconsider y = x as Element of X by A3;
A5: (the carrier of X)-POS_prod ((the carrier of X) => L) = L|^the
carrier of X by YELLOW_1:def 5;
A6: ((the carrier of X) => L).y = L;
then
A7: pi(aF,y) is directed non empty by A5,YELLOW16:35;
A8: ex_sup_of aF, L|^the carrier of X by WAYBEL_0:75;
then (sup aF).y = sup pi(aF,y) by A6,A5,YELLOW16:33;
then pi(aF,y) meets A by A2,A4,A7,WAYBEL11:def 1;
then consider a being object such that
A9: a in pi(aF,y) and
A10: a in A by XBOOLE_0:3;
consider f being Function such that
A11: f in aF and
A12: a = f.y by A9,CARD_3:def 6;
reconsider f as continuous Function of X, L by A11,WAYBEL24:21;
take Q = f"A;
[#]L <> {};
hence Q is open by A2,TOPS_2:43;
A13: dom sF = the carrier of X by FUNCT_2:def 1;
thus Q c= sF"A
proof
let b be object;
assume
A14: b in Q;
then
A15: f.b in A by FUNCT_1:def 7;
reconsider b as Element of X by A14;
A16: ((the carrier of X) => L).b = L;
then pi(aF,b) is directed non empty by A5,YELLOW16:35;
then
A17: ex_sup_of pi(aF,b), L by WAYBEL_0:75;
sF.b = sup pi(aF,b) by A8,A5,A16,YELLOW16:33;
then
A18: sF.b is_>=_than pi(aF,b) by A17,YELLOW_0:30;
f.b in pi(aF,b) by A11,CARD_3:def 6;
then f.b <= sF.b by A18;
then sF.b in A by A2,A15,WAYBEL_0:def 20;
hence thesis by A13,FUNCT_1:def 7;
end;
dom f = the carrier of X by FUNCT_2:def 1;
hence x in Q by A10,A12,FUNCT_1:def 7;
end;
thus (ex Q being Subset of X st Q is open & Q c= sF"A & x in Q) implies
x in sF"A;
end;
hence sF"A is open by TOPS_1:25;
end;
[#]L <> {};
hence thesis by A1,TOPS_2:43;
end;
theorem Th9:
for X being non empty TopSpace for L being Scott up-complete
non empty TopPoset holds ContMaps(X, L) is directed-sups-inheriting SubRelStr
of L|^the carrier of X
proof
let X be non empty TopSpace;
let L be Scott up-complete non empty TopPoset;
reconsider XL = ContMaps(X, L) as non empty full SubRelStr of L|^the carrier
of X by WAYBEL24:def 3;
XL is directed-sups-inheriting
proof
let A be directed Subset of XL;
assume that
A1: A <> {} and
ex_sup_of A, L|^the carrier of X;
reconsider A as directed non empty Subset of XL by A1;
"\/"(A, L|^the carrier of X) is continuous Function of X, L by Th8;
hence thesis by WAYBEL24:def 3;
end;
hence thesis;
end;
theorem Th10:
for S1,S2 being TopStruct st the TopStruct of S1 = the TopStruct
of S2 for T1,T2 being non empty TopRelStr st the TopRelStr of T1 = the
TopRelStr of T2 holds ContMaps(S1,T1) = ContMaps(S2,T2)
proof
let S1,S2 be TopStruct;
assume
A1: the TopStruct of S1 = the TopStruct of S2;
let T1,T2 be non empty TopRelStr;
assume
A2: the TopRelStr of T1 = the TopRelStr of T2;
then the RelStr of T1 = the RelStr of T2;
then T1 |^ the carrier of S1 = T2 |^ the carrier of S2 by A1,WAYBEL27:15;
then reconsider
C2 = ContMaps(S2,T2) as full SubRelStr of T1 |^ the carrier of S1
by WAYBEL24:def 3;
reconsider C1 = ContMaps(S1,T1) as full SubRelStr of T1 |^ the carrier of S1
by WAYBEL24:def 3;
the carrier of ContMaps(S1,T1) = the carrier of ContMaps(S2,T2)
proof
thus the carrier of ContMaps(S1,T1) c= the carrier of ContMaps(S2,T2)
proof
let x be object;
assume x in the carrier of ContMaps(S1,T1);
then consider f being Function of S1,T1 such that
A3: x=f and
A4: f is continuous by WAYBEL24:def 3;
reconsider f2=f as Function of S2,T2 by A1,A2;
f2 is continuous
proof
let P2 be Subset of T2;
reconsider P1=P2 as Subset of T1 by A2;
assume P2 is closed;
then [#]T2 \ P2 is open;
then [#]T2 \ P2 in the topology of T2;
then ([#]T1) \ P1 is open by A2;
then P1 is closed;
then f" P1 is closed by A4;
then [#]S1 \ (f" P1) is open;
then [#]S1 \ (f2" P2) in the topology of S2 by A1;
then [#]S2 \ (f2" P2) is open by A1;
hence thesis;
end;
hence thesis by A3,WAYBEL24:def 3;
end;
let x be object;
assume x in the carrier of ContMaps(S2,T2);
then consider f being Function of S2,T2 such that
A5: x=f and
A6: f is continuous by WAYBEL24:def 3;
reconsider f1=f as Function of S1,T1 by A1,A2;
f1 is continuous
proof
let P1 be Subset of T1;
reconsider P2=P1 as Subset of T2 by A2;
assume P1 is closed;
then [#]T1 \ P1 is open;
then ([#]T1) \ P2 in the topology of T2 by A2;
then ([#]T2) \ P2 is open by A2;
then P2 is closed;
then f" P2 is closed by A6;
then [#]S2 \ (f" P2) is open;
then [#]S2 \ (f1" P1) in the topology of S1 by A1;
then [#]S1 \ (f1" P1) is open by A1;
hence thesis;
end;
hence thesis by A5,WAYBEL24:def 3;
end;
then the RelStr of C1 = the RelStr of C2 by YELLOW_0:57;
hence thesis;
end;
registration
cluster Scott -> injective T_0 for complete continuous TopLattice;
coherence
proof
let T be complete continuous TopLattice;
assume T is Scott;
then T is Scott TopAugmentation of T by YELLOW_9:44;
hence thesis;
end;
end;
registration
cluster Scott continuous complete for TopLattice;
existence
proof
set L = the continuous complete LATTICE;
set T = the Scott TopAugmentation of L;
take T;
thus thesis;
end;
end;
registration
let X be non empty TopSpace;
let L be Scott up-complete non empty TopPoset;
cluster ContMaps(X, L) -> up-complete;
coherence
proof
ContMaps(X, L) is full directed-sups-inheriting SubRelStr of L|^the
carrier of X by Th9,WAYBEL24:def 3;
hence thesis by YELLOW16:5;
end;
end;
theorem Th11:
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I st for i being Element of I holds J.i is up-complete holds I
-POS_prod J is up-complete
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds J.i is up-complete;
set L = I-POS_prod J;
now
let A be non empty directed Subset of L;
now
let x be Element of I;
J.x is up-complete non empty Poset & pi(A,x) is directed non empty
by A1,YELLOW16:35;
hence ex_sup_of pi(A,x), J.x by WAYBEL_0:75;
end;
hence ex_sup_of A,L by YELLOW16:31;
end;
hence thesis by WAYBEL_0:75;
end;
theorem :: stolen (generalized) from WAYBEL_3:33
for I being non empty set for J being Poset-yielding non-Empty
ManySortedSet of I st for i being Element of I holds J.i is up-complete
lower-bounded for x,y being Element of product J holds x << y iff (for i being
Element of I holds x .i << y.i) & ex K being finite Subset of I st for i being
Element of I st not i in K holds x .i = Bottom (J.i)
proof
let I be non empty set;
let J be Poset-yielding non-Empty ManySortedSet of I;
set L = product J;
assume
A1: for i being Element of I holds J.i is up-complete lower-bounded;
then reconsider L9 = L as up-complete non empty Poset by Th11;
let x,y be Element of L;
hereby
assume
A2: x << y;
hereby
let i be Element of I;
thus x .i << y.i
proof
let Di be non empty directed Subset of J.i such that
A3: y.i <= sup Di;
set di = the Element of Di;
set D = {y+*(i,z) where z is Element of J.i: z in Di};
reconsider di as Element of J.i;
A4: dom y = I by WAYBEL_3:27;
D c= the carrier of L
proof
let a be object;
assume a in D;
then consider z being Element of J.i such that
A5: a = y+*(i,z) and
z in Di;
A6: now
let j be Element of I;
i = j or i <> j;
then (y+*(i,z)).j = z & i = j or (y+*(i,z)).j = y.j by A4,
FUNCT_7:31,32;
hence (y+*(i,z)).j is Element of J.j;
end;
dom (y+*(i,z)) = I by A4,FUNCT_7:30;
then a is Element of L by A5,A6,WAYBEL_3:27;
hence thesis;
end;
then reconsider D as Subset of L;
A7: y+*(i,di) in D;
then reconsider D as non empty Subset of L;
D is directed
proof
let z1,z2 be Element of L;
assume z1 in D;
then consider a1 being Element of J.i such that
A8: z1 = y+*(i,a1) and
A9: a1 in Di;
assume z2 in D;
then consider a2 being Element of J.i such that
A10: z2 = y+*(i,a2) and
A11: a2 in Di;
consider a being Element of J.i such that
A12: a in Di and
A13: a >= a1 and
A14: a >= a2 by A9,A11,WAYBEL_0:def 1;
y+*(i,a) in D by A12;
then reconsider z = y+*(i,a) as Element of L;
take z;
thus z in D by A12;
A15: dom y = I by WAYBEL_3:27;
now
let j be Element of I;
i = j or i <> j;
then
z.j = a & z1.j = a1 & i = j or z.j = y.j & z1.j = y.j by A8,A15,
FUNCT_7:31,32;
hence z.j >= z1.j by A13,YELLOW_0:def 1;
end;
hence z >= z1 by WAYBEL_3:28;
now
let j be Element of I;
i = j or i <> j;
then
z.j = a & z2.j = a2 & i = j or z.j = y.j & z2.j = y.j by A10,A15,
FUNCT_7:31,32;
hence z.j >= z2.j by A14,YELLOW_0:def 1;
end;
hence thesis by WAYBEL_3:28;
end;
then reconsider D as non empty directed Subset of L;
A16: dom y = I by WAYBEL_3:27;
now
A17: Di c= pi(D,i)
proof
let a be object;
assume
A18: a in Di;
then reconsider a as Element of J.i;
y+*(i,a) in D by A18;
then (y+*(i,a)).i in pi(D,i) by CARD_3:def 6;
hence thesis by A16,FUNCT_7:31;
end;
let j be Element of I;
A19: J.i is up-complete non empty Poset & J.j is up-complete non
empty Poset by A1;
pi(D,i) is non empty directed by YELLOW16:35;
then
A20: ex_sup_of pi(D,i),J.i by A19,WAYBEL_0:75;
ex_sup_of Di,J.i by A19,WAYBEL_0:75;
then
A21: sup Di <= sup pi(D,i) by A20,A17,YELLOW_0:34;
ex_sup_of D, L9 by WAYBEL_0:75;
then
A22: (sup D).j = sup pi(D,j) by YELLOW16:33;
A23: now
assume j <> i;
then (y+*(i,di)).j = y.j by FUNCT_7:32;
hence y.j in pi(D,j) by A7,CARD_3:def 6;
end;
pi(D,j) is non empty directed by YELLOW16:35;
then ex_sup_of pi(D,j),J.j by A19,WAYBEL_0:75;
then (sup D).j is_>=_than pi(D, j) by A22,YELLOW_0:30;
hence (sup D).j >= y.j by A3,A21,A22,A23,YELLOW_0:def 2;
end;
then sup D >= y by WAYBEL_3:28;
then consider d being Element of L such that
A24: d in D and
A25: d >= x by A2;
consider z being Element of J.i such that
A26: d = y+*(i,z) and
A27: z in Di by A24;
take z;
d.i = z by A4,A26,FUNCT_7:31;
hence thesis by A25,A27,WAYBEL_3:28;
end;
end;
set K = {i where i is Element of I: x .i <> Bottom (J.i)};
K c= I
proof
let a be object;
assume a in K;
then ex i being Element of I st a = i & x . i <> Bottom (J.i);
hence thesis;
end;
then reconsider K as Subset of I;
deffunc F(Element of I) = Bottom (J.$1);
consider f being ManySortedSet of I such that
A28: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A29: now
let i be Element of I;
f.i = Bottom (J.i) by A28;
hence f.i is Element of J.i;
end;
A30: dom f = I by PARTFUN1:def 2;
then reconsider f as Element of product J by A29,WAYBEL_3:27;
set X = the set of all f+*(y|a) where a is finite Subset of I;
X c= the carrier of L
proof
let a be object;
assume a in X;
then consider b being finite Subset of I such that
A31: a = f+*(y|b);
dom y = I by WAYBEL_3:27;
then
A32: dom (y|b) = b by RELAT_1:62;
A33: now
let i be Element of I;
(f+*(y|b)).i = f.i or (f+*(y|b)).i = (y|b).i & (y|b).i = y.i by A32,
FUNCT_1:47,FUNCT_4:11,13;
hence (f+*(y|b)).i is Element of J.i;
end;
I = I \/ dom (y|b) by A32,XBOOLE_1:12
.= dom (f+*(y|b)) by A30,FUNCT_4:def 1;
then a is Element of L by A31,A33,WAYBEL_3:27;
hence thesis;
end;
then reconsider X as Subset of L;
f+*(y|({}I qua finite Subset of I)) in X;
then reconsider X as non empty Subset of L;
X is directed
proof
let z1,z2 be Element of L;
assume z1 in X;
then consider a1 being finite Subset of I such that
A34: z1 = f+*(y|a1);
assume z2 in X;
then consider a2 being finite Subset of I such that
A35: z2 = f+*(y|a2);
reconsider a = a1 \/ a2 as finite Subset of I;
f+*(y|a) in X;
then reconsider z = f+*(y|a) as Element of L;
take z;
thus z in X;
A36: dom y = I by WAYBEL_3:27;
then
A37: dom (y|a) = a by RELAT_1:62;
A38: dom (y|a1) = a1 by A36,RELAT_1:62;
now
let i be Element of I;
A39: f.i = Bottom (J.i) by A28;
J.i is up-complete lower-bounded non empty Poset by A1;
then
A40: Bottom (J.i) <= y.i by YELLOW_0:44;
per cases by XBOOLE_0:def 3;
suppose
A41: not i in a1 & i in a;
then z.i = (y|a).i & (y|a).i = y.i by A37,FUNCT_1:47,FUNCT_4:13;
hence z.i >= z1.i by A34,A38,A40,A39,A41,FUNCT_4:11;
end;
suppose
not i in a & not i in a1;
then z.i = f.i & z1.i = f.i by A34,A37,A38,FUNCT_4:11;
hence z.i >= z1.i by YELLOW_0:def 1;
end;
suppose
A42: i in a1 & i in a;
then
A43: z.i = (y|a).i & (y|a).i = y.i by A37,FUNCT_1:47,FUNCT_4:13;
z1.i = (y|a1).i & (y|a1).i = y. i by A34,A38,A42,FUNCT_1:47
,FUNCT_4:13;
hence z.i >= z1.i by A43,YELLOW_0:def 1;
end;
end;
hence z >= z1 by WAYBEL_3:28;
A44: dom (y|a2) = a2 by A36,RELAT_1:62;
now
let i be Element of I;
A45: f.i = Bottom (J.i) by A28;
J.i is up-complete lower-bounded non empty Poset by A1;
then
A46: Bottom (J.i) <= y.i by YELLOW_0:44;
per cases by XBOOLE_0:def 3;
suppose
A47: not i in a2 & i in a;
then z.i = (y|a).i & (y|a).i = y.i by A37,FUNCT_1:47,FUNCT_4:13;
hence z.i >= z2.i by A35,A44,A46,A45,A47,FUNCT_4:11;
end;
suppose
not i in a & not i in a2;
then z.i = f.i & z2.i = f.i by A35,A37,A44,FUNCT_4:11;
hence z.i >= z2.i by YELLOW_0:def 1;
end;
suppose
A48: i in a2 & i in a;
then
A49: z.i = (y|a).i & (y|a).i = y.i by A37,FUNCT_1:47,FUNCT_4:13;
z2.i = (y|a2).i & (y|a2).i = y. i by A35,A44,A48,FUNCT_1:47
,FUNCT_4:13;
hence z.i >= z2.i by A49,YELLOW_0:def 1;
end;
end;
hence thesis by WAYBEL_3:28;
end;
then reconsider X as non empty directed Subset of L;
now
let i be Element of I;
reconsider a = {i} as finite Subset of I by ZFMISC_1:31;
A50: f+*(y|a) in X;
then reconsider z = f+*(y|a) as Element of L;
ex_sup_of X, L9 by WAYBEL_0:75;
then sup X is_>=_than X by YELLOW_0:30;
then
A51: z <= sup X by A50;
dom y = I by WAYBEL_3:27;
then
A52: dom (y|a) = a by RELAT_1:62;
A53: i in a by TARSKI:def 1;
then (y|a).i = y.i by FUNCT_1:49;
then z.i = y.i by A53,A52,FUNCT_4:13;
hence (sup X).i >= y.i by A51,WAYBEL_3:28;
end;
then y <= sup X by WAYBEL_3:28;
then consider d being Element of L such that
A54: d in X and
A55: x <= d by A2;
consider a being finite Subset of I such that
A56: d = f+*(y|a) by A54;
K c= a
proof
dom y = I by WAYBEL_3:27;
then
A57: dom (y|a) = a by RELAT_1:62;
let j be object;
assume j in K;
then consider i being Element of I such that
A58: j = i and
A59: x .i <> Bottom (J.i);
J.i is up-complete lower-bounded non empty Poset by A1;
then
A60: x .i >= Bottom (J.i) by YELLOW_0:44;
assume not j in a;
then
A61: d.i = f.i by A56,A58,A57,FUNCT_4:11
.= Bottom (J.i) by A28;
x .i <= d.i by A55,WAYBEL_3:28;
hence contradiction by A59,A61,A60,ORDERS_2:2;
end;
then reconsider K as finite Subset of I;
take K;
thus for i being Element of I st not i in K holds x .i = Bottom (J.i);
end;
defpred P[object,object] means
ex i being Element of I, z being Element of L st $1
= i & $2 = z & z.i >= x .i;
assume
A62: for i being Element of I holds x .i << y.i;
given K being finite Subset of I such that
A63: for i being Element of I st not i in K holds x .i = Bottom (J.i);
let D be non empty directed Subset of L such that
A64: y <= sup D;
A65: now
let k be object;
assume k in K;
then reconsider i = k as Element of I;
A66: pi(D,i) is directed
proof
let a,b be Element of J.i;
assume a in pi(D,i);
then consider f being Function such that
A67: f in D and
A68: a = f.i by CARD_3:def 6;
assume b in pi(D,i);
then consider g being Function such that
A69: g in D and
A70: b = g.i by CARD_3:def 6;
reconsider f,g as Element of L by A67,A69;
consider h being Element of L such that
A71: h in D & h >= f & h >= g by A67,A69,WAYBEL_0:def 1;
take h.i;
thus thesis by A68,A70,A71,CARD_3:def 6,WAYBEL_3:28;
end;
ex_sup_of D, L9 by WAYBEL_0:75;
then
A72: (sup D).i = sup pi(D,i) by YELLOW16:33;
x .i << y.i & y.i <= (sup D).i by A62,A64,WAYBEL_3:28;
then consider zi being Element of J.i such that
A73: zi in pi(D,i) and
A74: zi >= x .i by A66,A72;
consider a being Function such that
A75: a in D and
A76: zi = a.i by A73,CARD_3:def 6;
reconsider a as object;
take a;
thus a in D by A75;
thus P[k,a] by A74,A75,A76;
end;
consider F being Function such that
A77: dom F = K & rng F c= D and
A78: for k being object st k in K holds P[k,F.k] from FUNCT_1:sch 6(A65);
reconsider Y = rng F as finite Subset of D by A77,FINSET_1:8;
consider d being Element of L such that
A79: d in D and
A80: d is_>=_than Y by WAYBEL_0:1;
take d;
thus d in D by A79;
now
let i be Element of I;
A81: J.i is up-complete lower-bounded non empty Poset by A1;
per cases;
suppose
A82: i in K;
then consider j being Element of I, z being Element of L such that
A83: i = j and
A84: F.i = z and
A85: z.j >= x .j by A78;
z in Y by A77,A82,A84,FUNCT_1:def 3;
then d >= z by A80;
then d.i >= z.i by WAYBEL_3:28;
hence d.i >= x .i by A81,A83,A85,YELLOW_0:def 2;
end;
suppose
not i in K;
then x .i = Bottom (J.i) by A63;
hence d.i >= x .i by A81,YELLOW_0:44;
end;
end;
hence thesis by WAYBEL_3:28;
end;
registration
let X be set;
let L be lower-bounded non empty reflexive antisymmetric RelStr;
cluster L|^X -> lower-bounded;
coherence
proof
A1: rng (X --> Bottom L) c= the carrier of L;
the carrier of L|^X = Funcs(X, the carrier of L) & dom (X --> Bottom L
) = X by YELLOW_1:28;
then reconsider f = X --> Bottom L as Element of L|^X by A1,FUNCT_2:def 2;
take f;
let g be Element of L|^X;
per cases;
suppose
A2: X is empty;
A3: f <= f;
L|^X = RelStr (#{{}}, id {{}}#) & f = {} by A2,YELLOW_1:27;
hence thesis by A3,TARSKI:def 1;
end;
suppose
X is non empty;
then reconsider X as non empty set;
reconsider f, g as Element of L|^X;
for x be Element of X holds f.x <= g.x by YELLOW_0:44;
hence thesis by WAYBEL27:14;
end;
end;
end;
registration
let X be non empty TopSpace;
let L be lower-bounded non empty TopPoset;
cluster ContMaps(X, L) -> lower-bounded;
coherence
proof
reconsider f = X --> Bottom L as Element of ContMaps(X, L) by WAYBEL24:21;
take f;
let g be Element of ContMaps(X, L);
A1: ContMaps(X, L) is full SubRelStr of L|^the carrier of X by WAYBEL24:def 3;
then reconsider a = g as Element of L|^the carrier of X by YELLOW_0:58;
A2: the TopStruct of Omega X = the TopStruct of X by WAYBEL25:def 2;
then (Omega X) --> Bottom L = (the carrier of X) --> Bottom L
.= X --> Bottom L;
then a >= Bottom (L|^the carrier of X) & Bottom (L|^the carrier of X) = f
by A2,WAYBEL24:33,YELLOW_0:44;
hence thesis by A1,YELLOW_0:60;
end;
end;
registration
let L be up-complete non empty Poset;
cluster -> up-complete for TopAugmentation of L;
coherence
proof
let S be TopAugmentation of L;
the RelStr of L = the RelStr of S by YELLOW_9:def 4;
hence thesis by WAYBEL_8:15;
end;
cluster Scott -> correct for TopAugmentation of L;
coherence
proof
let IT be TopAugmentation of L;
assume
A1: IT is Scott;
then [#]IT is open;
hence the carrier of IT in the topology of IT;
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
A2: a c= the topology of IT;
A3: union a is inaccessible
proof
let D be non empty directed Subset of IT;
assume sup D in union a;
then consider A being set such that
A4: sup D in A and
A5: A in a by TARSKI:def 4;
reconsider A as Subset of IT by A5;
A is open by A2,A5;
then D meets A by A1,A4,WAYBEL11:def 1;
then consider x being object such that
A6: x in D and
A7: x in A by XBOOLE_0:3;
x in union a by A5,A7,TARSKI:def 4;
hence thesis by A6,XBOOLE_0:3;
end;
now
let X be Subset of IT;
assume X in a;
then X is open by A2;
hence X is upper by A1;
end;
then union a is upper by WAYBEL_0:28;
hence thesis by A1,A3,PRE_TOPC:def 2;
end;
thus for a,b being Subset of IT st a in the topology of IT & b in the
topology of IT holds a /\ b in the topology of IT
proof
let a,b be Subset of IT;
assume that
A8: a in the topology of IT and
A9: b in the topology of IT;
reconsider a1=a,b1=b as Subset of IT;
A10: b1 is open by A9;
A11: a1 is open by A8;
A12: a /\ b is inaccessible
proof
let D be non empty directed Subset of IT;
assume
A13: sup D in a /\ b;
then sup D in a1 by XBOOLE_0:def 4;
then D meets a1 by A1,A11,WAYBEL11:def 1;
then consider d1 being object such that
A14: d1 in D and
A15: d1 in a1 by XBOOLE_0:3;
sup D in b1 by A13,XBOOLE_0:def 4;
then D meets b1 by A1,A10,WAYBEL11:def 1;
then consider d2 being object such that
A16: d2 in D and
A17: d2 in b1 by XBOOLE_0:3;
reconsider d1,d2 as Element of IT by A14,A16;
consider z being Element of IT such that
A18: z in D and
A19: d1 <= z and
A20: d2 <= z by A14,A16,WAYBEL_0:def 1;
A21: z in b1 by A1,A10,A17,A20,WAYBEL_0:def 20;
z in a1 by A1,A11,A15,A19,WAYBEL_0:def 20;
then z in a /\ b by A21,XBOOLE_0:def 4;
hence thesis by A18,XBOOLE_0:3;
end;
a /\ b is upper by A1,A11,A10,WAYBEL_0:29;
hence thesis by A1,A12,PRE_TOPC:def 2;
end;
end;
end;
registration
let L be up-complete non empty Poset;
cluster strict Scott for TopAugmentation of L;
existence
proof
set T = {S where S is Subset of L : S is upper inaccessible};
T c= bool the carrier of L
proof
let x be object;
assume x in T;
then ex S being Subset of L st x=S & S is upper inaccessible;
hence thesis;
end;
then reconsider T as Subset-Family of L;
set SL=TopRelStr(#the carrier of L, the InternalRel of L, T#);
A1: the RelStr of L = the RelStr of SL;
then reconsider SL as TopAugmentation of L by YELLOW_9:def 4;
take SL;
for S being Subset of SL holds S is open iff S is inaccessible upper
proof
let S be Subset of SL;
thus S is open implies S is inaccessible upper
proof
assume S is open;
then S in T;
then ex S1 being Subset of L st S1=S & S1 is upper inaccessible;
hence thesis by A1,WAYBEL_0:25,YELLOW_9:47;
end;
thus S is inaccessible upper implies S is open
proof
reconsider S1=S as Subset of L;
assume S is inaccessible upper;
then S1 is inaccessible upper by A1,WAYBEL_0:25,YELLOW_9:47;
then S in the topology of SL;
hence thesis;
end;
end;
hence thesis;
end;
end;
theorem Th13:
for L being up-complete non empty Poset for S1, S2 being Scott
TopAugmentation of L holds the topology of S1 = the topology of S2
proof
let L be up-complete non empty Poset;
let S1, S2 be Scott TopAugmentation of L;
A1: the RelStr of S1 = the RelStr of L by YELLOW_9:def 4
.= the RelStr of S2 by YELLOW_9:def 4;
thus the topology of S1 c= the topology of S2
proof
let x be object;
assume x in the topology of S1;
then reconsider y=x as open Subset of S1 by PRE_TOPC:def 2;
reconsider z=y as Subset of S2 by A1;
z is inaccessible upper by A1,WAYBEL_0:25,YELLOW_9:47;
hence thesis by PRE_TOPC:def 2;
end;
let x be object;
assume x in the topology of S2;
then reconsider y=x as open Subset of S2 by PRE_TOPC:def 2;
reconsider z=y as Subset of S1 by A1;
z is inaccessible upper by A1,WAYBEL_0:25,YELLOW_9:47;
hence thesis by PRE_TOPC:def 2;
end;
theorem Th14:
for S1, S2 being up-complete antisymmetric non empty reflexive
TopRelStr st the TopRelStr of S1 = the TopRelStr of S2 & S1 is Scott holds S2
is Scott
proof
let S1, S2 be up-complete antisymmetric non empty reflexive TopRelStr;
assume
A1: the TopRelStr of S1 = the TopRelStr of S2;
assume
A2: S1 is Scott;
let T be Subset of S2;
reconsider T1=T as Subset of S1 by A1;
A3: the RelStr of S1 = the RelStr of S2 by A1;
thus T is open implies T is inaccessible upper
proof
assume T is open;
then T in the topology of S2;
then T1 is open by A1;
hence thesis by A3,A2,WAYBEL_0:25,YELLOW_9:47;
end;
thus T is inaccessible upper implies T is open
proof
assume T is inaccessible upper;
then T1 is inaccessible upper by A3,WAYBEL_0:25,YELLOW_9:47;
then T1 in the topology of S1 by A2,PRE_TOPC:def 2;
hence thesis by A1;
end;
end;
definition
let L be up-complete non empty Poset;
func Sigma L -> strict Scott TopAugmentation of L means
: Def1:
not contradiction;
uniqueness
proof
let S1,S2 be strict Scott TopAugmentation of L;
the RelStr of S1 = the RelStr of L & the RelStr of S2 = the RelStr of
L by YELLOW_9:def 4;
hence thesis by Th13;
end;
existence;
end;
theorem Th15:
for S being Scott up-complete non empty TopPoset holds Sigma S
= the TopRelStr of S
proof
let S be Scott up-complete non empty TopPoset;
the RelStr of the TopRelStr of S = the RelStr of S;
then reconsider T = the TopRelStr of S as TopAugmentation of S by
YELLOW_9:def 4;
T is Scott by Th14;
hence thesis by Def1;
end;
theorem Th16:
for L1, L2 being up-complete non empty Poset st the RelStr of
L1 = the RelStr of L2 holds Sigma L1 = Sigma L2
proof
let L1, L2 be up-complete non empty Poset;
assume the RelStr of L1 = the RelStr of L2;
then
A1: the RelStr of Sigma L2 = the RelStr of L1 by YELLOW_9:def 4;
then
the RelStr of Sigma L1 = the RelStr of L1 & Sigma L2 is TopAugmentation
of L1 by YELLOW_9:def 4;
hence thesis by A1,Th13;
end;
definition
let S,T be up-complete non empty Poset;
let f be Function of S,T;
func Sigma f -> Function of Sigma S, Sigma T equals
f;
coherence
proof
the RelStr of Sigma S = the RelStr of S & the RelStr of Sigma T = the
RelStr of T by YELLOW_9:def 4;
hence thesis;
end;
end;
registration
let S,T be up-complete non empty Poset;
let f be directed-sups-preserving Function of S,T;
cluster Sigma f -> continuous;
coherence
proof
the RelStr of Sigma S = the RelStr of S & the RelStr of Sigma T = the
RelStr of T by YELLOW_9:def 4;
hence thesis by WAYBEL17:29,WAYBEL21:6;
end;
end;
theorem
for S, T being up-complete non empty Poset for f being Function of S
, T holds f is isomorphic iff Sigma f is isomorphic
proof
let S, T be up-complete non empty Poset;
let f be Function of S, T;
the RelStr of Sigma S = the RelStr of S & the RelStr of Sigma T = the
RelStr of T by YELLOW_9:def 4;
hence thesis by Th5;
end;
theorem Th18:
for X being non empty TopSpace for S being Scott complete
TopLattice holds oContMaps(X, S) = ContMaps(X, S)
proof
let X be non empty TopSpace;
let S be Scott complete TopLattice;
A1: Omega S = the TopRelStr of S & the TopStruct of X = the TopStruct of X
by WAYBEL25:15;
thus oContMaps(X, S) = ContMaps(X, Omega S) by WAYBEL26:def 1
.= ContMaps(X, S) by A1,Th10;
end;
definition
let X,Y be non empty TopSpace;
func Theta(X,Y) -> Function of InclPoset the topology of [:X, Y:], ContMaps(
X, Sigma InclPoset the topology of Y) means
: Def3:
for W being open Subset of [:X, Y:] holds it.W = (W, the carrier of X)*graph;
existence
proof
Omega Sigma InclPoset the topology of Y = Sigma InclPoset the topology
of Y by WAYBEL25:15;
then
(ex F being Function of InclPoset the topology of [:X, Y:], oContMaps(
X, Sigma InclPoset the topology of Y) st F is monotone & for W being open
Subset of [:X,Y:] holds F.W = (W, the carrier of X)*graph )& oContMaps(X, Sigma
InclPoset the topology of Y) = ContMaps(X, Sigma InclPoset the topology of Y)
by WAYBEL26:45,def 1;
hence thesis;
end;
correctness
proof
let F,G be Function of InclPoset the topology of [:X, Y:], ContMaps(X,
Sigma InclPoset the topology of Y) such that
A1: for W being open Subset of [:X, Y:] holds F.W = (W, the carrier of
X)*graph and
A2: for W being open Subset of [:X, Y:] holds G.W = (W, the carrier of
X)*graph;
now
let x be Element of InclPoset the topology of [:X, Y:];
the carrier of InclPoset the topology of [:X, Y:] = the topology of
[:X, Y:] by YELLOW_1:1;
then x in the topology of [:X, Y:];
then reconsider W = x as open Subset of [:X,Y:] by PRE_TOPC:def 2;
thus F.x = (W, the carrier of X)*graph by A1
.= G.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
end;
defpred a4101[T_0-TopSpace] means for X being non empty TopSpace for L being
Scott continuous complete TopLattice for T being Scott TopAugmentation of
ContMaps($1, L) ex f being Function of ContMaps(X, T), ContMaps([:X, $1:], L),
g being Function of ContMaps([:X, $1:], L), ContMaps(X, T) st f is uncurrying
one-to-one onto & g is currying one-to-one onto;
defpred a41019[T_0-TopSpace] means for X being non empty TopSpace for L being
Scott continuous complete TopLattice for T being Scott TopAugmentation of
ContMaps($1, L) ex f being Function of ContMaps(X, T), ContMaps([:X, $1:], L),
g being Function of ContMaps([:X, $1:], L), ContMaps(X, T) st f is uncurrying
isomorphic & g is currying isomorphic;
defpred a4102[T_0-TopSpace] means for X being non empty TopSpace holds Theta(X
, $1) is isomorphic;
defpred a4103[T_0-TopSpace] means for X being non empty TopSpace for T being
Scott TopAugmentation of InclPoset the topology of $1 for f being continuous
Function of X, T holds *graph f is open Subset of [:X, $1:];
defpred a4104[T_0-TopSpace] means for T being Scott TopAugmentation of
InclPoset the topology of $1 holds {[W,y] where W is open Subset of $1, y is
Element of $1: y in W} is open Subset of [:T, $1:];
defpred a4105[T_0-TopSpace] means for S being Scott TopAugmentation of
InclPoset the topology of $1 for y being Element of $1, V being open
a_neighborhood of y ex H being open Subset of S st V in H & meet H is
a_neighborhood of y;
Lm1: for T being T_0-TopSpace holds a4101[T] iff a41019[T]
proof
let T be T_0-TopSpace;
thus a4101[T] implies a41019[T]
proof
assume
A1: a4101[T];
let X be non empty TopSpace;
let L be Scott continuous complete TopLattice;
let S be Scott TopAugmentation of ContMaps(T, L);
consider f being Function of ContMaps(X, S), ContMaps([:X, T:], L), g
being Function of ContMaps([:X, T:], L), ContMaps(X, S) such that
A2: f is uncurrying one-to-one onto and
A3: g is currying one-to-one onto by A1;
A4: the RelStr of S = the RelStr of ContMaps(T,L) by YELLOW_9:def 4;
A5: ContMaps(T,L) is full non empty SubRelStr of (L|^the carrier of T) by
WAYBEL24:def 3;
then
A6: the InternalRel of ContMaps(T,L) = (the InternalRel of (L|^the carrier
of T))|_2 the carrier of ContMaps(T,L) by YELLOW_0:def 14;
the carrier of ContMaps(T,L) c= the carrier of L|^the carrier of T &
the InternalRel of ContMaps(T,L) c= the InternalRel of L|^the carrier of T by
A5,YELLOW_0:def 13;
then S is full non empty SubRelStr of (L|^the carrier of T) by A4,A6,
YELLOW_0:def 13,def 14;
then
A7: S |^ the carrier of X is full non empty SubRelStr of (L|^the carrier
of T) |^ the carrier of X by YELLOW16:39;
L|^ the carrier of [:X,T:] = L|^[:the carrier of X,the carrier of T
:] by BORSUK_1:def 2;
then
A8: ContMaps([:X, T:], L) is full non empty SubRelStr of L|^[:the carrier
of X,the carrier of T:] by WAYBEL24:def 3;
ContMaps(X, S) is full non empty SubRelStr of S|^the carrier of X by
WAYBEL24:def 3;
then
ContMaps(X, S) is full non empty SubRelStr of (L|^the carrier of T)|^
the carrier of X by A7,WAYBEL15:1;
then
A9: f is monotone & g is monotone by A2,A3,A8,WAYBEL27:20,21;
take f,g;
ContMaps(T,L) is full non empty SubRelStr of L|^the carrier of T by
WAYBEL24:def 3;
then ContMaps(T,L)|^the carrier of X is full SubRelStr of (L|^the carrier
of T)|^the carrier of X by YELLOW16:39;
then
A10: the carrier of ContMaps(T,L)|^the carrier of X c= the carrier of (L|^
the carrier of T)|^the carrier of X by YELLOW_0:def 13;
A11: rng f = the carrier of ContMaps([:X, T:], L) by A2,FUNCT_2:def 3
.= dom g by FUNCT_2:def 1;
ContMaps(X, S) is non empty full SubRelStr of S|^the carrier of X by
WAYBEL24:def 3;
then the carrier of ContMaps(X, S) c= the carrier of (S|^the carrier of X
) by YELLOW_0:def 13;
then dom f c= the carrier of (S|^the carrier of X);
then dom f c= the carrier of ContMaps(T,L)|^the carrier of X by A4,
WAYBEL27:15;
then dom f c= the carrier of (L|^the carrier of T)|^the carrier of X by A10
;
then dom f c= Funcs(the carrier of X,the carrier of L|^the carrier of T)
by YELLOW_1:28;
then
dom f c= Funcs(the carrier of X,Funcs(the carrier of T,the carrier of
L)) by YELLOW_1:28;
then g*f = id dom f by A2,A3,A11,WAYBEL27:4;
then g = f qua Function" by A2,A11,FUNCT_1:41;
hence f is uncurrying isomorphic by A2,A9,WAYBEL_0:def 38;
A12: rng g = the carrier of ContMaps(X, S) by A3,FUNCT_2:def 3
.= dom f by FUNCT_2:def 1;
ContMaps([:X,T:],L) is non empty full SubRelStr of L |^ the carrier
of [:X,T:] by WAYBEL24:def 3;
then the carrier of ContMaps([:X,T:],L) c= the carrier of (L |^ the
carrier of [:X,T:]) by YELLOW_0:def 13;
then dom g c= the carrier of (L |^ the carrier of [:X,T:]);
then dom g c= Funcs(the carrier of [:X,T:],the carrier of L) by YELLOW_1:28
;
then
dom g c= Funcs([:the carrier of X,the carrier of T:],the carrier of L
) by BORSUK_1:def 2;
then f*g = id dom g by A2,A3,A12,WAYBEL27:5;
then f = g qua Function" by A3,A12,FUNCT_1:41;
hence thesis by A3,A9,WAYBEL_0:def 38;
end;
assume
A13: a41019[T];
let X be non empty TopSpace;
let L be Scott continuous complete TopLattice;
let S be Scott TopAugmentation of ContMaps(T, L);
consider f being Function of ContMaps(X, S), ContMaps([:X, T:], L), g being
Function of ContMaps([:X, T:], L), ContMaps(X, S) such that
A14: f is uncurrying isomorphic and
A15: g is currying isomorphic by A13;
take f,g;
thus f is uncurrying one-to-one onto by A14;
thus thesis by A15;
end;
begin :: Some Natural Isomorphisms
definition
let X be non empty TopSpace;
func alpha X -> Function of oContMaps(X, Sierpinski_Space), InclPoset the
topology of X means
: Def4:
for g being continuous Function of X, Sierpinski_Space holds it.g = g"{1};
existence
proof
deffunc F(Function) = $1"{1};
consider f being Function such that
A1: dom f = the carrier of oContMaps(X, Sierpinski_Space) and
A2: for x being Element of oContMaps(X, Sierpinski_Space) holds f.x =
F(x) from FUNCT_1:sch 4;
rng f c= the topology of X
proof
the topology of Sierpinski_Space = {{}, {1}, {0,1}} by WAYBEL18:def 9;
then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;
then reconsider A = {1} as open Subset of Sierpinski_Space by
PRE_TOPC:def 2;
let y be object;
assume y in rng f;
then consider x being object such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 3;
reconsider x as Element of oContMaps(X, Sierpinski_Space) by A1,A3;
reconsider g = x as continuous Function of X, Sierpinski_Space by
WAYBEL26:2;
[#]Sierpinski_Space <> {};
then
A5: g"A is open by TOPS_2:43;
y = g"A by A2,A4;
hence thesis by A5;
end;
then rng f c= the carrier of InclPoset the topology of X by YELLOW_1:1;
then reconsider
f as Function of oContMaps(X, Sierpinski_Space), InclPoset the
topology of X by A1,FUNCT_2:2;
take f;
let g be continuous Function of X, Sierpinski_Space;
g is Element of oContMaps(X, Sierpinski_Space) by WAYBEL26:2;
hence thesis by A2;
end;
uniqueness
proof
let f1, f2 be Function of oContMaps(X, Sierpinski_Space), InclPoset the
topology of X such that
A6: for g being continuous Function of X, Sierpinski_Space holds f1.g
= g"{1} and
A7: for g being continuous Function of X, Sierpinski_Space holds f2.g = g"{1};
now
let x be Element of oContMaps(X, Sierpinski_Space);
reconsider g = x as continuous Function of X, Sierpinski_Space by
WAYBEL26:2;
thus f1.x = g"{1} by A6
.= f2.x by A7;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
for X being non empty TopSpace for V being open Subset of X holds (
alpha X)".V = chi(V, the carrier of X)
proof
A1: the carrier of Sierpinski_Space = {0, 1} by WAYBEL18:def 9;
the topology of Sierpinski_Space = {{}, {1}, {0,1}} by WAYBEL18:def 9;
then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;
then reconsider A = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def 2;
let X be non empty TopSpace;
consider f be Function of InclPoset the topology of X, oContMaps(X,
Sierpinski_Space) such that
A2: f is isomorphic and
A3: for V being open Subset of X holds f.V = chi(V, the carrier of X) by
WAYBEL26:5;
A4: the carrier of InclPoset the topology of X = the topology of X by
YELLOW_1:1;
A5: rng f = [#]oContMaps(X, Sierpinski_Space) by A2,WAYBEL_0:66;
A6: f" = f qua Function" by A2,TOPS_2:def 4;
now
let x be Element of oContMaps(X, Sierpinski_Space);
reconsider g = x as continuous Function of X, Sierpinski_Space by
WAYBEL26:2;
[#]Sierpinski_Space <> {};
then
A7: g"A is open by TOPS_2:43;
then
A8: g"A in the topology of X;
A9: f.(g"A) = chi(g"A, the carrier of X) by A3,A7
.= x by A1,FUNCT_3:40;
thus (alpha X).x = g"A by Def4
.= f".x by A2,A6,A4,A8,A9,FUNCT_2:26;
end;
then alpha X = f" by FUNCT_2:63;
then (alpha X)" = f by A2,A5,TOPS_2:51;
hence thesis by A3;
end;
registration
let X be non empty TopSpace;
cluster alpha X -> isomorphic;
coherence
proof
the topology of Sierpinski_Space = {{}, {1}, {0,1}} by WAYBEL18:def 9;
then {1} in the topology of Sierpinski_Space by ENUMSET1:def 1;
then reconsider A = {1} as open Subset of Sierpinski_Space by
PRE_TOPC:def 2;
consider f be Function of InclPoset the topology of X, oContMaps(X,
Sierpinski_Space) such that
A1: f is isomorphic and
A2: for V being open Subset of X holds f.V = chi(V, the carrier of X)
by WAYBEL26:5;
A3: f" = f qua Function" by A1,TOPS_2:def 4;
A4: the carrier of InclPoset the topology of X = the topology of X by
YELLOW_1:1;
A5: the carrier of Sierpinski_Space = {0, 1} by WAYBEL18:def 9;
now
let x be Element of oContMaps(X, Sierpinski_Space);
reconsider g = x as continuous Function of X, Sierpinski_Space by
WAYBEL26:2;
[#]Sierpinski_Space <> {};
then
A6: g"A is open by TOPS_2:43;
then
A7: g"A in the topology of X;
A8: f.(g"A) = chi(g"A, the carrier of X) by A2,A6
.= x by A5,FUNCT_3:40;
thus (alpha X).x = g"A by Def4
.= f".x by A1,A3,A4,A7,A8,FUNCT_2:26;
end;
hence thesis by A1,A3,FUNCT_2:63,WAYBEL_0:68;
end;
end;
registration
let X be non empty TopSpace;
cluster (alpha X)" -> isomorphic;
coherence by YELLOW14:10;
end;
registration
let S be injective T_0-TopSpace;
cluster Omega S -> Scott;
coherence
proof
set T = the strict Scott TopAugmentation of Omega S;
A1: the TopStruct of T = the TopStruct of S by WAYBEL25:37
.= the TopStruct of Omega S by WAYBEL25:def 2;
the RelStr of T = the RelStr of Omega S by YELLOW_9:def 4;
hence thesis by A1;
end;
end;
registration
let X be non empty TopSpace;
cluster oContMaps(X, Sierpinski_Space) -> complete;
coherence
proof
InclPoset the topology of X, oContMaps(X, Sierpinski_Space)
are_isomorphic by WAYBEL26:6;
hence thesis by WAYBEL20:18;
end;
end;
theorem
Omega Sierpinski_Space = Sigma BoolePoset{0}
proof
set S = Sigma BoolePoset{0};
reconsider T = Omega Sierpinski_Space as Scott strict TopAugmentation of
BoolePoset{0} by WAYBEL26:4;
A1: the topology of T = sigma BoolePoset{0} by YELLOW_9:51
.= the topology of S by YELLOW_9:51;
the RelStr of T = BoolePoset{0} by YELLOW_9:def 4
.= the RelStr of S by YELLOW_9:def 4;
hence thesis by A1;
end;
registration
let M be non empty set;
let S be injective T_0-TopSpace;
cluster M-TOP_prod (M => S) -> injective;
coherence
proof
for m being Element of M holds (M => S).m is injective;
hence thesis by WAYBEL18:7;
end;
end;
theorem
for M being non empty set, L being complete continuous LATTICE holds
Omega (M-TOP_prod (M => Sigma L)) = Sigma (M-POS_prod (M => L))
proof
let M be non empty set, L be complete continuous LATTICE;
A1: the RelStr of Sigma L = the RelStr of L by YELLOW_9:def 4;
reconsider S = Sigma L as injective T_0-TopSpace;
Omega Sigma L = Sigma L by WAYBEL25:15;
then
the RelStr of Omega (M-TOP_prod (M => Sigma L)) = M-POS_prod (M => Sigma
L) by WAYBEL25:14
.= (Sigma L)|^M by YELLOW_1:def 5
.= L|^M by A1,WAYBEL27:15;
then Sigma (L|^M) = Sigma Omega (M-TOP_prod (M => S)) by Th16
.= Omega (M-TOP_prod (M => Sigma L)) by Th15;
hence thesis by YELLOW_1:def 5;
end;
theorem
for M being non empty set, T being injective T_0-TopSpace holds Omega
(M-TOP_prod (M => T)) = Sigma (M-POS_prod (M => Omega T))
proof
let M be non empty set, T be injective T_0-TopSpace;
set L = Omega T;
the RelStr of Omega (M-TOP_prod (M => T)) = M-POS_prod (M => L) by
WAYBEL25:14;
then Sigma Omega (M-TOP_prod (M => T)) = Sigma (M-POS_prod (M => L)) by Th16;
hence thesis by Th15;
end;
definition
let M be non empty set;
let X,Y be non empty TopSpace;
func commute(X, M, Y) -> Function of oContMaps(X, M-TOP_prod (M => Y)),
oContMaps(X, Y)|^M means
: Def5:
for f being continuous Function of X, M
-TOP_prod (M => Y) holds it.f = commute f;
uniqueness
proof
let F1, F2 be Function of oContMaps(X, M-TOP_prod (M => Y)), oContMaps(X,
Y)|^M such that
A1: for f being continuous Function of X, M-TOP_prod (M => Y) holds F1
.f = commute f and
A2: for f being continuous Function of X, M-TOP_prod (M => Y) holds F2
.f = commute f;
now
let f be Element of oContMaps(X, M-TOP_prod (M => Y));
reconsider g = f as continuous Function of X, M-TOP_prod (M => Y) by
WAYBEL26:2;
thus F1.f = commute g by A1
.= F2.f by A2;
end;
hence thesis by FUNCT_2:63;
end;
existence
proof
deffunc F(Function) = commute $1;
consider F being Function such that
A3: dom F = the carrier of oContMaps(X, M-TOP_prod (M => Y)) and
A4: for f being Element of oContMaps(X, M-TOP_prod (M => Y)) holds F.f
= F(f) from FUNCT_1:sch 4;
rng F c= the carrier of oContMaps(X, Y)|^M
proof
let y be object;
assume y in rng F;
then consider x being object such that
A5: x in dom F and
A6: y = F.x by FUNCT_1:def 3;
reconsider x as Element of oContMaps(X, M-TOP_prod (M => Y)) by A3,A5;
reconsider f = x as continuous Function of X, M-TOP_prod (M => Y) by
WAYBEL26:2;
commute f is Function of M, the carrier of oContMaps(X, Y) & y =
commute x by A4,A6,WAYBEL26:31;
then y in Funcs(M, the carrier of oContMaps(X, Y)) by FUNCT_2:8;
hence thesis by YELLOW_1:28;
end;
then reconsider
F as Function of oContMaps(X, M-TOP_prod (M => Y)), oContMaps(X
, Y)|^M by A3,FUNCT_2:2;
take F;
let f be continuous Function of X, M-TOP_prod (M => Y);
f is Element of oContMaps(X, M-TOP_prod (M => Y)) by WAYBEL26:2;
hence thesis by A4;
end;
end;
registration
let M be non empty set;
let X,Y be non empty TopSpace;
cluster commute(X,M,Y) -> one-to-one onto;
correctness
proof
set f = commute(X,M,Y);
Carrier (M => Y) = M => the carrier of Y by WAYBEL26:30;
then the carrier of M-TOP_prod (M => Y) = product (M => the carrier of Y)
by WAYBEL18:def 3
.= Funcs(M, the carrier of Y) by CARD_3:11;
then
A1: the carrier of oContMaps(X, M-TOP_prod (M => Y)) c= Funcs(the carrier
of X, Funcs(M, the carrier of Y)) by WAYBEL26:32;
now
thus the carrier of oContMaps(X, Y)|^M <> {};
let x1,x2 be object;
assume that
A2: x1 in the carrier of oContMaps(X, M-TOP_prod (M => Y)) and
A3: x2 in the carrier of oContMaps(X, M-TOP_prod (M => Y));
reconsider a1 = x1, a2 = x2 as Element of oContMaps(X, M-TOP_prod (M =>
Y)) by A2,A3;
reconsider f1 = a1, f2 = a2 as continuous Function of X, M-TOP_prod (M
=> Y) by WAYBEL26:2;
assume f.x1 = f.x2;
then commute f1 = f.x2 by Def5
.= commute f2 by Def5;
then f1 = commute commute f2 by A1,FUNCT_6:57;
hence x1 = x2 by A1,FUNCT_6:57;
end;
hence commute(X,M,Y) is one-to-one;
rng f = the carrier of oContMaps(X, Y)|^M
proof
thus rng f c= the carrier of oContMaps(X, Y)|^M;
let x be object;
assume
x in the carrier of oContMaps(X, Y)|^M;
then reconsider x as Element of oContMaps(X, Y)|^M;
A4: the carrier of oContMaps(X, Y)|^M = Funcs(M, the carrier of
oContMaps(X, Y)) by YELLOW_1:28;
then reconsider x as Function of M, the carrier of oContMaps(X, Y) by
FUNCT_2:66;
reconsider g = commute x as continuous Function of X, M-TOP_prod(M => Y)
by WAYBEL26:33;
reconsider y = g as Element of oContMaps(X, M-TOP_prod(M => Y)) by
WAYBEL26:2;
the carrier of oContMaps(X, Y)|^M c= Funcs(M, Funcs(the carrier of
X, the carrier of Y)) by A4,FUNCT_5:56,WAYBEL26:32;
then commute commute x = x by FUNCT_6:57;
then
A5: f.y = x by Def5;
dom f = the carrier of oContMaps(X, M-TOP_prod(M => Y)) by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:def 3;
end;
hence thesis by FUNCT_2:def 3;
end;
end;
registration
let M be non empty set;
let X be non empty TopSpace;
cluster commute(X, M, Sierpinski_Space) -> isomorphic;
correctness
proof
M-POS_prod (M => oContMaps(X, Sierpinski_Space)) = oContMaps(X,
Sierpinski_Space)|^M by YELLOW_1:def 5;
then
ex f1 being Function of oContMaps(X, M-TOP_prod (M => Sierpinski_Space)
), oContMaps(X, Sierpinski_Space)|^M st f1 is isomorphic & for f being
continuous Function of X, M-TOP_prod (M => Sierpinski_Space) holds f1.f =
commute f by WAYBEL26:34;
hence thesis by Def5;
end;
end;
Lm2: for T being T_0-TopSpace st a4102[T] holds a4103[T]
proof
let Y be T_0-TopSpace such that
A1: a4102[Y];
set S = Sigma InclPoset the topology of Y;
let X be non empty TopSpace;
let T be Scott TopAugmentation of InclPoset the topology of Y;
A2: the topology of T = sigma InclPoset the topology of Y by YELLOW_9:51;
let f be continuous Function of X, T;
the RelStr of T = InclPoset the topology of Y & the RelStr of S =
InclPoset the topology of Y by YELLOW_9:def 4;
then
A3: the TopStruct of X = the TopStruct of X & the TopRelStr of T = the
TopRelStr of S by A2,YELLOW_9:51;
then reconsider
F = Theta(X,Y) as Function of InclPoset the topology of [:X, Y:],
ContMaps(X, T) by Th10;
ContMaps(X, T) = ContMaps(X, S) by A3,Th10;
then F is isomorphic by A1;
then
f in the carrier of ContMaps(X, T) & rng F = the carrier of ContMaps(X,
T) by WAYBEL24:def 3,WAYBEL_0:66;
then consider W being object such that
A4: W in dom F and
A5: f = F.W by FUNCT_1:def 3;
dom F = the carrier of InclPoset the topology of [:X, Y:] by FUNCT_2:def 1
.= the topology of [:X, Y:] by YELLOW_1:1;
then reconsider W as open Subset of [:X,Y:] by A4,PRE_TOPC:def 2;
reconsider R = W as Relation of the carrier of X, the carrier of Y by
BORSUK_1:def 2;
A6: dom R c= the carrier of X;
f = (W, the carrier of X)*graph by A5,Def3;
hence thesis by A6,WAYBEL26:41;
end;
theorem Th23:
for X,Y being non empty TopSpace for S being Scott
TopAugmentation of InclPoset the topology of Y for f1, f2 being Element of
ContMaps(X, S) st f1 <= f2 holds *graph f1 c= *graph f2
proof
let X,Y be non empty TopSpace;
let S be Scott TopAugmentation of InclPoset the topology of Y;
let f1, f2 be Element of ContMaps(X, S);
assume
A1: f1 <= f2;
reconsider F1=f1,F2=f2 as Function of X,S by WAYBEL24:21;
let a,b be object;
A2: the RelStr of S = the RelStr of InclPoset the topology of Y by
YELLOW_9:def 4;
f2 is Function of X,S by WAYBEL24:21;
then
A3: dom f2 = the carrier of X by FUNCT_2:def 1;
assume
A4: [a,b] in *graph f1;
then
A5: a in dom f1 & b in f1.a by WAYBEL26:38;
f1 is Function of X,S by WAYBEL24:21;
then
A6: dom f1 = the carrier of X by FUNCT_2:def 1;
then reconsider a9=a as Element of X by A4,WAYBEL26:38;
F1.a9 is Element of S;
then f1.a in the carrier of InclPoset the topology of Y by A2;
then
A7: f1.a in the topology of Y by YELLOW_1:1;
F2.a9 is Element of S;
then f2.a in the carrier of InclPoset the topology of Y by A2;
then
A8: f2.a in the topology of Y by YELLOW_1:1;
[f1.a9,f2.a9] in the InternalRel of S by A1,WAYBEL24:20;
then [f1.a,f2.a] in RelIncl the topology of Y by A2,YELLOW_1:1;
then f1.a c= f2.a by A7,A8,WELLORD2:def 1;
hence thesis by A6,A3,A5,WAYBEL26:38;
end;
Lm3: for T being T_0-TopSpace st a4103[T] holds a4102[T]
proof
deffunc F(Function) = *graph $1;
let Y be T_0-TopSpace such that
A1: a4103[Y];
set T = Sigma InclPoset the topology of Y;
let X be non empty TopSpace;
consider G being Function such that
A2: dom G = the carrier of ContMaps(X, T) and
A3: for f being Element of ContMaps(X, T) holds G.f = F(f) from FUNCT_1:
sch 4;
rng G c= the carrier of InclPoset the topology of [:X, Y:]
proof
let x be object;
assume x in rng G;
then consider a being object such that
A4: a in dom G and
A5: x=G.a by FUNCT_1:def 3;
reconsider a as Element of ContMaps(X,T) by A2,A4;
reconsider a as continuous Function of X,T by WAYBEL24:21;
x = *graph a by A3,A5;
then x is open Subset of [:X,Y:] by A1;
then x in the topology of [:X,Y:] by PRE_TOPC:def 2;
hence thesis by YELLOW_1:1;
end;
then reconsider
G as Function of ContMaps(X, T), InclPoset the topology of [:X, Y
:] by A2,FUNCT_2:2;
consider F be Function of InclPoset the topology of [:X, Y:], oContMaps(X, T
) such that
A6: F is monotone and
A7: for W being open Subset of [:X,Y:] holds F.W = (W, the carrier of X)
*graph by WAYBEL26:45;
A8: G is monotone
proof
let f1,f2 be Element of ContMaps(X, T);
assume f1 <= f2;
then *graph f1 c= *graph f2 by Th23;
then G.f1 c= *graph f2 by A3;
then G.f1 c= G.f2 by A3;
hence G.f1 <= G.f2 by YELLOW_1:3;
end;
reconsider F as Function of InclPoset the topology of [:X, Y:], ContMaps(X,
T) by Th18;
dom F = the carrier of InclPoset the topology of [:X, Y:] by FUNCT_2:def 1;
then rng G c= dom F;
then
A9: dom (F*G) = the carrier of ContMaps(X, T) by A2,RELAT_1:27;
now
let x be object;
assume
A10: x in the carrier of ContMaps(X, T);
then reconsider x1=x as continuous Function of X,T by WAYBEL24:21;
reconsider gx = *graph x1 as open Subset of [:X,Y:] by A1;
A11: dom x1 = the carrier of X by FUNCT_2:def 1;
A12: now
let i be object;
assume i in the carrier of X;
then
A13: i in dom x1 by FUNCT_2:def 1;
A14: i in {i} by TARSKI:def 1;
thus x1.i = Im(gx,i)
proof
thus x1.i c= Im(gx,i)
proof
let b be object;
assume b in x1.i;
then [i,b] in gx by A13,WAYBEL26:38;
hence thesis by A14,RELAT_1:def 13;
end;
let b be object;
assume b in Im(gx,i);
then ex j being object st [j,b] in gx & j in {i} by RELAT_1:def 13;
then [i,b] in gx by TARSKI:def 1;
hence thesis by WAYBEL26:38;
end;
end;
(F*G).x = F.(G.x1) by A9,A10,FUNCT_1:12
.= F.gx by A3,A10
.= (gx, the carrier of X)*graph by A7;
hence (F*G).x = x by A11,A12,WAYBEL26:def 5;
end;
then
A15: F*G = id ContMaps(X, T) by A9,FUNCT_1:17;
A16: dom (G*F) = the carrier of InclPoset the topology of [:X, Y:] by
FUNCT_2:def 1;
now
let x be object;
assume
A17: x in the carrier of InclPoset the topology of [:X, Y:];
then x in the topology of [:X, Y:] by YELLOW_1:1;
then reconsider x1=x as open Subset of [:X, Y:] by PRE_TOPC:def 2;
(x1,the carrier of X)*graph is continuous Function of X,T by WAYBEL26:43;
then reconsider
x1X = (x1,the carrier of X)*graph as Element of ContMaps(X,T )
by WAYBEL24:21;
x1 c= the carrier of [:X,Y:];
then
A18: x1 c= [:the carrier of X,the carrier of Y:] by BORSUK_1:def 2;
A19: dom x1 c= the carrier of X
proof
let d be object;
assume d in dom x1;
then ex e being object st [d,e] in x1 by XTUPLE_0:def 12;
hence thesis by A18,ZFMISC_1:87;
end;
thus (G*F).x = G.(F.x1) by A16,A17,FUNCT_1:12
.= G.x1X by A7
.= *graph x1X by A3
.= x by A19,WAYBEL26:41;
end;
then
A20: G*F = id InclPoset the topology of [:X, Y:] by A16,FUNCT_1:17;
ContMaps(X, T) = oContMaps(X, T) by Th18;
then F is isomorphic by A6,A8,A15,A20,YELLOW16:15;
hence thesis by A7,Def3;
end;
Lm4: for T being T_0-TopSpace st a4103[T] holds a4104[T]
proof
let Y be T_0-TopSpace such that
A1: a4103[Y];
let X be Scott TopAugmentation of InclPoset the topology of Y;
reconsider f = id X as continuous Function of X, X;
A2: the RelStr of X = the RelStr of InclPoset the topology of Y by
YELLOW_9:def 4;
*graph f = {[W,y] where W is open Subset of Y, y is Element of Y: y in W }
proof
thus *graph f c= {[W,y] where W is open Subset of Y, y is Element of Y: y
in W}
proof
let a,b be object;
assume
A3: [a,b] in *graph f;
then
A4: a in dom f by WAYBEL26:38;
A5: b in f.a by A3,WAYBEL26:38;
dom f = the carrier of InclPoset the topology of Y by A2,FUNCT_2:def 1
.= the topology of Y by YELLOW_1:1;
then reconsider a as open Subset of Y by A4,PRE_TOPC:def 2;
f.a = a by A4,FUNCT_1:18;
then reconsider b as Element of Y by A5;
b in a by A4,A5,FUNCT_1:18;
hence thesis;
end;
let e be object;
assume e in {[W,y] where W is open Subset of Y, y is Element of Y: y in W};
then consider W being open Subset of Y, y being Element of Y such that
A6: e=[W,y] & y in W;
W in the topology of Y by PRE_TOPC:def 2;
then W in the carrier of InclPoset the topology of Y by YELLOW_1:1;
then W in dom f & f.W = W by A2,FUNCT_1:18,FUNCT_2:def 1;
hence thesis by A6,WAYBEL26:38;
end;
hence thesis by A1;
end;
Lm5: for T being T_0-TopSpace st a4104[T] holds a4105[T]
proof
let Y be T_0-TopSpace such that
A1: a4104[Y];
let S be Scott TopAugmentation of InclPoset the topology of Y;
reconsider A = {[W,z] where W is open Subset of Y, z is Element of Y: z in W
} as open Subset of [:S, Y:] by A1;
let y be Element of Y, V be open a_neighborhood of y;
the topology of S is Basis of S & the topology of Y is Basis of Y by
CANTOR_1:2;
then reconsider
B = {[:a,b:] where a is Subset of S, b is Subset of Y: a in the
topology of S & b in the topology of Y} as Basis of [:S, Y:] by YELLOW_9:40;
y in V by CONNSP_2:4;
then [V,y] in A;
then consider ab being Subset of [:S, Y:] such that
A2: ab in B and
A3: [V,y] in ab and
A4: ab c= A by YELLOW_9:31;
consider H being Subset of S, W being Subset of Y such that
A5: ab = [:H,W:] and
A6: H in the topology of S and
A7: W in the topology of Y by A2;
reconsider H as open Subset of S by A6,PRE_TOPC:def 2;
A8: the RelStr of S=the RelStr of InclPoset the topology of Y by YELLOW_9:def 4
;
meet H c= the carrier of Y
proof
let x be object;
H <> {} by A3,A5;
then consider A being object such that
A9: A in H by XBOOLE_0:def 1;
A in the carrier of S by A9;
then
A10: A in the topology of Y by A8,YELLOW_1:1;
reconsider A as set by TARSKI:1;
assume x in meet H;
then x in A by A9,SETFAM_1:def 1;
hence thesis by A10;
end;
then reconsider mH=meet H as Subset of Y;
reconsider W as open Subset of Y by A7,PRE_TOPC:def 2;
W c= mH
proof
let w be object;
assume
A11: w in W;
A12: now
let a be set;
assume a in H;
then [a,w] in ab by A5,A11,ZFMISC_1:87;
then [a,w] in A by A4;
then consider a1 being open Subset of Y, w1 being Element of Y such that
A13: [a,w] = [a1,w1] and
A14: w1 in a1;
a = a1 by A13,XTUPLE_0:1;
hence w in a by A13,A14,XTUPLE_0:1;
end;
H <> {} by A3,A5;
hence thesis by A12,SETFAM_1:def 1;
end;
then
A15: W c= Int mH by TOPS_1:24;
take H;
thus V in H by A3,A5,ZFMISC_1:87;
y in W by A3,A5,ZFMISC_1:87;
hence thesis by A15,CONNSP_2:def 1;
end;
Lm6: for T being T_0-TopSpace st a4105[T] holds a4103[T]
proof
let Y be T_0-TopSpace such that
A1: a4105[Y];
let X be non empty TopSpace;
let T be Scott TopAugmentation of InclPoset the topology of Y;
let f be continuous Function of X, T;
the topology of X is Basis of X & the topology of Y is Basis of Y by
CANTOR_1:2;
then reconsider
B = {[:a,b:] where a is Subset of X, b is Subset of Y: a in the
topology of X & b in the topology of Y} as Basis of [:X, Y:] by YELLOW_9:40;
A2: the RelStr of T=the RelStr of InclPoset the topology of Y by YELLOW_9:def 4
;
now
let s be object;
assume
A3: s in *graph f;
then consider s1,s2 being object such that
A4: s = [s1,s2] by RELAT_1:def 1;
A5: s1 in dom f by A3,A4,WAYBEL26:38;
then f.s1 in rng f by FUNCT_1:def 3;
then f.s1 in the carrier of T;
then
A6: f.s1 in the topology of Y by A2,YELLOW_1:1;
s2 in f.s1 by A3,A4,WAYBEL26:38;
then s in [:the carrier of X, the carrier of Y:] by A4,A5,A6,ZFMISC_1:87;
hence s in the carrier of [:X,Y:] by BORSUK_1:def 2;
end;
then reconsider A = *graph f as Subset of [:X,Y:] by TARSKI:def 3;
now
let p be Point of [:X, Y:];
assume
A7: p in A;
then consider x,y being object such that
A8: p = [x,y] by RELAT_1:def 1;
A9: y in f.x by A7,A8,WAYBEL26:38;
A10: x in dom f by A7,A8,WAYBEL26:38;
then reconsider x as Element of X;
f.x in the carrier of InclPoset the topology of Y by A2;
then
A11: f.x in the topology of Y by YELLOW_1:1;
then reconsider y as Element of Y by A9;
reconsider W=f.x as open Subset of Y by A11,PRE_TOPC:def 2;
y in Int W by A9,TOPS_1:23;
then reconsider W as open a_neighborhood of y by CONNSP_2:def 1;
consider H being open Subset of T such that
A12: W in H and
A13: meet H is a_neighborhood of y by A1;
[#]T <> {};
then reconsider fH = f"H as open Subset of X by TOPS_2:43;
reconsider mH = meet H as a_neighborhood of y by A13;
Int Int mH = Int mH;
then reconsider V = Int mH as open a_neighborhood of y by CONNSP_2:def 1;
reconsider a = [:fH, V:] as Subset of [:X, Y:];
take a;
V in the topology of Y & fH in the topology of X by PRE_TOPC:def 2;
hence a in B;
y in Int mH & x in fH by A10,A12,CONNSP_2:def 1,FUNCT_1:def 7;
hence p in a by A8,ZFMISC_1:87;
thus a c= A
proof
let s1,s2 be object;
A14: V c= mH by TOPS_1:16;
assume
A15: [s1,s2] in a;
then
A16: s1 in fH by ZFMISC_1:87;
then
A17: f.s1 in H by FUNCT_1:def 7;
A18: s1 in dom f by A16,FUNCT_1:def 7;
s2 in V by A15,ZFMISC_1:87;
then s2 in f.s1 by A17,A14,SETFAM_1:def 1;
hence thesis by A18,WAYBEL26:38;
end;
end;
hence thesis by YELLOW_9:31;
end;
Lm7: for T being T_0-TopSpace st a4105[T] holds InclPoset the topology of T is
continuous
proof
let Y be T_0-TopSpace such that
A1: a4105[Y];
set L = InclPoset the topology of Y;
set S = the Scott TopAugmentation of L;
thus for x being Element of L holds waybelow x is non empty directed;
thus L is up-complete;
let A be Element of L;
the carrier of L = the topology of Y by YELLOW_1:1;
then A in the topology of Y;
then reconsider B = A as open Subset of Y by PRE_TOPC:def 2;
A2: the RelStr of S = the RelStr of L by YELLOW_9:def 4;
thus A c= sup waybelow A
proof
let x be object;
assume
A3: x in A;
then x in B;
then reconsider x9 = x as Element of Y;
reconsider B as open a_neighborhood of x9 by A3,CONNSP_2:3;
consider H being open Subset of S such that
A4: B in H and
A5: meet H is a_neighborhood of x9 by A1;
reconsider mH = meet H as a_neighborhood of x9 by A5;
reconsider H1 = H as Subset of L by A2;
Int mH in the topology of Y by PRE_TOPC:def 2;
then reconsider ImH = Int mH as Element of L by YELLOW_1:1;
ImH << A
proof
let D be non empty directed Subset of L;
A6: H1 is inaccessible upper by A2,WAYBEL_0:25,YELLOW_9:47;
assume A <= sup D;
then sup D in H1 by A4,A6;
then D meets H1 by A6;
then consider d being object such that
A7: d in D and
A8: d in H1 by XBOOLE_0:3;
reconsider d as Element of L by A7;
take d;
thus d in D by A7;
Int mH c= mH & mH c= d by A8,SETFAM_1:3,TOPS_1:16;
then ImH c= d;
hence thesis by YELLOW_1:3;
end;
then x in Int mH & Int mH in waybelow A by CONNSP_2:def 1;
then x in union waybelow A by TARSKI:def 4;
hence thesis by YELLOW_1:22;
end;
union waybelow A c= union downarrow A by WAYBEL_3:11,ZFMISC_1:77;
then sup waybelow A c= union downarrow A by YELLOW_1:22;
then sup waybelow A c= sup downarrow A by YELLOW_1:22;
hence thesis by WAYBEL_0:34;
end;
Lm8: for T being T_0-TopSpace st InclPoset the topology of T is continuous
holds a4105[T]
proof
let T be T_0-TopSpace;
assume
A1: InclPoset the topology of T is continuous;
let S be Scott TopAugmentation of InclPoset the topology of T;
let y be Element of T, V be open a_neighborhood of y;
A2: Int V c= V & y in Int V by CONNSP_2:def 1,TOPS_1:16;
V in the topology of T by PRE_TOPC:def 2;
then reconsider W=V as Element of InclPoset the topology of T by YELLOW_1:1;
W = sup waybelow W by A1,WAYBEL_3:def 5
.= union waybelow W by YELLOW_1:22;
then consider Z being set such that
A3: y in Z and
A4: Z in waybelow W by A2,TARSKI:def 4;
reconsider Z as Element of InclPoset the topology of T by A4;
A5: the RelStr of InclPoset the topology of T = the RelStr of S by
YELLOW_9:def 4;
then reconsider Z1=Z as Element of S;
Z in the carrier of InclPoset the topology of T;
then Z in the topology of T by YELLOW_1:1;
then reconsider Z2=Z as open Subset of T by PRE_TOPC:def 2;
A6: Z c= meet uparrow Z
proof
let s be object;
assume
A7: s in Z;
now
let z be set;
assume
A8: z in uparrow Z;
then reconsider z1=z as Element of InclPoset the topology of T;
Z <= z1 by A8,WAYBEL_0:18;
then Z c= z by YELLOW_1:3;
hence s in z by A7;
end;
hence thesis by SETFAM_1:def 1;
end;
reconsider H = wayabove Z1 as open Subset of S by A1,WAYBEL11:36;
take H;
Z << W by A4,WAYBEL_3:7;
then
A9: V in wayabove Z;
hence
A10: V in H by A5,YELLOW12:13;
meet H c= the carrier of T
proof
let s be object;
assume s in meet H;
then s in V by A10,SETFAM_1:def 1;
hence thesis;
end;
then reconsider mH = meet H as Subset of T;
meet uparrow Z c= meet wayabove Z by A9,SETFAM_1:6,WAYBEL_3:11;
then meet uparrow Z c= meet wayabove Z1 by A5,YELLOW12:13;
then Z2 c= mH by A6;
then Z2 c= Int mH by TOPS_1:24;
hence thesis by A3,CONNSP_2:def 1;
end;
begin :: The Poset of Open Sets
:: 4.10. THEOREM, (1) <=> (1'), pp. 131-133
theorem
for Y being T_0-TopSpace holds (for X being non empty TopSpace for L
being Scott continuous complete TopLattice for T being Scott TopAugmentation of
ContMaps(Y, L) ex f being Function of ContMaps(X, T), ContMaps([:X, Y:], L), g
being Function of ContMaps([:X, Y:], L), ContMaps(X, T) st f is uncurrying
one-to-one onto & g is currying one-to-one onto) iff for X being non empty
TopSpace for L being Scott continuous complete TopLattice for T being Scott
TopAugmentation of ContMaps(Y, L) ex f being Function of ContMaps(X, T),
ContMaps([:X, Y:], L), g being Function of ContMaps([:X, Y:], L), ContMaps(X, T
) st f is uncurrying isomorphic & g is currying isomorphic by Lm1;
:: 4.10. THEOREM, (6) <=> (2), pp. 131-133
theorem
for Y being T_0-TopSpace holds InclPoset the topology of Y is
continuous iff for X being non empty TopSpace holds Theta(X, Y) is isomorphic
proof
let Y be T_0-TopSpace;
hereby
assume InclPoset the topology of Y is continuous;
then a4105[Y] by Lm8;
then a4103[Y] by Lm6;
hence a4102[Y] by Lm3;
end;
assume a4102[Y];
then a4103[Y] by Lm2;
then a4104[Y] by Lm4;
then a4105[Y] by Lm5;
hence thesis by Lm7;
end;
:: 4.10. THEOREM, (6) <=> (3), pp. 131-133
theorem
for Y being T_0-TopSpace holds InclPoset the topology of Y is
continuous iff for X being non empty TopSpace for f being continuous Function
of X, Sigma InclPoset the topology of Y holds *graph f is open Subset of [:X, Y
:]
proof
let Y be T_0-TopSpace;
hereby
assume InclPoset the topology of Y is continuous;
then a4105[Y] by Lm8;
hence for X being non empty TopSpace for f being continuous Function of X,
Sigma InclPoset the topology of Y holds *graph f is open Subset of [:X, Y:] by
Lm6;
end;
assume
A1: for X being non empty TopSpace for f being continuous Function of X,
Sigma InclPoset the topology of Y holds *graph f is open Subset of [:X, Y:];
a4103[Y]
proof
let X be non empty TopSpace;
let T be Scott TopAugmentation of InclPoset the topology of Y;
let f be continuous Function of X, T;
A2: the RelStr of T = InclPoset the topology of Y & the RelStr of Sigma
InclPoset the topology of Y = InclPoset the topology of Y by YELLOW_9:def 4;
then reconsider g = f as Function of X, Sigma InclPoset the topology of Y;
the TopStruct of X = the TopStruct of X & the TopStruct of T = the
TopStruct of Sigma InclPoset the topology of Y by A2,Th13;
then g is continuous by YELLOW12:36;
hence thesis by A1;
end;
then a4104[Y] by Lm4;
then a4105[Y] by Lm5;
hence thesis by Lm7;
end;
:: 4.10. THEOREM, (6) <=> (4), pp. 131-133
theorem
for Y being T_0-TopSpace holds InclPoset the topology of Y is
continuous iff {[W,y] where W is open Subset of Y, y is Element of Y: y in W}
is open Subset of [:Sigma InclPoset the topology of Y, Y:]
proof
let Y be T_0-TopSpace;
hereby
assume InclPoset the topology of Y is continuous;
then a4105[Y] by Lm8;
then a4103[Y] by Lm6;
hence {[W,y] where W is open Subset of Y, y is Element of Y: y in W} is
open Subset of [:Sigma InclPoset the topology of Y, Y:] by Lm4;
end;
assume
A1: {[W,y] where W is open Subset of Y, y is Element of Y: y in W} is
open Subset of [:Sigma InclPoset the topology of Y, Y:];
a4104[Y]
proof
let T be Scott TopAugmentation of InclPoset the topology of Y;
the RelStr of T = InclPoset the topology of Y & the RelStr of Sigma
InclPoset the topology of Y = InclPoset the topology of Y by YELLOW_9:def 4;
then the TopStruct of Y = the TopStruct of Y & the TopStruct of T = the
TopStruct of Sigma InclPoset the topology of Y by Th13;
then [:T, Y:] = [:Sigma InclPoset the topology of Y, Y:] by Th7;
hence thesis by A1;
end;
then a4105[Y] by Lm5;
hence thesis by Lm7;
end;
:: 4.10. THEOREM, (6) <=> (5), pp. 131-133
theorem
for Y being T_0-TopSpace holds InclPoset the topology of Y is
continuous iff for y being Element of Y, V being open a_neighborhood of y ex H
being open Subset of Sigma InclPoset the topology of Y st V in H & meet H is
a_neighborhood of y
proof
let Y be T_0-TopSpace;
thus InclPoset the topology of Y is continuous implies for y being Element
of Y, V being open a_neighborhood of y ex H being open Subset of Sigma
InclPoset the topology of Y st V in H & meet H is a_neighborhood of y by Lm8;
assume
A1: for y being Element of Y, V being open a_neighborhood of y ex H
being open Subset of Sigma InclPoset the topology of Y st V in H & meet H is
a_neighborhood of y;
a4105[Y]
proof
let T be Scott TopAugmentation of InclPoset the topology of Y;
let y be Element of Y, V be open a_neighborhood of y;
consider H being open Subset of Sigma InclPoset the topology of Y such
that
A2: V in H & meet H is a_neighborhood of y by A1;
the RelStr of T = InclPoset the topology of Y & the RelStr of Sigma
InclPoset the topology of Y = InclPoset the topology of Y by YELLOW_9:def 4;
then reconsider G = H as Subset of T;
the topology of T = the topology of Sigma InclPoset the topology of Y
by Th13;
then G in the topology of T by PRE_TOPC:def 2;
then H is open Subset of T by PRE_TOPC:def 2;
hence thesis by A2;
end;
hence thesis by Lm7;
end;
::Theorem II.4.11
defpred a4111[complete LATTICE] means InclPoset(sigma $1) is continuous;
defpred a4112[complete LATTICE] means for SL being Scott TopAugmentation of $1
for S being complete LATTICE for SS being Scott TopAugmentation of S holds
sigma [:S,$1:] = the topology of [:SS,SL:];
defpred a4113[complete LATTICE] means for SL being Scott TopAugmentation of $1
for S being complete LATTICE for SS being Scott TopAugmentation of S for SSL
being Scott TopAugmentation of [:S,$1:] holds the TopStruct of SSL = [:SS,SL:];
Lm9: for L being complete LATTICE holds a4112[L] iff a4113[L]
proof
let L be complete LATTICE;
thus a4112[L] implies a4113[L]
proof
assume
A1: a4112[L];
let SL be Scott TopAugmentation of L;
let S be complete LATTICE;
let SS be Scott TopAugmentation of S;
let SSL be Scott TopAugmentation of [:S,L:];
A2: the topology of [:SS,SL:] = sigma [:S,L:] by A1
.= the topology of SSL by YELLOW_9:51;
A3: the RelStr of SSL = the RelStr of [:S,L:] by YELLOW_9:def 4;
the RelStr of SL = the RelStr of L & the RelStr of SS = the RelStr of
S by YELLOW_9:def 4;
then the carrier of SSL = [:the carrier of SS,the carrier of SL:] by A3,
YELLOW_3:def 2
.= the carrier of [:SS,SL:] by BORSUK_1:def 2;
hence thesis by A2;
end;
assume
A4: a4113[L];
let SL be Scott TopAugmentation of L;
let S be complete LATTICE;
let SS be Scott TopAugmentation of S;
now
let SSL be Scott TopAugmentation of [:S,L:];
the TopStruct of SSL = the TopStruct of [:SS,SL:] by A4;
hence thesis by YELLOW_9:51;
end;
hence thesis;
end;
begin :: The Poset of Scott Open Sets
theorem
for R1,R2,R3 being non empty RelStr for f1 being Function of R1,R3 st
f1 is isomorphic for f2 being Function of R2,R3 st f2=f1 & f2 is isomorphic
holds the RelStr of R1 = the RelStr of R2
proof
let R1,R2,R3 be non empty RelStr;
let f1 be Function of R1,R3;
assume
A1: f1 is isomorphic;
let f2 be Function of R2,R3;
assume that
A2: f2=f1 and
A3: f2 is isomorphic;
A4: the carrier of R1 = rng (f2 qua Function") by A1,A2,WAYBEL_0:67
.= the carrier of R2 by A3,WAYBEL_0:67;
A5: the InternalRel of R2 c= the InternalRel of R1
proof
let x1,x2 be object;
assume
A6: [x1,x2] in the InternalRel of R2;
then reconsider x19=x1,x29=x2 as Element of R2 by ZFMISC_1:87;
reconsider y1=x19,y2=x29 as Element of R1 by A4;
x19 <= x29 by A6,ORDERS_2:def 5;
then f2.x19 <= f2.x29 by A3,WAYBEL_0:66;
then y1 <= y2 by A1,A2,WAYBEL_0:66;
hence thesis by ORDERS_2:def 5;
end;
the InternalRel of R1 c= the InternalRel of R2
proof
let x1,x2 be object;
assume
A7: [x1,x2] in the InternalRel of R1;
then reconsider x19=x1,x29=x2 as Element of R1 by ZFMISC_1:87;
reconsider y1=x19,y2=x29 as Element of R2 by A4;
x19 <= x29 by A7,ORDERS_2:def 5;
then f1.x19 <= f1.x29 by A1,WAYBEL_0:66;
then y1 <= y2 by A2,A3,WAYBEL_0:66;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by A4,A5,XBOOLE_0:def 10;
end;
Lm10: for L being complete LATTICE holds a4111[L] implies a4112[L]
proof
let L be complete LATTICE;
assume
A1: a4111[L];
let SL be Scott TopAugmentation of L;
let S be complete LATTICE;
let SS be Scott TopAugmentation of S;
A2: the RelStr of SS = the RelStr of S by YELLOW_9:def 4;
UPS(L, BoolePoset{0}) is non empty full SubRelStr of (BoolePoset{0})|^the
carrier of L by WAYBEL27:def 4;
then
A3: UPS(L, BoolePoset{0})|^the carrier of S is non empty full SubRelStr of (
(BoolePoset{0})|^the carrier of L)|^the carrier of S by YELLOW16:39;
UPS(S, UPS(L, BoolePoset{0})) is non empty full SubRelStr of UPS(L,
BoolePoset{0})|^the carrier of S by WAYBEL27:def 4;
then
A4: UPS(S, UPS(L, BoolePoset{0})) is non empty full SubRelStr of ((
BoolePoset{0})|^the carrier of L)|^the carrier of S by A3,WAYBEL15:1;
consider f5 being Function of UPS(L, BoolePoset{0}), InclPoset sigma L such
that
A5: f5 is isomorphic and
A6: for f being directed-sups-preserving Function of L, BoolePoset{0}
holds f5.f = f"{1} by WAYBEL27:33;
set f6 = UPS(id S, f5);
consider f3 being Function of UPS(S, UPS(L, BoolePoset{0})), UPS([:S,L:],
BoolePoset{0}) such that
A7: f3 is uncurrying isomorphic by WAYBEL27:47;
set f4 = f3";
set T = Sigma InclPoset the topology of SL;
consider f1 being Function of UPS([:S,L:], BoolePoset{0}), InclPoset sigma [:
S,L:] such that
A8: f1 is isomorphic and
A9: for f being directed-sups-preserving Function of [:S,L:], BoolePoset
{0} holds f1.f = f"{1} by WAYBEL27:33;
A10: f4 is isomorphic by A7,YELLOW14:10;
set f2 = f1";
set G = f6*f4*f2;
A11: the topology of SL = sigma L by YELLOW_9:51;
then
A12: the RelStr of T = the RelStr of InclPoset sigma L by YELLOW_9:def 4;
A13: the carrier of UPS(S,InclPoset sigma L) = the carrier of ContMaps(SS,T)
proof
thus the carrier of UPS(S,InclPoset sigma L) c= the carrier of ContMaps(SS
,T)
proof
let x be object;
assume
A14: x in the carrier of UPS(S,InclPoset sigma L);
then reconsider x1 = x as Function of SS, T by A2,A12,WAYBEL27:def 4;
x is directed-sups-preserving Function of S, InclPoset sigma L by A14,
WAYBEL27:def 4;
then x1 is directed-sups-preserving by A2,A12,WAYBEL21:6;
then x1 is continuous by WAYBEL17:22;
hence thesis by WAYBEL24:def 3;
end;
let x be object;
assume x in the carrier of ContMaps(SS,T);
then consider x1 being Function of SS,T such that
A15: x1 = x and
A16: x1 is continuous by WAYBEL24:def 3;
reconsider x2=x1 as Function of S, InclPoset sigma L by A2,A12;
x1 is directed-sups-preserving by A16,WAYBEL17:22;
then x2 is directed-sups-preserving by A2,A12,WAYBEL21:6;
hence thesis by A15,WAYBEL27:def 4;
end;
then reconsider G as Function of InclPoset sigma [:S,L:], ContMaps(SS,T);
set F = Theta(SS, SL);
A17: the RelStr of SL = the RelStr of L by YELLOW_9:def 4;
(BoolePoset{0})|^the carrier of [:S,L:] = (BoolePoset{0})|^[:the carrier
of S, the carrier of L:] & UPS([:S,L:], BoolePoset{0}) is non empty full
SubRelStr of (BoolePoset{0})|^the carrier of [:S,L:] by WAYBEL27:def 4
,YELLOW_3:def 2;
then
A18: f4 is currying by A7,A4,Th2;
A19: for V being Element of InclPoset sigma [:S, L:] for s being Element of
S holds (G.V).s = {y where y is Element of L : [s,y] in V}
proof
let V be Element of InclPoset sigma [:S, L:];
let s be Element of S;
reconsider fff = f4.(f2.V) as directed-sups-preserving Function of S, UPS(
L, BoolePoset{0}) by WAYBEL27:def 4;
reconsider f2V = f2.V as directed-sups-preserving Function of [:S,L:],
BoolePoset{0} by WAYBEL27:def 4;
A20: f5 is sups-preserving & f5*fff*id the carrier of S = f5*fff by A5,
FUNCT_2:17,WAYBEL13:20;
A21: (f4.(f2.V)).s is directed-sups-preserving Function of L, BoolePoset{0}
by WAYBEL27:def 4;
then
A22: dom ((f4.(f2.V)).s) = the carrier of L by FUNCT_2:def 1;
G.V = (f6*f4).(f2.V) by FUNCT_2:15
.= UPS(id S, f5).(f4.(f2.V)) by FUNCT_2:15
.= f5*fff by A20,WAYBEL27:def 5;
then
A23: (G.V).s = f5.(fff.s) by FUNCT_2:15
.= ((f4.(f2.V)).s)"{1} by A6,A21;
A24: rng f1 = [#]InclPoset sigma [:S,L:] by A8,FUNCT_2:def 3;
dom f4 = the carrier of UPS([:S,L:], BoolePoset{0}) by FUNCT_2:def 1;
then
A25: f4.(f2.V) = curry(f2.V) by A18;
rng f1 = the carrier of InclPoset sigma [:S,L:] by A8,FUNCT_2:def 3;
then
A26: V = (id rng f1).V
.=(f1*f2).V by A8,A24,TOPS_2:52
.= f1.(f2.V) by FUNCT_2:15
.= f2V"{1} by A9;
thus (G.V).s c= {y where y is Element of L : [s,y] in V}
proof
let x be object;
assume
A27: x in (G.V).s;
then x in dom ((f4.(f2.V)).s) by A23,FUNCT_1:def 7;
then reconsider y = x as Element of L by A21,FUNCT_2:def 1;
((f4.(f2.V)).s).x in {1} by A23,A27,FUNCT_1:def 7;
then
A28: ((f4.(f2.V)).s).y = 1 by TARSKI:def 1;
A29: dom (f2V) = the carrier of [:S,L:] by FUNCT_2:def 1;
then [s,y] in dom(f2.V);
then (f2.V).(s,y) = 1 by A25,A28,FUNCT_5:20;
then (f2.V).(s,y) in {1} by TARSKI:def 1;
then [s,y] in (f2.V)"{1} by A29,FUNCT_1:def 7;
hence thesis by A26;
end;
let x be object;
assume x in {y where y is Element of L : [s,y] in V};
then consider y being Element of L such that
A30: y=x and
A31: [s,y] in V;
dom (f2V) = the carrier of [:S,L:] by FUNCT_2:def 1;
then
A32: [s,y] in dom (f2.V);
reconsider cs = (curry(f2.V)).s as Function;
(f2.V).(s,y) in {1} by A26,A31,FUNCT_1:def 7;
then (f2.V).(s,y) = 1 by TARSKI:def 1;
then cs.y = 1 by A32,FUNCT_5:20;
then ((f4.(f2.V)).s).y in {1} by A25,TARSKI:def 1;
hence thesis by A23,A30,A22,FUNCT_1:def 7;
end;
a4105[SL] by A1,A11,Lm8;
then a4103[SL] by Lm6;
then
A33: F is isomorphic by Lm3;
A34: the carrier of InclPoset sigma [:S,L:] c= the carrier of InclPoset the
topology of [:SS,SL:]
proof
let V be object;
assume V in the carrier of InclPoset sigma [:S,L:];
then reconsider V1 = V as Element of InclPoset sigma [:S,L:];
rng F = the carrier of ContMaps(SS,T) by A33,FUNCT_2:def 3;
then consider W being object such that
A35: W in dom F and
A36: F.W = G.V1 by FUNCT_1:def 3;
reconsider W2=W as Element of InclPoset the topology of [:SS,SL:] by A35;
dom F = the carrier of InclPoset the topology of [:SS, SL:] by
FUNCT_2:def 1;
then W in the topology of [:SS,SL:] by A35,YELLOW_1:1;
then reconsider W1=W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;
A37: V1 c= W1
proof
let v be object;
assume
A38: v in V1;
V1 in the carrier of InclPoset sigma [:S, L:];
then V in sigma [:S, L:] by YELLOW_1:1;
then V1 c= the carrier of [:S, L:];
then V1 c= [:the carrier of S, the carrier of L:] by YELLOW_3:def 2;
then consider v1,v2 being object such that
A39: v1 in the carrier of S and
A40: v2 in the carrier of L and
A41: v=[v1,v2] by A38,ZFMISC_1:84;
reconsider v2 as Element of L by A40;
reconsider v1 as Element of S by A39;
v2 in {y where y is Element of L : [v1,y] in V1} by A38,A41;
then v2 in (G.V1).v1 by A19;
then v2 in ((W1, the carrier of S)*graph).v1 by A2,A36,Def3;
then v2 in Im(W1,v1) by WAYBEL26:def 5;
then ex v19 being object st [v19,v2] in W1 & v19 in {v1}
by RELAT_1:def 13;
hence thesis by A41,TARSKI:def 1;
end;
W2 c= V1
proof
let w be object;
assume
A42: w in W2;
W1 c= the carrier of [:SS,SL:];
then W1 c= [:the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;
then consider w1,w2 being object such that
A43: w1 in the carrier of S and
A44: w2 in the carrier of L and
A45: w=[w1,w2] by A2,A17,A42,ZFMISC_1:84;
reconsider w2 as Element of L by A44;
reconsider w1 as Element of S by A43;
w1 in {w1} by TARSKI:def 1;
then w2 in Im(W1,w1) by A42,A45,RELAT_1:def 13;
then w2 in ((W1, the carrier of S)*graph).w1 by WAYBEL26:def 5;
then w2 in (F.W2).w1 by A2,Def3;
then w2 in {y where y is Element of L : [w1,y] in V1} by A19,A36;
then ex w29 being Element of L st w29 = w2 & [w1,w29] in V1;
hence thesis by A45;
end;
then W2=V by A37,XBOOLE_0:def 10;
hence thesis;
end;
InclPoset sigma L = InclPoset the topology of SL by YELLOW_9:51;
then f6 is isomorphic by A5,WAYBEL27:35;
then
A46: f6*f4 is isomorphic by A10,Th6;
A47: f2 is isomorphic by A8,YELLOW14:10;
the carrier of InclPoset the topology of [:SS,SL:] c= the carrier of
InclPoset sigma [:S,L:]
proof
let W be object;
assume
A48: W in the carrier of InclPoset the topology of [:SS,SL:];
then reconsider W2 = W as Element of InclPoset the topology of [:SS,SL:];
W in the topology of [:SS,SL:] by A48,YELLOW_1:1;
then reconsider W1 = W2 as open Subset of [:SS,SL:] by PRE_TOPC:def 2;
G is onto by A47,A46,A13,Th6,YELLOW14:9;
then rng G = the carrier of ContMaps(SS,T) by FUNCT_2:def 3;
then consider V being object such that
A49: V in dom G and
A50: G.V = F.W2 by FUNCT_1:def 3;
reconsider V as Element of InclPoset sigma [:S, L:] by A49;
A51: V c= W2
proof
let v be object;
assume
A52: v in V;
V in the carrier of InclPoset sigma [:S, L:];
then V in sigma [:S, L:] by YELLOW_1:1;
then V c= the carrier of [:S, L:];
then V c= [:the carrier of S, the carrier of L:] by YELLOW_3:def 2;
then consider v1,v2 being object such that
A53: v1 in the carrier of S and
A54: v2 in the carrier of L and
A55: v=[v1,v2] by A52,ZFMISC_1:84;
reconsider v2 as Element of L by A54;
reconsider v1 as Element of S by A53;
v2 in {y where y is Element of L : [v1,y] in V} by A52,A55;
then v2 in (G.V).v1 by A19;
then v2 in ((W1, the carrier of S)*graph).v1 by A2,A50,Def3;
then v2 in Im(W1,v1) by WAYBEL26:def 5;
then ex v19 being object st [v19,v2] in W2 & v19 in {v1}
by RELAT_1:def 13;
hence thesis by A55,TARSKI:def 1;
end;
W2 c= V
proof
let w be object;
assume
A56: w in W2;
W1 c= the carrier of [:SS,SL:];
then W1 c= [:the carrier of SS, the carrier of SL:] by BORSUK_1:def 2;
then consider w1,w2 being object such that
A57: w1 in the carrier of S and
A58: w2 in the carrier of L and
A59: w=[w1,w2] by A2,A17,A56,ZFMISC_1:84;
reconsider w2 as Element of L by A58;
reconsider w1 as Element of S by A57;
w1 in {w1} by TARSKI:def 1;
then w2 in Im(W1,w1) by A56,A59,RELAT_1:def 13;
then w2 in ((W1, the carrier of S)*graph).w1 by WAYBEL26:def 5;
then w2 in (F.W2).w1 by A2,Def3;
then w2 in {y where y is Element of L : [w1,y] in V} by A19,A50;
then ex w29 being Element of L st w29 = w2 & [w1,w29] in V;
hence thesis by A59;
end;
then W = V by A51,XBOOLE_0:def 10;
hence thesis;
end;
then the carrier of InclPoset sigma [:S,L:] = the carrier of InclPoset the
topology of [:SS,SL:] by A34;
hence sigma [:S,L:] = the carrier of InclPoset the topology of [:SS,SL:] by
YELLOW_1:1
.= the topology of [:SS,SL:] by YELLOW_1:1;
end;
Lm11: for L being complete LATTICE holds a4112[L] implies a4111[L]
proof
let L be complete LATTICE;
set SL = the Scott TopAugmentation of L;
A1: the RelStr of SL = the RelStr of L by YELLOW_9:def 4;
the TopStruct of SL = ConvergenceSpace Scott-Convergence SL by WAYBEL11:32;
then
A2: the topology of SL = sigma SL;
then
A3: InclPoset (sigma L) = InclPoset(the topology of SL) by A1,YELLOW_9:52;
then reconsider S = InclPoset(sigma L) as complete LATTICE;
set SS = the Scott TopAugmentation of S;
assume a4112[L];
then
A4: sigma [:S,L:] = the topology of [:SS,SL:];
A5: a4104[SL]
proof
set Wy = {[W,y] where W is open Subset of SL, y is Element of SL: y in W};
let T be Scott TopAugmentation of InclPoset(the topology of SL);
Wy c= the carrier of [:T, SL:]
proof
let x be object;
A6: the RelStr of T = the RelStr of InclPoset(the topology of SL) by
YELLOW_9:def 4;
assume x in Wy;
then consider W being open Subset of SL,y being Element of SL such that
A7: x = [W,y] and
y in W;
W in the topology of SL by PRE_TOPC:def 2;
then W in the carrier of InclPoset(the topology of SL) by YELLOW_1:1;
then [W,y] in [:the carrier of T,the carrier of SL:] by A6,ZFMISC_1:87;
hence thesis by A7,BORSUK_1:def 2;
end;
then reconsider WY = Wy as Subset of [:T,SL:];
A8: the RelStr of SS = the RelStr of InclPoset(the topology of SL) by A3,
YELLOW_9:def 4
.= the RelStr of T by YELLOW_9:def 4;
reconsider T1 = T as Scott TopAugmentation of S by A1,A2,YELLOW_9:52;
A9: the RelStr of SS = the RelStr of S by YELLOW_9:def 4;
the carrier of [:T, SL:] = [:the carrier of T,the carrier of SL:] by
BORSUK_1:def 2
.= the carrier of [:S,L:] by A1,A8,A9,YELLOW_3:def 2;
then reconsider wy = WY as Subset of [:S,L:];
A10: wy is inaccessible
proof
let D be non empty directed Subset of [:S,L:];
assume sup D in wy;
then [sup proj1 D,sup proj2 D] in wy by YELLOW_3:46;
then consider
sp1D being open Subset of SL, sp2D being Element of SL such
that
A11: [sup proj1 D,sup proj2 D] = [sp1D,sp2D] and
A12: sp2D in sp1D;
reconsider sp1D9 = sp1D as Subset of L by A1;
reconsider sp1D9 as inaccessible upper Subset of L by A1,WAYBEL_0:25
,YELLOW_9:47;
reconsider pD = proj1 D as Subset of InclPoset(the topology of SL) by A1
,A2,YELLOW_9:52;
reconsider proj2D = proj2 D as directed non empty Subset of L by
YELLOW_3:21,22;
A13: sup proj1 D = union pD by A3,YELLOW_1:22;
sup proj2D in sp1D9 by A11,A12,XTUPLE_0:1;
then proj2 D meets sp1D by WAYBEL11:def 1;
then consider d being object such that
A14: d in proj2 D and
A15: d in sp1D by XBOOLE_0:3;
reconsider d as Element of L by A14;
d in sup proj1 D by A11,A15,XTUPLE_0:1;
then consider V being set such that
A16: d in V and
A17: V in proj1 D by A13,TARSKI:def 4;
consider Y being object such that
A18: [Y,d] in D by A14,XTUPLE_0:def 13;
reconsider V as Element of S by A17;
consider e being object such that
A19: [V,e] in D by A17,XTUPLE_0:def 12;
A20: Y in proj1 D by A18,XTUPLE_0:def 12;
A21: e in proj2 D by A19,XTUPLE_0:def 13;
reconsider Y as Element of S by A20;
reconsider e as Element of L by A21;
consider DD being Element of [:S,L:] such that
A22: DD in D and
A23: [V,e] <= DD and
A24: [Y,d] <= DD by A18,A19,WAYBEL_0:def 1;
D c= the carrier of [:S,L:];
then D c= [:the carrier of S,the carrier of L:] by YELLOW_3:def 2;
then consider DD1,DD2 being object such that
A25: DD = [DD1,DD2] by A22,RELAT_1:def 1;
A26: DD2 in proj2 D by A22,A25,XTUPLE_0:def 13;
A27: DD1 in proj1 D by A22,A25,XTUPLE_0:def 12;
reconsider DD2 as Element of L by A26;
reconsider DD1 as Element of S by A27;
[V,e] <= [DD1,DD2] by A23,A25;
then V <= DD1 by YELLOW_3:11;
then
A28: V c= DD1 by YELLOW_1:3;
DD1 in the carrier of S;
then DD1 in sigma L by YELLOW_1:1;
then DD1 in the topology of SL by A1,A2,YELLOW_9:52;
then DD1 is open Subset of SL by PRE_TOPC:def 2;
then
A29: DD1 is upper Subset of L by A1,WAYBEL_0:25;
[Y,d] <= [DD1,DD2] by A24,A25;
then d <= DD2 by YELLOW_3:11;
then
A30: DD2 in DD1 by A16,A28,A29,WAYBEL_0:def 20;
DD1 in the carrier of S;
then DD1 in sigma L by YELLOW_1:1;
then DD1 in the topology of SL by A1,A2,YELLOW_9:52;
then reconsider DD1 as open Subset of SL by PRE_TOPC:def 2;
reconsider DD2 as Element of SL by A1;
[DD1,DD2] in wy by A30;
hence thesis by A22,A25,XBOOLE_0:3;
end;
wy is upper
proof
let x,y be Element of [:S,L:];
assume that
A31: x in wy and
A32: x <= y;
consider x1 being open Subset of SL, x2 being Element of SL such that
A33: x = [x1,x2] and
A34: x2 in x1 by A31;
reconsider u2=x2 as Element of L by A1;
x1 in the topology of SL by PRE_TOPC:def 2;
then x1 in sigma L by A1,A2,YELLOW_9:52;
then reconsider u1=x1 as Element of S by YELLOW_1:1;
the carrier of [:S,L:] = [:the carrier of S,the carrier of L:] by
YELLOW_3:def 2;
then consider y1,y2 being object such that
A35: y1 in the carrier of S and
A36: y2 in the carrier of L and
A37: y = [y1,y2] by ZFMISC_1:def 2;
y1 in sigma L by A35,YELLOW_1:1;
then y1 in the topology of SL by A1,A2,YELLOW_9:52;
then reconsider y1 as open Subset of SL by PRE_TOPC:def 2;
reconsider y2 as Element of SL by A1,A36;
reconsider v2=y2 as Element of L by A36;
y1 in the topology of SL by PRE_TOPC:def 2;
then y1 in sigma L by A1,A2,YELLOW_9:52;
then reconsider v1=y1 as Element of S by YELLOW_1:1;
A38: [u1,u2] <= [v1,v2] by A32,A37,A33;
then u2 <= v2 by YELLOW_3:11;
then x2 <= y2 by A1,YELLOW_0:1;
then
A39: y2 in x1 by A34,WAYBEL_0:def 20;
u1 <= v1 by A38,YELLOW_3:11;
then x1 c= y1 by YELLOW_1:3;
hence thesis by A37,A39;
end;
then
A40: wy in the topology of ConvergenceSpace Scott-Convergence [:S,L:] by A10,
WAYBEL11:31;
the topology of SS = sigma S by YELLOW_9:51
.= the topology of T1 by YELLOW_9:51
.= the topology of T;
then
A41: the TopStruct of SS = the TopStruct of T by A8;
the TopStruct of SL = the TopStruct of SL;
then [:SS, SL:] = [:T, SL:] by A41,Th7;
hence thesis by A4,A40,PRE_TOPC:def 2;
end;
a4104[SL] implies InclPoset the topology of SL is continuous
proof
assume a4104[SL];
then a4105[SL] by Lm5;
hence thesis by Lm7;
end;
hence thesis by A1,A2,A5,YELLOW_9:52;
end;
:: 4.11. THEOREM, (1) <=> (2), p. 133.
theorem Th30:
for L being complete LATTICE holds InclPoset sigma L is
continuous iff for S being complete LATTICE holds sigma [:S, L:] = the topology
of [:Sigma S, Sigma L:]
proof
let L be complete LATTICE;
thus InclPoset sigma L is continuous implies for S being complete LATTICE
holds sigma [:S, L:] = the topology of [:Sigma S, Sigma L:] by Lm10;
assume
A1: for S being complete LATTICE holds sigma [:S, L:] = the topology of
[:Sigma S, Sigma L:];
now
let SL be Scott TopAugmentation of L;
let S be complete LATTICE, SS be Scott TopAugmentation of S;
the RelStr of SL = the RelStr of L & the RelStr of Sigma L = the
RelStr of L by YELLOW_9:def 4;
then
A2: the TopStruct of Sigma L = the TopStruct of SL by Th13;
the RelStr of SS = the RelStr of S & the RelStr of Sigma S = the
RelStr of S by YELLOW_9:def 4;
then the TopStruct of Sigma S = the TopStruct of SS by Th13;
then [:SS, SL:] = [:Sigma S, Sigma L:] by A2,Th7;
hence sigma [:S,L:] = the topology of [:SS,SL:] by A1;
end;
hence thesis by Lm11;
end;
:: 4.11. THEOREM, (2) <=> (3), p. 133.
theorem Th31:
for L being complete LATTICE holds (for S being complete LATTICE
holds sigma [:S, L:] = the topology of [:Sigma S, Sigma L:]) iff for S being
complete LATTICE holds the TopStruct of Sigma [:S, L:] = [:Sigma S, Sigma L:]
proof
let L be complete LATTICE;
hereby
assume
A1: for S being complete LATTICE holds sigma [:S, L:] = the topology
of [:Sigma S, Sigma L:];
a4112[L]
proof
let SL be Scott TopAugmentation of L;
let S be complete LATTICE;
let SS be Scott TopAugmentation of S;
the RelStr of SL = the RelStr of L & the RelStr of Sigma L = the
RelStr of L by YELLOW_9:def 4;
then
A2: the TopStruct of Sigma L = the TopStruct of SL by Th13;
the RelStr of SS = the RelStr of S & the RelStr of Sigma S = the
RelStr of S by YELLOW_9:def 4;
then the TopStruct of Sigma S = the TopStruct of SS by Th13;
then [:SS, SL:] = [:Sigma S, Sigma L:] by A2,Th7;
hence thesis by A1;
end;
hence for S being complete LATTICE holds the TopStruct of Sigma [:S, L:] =
[:Sigma S, Sigma L:] by Lm9;
end;
assume
A3: for S being complete LATTICE holds the TopStruct of Sigma [:S, L:] =
[:Sigma S, Sigma L:];
let S be complete LATTICE;
the TopStruct of Sigma [:S, L:] = [:Sigma S, Sigma L:] by A3;
hence thesis by YELLOW_9:51;
end;
:: 4.11. THEOREM, (2) <=> (3+), p. 133.
theorem Th32:
for L being complete LATTICE holds (for S being complete LATTICE
holds sigma [:S, L:] = the topology of [:Sigma S, Sigma L:]) iff for S being
complete LATTICE holds Sigma [:S, L:] = Omega [:Sigma S, Sigma L:]
proof
let L be complete LATTICE;
hereby
assume
A1: for S being complete LATTICE holds sigma [:S, L:] = the topology
of [:Sigma S, Sigma L:];
let S be complete LATTICE;
the TopStruct of Sigma [:S, L:] = [:Sigma S, Sigma L:] by A1,Th31;
then Omega Sigma [:S, L:] = Omega [:Sigma S, Sigma L:] by WAYBEL25:13;
hence Sigma [:S, L:] = Omega [:Sigma S, Sigma L:] by WAYBEL25:15;
end;
assume
A2: for S being complete LATTICE holds Sigma [:S, L:] = Omega [:Sigma S,
Sigma L:];
let S be complete LATTICE;
Sigma [:S, L:] = Omega [:Sigma S, Sigma L:] by A2;
then the TopStruct of Sigma [:S, L:] = [:Sigma S, Sigma L:] by WAYBEL25:def 2
;
hence thesis by YELLOW_9:51;
end;
:: 4.11. THEOREM, (1) <=> (3+), p. 133.
theorem
for L being complete LATTICE holds InclPoset sigma L is continuous iff
for S being complete LATTICE holds Sigma [:S, L:] = Omega [:Sigma S, Sigma L:]
proof
let L be complete LATTICE;
InclPoset sigma L is continuous iff for S being complete LATTICE holds
sigma [:S, L:] = the topology of [:Sigma S, Sigma L:] by Th30;
hence thesis by Th32;
end;