:: WAYBEL29 semantic presentation
begin
theorem Th1: :: WAYBEL29:1
for X, Y being non empty set
for 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 & f is V7() & f is onto holds
f " is uncurrying
proof
let X, Y be non empty set ; ::_thesis: for 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 & f is V7() & f is onto holds
f " is uncurrying
let Z be non empty RelStr ; ::_thesis: 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 & f is V7() & f is onto holds
f " is uncurrying
let S be non empty SubRelStr of Z |^ [:X,Y:]; ::_thesis: for T being non empty SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is currying & f is V7() & f is onto holds
f " is uncurrying
let T be non empty SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of S,T st f is currying & f is V7() & f is onto holds
f " is uncurrying
let f be Function of S,T; ::_thesis: ( f is currying & f is V7() & f is onto implies f " is uncurrying )
assume A1: ( f is currying & f is V7() & f is onto ) ; ::_thesis: f " is uncurrying
then A2: rng f = the carrier of T by FUNCT_2:def_3;
A3: f " = f " 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 :: according to WAYBEL27:def_1 ::_thesis: for b1 being set holds
( not b1 in proj1 (f ") or (f ") . b1 = uncurry b1 )
let x be set ; ::_thesis: ( x in dom (f ") implies x is Function-yielding Function )
assume x in dom (f ") ; ::_thesis: x is Function-yielding Function
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 ; ::_thesis: verum
end;
let g be Function; ::_thesis: ( not g in proj1 (f ") or (f ") . g = uncurry g )
assume g in dom (f ") ; ::_thesis: (f ") . g = uncurry g
then consider h being set such that
A5: h in dom f and
A6: g = f . h by A2, FUNCT_1:def_3;
reconsider h = 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, WAYBEL27:def_2;
then uncurry g = h by A7, FUNCT_5:49;
hence (f ") . g = uncurry g by A1, A3, A5, A6, FUNCT_1:32; ::_thesis: verum
end;
theorem Th2: :: WAYBEL29:2
for X, Y being non empty set
for 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 & f is V7() & f is onto holds
f " is currying
proof
let X, Y be non empty set ; ::_thesis: for 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 & f is V7() & f is onto holds
f " is currying
let Z be non empty RelStr ; ::_thesis: 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 & f is V7() & f is onto holds
f " is currying
let S be non empty SubRelStr of Z |^ [:X,Y:]; ::_thesis: for T being non empty SubRelStr of (Z |^ Y) |^ X
for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds
f " is currying
let T be non empty SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of T,S st f is uncurrying & f is V7() & f is onto holds
f " is currying
let f be Function of T,S; ::_thesis: ( f is uncurrying & f is V7() & f is onto implies f " is currying )
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 & f is V7() & f is onto ) ; ::_thesis: f " is currying
then A3: rng f = the carrier of S by FUNCT_2:def_3;
A4: f " = f " 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 :: according to WAYBEL27:def_2 ::_thesis: for b1 being set holds
( not b1 in proj1 (f ") or (f ") . b1 = curry b1 )
let x be set ; ::_thesis: ( x in dom (f ") implies ( x is Function & proj1 x is Relation ) )
assume x in dom (f ") ; ::_thesis: ( x is Function & proj1 x is Relation )
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 ) ; ::_thesis: verum
end;
let g be Function; ::_thesis: ( not g in proj1 (f ") or (f ") . g = curry g )
assume g in dom (f ") ; ::_thesis: (f ") . g = curry g
then consider h being set such that
A6: h in dom f and
A7: g = f . h by A3, FUNCT_1:def_3;
reconsider h = 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, WAYBEL27:def_1;
then curry g = h by A8, FUNCT_5:48;
hence (f ") . g = curry g by A2, A4, A6, A7, FUNCT_1:32; ::_thesis: verum
end;
theorem :: WAYBEL29:3
for X, Y being non empty set
for 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 & f is V7() & f is onto holds
f is isomorphic
proof
let X, Y be non empty set ; ::_thesis: for 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 & f is V7() & f is onto holds
f is isomorphic
let Z be non empty Poset; ::_thesis: 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 & f is V7() & f is onto holds
f is isomorphic
let S be non empty full SubRelStr of Z |^ [:X,Y:]; ::_thesis: for T being non empty full SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is currying & f is V7() & f is onto holds
f is isomorphic
let T be non empty full SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of S,T st f is currying & f is V7() & f is onto holds
f is isomorphic
let f be Function of S,T; ::_thesis: ( f is currying & f is V7() & f is onto implies f is isomorphic )
assume A1: ( f is currying & f is V7() & f is onto ) ; ::_thesis: f is isomorphic
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, WAYBEL27:21;
hence f is isomorphic by A2, YELLOW16:15; ::_thesis: verum
end;
theorem :: WAYBEL29:4
for X, Y being non empty set
for 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 & f is V7() & f is onto holds
f is isomorphic
proof
let X, Y be non empty set ; ::_thesis: for 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 & f is V7() & f is onto holds
f is isomorphic
let Z be non empty Poset; ::_thesis: 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 & f is V7() & f is onto holds
f is isomorphic
let T be non empty full SubRelStr of Z |^ [:X,Y:]; ::_thesis: for S being non empty full SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds
f is isomorphic
let S be non empty full SubRelStr of (Z |^ Y) |^ X; ::_thesis: for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds
f is isomorphic
let f be Function of S,T; ::_thesis: ( f is uncurrying & f is V7() & f is onto implies f is isomorphic )
assume A1: ( f is uncurrying & f is V7() & f is onto ) ; ::_thesis: f is isomorphic
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, WAYBEL27:21;
hence f is isomorphic by A2, YELLOW16:15; ::_thesis: verum
end;
theorem Th5: :: WAYBEL29:5
for S1, S2, T1, T2 being RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f being Function of S1,T1 st f is isomorphic holds
for g being Function of S2,T2 st g = f holds
g is isomorphic
proof
let S1, S2, T1, T2 be RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f being Function of S1,T1 st f is isomorphic holds
for g being Function of S2,T2 st g = f holds
g is isomorphic )
assume that
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and
A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f being Function of S1,T1 st f is isomorphic holds
for g being Function of S2,T2 st g = f holds
g is isomorphic
let f be Function of S1,T1; ::_thesis: ( f is isomorphic implies for g being Function of S2,T2 st g = f holds
g is isomorphic )
assume A3: f is isomorphic ; ::_thesis: for g being Function of S2,T2 st g = f holds
g is isomorphic
let g be Function of S2,T2; ::_thesis: ( g = f implies g is isomorphic )
assume A4: g = f ; ::_thesis: g is isomorphic
percases ( S1 is empty or not S1 is empty ) ;
supposeA5: S1 is empty ; ::_thesis: g is isomorphic
then T1 is empty by A3, WAYBEL_0:def_38;
then A6: T2 is empty by A2;
S2 is empty by A1, A5;
hence g is isomorphic by A6, WAYBEL_0:def_38; ::_thesis: verum
end;
suppose not S1 is empty ; ::_thesis: g is isomorphic
then reconsider S1 = S1, T1 = T1 as non empty RelStr by A3, WAYBEL_0:def_38;
reconsider f = f as Function of S1,T1 ;
( the carrier of S1 <> {} & the carrier of T1 <> {} ) ;
then reconsider S2 = S2, T2 = T2 as non empty RelStr by A1, A2;
reconsider g = g as Function of S2,T2 ;
A7: now__::_thesis:_for_x,_y_being_Element_of_S2_holds_
(_x_<=_y_iff_g_._x_<=_g_._y_)
let x, y be Element of S2; ::_thesis: ( x <= y iff g . x <= g . y )
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; ::_thesis: verum
end;
rng f = the carrier of T1 by A3, WAYBEL_0:66;
hence g is isomorphic by A2, A3, A4, A7, WAYBEL_0:66; ::_thesis: verum
end;
end;
end;
theorem Th6: :: WAYBEL29:6
for R, S, T being RelStr
for f being Function of R,S st f is isomorphic holds
for g being Function of S,T st g is isomorphic holds
for h being Function of R,T st h = g * f holds
h is isomorphic
proof
let L1, L2, L3 be RelStr ; ::_thesis: for f being Function of L1,L2 st f is isomorphic holds
for g being Function of L2,L3 st g is isomorphic holds
for h being Function of L1,L3 st h = g * f holds
h is isomorphic
let f1 be Function of L1,L2; ::_thesis: ( f1 is isomorphic implies for g being Function of L2,L3 st g is isomorphic holds
for h being Function of L1,L3 st h = g * f1 holds
h is isomorphic )
assume A1: f1 is isomorphic ; ::_thesis: for g being Function of L2,L3 st g is isomorphic holds
for h being Function of L1,L3 st h = g * f1 holds
h is isomorphic
let f2 be Function of L2,L3; ::_thesis: ( f2 is isomorphic implies for h being Function of L1,L3 st h = f2 * f1 holds
h is isomorphic )
assume A2: f2 is isomorphic ; ::_thesis: for h being Function of L1,L3 st h = f2 * f1 holds
h is isomorphic
let h be Function of L1,L3; ::_thesis: ( h = f2 * f1 implies h is isomorphic )
assume A3: h = f2 * f1 ; ::_thesis: h is isomorphic
percases ( ( not L1 is empty & not L2 is empty & not L3 is empty ) or L1 is empty or L2 is empty or L3 is empty ) ;
suppose ( not L1 is empty & not L2 is empty & not L3 is empty ) ; ::_thesis: h is isomorphic
then reconsider L1 = L1, L2 = L2, L3 = L3 as non empty RelStr ;
reconsider f1 = f1 as Function of L1,L2 ;
reconsider f2 = f2 as Function of L2,L3 ;
consider g1 being Function of L2,L1 such that
A4: ( g1 = f1 " & g1 is monotone ) by A1, WAYBEL_0:def_38;
consider g2 being Function of L3,L2 such that
A5: ( g2 = f2 " & 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) " ) by A1, A2, A4, A5, FUNCT_1:44, YELLOW_2:12;
hence h is isomorphic by A1, A2, A3, A6, WAYBEL_0:def_38; ::_thesis: verum
end;
supposeA7: L1 is empty ; ::_thesis: h is isomorphic
then L2 is empty by A1, WAYBEL_0:def_38;
then L3 is empty by A2, WAYBEL_0:def_38;
hence h is isomorphic by A7, WAYBEL_0:def_38; ::_thesis: verum
end;
suppose L2 is empty ; ::_thesis: h is isomorphic
then ( L1 is empty & L3 is empty ) by A1, A2, WAYBEL_0:def_38;
hence h is isomorphic by WAYBEL_0:def_38; ::_thesis: verum
end;
supposeA8: L3 is empty ; ::_thesis: h is isomorphic
then L2 is empty by A2, WAYBEL_0:def_38;
then L1 is empty by A1, WAYBEL_0:def_38;
hence h is isomorphic by A8, WAYBEL_0:def_38; ::_thesis: verum
end;
end;
end;
theorem Th7: :: WAYBEL29:7
for X, Y, X1, Y1 being TopSpace st TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
[:X,Y:] = [:X1,Y1:]
proof
let X, Y, X1, Y1 be TopSpace; ::_thesis: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) implies [:X,Y:] = [:X1,Y1:] )
assume A1: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X1, the topology of X1 #) & TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ) ; ::_thesis: [:X,Y:] = [:X1,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:] = { (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 ) } } by A1, BORSUK_1:def_2
.= the topology of [:X1,Y1:] by BORSUK_1:def_2 ;
hence [:X,Y:] = [:X1,Y1:] by A2; ::_thesis: verum
end;
theorem Th8: :: WAYBEL29:8
for X being non empty TopSpace
for L being non empty up-complete Scott 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; ::_thesis: for L being non empty up-complete Scott 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
let L be non empty up-complete Scott TopPoset; ::_thesis: for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L
let F be non empty directed Subset of (ContMaps (X,L)); ::_thesis: "\/" (F,(L |^ the carrier of X)) is continuous Function of 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 = "\/" (F,(L |^ the carrier of X)) 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__::_thesis:_for_A_being_Subset_of_L_st_A_is_open_holds_
sF_"_A_is_open
let A be Subset of L; ::_thesis: ( A is open implies sF " A is open )
assume A2: A is open ; ::_thesis: sF " A is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_sF_"_A_implies_ex_Q_being_Element_of_bool_the_carrier_of_X_st_
(_Q_is_open_&_Q_c=_sF_"_A_&_x_in_Q_)_)_&_(_ex_Q_being_Subset_of_X_st_
(_Q_is_open_&_Q_c=_sF_"_A_&_x_in_Q_)_implies_x_in_sF_"_A_)_)
let x be set ; ::_thesis: ( ( x in sF " A implies ex Q being Element of bool the carrier of X st
( Q is open & Q c= sF " A & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) )
hereby ::_thesis: ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A )
assume A3: x in sF " A ; ::_thesis: ex Q being Element of bool the carrier of X st
( Q is open & Q c= sF " A & x in Q )
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 by FUNCOP_1:7;
then A7: ( pi (aF,y) is directed & not pi (aF,y) is 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 set 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 = f as continuous Function of X,L by A11, WAYBEL24:21;
take Q = f " A; ::_thesis: ( Q is open & Q c= sF " A & x in Q )
[#] L <> {} ;
hence Q is open by A2, TOPS_2:43; ::_thesis: ( Q c= sF " A & x in Q )
A13: dom sF = the carrier of X by FUNCT_2:def_1;
thus Q c= sF " A ::_thesis: x in Q
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Q or b in sF " A )
assume A14: b in Q ; ::_thesis: b in sF " A
then A15: f . b in A by FUNCT_1:def_7;
reconsider b = b as Element of X by A14;
A16: ( the carrier of X => L) . b = L by FUNCOP_1:7;
then ( pi (aF,b) is directed & not pi (aF,b) is 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, LATTICE3:def_9;
then sF . b in A by A2, A15, WAYBEL_0:def_20;
hence b in sF " A by A13, FUNCT_1:def_7; ::_thesis: verum
end;
dom f = the carrier of X by FUNCT_2:def_1;
hence x in Q by A10, A12, FUNCT_1:def_7; ::_thesis: verum
end;
thus ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) ; ::_thesis: verum
end;
hence sF " A is open by TOPS_1:25; ::_thesis: verum
end;
[#] L <> {} ;
hence "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L by A1, TOPS_2:43; ::_thesis: verum
end;
theorem Th9: :: WAYBEL29:9
for X being non empty TopSpace
for L being non empty up-complete Scott TopPoset holds ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X
proof
let X be non empty TopSpace; ::_thesis: for L being non empty up-complete Scott TopPoset holds ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X
let L be non empty up-complete Scott TopPoset; ::_thesis: ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X
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; :: according to WAYBEL_0:def_4 ::_thesis: ( A = {} or not ex_sup_of A,L |^ the carrier of X or "\/" (A,(L |^ the carrier of X)) in the carrier of XL )
assume that
A1: A <> {} and
ex_sup_of A,L |^ the carrier of X ; ::_thesis: "\/" (A,(L |^ the carrier of X)) in the carrier of XL
reconsider A = A as non empty directed Subset of XL by A1;
"\/" (A,(L |^ the carrier of X)) is continuous Function of X,L by Th8;
hence "\/" (A,(L |^ the carrier of X)) in the carrier of XL by WAYBEL24:def_3; ::_thesis: verum
end;
hence ContMaps (X,L) is directed-sups-inheriting SubRelStr of L |^ the carrier of X ; ::_thesis: verum
end;
theorem Th10: :: WAYBEL29:10
for S1, S2 being TopStruct st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) holds
for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds
ContMaps (S1,T1) = ContMaps (S2,T2)
proof
let S1, S2 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) implies for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds
ContMaps (S1,T1) = ContMaps (S2,T2) )
assume A1: TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) ; ::_thesis: for T1, T2 being non empty TopRelStr st TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) holds
ContMaps (S1,T1) = ContMaps (S2,T2)
let T1, T2 be non empty TopRelStr ; ::_thesis: ( TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) implies ContMaps (S1,T1) = ContMaps (S2,T2) )
assume A2: TopRelStr(# the carrier of T1, the InternalRel of T1, the topology of T1 #) = TopRelStr(# the carrier of T2, the InternalRel of T2, the topology of T2 #) ; ::_thesis: ContMaps (S1,T1) = ContMaps (S2,T2)
then RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel 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)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (ContMaps (S2,T2)) c= the carrier of (ContMaps (S1,T1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ContMaps (S1,T1)) or x in the carrier of (ContMaps (S2,T2)) )
assume x in the carrier of (ContMaps (S1,T1)) ; ::_thesis: x in the carrier of (ContMaps (S2,T2))
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; :: according to PRE_TOPC:def_6 ::_thesis: ( not P2 is closed or f2 " P2 is closed )
reconsider P1 = P2 as Subset of T1 by A2;
assume P2 is closed ; ::_thesis: f2 " P2 is closed
then ([#] T2) \ P2 is open by PRE_TOPC:def_3;
then ([#] T2) \ P2 in the topology of T2 by PRE_TOPC:def_2;
then ([#] T1) \ P1 is open by A2, PRE_TOPC:def_2;
then P1 is closed by PRE_TOPC:def_3;
then f " P1 is closed by A4, PRE_TOPC:def_6;
then ([#] S1) \ (f " P1) is open by PRE_TOPC:def_3;
then ([#] S1) \ (f2 " P2) in the topology of S2 by A1, PRE_TOPC:def_2;
then ([#] S2) \ (f2 " P2) is open by A1, PRE_TOPC:def_2;
hence f2 " P2 is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
hence x in the carrier of (ContMaps (S2,T2)) by A3, WAYBEL24:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ContMaps (S2,T2)) or x in the carrier of (ContMaps (S1,T1)) )
assume x in the carrier of (ContMaps (S2,T2)) ; ::_thesis: x in the carrier of (ContMaps (S1,T1))
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; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f1 " P1 is closed )
reconsider P2 = P1 as Subset of T2 by A2;
assume P1 is closed ; ::_thesis: f1 " P1 is closed
then ([#] T1) \ P1 is open by PRE_TOPC:def_3;
then ([#] T1) \ P2 in the topology of T2 by A2, PRE_TOPC:def_2;
then ([#] T2) \ P2 is open by A2, PRE_TOPC:def_2;
then P2 is closed by PRE_TOPC:def_3;
then f " P2 is closed by A6, PRE_TOPC:def_6;
then ([#] S2) \ (f " P2) is open by PRE_TOPC:def_3;
then ([#] S2) \ (f1 " P1) in the topology of S1 by A1, PRE_TOPC:def_2;
then ([#] S1) \ (f1 " P1) is open by A1, PRE_TOPC:def_2;
hence f1 " P1 is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
hence x in the carrier of (ContMaps (S1,T1)) by A5, WAYBEL24:def_3; ::_thesis: verum
end;
then RelStr(# the carrier of C1, the InternalRel of C1 #) = RelStr(# the carrier of C2, the InternalRel of C2 #) by YELLOW_0:57;
hence ContMaps (S1,T1) = ContMaps (S2,T2) ; ::_thesis: verum
end;
registration
cluster TopSpace-like reflexive transitive antisymmetric Scott continuous with_suprema with_infima complete -> T_0 continuous injective complete for TopRelStr ;
coherence
for b1 being continuous complete TopLattice st b1 is Scott holds
( b1 is injective & b1 is T_0 )
proof
let T be continuous complete TopLattice; ::_thesis: ( T is Scott implies ( T is injective & T is T_0 ) )
assume T is Scott ; ::_thesis: ( T is injective & T is T_0 )
then T is Scott TopAugmentation of T by YELLOW_9:44;
hence ( T is injective & T is T_0 ) ; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like reflexive transitive antisymmetric Scott continuous non void with_suprema with_infima complete for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is Scott & b1 is continuous & b1 is complete )
proof
set L = the continuous complete LATTICE;
set T = the Scott TopAugmentation of the continuous complete LATTICE;
take the Scott TopAugmentation of the continuous complete LATTICE ; ::_thesis: ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete )
thus ( the Scott TopAugmentation of the continuous complete LATTICE is Scott & the Scott TopAugmentation of the continuous complete LATTICE is continuous & the Scott TopAugmentation of the continuous complete LATTICE is complete ) ; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
let L be non empty up-complete Scott TopPoset;
cluster ContMaps (X,L) -> up-complete ;
coherence
ContMaps (X,L) is up-complete
proof
ContMaps (X,L) is full directed-sups-inheriting SubRelStr of L |^ the carrier of X by Th9, WAYBEL24:def_3;
hence ContMaps (X,L) is up-complete by YELLOW16:5; ::_thesis: verum
end;
end;
theorem Th11: :: WAYBEL29:11
for I being non empty set
for J being non-Empty Poset-yielding 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 ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds J . i is up-complete ) holds
I -POS_prod J is up-complete
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is up-complete ) implies I -POS_prod J is up-complete )
assume A1: for i being Element of I holds J . i is up-complete ; ::_thesis: I -POS_prod J is up-complete
set L = I -POS_prod J;
now__::_thesis:_for_A_being_non_empty_directed_Subset_of_(I_-POS_prod_J)_holds_ex_sup_of_A,I_-POS_prod_J
let A be non empty directed Subset of (I -POS_prod J); ::_thesis: ex_sup_of A,I -POS_prod J
now__::_thesis:_for_x_being_Element_of_I_holds_ex_sup_of_pi_(A,x),J_._x
let x be Element of I; ::_thesis: ex_sup_of pi (A,x),J . x
( J . x is non empty up-complete Poset & pi (A,x) is directed & not pi (A,x) is empty ) by A1, YELLOW16:35;
hence ex_sup_of pi (A,x),J . x by WAYBEL_0:75; ::_thesis: verum
end;
hence ex_sup_of A,I -POS_prod J by YELLOW16:31; ::_thesis: verum
end;
hence I -POS_prod J is up-complete by WAYBEL_0:75; ::_thesis: verum
end;
theorem :: WAYBEL29:12
for I being non empty set
for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) holds
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 ; ::_thesis: for J being non-Empty Poset-yielding ManySortedSet of I st ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) holds
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) ) )
let J be non-Empty Poset-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ) implies 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) ) ) )
set L = product J;
assume A1: for i being Element of I holds
( J . i is up-complete & J . i is lower-bounded ) ; ::_thesis: 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) ) )
then reconsider L9 = product J as non empty up-complete Poset by Th11;
let x, y be Element of (product J); ::_thesis: ( 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) ) )
hereby ::_thesis: ( ( 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) implies x << y )
assume A2: x << y ; ::_thesis: ( ( 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) )
hereby ::_thesis: 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)
let i be Element of I; ::_thesis: x . i << y . i
thus x . i << y . i ::_thesis: verum
proof
let Di be non empty directed Subset of (J . i); :: according to WAYBEL_3:def_1 ::_thesis: ( not y . i <= "\/" (Di,(J . i)) or ex b1 being Element of the carrier of (J . i) st
( b1 in Di & x . i <= b1 ) )
assume A3: y . i <= sup Di ; ::_thesis: ex b1 being Element of the carrier of (J . i) st
( b1 in Di & x . i <= b1 )
set di = the Element of Di;
set D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } ;
reconsider di = the Element of Di as Element of (J . i) ;
A4: dom y = I by WAYBEL_3:27;
{ (y +* (i,z)) where z is Element of (J . i) : z in Di } c= the carrier of (product J)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (y +* (i,z)) where z is Element of (J . i) : z in Di } or a in the carrier of (product J) )
assume a in { (y +* (i,z)) where z is Element of (J . i) : z in Di } ; ::_thesis: a in the carrier of (product J)
then consider z being Element of (J . i) such that
A5: a = y +* (i,z) and
z in Di ;
A6: now__::_thesis:_for_j_being_Element_of_I_holds_(y_+*_(i,z))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: (y +* (i,z)) . j is Element of (J . j)
( 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, FUNCT_7:32;
hence (y +* (i,z)) . j is Element of (J . j) ; ::_thesis: verum
end;
dom (y +* (i,z)) = I by A4, FUNCT_7:30;
then a is Element of (product J) by A5, A6, WAYBEL_3:27;
hence a in the carrier of (product J) ; ::_thesis: verum
end;
then reconsider D = { (y +* (i,z)) where z is Element of (J . i) : z in Di } as Subset of (product J) ;
A7: y +* (i,di) in D ;
then reconsider D = D as non empty Subset of (product J) ;
D is directed
proof
let z1, z2 be Element of (product J); :: according to WAYBEL_0:def_1 ::_thesis: ( not z1 in D or not z2 in D or ex b1 being Element of the carrier of (product J) st
( b1 in D & z1 <= b1 & z2 <= b1 ) )
assume z1 in D ; ::_thesis: ( not z2 in D or ex b1 being Element of the carrier of (product J) st
( b1 in D & z1 <= b1 & z2 <= b1 ) )
then consider a1 being Element of (J . i) such that
A8: z1 = y +* (i,a1) and
A9: a1 in Di ;
assume z2 in D ; ::_thesis: ex b1 being Element of the carrier of (product J) st
( b1 in D & z1 <= b1 & z2 <= b1 )
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 (product J) ;
take z ; ::_thesis: ( z in D & z1 <= z & z2 <= z )
thus z in D by A12; ::_thesis: ( z1 <= z & z2 <= z )
A15: dom y = I by WAYBEL_3:27;
now__::_thesis:_for_j_being_Element_of_I_holds_z_._j_>=_z1_._j
let j be Element of I; ::_thesis: z . j >= z1 . j
( 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, FUNCT_7:32;
hence z . j >= z1 . j by A13, YELLOW_0:def_1; ::_thesis: verum
end;
hence z >= z1 by WAYBEL_3:28; ::_thesis: z2 <= z
now__::_thesis:_for_j_being_Element_of_I_holds_z_._j_>=_z2_._j
let j be Element of I; ::_thesis: z . j >= z2 . j
( 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, FUNCT_7:32;
hence z . j >= z2 . j by A14, YELLOW_0:def_1; ::_thesis: verum
end;
hence z2 <= z by WAYBEL_3:28; ::_thesis: verum
end;
then reconsider D = D as non empty directed Subset of (product J) ;
A16: dom y = I by WAYBEL_3:27;
now__::_thesis:_for_j_being_Element_of_I_holds_(sup_D)_._j_>=_y_._j
A17: Di c= pi (D,i)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Di or a in pi (D,i) )
assume A18: a in Di ; ::_thesis: a in pi (D,i)
then reconsider a = 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 a in pi (D,i) by A16, FUNCT_7:31; ::_thesis: verum
end;
let j be Element of I; ::_thesis: (sup D) . j >= y . j
A19: ( J . i is non empty up-complete Poset & J . j is non empty up-complete Poset ) by A1;
( not pi (D,i) is empty & pi (D,i) is 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__::_thesis:_(_j_<>_i_implies_y_._j_in_pi_(D,j)_)
assume j <> i ; ::_thesis: y . j in pi (D,j)
then (y +* (i,di)) . j = y . j by FUNCT_7:32;
hence y . j in pi (D,j) by A7, CARD_3:def_6; ::_thesis: verum
end;
( not pi (D,j) is empty & pi (D,j) is 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, LATTICE3:def_9, YELLOW_0:def_2; ::_thesis: verum
end;
then sup D >= y by WAYBEL_3:28;
then consider d being Element of (product J) such that
A24: d in D and
A25: d >= x by A2, WAYBEL_3:def_1;
consider z being Element of (J . i) such that
A26: d = y +* (i,z) and
A27: z in Di by A24;
take z ; ::_thesis: ( z in Di & x . i <= z )
d . i = z by A4, A26, FUNCT_7:31;
hence ( z in Di & x . i <= z ) by A25, A27, WAYBEL_3:28; ::_thesis: verum
end;
end;
set K = { i where i is Element of I : x . i <> Bottom (J . i) } ;
{ i where i is Element of I : x . i <> Bottom (J . i) } c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of I : x . i <> Bottom (J . i) } or a in I )
assume a in { i where i is Element of I : x . i <> Bottom (J . i) } ; ::_thesis: a in I
then ex i being Element of I st
( a = i & x . i <> Bottom (J . i) ) ;
hence a in I ; ::_thesis: verum
end;
then reconsider K = { i where i is Element of I : x . i <> Bottom (J . i) } as Subset of I ;
deffunc H1( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
consider f being ManySortedSet of I such that
A28: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A29: now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
f . i = Bottom (J . i) by A28;
hence f . i is Element of (J . i) ; ::_thesis: verum
end;
A30: dom f = I by PARTFUN1:def_2;
then reconsider f = f as Element of (product J) by A29, WAYBEL_3:27;
set X = { (f +* (y | a)) where a is finite Subset of I : verum } ;
{ (f +* (y | a)) where a is finite Subset of I : verum } c= the carrier of (product J)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f +* (y | a)) where a is finite Subset of I : verum } or a in the carrier of (product J) )
assume a in { (f +* (y | a)) where a is finite Subset of I : verum } ; ::_thesis: a in the carrier of (product J)
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__::_thesis:_for_i_being_Element_of_I_holds_(f_+*_(y_|_b))_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: (f +* (y | b)) . i is Element of (J . 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, FUNCT_4:13;
hence (f +* (y | b)) . i is Element of (J . i) ; ::_thesis: verum
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 (product J) by A31, A33, WAYBEL_3:27;
hence a in the carrier of (product J) ; ::_thesis: verum
end;
then reconsider X = { (f +* (y | a)) where a is finite Subset of I : verum } as Subset of (product J) ;
f +* (y | ({} I)) in X ;
then reconsider X = X as non empty Subset of (product J) ;
X is directed
proof
let z1, z2 be Element of (product J); :: according to WAYBEL_0:def_1 ::_thesis: ( not z1 in X or not z2 in X or ex b1 being Element of the carrier of (product J) st
( b1 in X & z1 <= b1 & z2 <= b1 ) )
assume z1 in X ; ::_thesis: ( not z2 in X or ex b1 being Element of the carrier of (product J) st
( b1 in X & z1 <= b1 & z2 <= b1 ) )
then consider a1 being finite Subset of I such that
A34: z1 = f +* (y | a1) ;
assume z2 in X ; ::_thesis: ex b1 being Element of the carrier of (product J) st
( b1 in X & z1 <= b1 & z2 <= b1 )
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 (product J) ;
take z ; ::_thesis: ( z in X & z1 <= z & z2 <= z )
thus z in X ; ::_thesis: ( z1 <= z & z2 <= z )
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__::_thesis:_for_i_being_Element_of_I_holds_z_._i_>=_z1_._i
let i be Element of I; ::_thesis: z . b1 >= z1 . b1
A39: f . i = Bottom (J . i) by A28;
J . i is non empty lower-bounded up-complete Poset by A1;
then A40: Bottom (J . i) <= y . i by YELLOW_0:44;
percases ( ( not i in a1 & i in a ) or ( not i in a & not i in a1 ) or ( i in a1 & i in a ) ) by XBOOLE_0:def_3;
supposeA41: ( not i in a1 & i in a ) ; ::_thesis: z . b1 >= z1 . b1
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; ::_thesis: verum
end;
suppose ( not i in a & not i in a1 ) ; ::_thesis: z . b1 >= z1 . b1
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; ::_thesis: verum
end;
supposeA42: ( i in a1 & i in a ) ; ::_thesis: z . b1 >= z1 . b1
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; ::_thesis: verum
end;
end;
end;
hence z >= z1 by WAYBEL_3:28; ::_thesis: z2 <= z
A44: dom (y | a2) = a2 by A36, RELAT_1:62;
now__::_thesis:_for_i_being_Element_of_I_holds_z_._i_>=_z2_._i
let i be Element of I; ::_thesis: z . b1 >= z2 . b1
A45: f . i = Bottom (J . i) by A28;
J . i is non empty lower-bounded up-complete Poset by A1;
then A46: Bottom (J . i) <= y . i by YELLOW_0:44;
percases ( ( not i in a2 & i in a ) or ( not i in a & not i in a2 ) or ( i in a2 & i in a ) ) by XBOOLE_0:def_3;
supposeA47: ( not i in a2 & i in a ) ; ::_thesis: z . b1 >= z2 . b1
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; ::_thesis: verum
end;
suppose ( not i in a & not i in a2 ) ; ::_thesis: z . b1 >= z2 . b1
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; ::_thesis: verum
end;
supposeA48: ( i in a2 & i in a ) ; ::_thesis: z . b1 >= z2 . b1
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; ::_thesis: verum
end;
end;
end;
hence z2 <= z by WAYBEL_3:28; ::_thesis: verum
end;
then reconsider X = X as non empty directed Subset of (product J) ;
now__::_thesis:_for_i_being_Element_of_I_holds_(sup_X)_._i_>=_y_._i
let i be Element of I; ::_thesis: (sup X) . i >= y . 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 (product J) ;
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, LATTICE3:def_9;
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; ::_thesis: verum
end;
then y <= sup X by WAYBEL_3:28;
then consider d being Element of (product J) such that
A54: d in X and
A55: x <= d by A2, WAYBEL_3:def_1;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not j in K or j in a )
assume j in K ; ::_thesis: j in a
then consider i being Element of I such that
A58: j = i and
A59: x . i <> Bottom (J . i) ;
J . i is non empty lower-bounded up-complete Poset by A1;
then A60: x . i >= Bottom (J . i) by YELLOW_0:44;
assume not j in a ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then reconsider K = K as finite Subset of I ;
take K = K; ::_thesis: for i being Element of I st not i in K holds
x . i = Bottom (J . i)
thus for i being Element of I st not i in K holds
x . i = Bottom (J . i) ; ::_thesis: verum
end;
defpred S1[ set , set ] means ex i being Element of I ex z being Element of (product J) st
( $1 = i & $2 = z & z . i >= x . i );
assume A62: for i being Element of I holds x . i << y . i ; ::_thesis: ( for K being finite Subset of I ex i being Element of I st
( not i in K & not x . i = Bottom (J . i) ) or x << y )
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) ; ::_thesis: x << y
let D be non empty directed Subset of (product J); :: according to WAYBEL_3:def_1 ::_thesis: ( not y <= "\/" (D,(product J)) or ex b1 being Element of the carrier of (product J) st
( b1 in D & x <= b1 ) )
assume A64: y <= sup D ; ::_thesis: ex b1 being Element of the carrier of (product J) st
( b1 in D & x <= b1 )
A65: now__::_thesis:_for_k_being_set_st_k_in_K_holds_
ex_a_being_set_st_
(_a_in_D_&_S1[k,a]_)
let k be set ; ::_thesis: ( k in K implies ex a being set st
( a in D & S1[k,a] ) )
assume k in K ; ::_thesis: ex a being set st
( a in D & S1[k,a] )
then reconsider i = k as Element of I ;
A66: pi (D,i) is directed
proof
let a, b be Element of (J . i); :: according to WAYBEL_0:def_1 ::_thesis: ( not a in pi (D,i) or not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )
assume a in pi (D,i) ; ::_thesis: ( not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )
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) ; ::_thesis: ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 )
then consider g being Function such that
A69: g in D and
A70: b = g . i by CARD_3:def_6;
reconsider f = f, g = g as Element of (product J) by A67, A69;
consider h being Element of (product J) such that
A71: ( h in D & h >= f & h >= g ) by A67, A69, WAYBEL_0:def_1;
take h . i ; ::_thesis: ( h . i in pi (D,i) & a <= h . i & b <= h . i )
thus ( h . i in pi (D,i) & a <= h . i & b <= h . i ) by A68, A70, A71, CARD_3:def_6, WAYBEL_3:28; ::_thesis: verum
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, WAYBEL_3:def_1;
consider a being Function such that
A75: a in D and
A76: zi = a . i by A73, CARD_3:def_6;
reconsider a = a as set ;
take a = a; ::_thesis: ( a in D & S1[k,a] )
thus a in D by A75; ::_thesis: S1[k,a]
thus S1[k,a] by A74, A75, A76; ::_thesis: verum
end;
consider F being Function such that
A77: ( dom F = K & rng F c= D ) and
A78: for k being set st k in K holds
S1[k,F . k] from FUNCT_1:sch_5(A65);
reconsider Y = rng F as finite Subset of D by A77, FINSET_1:8;
consider d being Element of (product J) such that
A79: d in D and
A80: d is_>=_than Y by WAYBEL_0:1;
take d ; ::_thesis: ( d in D & x <= d )
thus d in D by A79; ::_thesis: x <= d
now__::_thesis:_for_i_being_Element_of_I_holds_d_._i_>=_x_._i
let i be Element of I; ::_thesis: d . b1 >= x . b1
A81: J . i is non empty lower-bounded up-complete Poset by A1;
percases ( i in K or not i in K ) ;
supposeA82: i in K ; ::_thesis: d . b1 >= x . b1
then consider j being Element of I, z being Element of (product J) 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, LATTICE3:def_9;
then d . i >= z . i by WAYBEL_3:28;
hence d . i >= x . i by A81, A83, A85, YELLOW_0:def_2; ::_thesis: verum
end;
suppose not i in K ; ::_thesis: d . b1 >= x . b1
then x . i = Bottom (J . i) by A63;
hence d . i >= x . i by A81, YELLOW_0:44; ::_thesis: verum
end;
end;
end;
hence x <= d by WAYBEL_3:28; ::_thesis: verum
end;
registration
let X be set ;
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
clusterL |^ X -> lower-bounded ;
coherence
L |^ X is lower-bounded
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 FUNCT_2:def_1, YELLOW_1:28;
then reconsider f = X --> (Bottom L) as Element of (L |^ X) by A1, FUNCT_2:def_2;
take f ; :: according to YELLOW_0:def_4 ::_thesis: f is_<=_than the carrier of (L |^ X)
let g be Element of (L |^ X); :: according to LATTICE3:def_8 ::_thesis: ( not g in the carrier of (L |^ X) or f <= g )
percases ( X is empty or not X is empty ) ;
supposeA2: X is empty ; ::_thesis: ( not g in the carrier of (L |^ X) or f <= g )
A3: f <= f ;
( L |^ X = RelStr(# {{}},(id {{}}) #) & f = {} ) by A2, YELLOW_1:27;
hence ( not g in the carrier of (L |^ X) or f <= g ) by A3, TARSKI:def_1; ::_thesis: verum
end;
suppose not X is empty ; ::_thesis: ( not g in the carrier of (L |^ X) or f <= g )
then reconsider X = X as non empty set ;
reconsider f = f, g = g as Element of (L |^ X) ;
now__::_thesis:_for_x_being_Element_of_X_holds_f_._x_<=_g_._x
let x be Element of X; ::_thesis: f . x <= g . x
f . x = Bottom L by FUNCOP_1:7;
hence f . x <= g . x by YELLOW_0:44; ::_thesis: verum
end;
hence ( not g in the carrier of (L |^ X) or f <= g ) by WAYBEL27:14; ::_thesis: verum
end;
end;
end;
end;
registration
let X be non empty TopSpace;
let L be non empty lower-bounded TopPoset;
cluster ContMaps (X,L) -> lower-bounded ;
coherence
ContMaps (X,L) is lower-bounded
proof
reconsider f = X --> (Bottom L) as Element of (ContMaps (X,L)) by WAYBEL24:21;
take f ; :: according to YELLOW_0:def_4 ::_thesis: f is_<=_than the carrier of (ContMaps (X,L))
let g be Element of (ContMaps (X,L)); :: according to LATTICE3:def_8 ::_thesis: ( not g in the carrier of (ContMaps (X,L)) or f <= g )
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: TopStruct(# the carrier of (Omega X), the topology of (Omega X) #) = TopStruct(# the carrier of X, the topology 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 ( not g in the carrier of (ContMaps (X,L)) or f <= g ) by A1, YELLOW_0:60; ::_thesis: verum
end;
end;
registration
let L be non empty up-complete Poset;
cluster -> up-complete for TopAugmentation of L;
coherence
for b1 being TopAugmentation of L holds b1 is up-complete
proof
let S be TopAugmentation of L; ::_thesis: S is up-complete
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
hence S is up-complete by WAYBEL_8:15; ::_thesis: verum
end;
cluster Scott -> correct for TopAugmentation of L;
coherence
for b1 being TopAugmentation of L st b1 is Scott holds
b1 is correct
proof
let IT be TopAugmentation of L; ::_thesis: ( IT is Scott implies IT is correct )
assume A1: IT is Scott ; ::_thesis: IT is correct
then [#] IT is open ;
hence the carrier of IT in the topology of IT by PRE_TOPC:def_2; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of IT) holds
( not b1 c= the topology of IT or union b1 in the topology of IT ) ) & ( for b1, b2 being Element of bool the carrier of IT holds
( not b1 in the topology of IT or not b2 in the topology of IT or b1 /\ b2 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 ::_thesis: for b1, b2 being Element of bool the carrier of IT holds
( not b1 in the topology of IT or not b2 in the topology of IT or b1 /\ b2 in the topology of IT )
proof
let a be Subset-Family of IT; ::_thesis: ( a c= the topology of IT implies union a in the topology of IT )
assume A2: a c= the topology of IT ; ::_thesis: union a in the topology of IT
A3: union a is inaccessible
proof
let D be non empty directed Subset of IT; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,IT) in union a or not D misses union a )
assume sup D in union a ; ::_thesis: not D misses 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 = A as Subset of IT by A5;
A is open by A2, A5, PRE_TOPC:def_2;
then D meets A by A1, A4, WAYBEL11:def_1;
then consider x being set 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 not D misses union a by A6, XBOOLE_0:3; ::_thesis: verum
end;
now__::_thesis:_for_X_being_Subset_of_IT_st_X_in_a_holds_
X_is_upper
let X be Subset of IT; ::_thesis: ( X in a implies X is upper )
assume X in a ; ::_thesis: X is upper
then X is open by A2, PRE_TOPC:def_2;
hence X is upper by A1; ::_thesis: verum
end;
then union a is upper by WAYBEL_0:28;
hence union a in the topology of IT by A1, A3, PRE_TOPC:def_2; ::_thesis: verum
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 ::_thesis: verum
proof
let a, b be Subset of IT; ::_thesis: ( a in the topology of IT & b in the topology of IT implies a /\ b in the topology of IT )
assume that
A8: a in the topology of IT and
A9: b in the topology of IT ; ::_thesis: a /\ b in the topology of IT
reconsider a1 = a, b1 = b as Subset of IT ;
A10: b1 is open by A9, PRE_TOPC:def_2;
A11: a1 is open by A8, PRE_TOPC:def_2;
A12: a /\ b is inaccessible
proof
let D be non empty directed Subset of IT; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,IT) in a /\ b or not D misses a /\ b )
assume A13: sup D in a /\ b ; ::_thesis: not D misses 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 set 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 set such that
A16: d2 in D and
A17: d2 in b1 by XBOOLE_0:3;
reconsider d1 = d1, d2 = 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 not D misses a /\ b by A18, XBOOLE_0:3; ::_thesis: verum
end;
a /\ b is upper by A1, A11, A10, WAYBEL_0:29;
hence a /\ b in the topology of IT by A1, A12, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
registration
let L be non empty up-complete Poset;
cluster non empty reflexive transitive antisymmetric up-complete strict Scott non void for TopAugmentation of L;
existence
ex b1 being TopAugmentation of L st
( b1 is strict & b1 is Scott )
proof
set T = { S where S is Subset of L : ( S is upper & S is inaccessible ) } ;
{ S where S is Subset of L : ( S is upper & S is inaccessible ) } c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { S where S is Subset of L : ( S is upper & S is inaccessible ) } or x in bool the carrier of L )
assume x in { S where S is Subset of L : ( S is upper & S is inaccessible ) } ; ::_thesis: x in bool the carrier of L
then ex S being Subset of L st
( x = S & S is upper & S is inaccessible ) ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider T = { S where S is Subset of L : ( S is upper & S is inaccessible ) } as Subset-Family of L ;
set SL = TopRelStr(# the carrier of L, the InternalRel of L,T #);
A1: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,T #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,T #) #) ;
then reconsider SL = TopRelStr(# the carrier of L, the InternalRel of L,T #) as TopAugmentation of L by YELLOW_9:def_4;
take SL ; ::_thesis: ( SL is strict & SL is Scott )
for S being Subset of SL holds
( S is open iff ( S is inaccessible & S is upper ) )
proof
let S be Subset of SL; ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) )
thus ( S is open implies ( S is inaccessible & S is upper ) ) ::_thesis: ( S is inaccessible & S is upper implies S is open )
proof
assume S is open ; ::_thesis: ( S is inaccessible & S is upper )
then S in T by PRE_TOPC:def_2;
then ex S1 being Subset of L st
( S1 = S & S1 is upper & S1 is inaccessible ) ;
hence ( S is inaccessible & S is upper ) by A1, WAYBEL_0:25, YELLOW_9:47; ::_thesis: verum
end;
thus ( S is inaccessible & S is upper implies S is open ) ::_thesis: verum
proof
reconsider S1 = S as Subset of L ;
assume ( S is inaccessible & S is upper ) ; ::_thesis: S is open
then ( S1 is inaccessible & S1 is upper ) by A1, WAYBEL_0:25, YELLOW_9:47;
then S in the topology of SL ;
hence S is open by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
hence ( SL is strict & SL is Scott ) by WAYBEL11:def_4; ::_thesis: verum
end;
end;
theorem Th13: :: WAYBEL29:13
for L being non empty up-complete Poset
for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2
proof
let L be non empty up-complete Poset; ::_thesis: for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2
let S1, S2 be Scott TopAugmentation of L; ::_thesis: the topology of S1 = the topology of S2
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4
.= RelStr(# the carrier of S2, the InternalRel of S2 #) by YELLOW_9:def_4 ;
thus the topology of S1 c= the topology of S2 :: according to XBOOLE_0:def_10 ::_thesis: the topology of S2 c= the topology of S1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of S1 or x in the topology of S2 )
assume x in the topology of S1 ; ::_thesis: x in the topology of S2
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 & z is upper ) by A1, WAYBEL_0:25, YELLOW_9:47;
hence x in the topology of S2 by PRE_TOPC:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of S2 or x in the topology of S1 )
assume x in the topology of S2 ; ::_thesis: x in the topology of S1
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 & z is upper ) by A1, WAYBEL_0:25, YELLOW_9:47;
hence x in the topology of S1 by PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th14: :: WAYBEL29:14
for S1, S2 being non empty reflexive antisymmetric up-complete TopRelStr st TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) & S1 is Scott holds
S2 is Scott
proof
let S1, S2 be non empty reflexive antisymmetric up-complete TopRelStr ; ::_thesis: ( TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) & S1 is Scott implies S2 is Scott )
assume A1: TopRelStr(# the carrier of S1, the InternalRel of S1, the topology of S1 #) = TopRelStr(# the carrier of S2, the InternalRel of S2, the topology of S2 #) ; ::_thesis: ( not S1 is Scott or S2 is Scott )
assume A2: S1 is Scott ; ::_thesis: S2 is Scott
let T be Subset of S2; :: according to WAYBEL11:def_4 ::_thesis: ( ( not T is open or ( T is inaccessible_by_directed_joins & T is upper ) ) & ( not T is inaccessible_by_directed_joins or not T is upper or T is open ) )
reconsider T1 = T as Subset of S1 by A1;
A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) by A1;
thus ( T is open implies ( T is inaccessible & T is upper ) ) ::_thesis: ( not T is inaccessible_by_directed_joins or not T is upper or T is open )
proof
assume T is open ; ::_thesis: ( T is inaccessible & T is upper )
then T in the topology of S2 by PRE_TOPC:def_2;
then T1 is open by A1, PRE_TOPC:def_2;
hence ( T is inaccessible & T is upper ) by A3, A2, WAYBEL_0:25, YELLOW_9:47; ::_thesis: verum
end;
thus ( T is inaccessible & T is upper implies T is open ) ::_thesis: verum
proof
assume ( T is inaccessible & T is upper ) ; ::_thesis: T is open
then ( T1 is inaccessible & T1 is upper ) by A3, WAYBEL_0:25, YELLOW_9:47;
then T1 in the topology of S1 by A2, PRE_TOPC:def_2;
hence T is open by A1, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
definition
let L be non empty up-complete Poset;
func Sigma L -> strict Scott TopAugmentation of L means :Def1: :: WAYBEL29:def 1
verum;
uniqueness
for b1, b2 being strict Scott TopAugmentation of L holds b1 = b2
proof
let S1, S2 be strict Scott TopAugmentation of L; ::_thesis: S1 = S2
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4;
hence S1 = S2 by Th13; ::_thesis: verum
end;
existence
ex b1 being strict Scott TopAugmentation of L st verum ;
end;
:: deftheorem Def1 defines Sigma WAYBEL29:def_1_:_
for L being non empty up-complete Poset
for b2 being strict Scott TopAugmentation of L holds
( b2 = Sigma L iff verum );
theorem Th15: :: WAYBEL29:15
for S being non empty up-complete Scott TopPoset holds Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
proof
let S be non empty up-complete Scott TopPoset; ::_thesis: Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
RelStr(# the carrier of TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #), the InternalRel of TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) #) = RelStr(# the carrier of S, the InternalRel of S #) ;
then reconsider T = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) as TopAugmentation of S by YELLOW_9:def_4;
T is Scott by Th14;
hence Sigma S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by Def1; ::_thesis: verum
end;
theorem Th16: :: WAYBEL29:16
for L1, L2 being non empty up-complete Poset st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
Sigma L1 = Sigma L2
proof
let L1, L2 be non empty up-complete Poset; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies Sigma L1 = Sigma L2 )
assume RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: Sigma L1 = Sigma L2
then A1: RelStr(# the carrier of (Sigma L2), the InternalRel of (Sigma L2) #) = RelStr(# the carrier of L1, the InternalRel of L1 #) by YELLOW_9:def_4;
then ( RelStr(# the carrier of (Sigma L1), the InternalRel of (Sigma L1) #) = RelStr(# the carrier of L1, the InternalRel of L1 #) & Sigma L2 is TopAugmentation of L1 ) by YELLOW_9:def_4;
hence Sigma L1 = Sigma L2 by A1, Th13; ::_thesis: verum
end;
definition
let S, T be non empty up-complete Poset;
let f be Function of S,T;
func Sigma f -> Function of (Sigma S),(Sigma T) equals :: WAYBEL29:def 2
f;
coherence
f is Function of (Sigma S),(Sigma T)
proof
( RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma T), the InternalRel of (Sigma T) #) = RelStr(# the carrier of T, the InternalRel of T #) ) by YELLOW_9:def_4;
hence f is Function of (Sigma S),(Sigma T) ; ::_thesis: verum
end;
end;
:: deftheorem defines Sigma WAYBEL29:def_2_:_
for S, T being non empty up-complete Poset
for f being Function of S,T holds Sigma f = f;
registration
let S, T be non empty up-complete Poset;
let f be directed-sups-preserving Function of S,T;
cluster Sigma f -> continuous ;
coherence
Sigma f is continuous
proof
( RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma T), the InternalRel of (Sigma T) #) = RelStr(# the carrier of T, the InternalRel of T #) ) by YELLOW_9:def_4;
hence Sigma f is continuous by WAYBEL17:29, WAYBEL21:6; ::_thesis: verum
end;
end;
theorem :: WAYBEL29:17
for S, T being non empty up-complete Poset
for f being Function of S,T holds
( f is isomorphic iff Sigma f is isomorphic )
proof
let S, T be non empty up-complete Poset; ::_thesis: for f being Function of S,T holds
( f is isomorphic iff Sigma f is isomorphic )
let f be Function of S,T; ::_thesis: ( f is isomorphic iff Sigma f is isomorphic )
( RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma T), the InternalRel of (Sigma T) #) = RelStr(# the carrier of T, the InternalRel of T #) ) by YELLOW_9:def_4;
hence ( f is isomorphic iff Sigma f is isomorphic ) by Th5; ::_thesis: verum
end;
theorem Th18: :: WAYBEL29:18
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; ::_thesis: for S being Scott complete TopLattice holds oContMaps (X,S) = ContMaps (X,S)
let S be Scott complete TopLattice; ::_thesis: oContMaps (X,S) = ContMaps (X,S)
A1: ( Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ) by WAYBEL25:15;
thus oContMaps (X,S) = ContMaps (X,(Omega S)) by WAYBEL26:def_1
.= ContMaps (X,S) by A1, Th10 ; ::_thesis: verum
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: :: WAYBEL29:def 3
for W being open Subset of [:X,Y:] holds it . W = (W, the carrier of X) *graph ;
existence
ex b1 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st
for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph
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, WAYBEL26:def_1;
hence ex b1 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st
for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) st ( for W being open Subset of [:X,Y:] holds b1 . W = (W, the carrier of X) *graph ) & ( for W being open Subset of [:X,Y:] holds b2 . W = (W, the carrier of X) *graph ) holds
b1 = b2;
proof
let F, G be Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))); ::_thesis: ( ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) & ( for W being open Subset of [:X,Y:] holds G . W = (W, the carrier of X) *graph ) implies F = G )
assume 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 ; ::_thesis: F = G
now__::_thesis:_for_x_being_Element_of_(InclPoset_the_topology_of_[:X,Y:])_holds_F_._x_=_G_._x
let x be Element of (InclPoset the topology of [:X,Y:]); ::_thesis: F . x = G . x
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 ; ::_thesis: verum
end;
hence F = G by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Theta WAYBEL29:def_3_:_
for X, Y being non empty TopSpace
for b3 being Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) holds
( b3 = Theta (X,Y) iff for W being open Subset of [:X,Y:] holds b3 . W = (W, the carrier of X) *graph );
defpred S1[ 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)) ex g being Function of (ContMaps ([:X,$1:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto );
defpred S2[ 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)) ex g being Function of (ContMaps ([:X,$1:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic );
defpred S3[ T_0-TopSpace] means for X being non empty TopSpace holds Theta (X,$1) is isomorphic ;
defpred S4[ 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 S5[ 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 S6[ T_0-TopSpace] means for S being Scott TopAugmentation of InclPoset the topology of $1
for y being Element of $1
for 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
( S1[T] iff S2[T] )
proof
let T be T_0-TopSpace; ::_thesis: ( S1[T] iff S2[T] )
thus ( S1[T] implies S2[T] ) ::_thesis: ( S2[T] implies S1[T] )
proof
assume A1: S1[T] ; ::_thesis: S2[T]
let X be non empty TopSpace; ::_thesis: for L being Scott continuous complete TopLattice
for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
let L be Scott continuous complete TopLattice; ::_thesis: for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
let S be Scott TopAugmentation of ContMaps (T,L); ::_thesis: ex f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
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 & f is V7() & f is onto ) and
A3: ( g is currying & g is V7() & g is onto ) by A1;
A4: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (ContMaps (T,L)), the InternalRel of (ContMaps (T,L)) #) by YELLOW_9:def_4;
A5: ContMaps (T,L) is non empty full 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 non empty full SubRelStr of L |^ the carrier of T by A4, A6, YELLOW_0:def_13, YELLOW_0:def_14;
then A7: S |^ the carrier of X is non empty full 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 non empty full SubRelStr of L |^ [: the carrier of X, the carrier of T:] by WAYBEL24:def_3;
ContMaps (X,S) is non empty full SubRelStr of S |^ the carrier of X by WAYBEL24:def_3;
then ContMaps (X,S) is non empty full 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, WAYBEL27:21;
take f ; ::_thesis: ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
take g ; ::_thesis: ( f is uncurrying & f is isomorphic & g is currying & g is isomorphic )
ContMaps (T,L) is non empty full 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) by FUNCT_2:def_1;
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, XBOOLE_1:1;
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 " by A2, A11, FUNCT_1:41;
hence ( f is uncurrying & f is isomorphic ) by A2, A9, WAYBEL_0:def_38; ::_thesis: ( g is currying & g is isomorphic )
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:]) by FUNCT_2:def_1;
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 " by A3, A12, FUNCT_1:41;
hence ( g is currying & g is isomorphic ) by A3, A9, WAYBEL_0:def_38; ::_thesis: verum
end;
assume A13: S2[T] ; ::_thesis: S1[T]
let X be non empty TopSpace; ::_thesis: for L being Scott continuous complete TopLattice
for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
let L be Scott continuous complete TopLattice; ::_thesis: for T being Scott TopAugmentation of ContMaps (T,L) ex f being Function of (ContMaps (X,T)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
let S be Scott TopAugmentation of ContMaps (T,L); ::_thesis: ex f being Function of (ContMaps (X,S)),(ContMaps ([:X,T:],L)) ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
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 & f is isomorphic ) and
A15: ( g is currying & g is isomorphic ) by A13;
take f ; ::_thesis: ex g being Function of (ContMaps ([:X,T:],L)),(ContMaps (X,S)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
take g ; ::_thesis: ( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is onto )
thus ( f is uncurrying & f is V7() & f is onto ) by A14; ::_thesis: ( g is currying & g is V7() & g is onto )
thus ( g is currying & g is V7() & g is onto ) by A15; ::_thesis: verum
end;
begin
definition
let X be non empty TopSpace;
func alpha X -> Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) means :Def4: :: WAYBEL29:def 4
for g being continuous Function of X,Sierpinski_Space holds it . g = g " {1};
existence
ex b1 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st
for g being continuous Function of X,Sierpinski_Space holds b1 . g = g " {1}
proof
deffunc H1( Function) -> set = $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 = H1(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 set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the topology of X )
assume y in rng f ; ::_thesis: y in the topology of X
then consider x being set such that
A3: x in dom f and
A4: y = f . x by FUNCT_1:def_3;
reconsider x = 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 y in the topology of X by A5, PRE_TOPC:def_2; ::_thesis: verum
end;
then rng f c= the carrier of (InclPoset the topology of X) by YELLOW_1:1;
then reconsider f = f as Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) by A1, FUNCT_2:2;
take f ; ::_thesis: for g being continuous Function of X,Sierpinski_Space holds f . g = g " {1}
let g be continuous Function of X,Sierpinski_Space; ::_thesis: f . g = g " {1}
g is Element of (oContMaps (X,Sierpinski_Space)) by WAYBEL26:2;
hence f . g = g " {1} by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) st ( for g being continuous Function of X,Sierpinski_Space holds b1 . g = g " {1} ) & ( for g being continuous Function of X,Sierpinski_Space holds b2 . g = g " {1} ) holds
b1 = b2
proof
let f1, f2 be Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X); ::_thesis: ( ( for g being continuous Function of X,Sierpinski_Space holds f1 . g = g " {1} ) & ( for g being continuous Function of X,Sierpinski_Space holds f2 . g = g " {1} ) implies f1 = f2 )
assume 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} ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_(oContMaps_(X,Sierpinski_Space))_holds_f1_._x_=_f2_._x
let x be Element of (oContMaps (X,Sierpinski_Space)); ::_thesis: f1 . x = f2 . x
reconsider g = x as continuous Function of X,Sierpinski_Space by WAYBEL26:2;
thus f1 . x = g " {1} by A6
.= f2 . x by A7 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines alpha WAYBEL29:def_4_:_
for X being non empty TopSpace
for b2 being Function of (oContMaps (X,Sierpinski_Space)),(InclPoset the topology of X) holds
( b2 = alpha X iff for g being continuous Function of X,Sierpinski_Space holds b2 . g = g " {1} );
theorem :: WAYBEL29:19
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; ::_thesis: for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X)
consider f being 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 " by A2, TOPS_2:def_4;
now__::_thesis:_for_x_being_Element_of_(oContMaps_(X,Sierpinski_Space))_holds_(alpha_X)_._x_=_(f_")_._x
let x be Element of (oContMaps (X,Sierpinski_Space)); ::_thesis: (alpha X) . x = (f ") . x
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 by PRE_TOPC:def_2;
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 ; ::_thesis: verum
end;
then alpha X = f " by FUNCT_2:63;
then (alpha X) " = f by A2, A5, TOPS_2:51;
hence for V being open Subset of X holds ((alpha X) ") . V = chi (V, the carrier of X) by A3; ::_thesis: verum
end;
registration
let X be non empty TopSpace;
cluster alpha X -> isomorphic ;
coherence
alpha X is isomorphic
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 being 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 " 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__::_thesis:_for_x_being_Element_of_(oContMaps_(X,Sierpinski_Space))_holds_(alpha_X)_._x_=_(f_")_._x
let x be Element of (oContMaps (X,Sierpinski_Space)); ::_thesis: (alpha X) . x = (f ") . x
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 by PRE_TOPC:def_2;
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 ; ::_thesis: verum
end;
hence alpha X is isomorphic by A1, A3, FUNCT_2:63, WAYBEL_0:68; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
cluster(alpha X) " -> isomorphic ;
coherence
(alpha X) " is isomorphic by YELLOW14:10;
end;
registration
let S be injective T_0-TopSpace;
cluster Omega S -> Scott ;
coherence
Omega S is Scott
proof
set T = the strict Scott TopAugmentation of Omega S;
A1: TopStruct(# the carrier of the strict Scott TopAugmentation of Omega S, the topology of the strict Scott TopAugmentation of Omega S #) = TopStruct(# the carrier of S, the topology of S #) by WAYBEL25:37
.= TopStruct(# the carrier of (Omega S), the topology of (Omega S) #) by WAYBEL25:def_2 ;
RelStr(# the carrier of the strict Scott TopAugmentation of Omega S, the InternalRel of the strict Scott TopAugmentation of Omega S #) = RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) by YELLOW_9:def_4;
hence Omega S is Scott by A1; ::_thesis: verum
end;
end;
registration
let X be non empty TopSpace;
cluster oContMaps (X,Sierpinski_Space) -> complete ;
coherence
oContMaps (X,Sierpinski_Space) is complete
proof
InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic by WAYBEL26:6;
hence oContMaps (X,Sierpinski_Space) is complete by WAYBEL20:18; ::_thesis: verum
end;
end;
theorem :: WAYBEL29:20
Omega Sierpinski_Space = Sigma (BoolePoset 1)
proof
set S = Sigma (BoolePoset 1);
reconsider T = Omega Sierpinski_Space as strict Scott TopAugmentation of BoolePoset 1 by WAYBEL26:4;
A1: the topology of T = sigma (BoolePoset 1) by YELLOW_9:51
.= the topology of (Sigma (BoolePoset 1)) by YELLOW_9:51 ;
RelStr(# the carrier of T, the InternalRel of T #) = BoolePoset 1 by YELLOW_9:def_4
.= RelStr(# the carrier of (Sigma (BoolePoset 1)), the InternalRel of (Sigma (BoolePoset 1)) #) by YELLOW_9:def_4 ;
hence Omega Sierpinski_Space = Sigma (BoolePoset 1) by A1; ::_thesis: verum
end;
registration
let M be non empty set ;
let S be injective T_0-TopSpace;
cluster product (M => S) -> injective ;
coherence
M -TOP_prod (M => S) is injective
proof
for m being Element of M holds (M => S) . m is injective by FUNCOP_1:7;
hence M -TOP_prod (M => S) is injective by WAYBEL18:7; ::_thesis: verum
end;
end;
theorem :: WAYBEL29:21
for M being non empty set
for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))
proof
let M be non empty set ; ::_thesis: for L being continuous complete LATTICE holds Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))
let L be continuous complete LATTICE; ::_thesis: Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L))
A1: RelStr(# the carrier of (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel 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 RelStr(# the carrier of (Omega (M -TOP_prod (M => (Sigma L)))), the InternalRel 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 Omega (M -TOP_prod (M => (Sigma L))) = Sigma (M -POS_prod (M => L)) by YELLOW_1:def_5; ::_thesis: verum
end;
theorem :: WAYBEL29:22
for M being non empty set
for 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 ; ::_thesis: for T being injective T_0-TopSpace holds Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T)))
let T be injective T_0-TopSpace; ::_thesis: Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T)))
set L = Omega T;
RelStr(# the carrier of (Omega (M -TOP_prod (M => T))), the InternalRel of (Omega (M -TOP_prod (M => T))) #) = M -POS_prod (M => (Omega T)) by WAYBEL25:14;
then Sigma (Omega (M -TOP_prod (M => T))) = Sigma (M -POS_prod (M => (Omega T))) by Th16;
hence Omega (M -TOP_prod (M => T)) = Sigma (M -POS_prod (M => (Omega T))) by Th15; ::_thesis: verum
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: :: WAYBEL29:def 5
for f being continuous Function of X,(M -TOP_prod (M => Y)) holds it . f = commute f;
uniqueness
for b1, b2 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f ) & ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b2 . f = commute f ) holds
b1 = b2
proof
let F1, F2 be Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M); ::_thesis: ( ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F1 . f = commute f ) & ( for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F2 . f = commute f ) implies F1 = F2 )
assume 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 ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Element_of_(oContMaps_(X,(M_-TOP_prod_(M_=>_Y))))_holds_F1_._f_=_F2_._f
let f be Element of (oContMaps (X,(M -TOP_prod (M => Y)))); ::_thesis: F1 . f = F2 . f
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 ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
existence
ex b1 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) st
for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b1 . f = commute f
proof
deffunc H1( Function) -> set = 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 = H1(f) from FUNCT_1:sch_4();
rng F c= the carrier of ((oContMaps (X,Y)) |^ M)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of ((oContMaps (X,Y)) |^ M) )
assume y in rng F ; ::_thesis: y in the carrier of ((oContMaps (X,Y)) |^ M)
then consider x being set such that
A5: x in dom F and
A6: y = F . x by FUNCT_1:def_3;
reconsider x = 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 y in the carrier of ((oContMaps (X,Y)) |^ M) by YELLOW_1:28; ::_thesis: verum
end;
then reconsider F = F as Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) by A3, FUNCT_2:2;
take F ; ::_thesis: for f being continuous Function of X,(M -TOP_prod (M => Y)) holds F . f = commute f
let f be continuous Function of X,(M -TOP_prod (M => Y)); ::_thesis: F . f = commute f
f is Element of (oContMaps (X,(M -TOP_prod (M => Y)))) by WAYBEL26:2;
hence F . f = commute f by A4; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines commute WAYBEL29:def_5_:_
for M being non empty set
for X, Y being non empty TopSpace
for b4 being Function of (oContMaps (X,(M -TOP_prod (M => Y)))),((oContMaps (X,Y)) |^ M) holds
( b4 = commute (X,M,Y) iff for f being continuous Function of X,(M -TOP_prod (M => Y)) holds b4 . f = commute f );
registration
let M be non empty set ;
let X, Y be non empty TopSpace;
cluster commute (X,M,Y) -> V7() onto ;
correctness
coherence
( commute (X,M,Y) is one-to-one & commute (X,M,Y) is onto );
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__::_thesis:_(_the_carrier_of_((oContMaps_(X,Y))_|^_M)_<>_{}_&_(_for_x1,_x2_being_set_st_x1_in_the_carrier_of_(oContMaps_(X,(M_-TOP_prod_(M_=>_Y))))_&_x2_in_the_carrier_of_(oContMaps_(X,(M_-TOP_prod_(M_=>_Y))))_&_(commute_(X,M,Y))_._x1_=_(commute_(X,M,Y))_._x2_holds_
x1_=_x2_)_)
thus the carrier of ((oContMaps (X,Y)) |^ M) <> {} ; ::_thesis: for x1, x2 being set st x1 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & x2 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 holds
x1 = x2
let x1, x2 be set ; ::_thesis: ( x1 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & x2 in the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) & (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 implies x1 = x2 )
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)))) ; ::_thesis: ( (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 implies x1 = x2 )
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 (commute (X,M,Y)) . x1 = (commute (X,M,Y)) . x2 ; ::_thesis: x1 = x2
then commute f1 = (commute (X,M,Y)) . x2 by Def5
.= commute f2 by Def5 ;
then f1 = commute (commute f2) by A1, A2, FUNCT_6:57;
hence x1 = x2 by A1, A3, FUNCT_6:57; ::_thesis: verum
end;
hence commute (X,M,Y) is V7() by FUNCT_2:19; ::_thesis: commute (X,M,Y) is onto
rng (commute (X,M,Y)) = the carrier of ((oContMaps (X,Y)) |^ M)
proof
thus rng (commute (X,M,Y)) c= the carrier of ((oContMaps (X,Y)) |^ M) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((oContMaps (X,Y)) |^ M) c= rng (commute (X,M,Y))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((oContMaps (X,Y)) |^ M) or x in rng (commute (X,M,Y)) )
assume A4: x in the carrier of ((oContMaps (X,Y)) |^ M) ; ::_thesis: x in rng (commute (X,M,Y))
then reconsider x = x as Element of ((oContMaps (X,Y)) |^ M) ;
A5: the carrier of ((oContMaps (X,Y)) |^ M) = Funcs (M, the carrier of (oContMaps (X,Y))) by YELLOW_1:28;
then reconsider x = 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 A5, FUNCT_5:56, WAYBEL26:32;
then commute (commute x) = x by A4, FUNCT_6:57;
then A6: (commute (X,M,Y)) . y = x by Def5;
dom (commute (X,M,Y)) = the carrier of (oContMaps (X,(M -TOP_prod (M => Y)))) by FUNCT_2:def_1;
hence x in rng (commute (X,M,Y)) by A6, FUNCT_1:def_3; ::_thesis: verum
end;
hence commute (X,M,Y) is onto by FUNCT_2:def_3; ::_thesis: verum
end;
end;
registration
let M be non empty set ;
let X be non empty TopSpace;
cluster commute (X,M,Sierpinski_Space) -> isomorphic ;
correctness
coherence
commute (X,M,Sierpinski_Space) is isomorphic ;
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 commute (X,M,Sierpinski_Space) is isomorphic by Def5; ::_thesis: verum
end;
end;
Lm2: for T being T_0-TopSpace st S3[T] holds
S4[T]
proof
let Y be T_0-TopSpace; ::_thesis: ( S3[Y] implies S4[Y] )
assume A1: S3[Y] ; ::_thesis: S4[Y]
set S = Sigma (InclPoset the topology of Y);
let X be non empty TopSpace; ::_thesis: for T being Scott TopAugmentation of InclPoset the topology of Y
for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
A2: the topology of T = sigma (InclPoset the topology of Y) by YELLOW_9:51;
let f be continuous Function of X,T; ::_thesis: *graph f is open Subset of [:X,Y:]
( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def_4;
then A3: ( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) & TopRelStr(# the carrier of T, the InternalRel of T, the topology of T #) = TopRelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) 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,(Sigma (InclPoset the topology of Y))) 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 set 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 = 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 *graph f is open Subset of [:X,Y:] by A6, WAYBEL26:41; ::_thesis: verum
end;
theorem Th23: :: WAYBEL29:23
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; ::_thesis: 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
let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f1, f2 being Element of (ContMaps (X,S)) st f1 <= f2 holds
*graph f1 c= *graph f2
let f1, f2 be Element of (ContMaps (X,S)); ::_thesis: ( f1 <= f2 implies *graph f1 c= *graph f2 )
assume A1: f1 <= f2 ; ::_thesis: *graph f1 c= *graph f2
reconsider F1 = f1, F2 = f2 as Function of X,S by WAYBEL24:21;
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in *graph f1 or [a,b] in *graph f2 )
A2: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel 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 ; ::_thesis: [a,b] in *graph f2
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 [a,b] in *graph f2 by A6, A3, A5, WAYBEL26:38; ::_thesis: verum
end;
Lm3: for T being T_0-TopSpace st S4[T] holds
S3[T]
proof
deffunc H1( Function) -> set = *graph $1;
let Y be T_0-TopSpace; ::_thesis: ( S4[Y] implies S3[Y] )
assume A1: S4[Y] ; ::_thesis: S3[Y]
set T = Sigma (InclPoset the topology of Y);
let X be non empty TopSpace; ::_thesis: Theta (X,Y) is isomorphic
consider G being Function such that
A2: dom G = the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) and
A3: for f being Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) holds G . f = H1(f) from FUNCT_1:sch_4();
rng G c= the carrier of (InclPoset the topology of [:X,Y:])
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng G or x in the carrier of (InclPoset the topology of [:X,Y:]) )
assume x in rng G ; ::_thesis: x in the carrier of (InclPoset the topology of [:X,Y:])
then consider a being set such that
A4: a in dom G and
A5: x = G . a by FUNCT_1:def_3;
reconsider a = a as Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) by A2, A4;
reconsider a = a as continuous Function of X,(Sigma (InclPoset the topology of Y)) 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 x in the carrier of (InclPoset the topology of [:X,Y:]) by YELLOW_1:1; ::_thesis: verum
end;
then reconsider G = G as Function of (ContMaps (X,(Sigma (InclPoset the topology of Y)))),(InclPoset the topology of [:X,Y:]) by A2, FUNCT_2:2;
consider F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,(Sigma (InclPoset the topology of Y)))) 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,(Sigma (InclPoset the topology of Y)))); :: according to WAYBEL_1:def_2 ::_thesis: ( not f1 <= f2 or G . f1 <= G . f2 )
assume f1 <= f2 ; ::_thesis: G . f1 <= G . 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; ::_thesis: verum
end;
reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) 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,(Sigma (InclPoset the topology of Y)))) by A2, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(ContMaps_(X,(Sigma_(InclPoset_the_topology_of_Y))))_holds_
(F_*_G)_._x_=_x
let x be set ; ::_thesis: ( x in the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) implies (F * G) . x = x )
assume A10: x in the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) ; ::_thesis: (F * G) . x = x
then reconsider x1 = x as continuous Function of X,(Sigma (InclPoset the topology of Y)) 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__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_X_holds_
x1_._i_=_Im_(gx,i)
let i be set ; ::_thesis: ( i in the carrier of X implies x1 . i = Im (gx,i) )
assume i in the carrier of X ; ::_thesis: x1 . i = Im (gx,i)
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) ::_thesis: verum
proof
thus x1 . i c= Im (gx,i) :: according to XBOOLE_0:def_10 ::_thesis: Im (gx,i) c= x1 . i
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in x1 . i or b in Im (gx,i) )
assume b in x1 . i ; ::_thesis: b in Im (gx,i)
then [i,b] in gx by A13, WAYBEL26:38;
hence b in Im (gx,i) by A14, RELAT_1:def_13; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Im (gx,i) or b in x1 . i )
assume b in Im (gx,i) ; ::_thesis: b in x1 . i
then ex j being set st
( [j,b] in gx & j in {i} ) by RELAT_1:def_13;
then [i,b] in gx by TARSKI:def_1;
hence b in x1 . i by WAYBEL26:38; ::_thesis: verum
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; ::_thesis: verum
end;
then A15: F * G = id (ContMaps (X,(Sigma (InclPoset the topology of Y)))) by A9, FUNCT_1:17;
A16: dom (G * F) = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(InclPoset_the_topology_of_[:X,Y:])_holds_
(G_*_F)_._x_=_x
let x be set ; ::_thesis: ( x in the carrier of (InclPoset the topology of [:X,Y:]) implies (G * F) . x = x )
assume A17: x in the carrier of (InclPoset the topology of [:X,Y:]) ; ::_thesis: (G * F) . x = x
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,(Sigma (InclPoset the topology of Y)) by WAYBEL26:43;
then reconsider x1X = (x1, the carrier of X) *graph as Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not d in dom x1 or d in the carrier of X )
assume d in dom x1 ; ::_thesis: d in the carrier of X
then ex e being set st [d,e] in x1 by XTUPLE_0:def_12;
hence d in the carrier of X by A18, ZFMISC_1:87; ::_thesis: verum
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 ; ::_thesis: verum
end;
then A20: G * F = id (InclPoset the topology of [:X,Y:]) by A16, FUNCT_1:17;
ContMaps (X,(Sigma (InclPoset the topology of Y))) = oContMaps (X,(Sigma (InclPoset the topology of Y))) by Th18;
then F is isomorphic by A6, A8, A15, A20, YELLOW16:15;
hence Theta (X,Y) is isomorphic by A7, Def3; ::_thesis: verum
end;
Lm4: for T being T_0-TopSpace st S4[T] holds
S5[T]
proof
let Y be T_0-TopSpace; ::_thesis: ( S4[Y] implies S5[Y] )
assume A1: S4[Y] ; ::_thesis: S5[Y]
let X be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:X,Y:]
reconsider f = id X as continuous Function of X,X ;
A2: RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel 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 } :: according to XBOOLE_0:def_10 ::_thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } c= *graph f
proof
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in *graph f or [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } )
assume A3: [a,b] in *graph f ; ::_thesis: [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
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 = a as open Subset of Y by A4, PRE_TOPC:def_2;
f . a = a by A4, FUNCT_1:18;
then reconsider b = b as Element of Y by A5;
b in a by A4, A5, FUNCT_1:18;
hence [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } or e in *graph f )
assume e in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } ; ::_thesis: e in *graph f
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 e in *graph f by A6, WAYBEL26:38; ::_thesis: verum
end;
hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:X,Y:] by A1; ::_thesis: verum
end;
Lm5: for T being T_0-TopSpace st S5[T] holds
S6[T]
proof
let Y be T_0-TopSpace; ::_thesis: ( S5[Y] implies S6[Y] )
assume A1: S5[Y] ; ::_thesis: S6[Y]
let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for y being Element of Y
for 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 )
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; ::_thesis: for 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 )
let V be open a_neighborhood of y; ::_thesis: ex H being open Subset of S st
( V in H & meet H is 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 = H as open Subset of S by A6, PRE_TOPC:def_2;
A8: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4;
meet H c= the carrier of Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet H or x in the carrier of Y )
H <> {} by A3, A5;
then consider A being set 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;
assume x in meet H ; ::_thesis: x in the carrier of Y
then x in A by A9, SETFAM_1:def_1;
hence x in the carrier of Y by A10; ::_thesis: verum
end;
then reconsider mH = meet H as Subset of Y ;
reconsider W = W as open Subset of Y by A7, PRE_TOPC:def_2;
W c= mH
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in W or w in mH )
assume A11: w in W ; ::_thesis: w in mH
A12: now__::_thesis:_for_a_being_set_st_a_in_H_holds_
w_in_a
let a be set ; ::_thesis: ( a in H implies w in a )
assume a in H ; ::_thesis: w in a
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; ::_thesis: verum
end;
H <> {} by A3, A5;
hence w in mH by A12, SETFAM_1:def_1; ::_thesis: verum
end;
then A15: W c= Int mH by TOPS_1:24;
take H ; ::_thesis: ( V in H & meet H is a_neighborhood of y )
thus V in H by A3, A5, ZFMISC_1:87; ::_thesis: meet H is a_neighborhood of y
y in W by A3, A5, ZFMISC_1:87;
hence meet H is a_neighborhood of y by A15, CONNSP_2:def_1; ::_thesis: verum
end;
Lm6: for T being T_0-TopSpace st S6[T] holds
S4[T]
proof
let Y be T_0-TopSpace; ::_thesis: ( S6[Y] implies S4[Y] )
assume A1: S6[Y] ; ::_thesis: S4[Y]
let X be non empty TopSpace; ::_thesis: for T being Scott TopAugmentation of InclPoset the topology of Y
for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
let f be continuous Function of X,T; ::_thesis: *graph f is open Subset of [:X,Y:]
( 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: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4;
now__::_thesis:_for_s_being_set_st_s_in_*graph_f_holds_
s_in_the_carrier_of_[:X,Y:]
let s be set ; ::_thesis: ( s in *graph f implies s in the carrier of [:X,Y:] )
assume A3: s in *graph f ; ::_thesis: s in the carrier of [:X,Y:]
then consider s1, s2 being set 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; ::_thesis: verum
end;
then reconsider A = *graph f as Subset of [:X,Y:] by TARSKI:def_3;
now__::_thesis:_for_p_being_Point_of_[:X,Y:]_st_p_in_A_holds_
ex_a_being_Subset_of_[:X,Y:]_st_
(_a_in_B_&_p_in_a_&_a_c=_A_)
let p be Point of [:X,Y:]; ::_thesis: ( p in A implies ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A ) )
assume A7: p in A ; ::_thesis: ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A )
then consider x, y being set 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 = 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 = 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 = 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 = a; ::_thesis: ( a in B & p in a & a c= A )
( V in the topology of Y & fH in the topology of X ) by PRE_TOPC:def_2;
hence a in B ; ::_thesis: ( p in a & a c= A )
( 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; ::_thesis: a c= A
thus a c= A ::_thesis: verum
proof
let s1, s2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [s1,s2] in a or [s1,s2] in A )
A14: V c= mH by TOPS_1:16;
assume A15: [s1,s2] in a ; ::_thesis: [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 [s1,s2] in A by A18, WAYBEL26:38; ::_thesis: verum
end;
end;
hence *graph f is open Subset of [:X,Y:] by YELLOW_9:31; ::_thesis: verum
end;
Lm7: for T being T_0-TopSpace st S6[T] holds
InclPoset the topology of T is continuous
proof
let Y be T_0-TopSpace; ::_thesis: ( S6[Y] implies InclPoset the topology of Y is continuous )
assume A1: S6[Y] ; ::_thesis: InclPoset the topology of Y is continuous
set L = InclPoset the topology of Y;
set S = the Scott TopAugmentation of InclPoset the topology of Y;
thus for x being Element of (InclPoset the topology of Y) holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( InclPoset the topology of Y is up-complete & InclPoset the topology of Y is satisfying_axiom_of_approximation )
thus InclPoset the topology of Y is up-complete ; ::_thesis: InclPoset the topology of Y is satisfying_axiom_of_approximation
let A be Element of (InclPoset the topology of Y); :: according to WAYBEL_3:def_5 ::_thesis: A = "\/" ((waybelow A),(InclPoset the topology of Y))
the carrier of (InclPoset the topology of Y) = 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: RelStr(# the carrier of the Scott TopAugmentation of InclPoset the topology of Y, the InternalRel of the Scott TopAugmentation of InclPoset the topology of Y #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4;
thus A c= sup (waybelow A) :: according to XBOOLE_0:def_10 ::_thesis: "\/" ((waybelow A),(InclPoset the topology of Y)) c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in sup (waybelow A) )
assume A3: x in A ; ::_thesis: x in sup (waybelow A)
then x in B ;
then reconsider x9 = x as Element of Y ;
reconsider B = B as open a_neighborhood of x9 by A3, CONNSP_2:3;
consider H being open Subset of the Scott TopAugmentation of InclPoset the topology of Y 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 (InclPoset the topology of Y) by A2;
Int mH in the topology of Y by PRE_TOPC:def_2;
then reconsider ImH = Int mH as Element of (InclPoset the topology of Y) by YELLOW_1:1;
ImH << A
proof
let D be non empty directed Subset of (InclPoset the topology of Y); :: according to WAYBEL_3:def_1 ::_thesis: ( not A <= "\/" (D,(InclPoset the topology of Y)) or ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in D & ImH <= b1 ) )
A6: ( H1 is inaccessible & H1 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;
assume A <= sup D ; ::_thesis: ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in D & ImH <= b1 )
then sup D in H1 by A4, A6, WAYBEL_0:def_20;
then D meets H1 by A6, WAYBEL11:def_1;
then consider d being set such that
A7: d in D and
A8: d in H1 by XBOOLE_0:3;
reconsider d = d as Element of (InclPoset the topology of Y) by A7;
take d ; ::_thesis: ( d in D & ImH <= d )
thus d in D by A7; ::_thesis: ImH <= d
( Int mH c= mH & mH c= d ) by A8, SETFAM_1:3, TOPS_1:16;
then ImH c= d by XBOOLE_1:1;
hence ImH <= d by YELLOW_1:3; ::_thesis: verum
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 x in sup (waybelow A) by YELLOW_1:22; ::_thesis: verum
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 "\/" ((waybelow A),(InclPoset the topology of Y)) c= A by WAYBEL_0:34; ::_thesis: verum
end;
Lm8: for T being T_0-TopSpace st InclPoset the topology of T is continuous holds
S6[T]
proof
let T be T_0-TopSpace; ::_thesis: ( InclPoset the topology of T is continuous implies S6[T] )
assume A1: InclPoset the topology of T is continuous ; ::_thesis: S6[T]
let S be Scott TopAugmentation of InclPoset the topology of T; ::_thesis: for y being Element of T
for 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 )
let y be Element of T; ::_thesis: for 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 )
let V be open a_neighborhood of y; ::_thesis: ex H being open Subset of S st
( V in H & meet H is 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 = Z as Element of (InclPoset the topology of T) by A4;
A5: RelStr(# the carrier of (InclPoset the topology of T), the InternalRel of (InclPoset the topology of T) #) = RelStr(# the carrier of S, the InternalRel 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not s in Z or s in meet (uparrow Z) )
assume A7: s in Z ; ::_thesis: s in meet (uparrow Z)
now__::_thesis:_for_z_being_set_st_z_in_uparrow_Z_holds_
s_in_z
let z be set ; ::_thesis: ( z in uparrow Z implies s in z )
assume A8: z in uparrow Z ; ::_thesis: s in 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; ::_thesis: verum
end;
hence s in meet (uparrow Z) by SETFAM_1:def_1; ::_thesis: verum
end;
reconsider H = wayabove Z1 as open Subset of S by A1, WAYBEL11:36;
take H ; ::_thesis: ( V in H & meet H is a_neighborhood of y )
Z << W by A4, WAYBEL_3:7;
then A9: V in wayabove Z ;
hence A10: V in H by A5, YELLOW12:13; ::_thesis: meet H is a_neighborhood of y
meet H c= the carrier of T
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in meet H or s in the carrier of T )
assume s in meet H ; ::_thesis: s in the carrier of T
then s in V by A10, SETFAM_1:def_1;
hence s in the carrier of T ; ::_thesis: verum
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, XBOOLE_1:1;
then Z2 c= Int mH by TOPS_1:24;
hence meet H is a_neighborhood of y by A3, CONNSP_2:def_1; ::_thesis: verum
end;
begin
theorem :: WAYBEL29:24
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)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is V7() & f is onto & g is currying & g is V7() & g is 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)) ex g being Function of (ContMaps ([:X,Y:],L)),(ContMaps (X,T)) st
( f is uncurrying & f is isomorphic & g is currying & g is isomorphic ) ) by Lm1;
theorem :: WAYBEL29:25
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; ::_thesis: ( InclPoset the topology of Y is continuous iff for X being non empty TopSpace holds Theta (X,Y) is isomorphic )
hereby ::_thesis: ( ( for X being non empty TopSpace holds Theta (X,Y) is isomorphic ) implies InclPoset the topology of Y is continuous )
assume InclPoset the topology of Y is continuous ; ::_thesis: S3[Y]
then S6[Y] by Lm8;
then S4[Y] by Lm6;
hence S3[Y] by Lm3; ::_thesis: verum
end;
assume S3[Y] ; ::_thesis: InclPoset the topology of Y is continuous
then S4[Y] by Lm2;
then S5[Y] by Lm4;
then S6[Y] by Lm5;
hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum
end;
theorem :: WAYBEL29:26
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; ::_thesis: ( 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:] )
hereby ::_thesis: ( ( 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:] ) implies InclPoset the topology of Y is continuous )
assume InclPoset the topology of Y is continuous ; ::_thesis: 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:]
then S6[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; ::_thesis: verum
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:] ; ::_thesis: InclPoset the topology of Y is continuous
S4[Y]
proof
let X be non empty TopSpace; ::_thesis: for T being Scott TopAugmentation of InclPoset the topology of Y
for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
let f be continuous Function of X,T; ::_thesis: *graph f is open Subset of [:X,Y:]
A2: ( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel 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)) ;
( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) & TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by A2, Th13;
then g is continuous by YELLOW12:36;
hence *graph f is open Subset of [:X,Y:] by A1; ::_thesis: verum
end;
then S5[Y] by Lm4;
then S6[Y] by Lm5;
hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum
end;
theorem :: WAYBEL29:27
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; ::_thesis: ( 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:] )
hereby ::_thesis: ( { [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:] implies InclPoset the topology of Y is continuous )
assume InclPoset the topology of Y is continuous ; ::_thesis: { [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:]
then S6[Y] by Lm8;
then S4[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; ::_thesis: verum
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:] ; ::_thesis: InclPoset the topology of Y is continuous
S5[Y]
proof
let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:T,Y:]
( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel of (Sigma (InclPoset the topology of Y)) #) = InclPoset the topology of Y ) by YELLOW_9:def_4;
then ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y, the topology of Y #) & TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (Sigma (InclPoset the topology of Y)), the topology of (Sigma (InclPoset the topology of Y)) #) ) by Th13;
then [:T,Y:] = [:(Sigma (InclPoset the topology of Y)),Y:] by Th7;
hence { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:T,Y:] by A1; ::_thesis: verum
end;
then S6[Y] by Lm5;
hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum
end;
theorem :: WAYBEL29:28
for Y being T_0-TopSpace holds
( InclPoset the topology of Y is continuous iff for y being Element of Y
for 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; ::_thesis: ( InclPoset the topology of Y is continuous iff for y being Element of Y
for 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 ) )
thus ( InclPoset the topology of Y is continuous implies for y being Element of Y
for 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; ::_thesis: ( ( for y being Element of Y
for 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 ) ) implies InclPoset the topology of Y is continuous )
assume A1: for y being Element of Y
for 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 ) ; ::_thesis: InclPoset the topology of Y is continuous
S6[Y]
proof
let T be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for y being Element of Y
for V being open a_neighborhood of y ex H being open Subset of T st
( V in H & meet H is a_neighborhood of y )
let y be Element of Y; ::_thesis: for V being open a_neighborhood of y ex H being open Subset of T st
( V in H & meet H is a_neighborhood of y )
let V be open a_neighborhood of y; ::_thesis: ex H being open Subset of T st
( V in H & meet H is 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;
( RelStr(# the carrier of T, the InternalRel of T #) = InclPoset the topology of Y & RelStr(# the carrier of (Sigma (InclPoset the topology of Y)), the InternalRel 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 ex H being open Subset of T st
( V in H & meet H is a_neighborhood of y ) by A2; ::_thesis: verum
end;
hence InclPoset the topology of Y is continuous by Lm7; ::_thesis: verum
end;
defpred S7[ complete LATTICE] means InclPoset (sigma $1) is continuous ;
defpred S8[ 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 S9[ 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 TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:];
Lm9: for L being complete LATTICE holds
( S8[L] iff S9[L] )
proof
let L be complete LATTICE; ::_thesis: ( S8[L] iff S9[L] )
thus ( S8[L] implies S9[L] ) ::_thesis: ( S9[L] implies S8[L] )
proof
assume A1: S8[L] ; ::_thesis: S9[L]
let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE
for SS being Scott TopAugmentation of S
for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]
let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S
for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]
let SS be Scott TopAugmentation of S; ::_thesis: for SSL being Scott TopAugmentation of [:S,L:] holds TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]
let SSL be Scott TopAugmentation of [:S,L:]; ::_thesis: TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:]
A2: the topology of [:SS,SL:] = sigma [:S,L:] by A1
.= the topology of SSL by YELLOW_9:51 ;
A3: RelStr(# the carrier of SSL, the InternalRel of SSL #) = RelStr(# the carrier of [:S,L:], the InternalRel of [:S,L:] #) by YELLOW_9:def_4;
( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel 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 TopStruct(# the carrier of SSL, the topology of SSL #) = [:SS,SL:] by A2; ::_thesis: verum
end;
assume A4: S9[L] ; ::_thesis: S8[L]
let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:]
now__::_thesis:_for_SSL_being_Scott_TopAugmentation_of_[:S,L:]_holds_sigma_[:S,L:]_=_the_topology_of_[:SS,SL:]
let SSL be Scott TopAugmentation of [:S,L:]; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:]
TopStruct(# the carrier of SSL, the topology of SSL #) = TopStruct(# the carrier of [:SS,SL:], the topology of [:SS,SL:] #) by A4;
hence sigma [:S,L:] = the topology of [:SS,SL:] by YELLOW_9:51; ::_thesis: verum
end;
hence sigma [:S,L:] = the topology of [:SS,SL:] ; ::_thesis: verum
end;
begin
theorem :: WAYBEL29:29
for R1, R2, R3 being non empty RelStr
for f1 being Function of R1,R3 st f1 is isomorphic holds
for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
proof
let R1, R2, R3 be non empty RelStr ; ::_thesis: for f1 being Function of R1,R3 st f1 is isomorphic holds
for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
let f1 be Function of R1,R3; ::_thesis: ( f1 is isomorphic implies for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )
assume A1: f1 is isomorphic ; ::_thesis: for f2 being Function of R2,R3 st f2 = f1 & f2 is isomorphic holds
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
let f2 be Function of R2,R3; ::_thesis: ( f2 = f1 & f2 is isomorphic implies RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) )
assume that
A2: f2 = f1 and
A3: f2 is isomorphic ; ::_thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
A4: the carrier of R1 = rng (f2 ") 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 set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in the InternalRel of R2 or [x1,x2] in the InternalRel of R1 )
assume A6: [x1,x2] in the InternalRel of R2 ; ::_thesis: [x1,x2] in the InternalRel of R1
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 [x1,x2] in the InternalRel of R1 by ORDERS_2:def_5; ::_thesis: verum
end;
the InternalRel of R1 c= the InternalRel of R2
proof
let x1, x2 be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x1,x2] in the InternalRel of R1 or [x1,x2] in the InternalRel of R2 )
assume A7: [x1,x2] in the InternalRel of R1 ; ::_thesis: [x1,x2] in the InternalRel of R2
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 [x1,x2] in the InternalRel of R2 by ORDERS_2:def_5; ::_thesis: verum
end;
hence RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by A4, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm10: for L being complete LATTICE st S7[L] holds
S8[L]
proof
let L be complete LATTICE; ::_thesis: ( S7[L] implies S8[L] )
assume A1: S7[L] ; ::_thesis: S8[L]
let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:]
A2: RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
UPS (L,(BoolePoset 1)) is non empty full SubRelStr of (BoolePoset 1) |^ the carrier of L by WAYBEL27:def_4;
then A3: (UPS (L,(BoolePoset 1))) |^ the carrier of S is non empty full SubRelStr of ((BoolePoset 1) |^ the carrier of L) |^ the carrier of S by YELLOW16:39;
UPS (S,(UPS (L,(BoolePoset 1)))) is non empty full SubRelStr of (UPS (L,(BoolePoset 1))) |^ the carrier of S by WAYBEL27:def_4;
then A4: UPS (S,(UPS (L,(BoolePoset 1)))) is non empty full SubRelStr of ((BoolePoset 1) |^ the carrier of L) |^ the carrier of S by A3, WAYBEL15:1;
consider f5 being Function of (UPS (L,(BoolePoset 1))),(InclPoset (sigma L)) such that
A5: f5 is isomorphic and
A6: for f being directed-sups-preserving Function of L,(BoolePoset 1) holds f5 . f = f " {1} by WAYBEL27:33;
set f6 = UPS ((id S),f5);
consider f3 being Function of (UPS (S,(UPS (L,(BoolePoset 1))))),(UPS ([:S,L:],(BoolePoset 1))) such that
A7: ( f3 is uncurrying & f3 is isomorphic ) by WAYBEL27:47;
set f4 = f3 " ;
set T = Sigma (InclPoset the topology of SL);
consider f1 being Function of (UPS ([:S,L:],(BoolePoset 1))),(InclPoset (sigma [:S,L:])) such that
A8: f1 is isomorphic and
A9: for f being directed-sups-preserving Function of [:S,L:],(BoolePoset 1) holds f1 . f = f " {1} by WAYBEL27:33;
A10: f3 " is isomorphic by A7, YELLOW14:10;
set f2 = f1 " ;
set G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ");
A11: the topology of SL = sigma L by YELLOW_9:51;
then A12: RelStr(# the carrier of (Sigma (InclPoset the topology of SL)), the InternalRel of (Sigma (InclPoset the topology of SL)) #) = RelStr(# the carrier of (InclPoset (sigma L)), the InternalRel of (InclPoset (sigma L)) #) by YELLOW_9:def_4;
A13: the carrier of (UPS (S,(InclPoset (sigma L)))) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))
proof
thus the carrier of (UPS (S,(InclPoset (sigma L)))) c= the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) c= the carrier of (UPS (S,(InclPoset (sigma L))))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (UPS (S,(InclPoset (sigma L)))) or x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) )
assume A14: x in the carrier of (UPS (S,(InclPoset (sigma L)))) ; ::_thesis: x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL))))
then reconsider x1 = x as Function of SS,(Sigma (InclPoset the topology of SL)) 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 x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by WAYBEL24:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) or x in the carrier of (UPS (S,(InclPoset (sigma L)))) )
assume x in the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ; ::_thesis: x in the carrier of (UPS (S,(InclPoset (sigma L))))
then consider x1 being Function of SS,(Sigma (InclPoset the topology of SL)) 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 x in the carrier of (UPS (S,(InclPoset (sigma L)))) by A15, WAYBEL27:def_4; ::_thesis: verum
end;
then reconsider G = ((UPS ((id S),f5)) * (f3 ")) * (f1 ") as Function of (InclPoset (sigma [:S,L:])),(ContMaps (SS,(Sigma (InclPoset the topology of SL)))) ;
set F = Theta (SS,SL);
A17: RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4;
( (BoolePoset 1) |^ the carrier of [:S,L:] = (BoolePoset 1) |^ [: the carrier of S, the carrier of L:] & UPS ([:S,L:],(BoolePoset 1)) is non empty full SubRelStr of (BoolePoset 1) |^ the carrier of [:S,L:] ) by WAYBEL27:def_4, YELLOW_3:def_2;
then A18: f3 " 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:])); ::_thesis: for s being Element of S holds (G . V) . s = { y where y is Element of L : [s,y] in V }
let s be Element of S; ::_thesis: (G . V) . s = { y where y is Element of L : [s,y] in V }
reconsider fff = (f3 ") . ((f1 ") . V) as directed-sups-preserving Function of S,(UPS (L,(BoolePoset 1))) by WAYBEL27:def_4;
reconsider f2V = (f1 ") . V as directed-sups-preserving Function of [:S,L:],(BoolePoset 1) 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: ((f3 ") . ((f1 ") . V)) . s is directed-sups-preserving Function of L,(BoolePoset 1) by WAYBEL27:def_4;
then A22: dom (((f3 ") . ((f1 ") . V)) . s) = the carrier of L by FUNCT_2:def_1;
G . V = ((UPS ((id S),f5)) * (f3 ")) . ((f1 ") . V) by FUNCT_2:15
.= (UPS ((id S),f5)) . ((f3 ") . ((f1 ") . V)) by FUNCT_2:15
.= f5 * fff by A20, WAYBEL27:def_5 ;
then A23: (G . V) . s = f5 . (fff . s) by FUNCT_2:15
.= (((f3 ") . ((f1 ") . V)) . s) " {1} by A6, A21 ;
A24: rng f1 = [#] (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def_3;
dom (f3 ") = the carrier of (UPS ([:S,L:],(BoolePoset 1))) by FUNCT_2:def_1;
then A25: (f3 ") . ((f1 ") . V) = curry ((f1 ") . V) by A18, WAYBEL27:def_2;
rng f1 = the carrier of (InclPoset (sigma [:S,L:])) by A8, FUNCT_2:def_3;
then A26: V = (id (rng f1)) . V by FUNCT_1:18
.= (f1 * (f1 ")) . V by A8, A24, TOPS_2:52
.= f1 . ((f1 ") . 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 } :: according to XBOOLE_0:def_10 ::_thesis: { y where y is Element of L : [s,y] in V } c= (G . V) . s
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (G . V) . s or x in { y where y is Element of L : [s,y] in V } )
assume A27: x in (G . V) . s ; ::_thesis: x in { y where y is Element of L : [s,y] in V }
then x in dom (((f3 ") . ((f1 ") . V)) . s) by A23, FUNCT_1:def_7;
then reconsider y = x as Element of L by A21, FUNCT_2:def_1;
(((f3 ") . ((f1 ") . V)) . s) . x in {1} by A23, A27, FUNCT_1:def_7;
then A28: (((f3 ") . ((f1 ") . 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 ((f1 ") . V) ;
then ((f1 ") . V) . (s,y) = 1 by A25, A28, FUNCT_5:20;
then ((f1 ") . V) . (s,y) in {1} by TARSKI:def_1;
then [s,y] in ((f1 ") . V) " {1} by A29, FUNCT_1:def_7;
hence x in { y where y is Element of L : [s,y] in V } by A26; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Element of L : [s,y] in V } or x in (G . V) . s )
assume x in { y where y is Element of L : [s,y] in V } ; ::_thesis: x in (G . V) . s
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 ((f1 ") . V) ;
then reconsider cs = (curry ((f1 ") . V)) . s as Function by FUNCT_5:19;
((f1 ") . V) . (s,y) in {1} by A26, A31, FUNCT_1:def_7;
then ((f1 ") . V) . (s,y) = 1 by TARSKI:def_1;
then cs . y = 1 by A32, FUNCT_5:20;
then (((f3 ") . ((f1 ") . V)) . s) . y in {1} by A25, TARSKI:def_1;
hence x in (G . V) . s by A23, A30, A22, FUNCT_1:def_7; ::_thesis: verum
end;
S6[SL] by A1, A11, Lm8;
then S4[SL] by Lm6;
then A33: Theta (SS,SL) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not V in the carrier of (InclPoset (sigma [:S,L:])) or V in the carrier of (InclPoset the topology of [:SS,SL:]) )
assume V in the carrier of (InclPoset (sigma [:S,L:])) ; ::_thesis: V in the carrier of (InclPoset the topology of [:SS,SL:])
then reconsider V1 = V as Element of (InclPoset (sigma [:S,L:])) ;
rng (Theta (SS,SL)) = the carrier of (ContMaps (SS,(Sigma (InclPoset the topology of SL)))) by A33, FUNCT_2:def_3;
then consider W being set such that
A35: W in dom (Theta (SS,SL)) and
A36: (Theta (SS,SL)) . W = G . V1 by FUNCT_1:def_3;
reconsider W2 = W as Element of (InclPoset the topology of [:SS,SL:]) by A35;
dom (Theta (SS,SL)) = 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: V c= W
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in V or v in W )
assume A38: v in V ; ::_thesis: v in W
V1 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 set 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 = v2 as Element of L by A40;
reconsider v1 = v1 as Element of S by A39;
v2 in { y where y is Element of L : [v1,y] in V } 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 set st
( [v19,v2] in W & v19 in {v1} ) by RELAT_1:def_13;
hence v in W by A41, TARSKI:def_1; ::_thesis: verum
end;
W c= V
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in W or w in V )
assume A42: w in W ; ::_thesis: w in V
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 set 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 = w2 as Element of L by A44;
reconsider w1 = 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 ((Theta (SS,SL)) . W2) . w1 by A2, Def3;
then w2 in { y where y is Element of L : [w1,y] in V } by A19, A36;
then ex w29 being Element of L st
( w29 = w2 & [w1,w29] in V ) ;
hence w in V by A45; ::_thesis: verum
end;
then W2 = V by A37, XBOOLE_0:def_10;
hence V in the carrier of (InclPoset the topology of [:SS,SL:]) ; ::_thesis: verum
end;
InclPoset (sigma L) = InclPoset the topology of SL by YELLOW_9:51;
then UPS ((id S),f5) is isomorphic by A5, WAYBEL27:35;
then A46: (UPS ((id S),f5)) * (f3 ") is isomorphic by A10, Th6;
A47: f1 " 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not W in the carrier of (InclPoset the topology of [:SS,SL:]) or W in the carrier of (InclPoset (sigma [:S,L:])) )
assume A48: W in the carrier of (InclPoset the topology of [:SS,SL:]) ; ::_thesis: W in the carrier of (InclPoset (sigma [:S,L:]))
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,(Sigma (InclPoset the topology of SL)))) by FUNCT_2:def_3;
then consider V being set such that
A49: V in dom G and
A50: G . V = (Theta (SS,SL)) . W2 by FUNCT_1:def_3;
reconsider V = V as Element of (InclPoset (sigma [:S,L:])) by A49;
A51: V c= W
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in V or v in W )
assume A52: v in V ; ::_thesis: v in W
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 set 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 = v2 as Element of L by A54;
reconsider v1 = 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 set st
( [v19,v2] in W & v19 in {v1} ) by RELAT_1:def_13;
hence v in W by A55, TARSKI:def_1; ::_thesis: verum
end;
W c= V
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in W or w in V )
assume A56: w in W ; ::_thesis: w in V
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 set 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 = w2 as Element of L by A58;
reconsider w1 = 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 ((Theta (SS,SL)) . 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 w in V by A59; ::_thesis: verum
end;
then W = V by A51, XBOOLE_0:def_10;
hence W in the carrier of (InclPoset (sigma [:S,L:])) ; ::_thesis: verum
end;
then the carrier of (InclPoset (sigma [:S,L:])) = the carrier of (InclPoset the topology of [:SS,SL:]) by A34, XBOOLE_0:def_10;
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 ;
::_thesis: verum
end;
Lm11: for L being complete LATTICE st S8[L] holds
S7[L]
proof
let L be complete LATTICE; ::_thesis: ( S8[L] implies S7[L] )
set SL = the Scott TopAugmentation of L;
A1: RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4;
TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) = ConvergenceSpace (Scott-Convergence the Scott TopAugmentation of L) by WAYBEL11:32;
then A2: the topology of the Scott TopAugmentation of L = sigma the Scott TopAugmentation of L ;
then A3: InclPoset (sigma L) = InclPoset the topology of the Scott TopAugmentation of L by A1, YELLOW_9:52;
then reconsider S = InclPoset (sigma L) as complete LATTICE ;
set SS = the Scott TopAugmentation of S;
assume S8[L] ; ::_thesis: S7[L]
then A4: sigma [:S,L:] = the topology of [: the Scott TopAugmentation of S, the Scott TopAugmentation of L:] ;
A5: S5[ the Scott TopAugmentation of L]
proof
set Wy = { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } ;
let T be Scott TopAugmentation of InclPoset the topology of the Scott TopAugmentation of L; ::_thesis: { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } is open Subset of [:T, the Scott TopAugmentation of L:]
{ [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } c= the carrier of [:T, the Scott TopAugmentation of L:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } or x in the carrier of [:T, the Scott TopAugmentation of L:] )
A6: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (InclPoset the topology of the Scott TopAugmentation of L), the InternalRel of (InclPoset the topology of the Scott TopAugmentation of L) #) by YELLOW_9:def_4;
assume x in { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } ; ::_thesis: x in the carrier of [:T, the Scott TopAugmentation of L:]
then consider W being open Subset of the Scott TopAugmentation of L, y being Element of the Scott TopAugmentation of L such that
A7: x = [W,y] and
y in W ;
W in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2;
then W in the carrier of (InclPoset the topology of the Scott TopAugmentation of L) by YELLOW_1:1;
then [W,y] in [: the carrier of T, the carrier of the Scott TopAugmentation of L:] by A6, ZFMISC_1:87;
hence x in the carrier of [:T, the Scott TopAugmentation of L:] by A7, BORSUK_1:def_2; ::_thesis: verum
end;
then reconsider WY = { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } as Subset of [:T, the Scott TopAugmentation of L:] ;
A8: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of (InclPoset the topology of the Scott TopAugmentation of L), the InternalRel of (InclPoset the topology of the Scott TopAugmentation of L) #) by A3, YELLOW_9:def_4
.= RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4 ;
reconsider T1 = T as Scott TopAugmentation of S by A1, A2, YELLOW_9:52;
A9: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
the carrier of [:T, the Scott TopAugmentation of L:] = [: the carrier of T, the carrier of the Scott TopAugmentation of L:] 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:]; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,[:S,L:]) in wy or not D misses wy )
assume sup D in wy ; ::_thesis: not D misses wy
then [(sup (proj1 D)),(sup (proj2 D))] in wy by YELLOW_3:46;
then consider sp1D being open Subset of the Scott TopAugmentation of L, sp2D being Element of the Scott TopAugmentation of L 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 = sp1D9 as upper inaccessible Subset of L by A1, WAYBEL_0:25, YELLOW_9:47;
reconsider pD = proj1 D as Subset of (InclPoset the topology of the Scott TopAugmentation of L) by A1, A2, YELLOW_9:52;
reconsider proj2D = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3: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 set such that
A14: d in proj2 D and
A15: d in sp1D by XBOOLE_0:3;
reconsider d = 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 set such that
A18: [Y,d] in D by A14, XTUPLE_0:def_13;
reconsider V = V as Element of S by A17;
consider e being set 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 = Y as Element of S by A20;
reconsider e = 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 set 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 = DD2 as Element of L by A26;
reconsider DD1 = 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 the Scott TopAugmentation of L by A1, A2, YELLOW_9:52;
then DD1 is open Subset of the Scott TopAugmentation of L 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 the Scott TopAugmentation of L by A1, A2, YELLOW_9:52;
then reconsider DD1 = DD1 as open Subset of the Scott TopAugmentation of L by PRE_TOPC:def_2;
reconsider DD2 = DD2 as Element of the Scott TopAugmentation of L by A1;
[DD1,DD2] in wy by A30;
hence not D misses wy by A22, A25, XBOOLE_0:3; ::_thesis: verum
end;
wy is upper
proof
let x, y be Element of [:S,L:]; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in wy or not x <= y or y in wy )
assume that
A31: x in wy and
A32: x <= y ; ::_thesis: y in wy
consider x1 being open Subset of the Scott TopAugmentation of L, x2 being Element of the Scott TopAugmentation of L 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 the Scott TopAugmentation of L 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 set 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 the Scott TopAugmentation of L by A1, A2, YELLOW_9:52;
then reconsider y1 = y1 as open Subset of the Scott TopAugmentation of L by PRE_TOPC:def_2;
reconsider y2 = y2 as Element of the Scott TopAugmentation of L by A1, A36;
reconsider v2 = y2 as Element of L by A36;
y1 in the topology of the Scott TopAugmentation of L 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 y in wy by A37, A39; ::_thesis: verum
end;
then A40: wy in the topology of (ConvergenceSpace (Scott-Convergence [:S,L:])) by A10, WAYBEL11:31;
the topology of the Scott TopAugmentation of S = sigma S by YELLOW_9:51
.= the topology of T1 by YELLOW_9:51
.= the topology of T ;
then A41: TopStruct(# the carrier of the Scott TopAugmentation of S, the topology of the Scott TopAugmentation of S #) = TopStruct(# the carrier of T, the topology of T #) by A8;
TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) = TopStruct(# the carrier of the Scott TopAugmentation of L, the topology of the Scott TopAugmentation of L #) ;
then [: the Scott TopAugmentation of S, the Scott TopAugmentation of L:] = [:T, the Scott TopAugmentation of L:] by A41, Th7;
hence { [W,y] where W is open Subset of the Scott TopAugmentation of L, y is Element of the Scott TopAugmentation of L : y in W } is open Subset of [:T, the Scott TopAugmentation of L:] by A4, A40, PRE_TOPC:def_2; ::_thesis: verum
end;
( S5[ the Scott TopAugmentation of L] implies InclPoset the topology of the Scott TopAugmentation of L is continuous )
proof
assume S5[ the Scott TopAugmentation of L] ; ::_thesis: InclPoset the topology of the Scott TopAugmentation of L is continuous
then S6[ the Scott TopAugmentation of L] by Lm5;
hence InclPoset the topology of the Scott TopAugmentation of L is continuous by Lm7; ::_thesis: verum
end;
hence S7[L] by A1, A2, A5, YELLOW_9:52; ::_thesis: verum
end;
theorem Th30: :: WAYBEL29:30
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; ::_thesis: ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )
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; ::_thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) implies InclPoset (sigma L) is continuous )
assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; ::_thesis: InclPoset (sigma L) is continuous
now__::_thesis:_for_SL_being_Scott_TopAugmentation_of_L
for_S_being_complete_LATTICE
for_SS_being_Scott_TopAugmentation_of_S_holds_sigma_[:S,L:]_=_the_topology_of_[:SS,SL:]
let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:]
( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4;
then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13;
( RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def_4;
then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology 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; ::_thesis: verum
end;
hence InclPoset (sigma L) is continuous by Lm11; ::_thesis: verum
end;
theorem Th31: :: WAYBEL29:31
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 TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] )
proof
let L be complete LATTICE; ::_thesis: ( ( for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ) iff for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] )
hereby ::_thesis: ( ( for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )
assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):]
S8[L]
proof
let SL be Scott TopAugmentation of L; ::_thesis: for S being complete LATTICE
for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let S be complete LATTICE; ::_thesis: for SS being Scott TopAugmentation of S holds sigma [:S,L:] = the topology of [:SS,SL:]
let SS be Scott TopAugmentation of S; ::_thesis: sigma [:S,L:] = the topology of [:SS,SL:]
( RelStr(# the carrier of SL, the InternalRel of SL #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of (Sigma L), the InternalRel of (Sigma L) #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4;
then A2: TopStruct(# the carrier of (Sigma L), the topology of (Sigma L) #) = TopStruct(# the carrier of SL, the topology of SL #) by Th13;
( RelStr(# the carrier of SS, the InternalRel of SS #) = RelStr(# the carrier of S, the InternalRel of S #) & RelStr(# the carrier of (Sigma S), the InternalRel of (Sigma S) #) = RelStr(# the carrier of S, the InternalRel of S #) ) by YELLOW_9:def_4;
then TopStruct(# the carrier of (Sigma S), the topology of (Sigma S) #) = TopStruct(# the carrier of SS, the topology 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; ::_thesis: verum
end;
hence for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by Lm9; ::_thesis: verum
end;
assume A3: for S being complete LATTICE holds TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
let S be complete LATTICE; ::_thesis: sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by A3;
hence sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] by YELLOW_9:51; ::_thesis: verum
end;
theorem Th32: :: WAYBEL29:32
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; ::_thesis: ( ( 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):] )
hereby ::_thesis: ( ( for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) implies for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] )
assume A1: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):]
let S be complete LATTICE; ::_thesis: Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):]
TopStruct(# the carrier of (Sigma [:S,L:]), the topology 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; ::_thesis: verum
end;
assume A2: for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ; ::_thesis: for S being complete LATTICE holds sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
let S be complete LATTICE; ::_thesis: sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):]
Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] by A2;
then TopStruct(# the carrier of (Sigma [:S,L:]), the topology of (Sigma [:S,L:]) #) = [:(Sigma S),(Sigma L):] by WAYBEL25:def_2;
hence sigma [:S,L:] = the topology of [:(Sigma S),(Sigma L):] by YELLOW_9:51; ::_thesis: verum
end;
theorem :: WAYBEL29:33
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; ::_thesis: ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] )
( 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 ( InclPoset (sigma L) is continuous iff for S being complete LATTICE holds Sigma [:S,L:] = Omega [:(Sigma S),(Sigma L):] ) by Th32; ::_thesis: verum
end;