:: WAYBEL24 semantic presentation
begin
theorem :: WAYBEL24:1
for S, T being up-complete Scott TopLattice
for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T
proof
let S, T be up-complete Scott TopLattice; ::_thesis: for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T
let M be Subset of (SCMaps (S,T)); ::_thesis: "\/" (M,(SCMaps (S,T))) is continuous Function of S,T
the carrier of (SCMaps (S,T)) c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13;
then "\/" (M,(SCMaps (S,T))) in the carrier of (MonMaps (S,T)) by TARSKI:def_3;
hence "\/" (M,(SCMaps (S,T))) is continuous Function of S,T by WAYBEL10:9, WAYBEL17:def_2; ::_thesis: verum
end;
registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
cluster Function-like constant quasi_total -> monotone for Element of bool [: the carrier of S, the carrier of T:];
coherence
for b1 being Function of S,T st b1 is constant holds
b1 is monotone
proof
let f be Function of S,T; ::_thesis: ( f is constant implies f is monotone )
assume A1: f is constant ; ::_thesis: f is monotone
for x, y being Element of S st x <= y holds
f . x <= f . y
proof
let x, y be Element of S; ::_thesis: ( x <= y implies f . x <= f . y )
assume x <= y ; ::_thesis: f . x <= f . y
y in the carrier of S ;
then A2: y in dom f by FUNCT_2:def_1;
x in the carrier of S ;
then x in dom f by FUNCT_2:def_1;
hence f . x <= f . y by A1, A2, FUNCT_1:def_10; ::_thesis: verum
end;
hence f is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;
end;
registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
let a be Element of T;
clusterS --> a -> monotone ;
coherence
S --> a is monotone
proof
set f = S --> a;
for x, y being Element of S st x <= y holds
(S --> a) . x <= (S --> a) . y
proof
let x, y be Element of S; ::_thesis: ( x <= y implies (S --> a) . x <= (S --> a) . y )
assume x <= y ; ::_thesis: (S --> a) . x <= (S --> a) . y
(S --> a) . x = ( the carrier of S --> a) . x
.= a by FUNCOP_1:7
.= ( the carrier of S --> a) . y by FUNCOP_1:7
.= (S --> a) . y ;
hence (S --> a) . x <= (S --> a) . y ; ::_thesis: verum
end;
hence S --> a is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;
end;
theorem :: WAYBEL24:2
for S being non empty RelStr
for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T)
let T be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: Bottom (MonMaps (S,T)) = S --> (Bottom T)
set L = MonMaps (S,T);
reconsider f = S --> (Bottom T) as Element of (MonMaps (S,T)) by WAYBEL10:9;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (MonMaps (S,T)) st b is_>=_than {} holds
f <= b
proof
let b be Element of (MonMaps (S,T)); ::_thesis: ( b is_>=_than {} implies f <= b )
assume b is_>=_than {} ; ::_thesis: f <= b
reconsider b9 = b as Function of S,T by WAYBEL10:9;
reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:58;
for x being Element of S holds f9 . x <= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x <= b9 . x
f9 . x = ( the carrier of S --> (Bottom T)) . x
.= Bottom T by FUNCOP_1:7 ;
hence f9 . x <= b9 . x by YELLOW_0:44; ::_thesis: verum
end;
then f9 <= b9 by YELLOW_2:9;
then f99 <= b99 by WAYBEL10:11;
hence f <= b by YELLOW_0:60; ::_thesis: verum
end;
f is_>=_than {} by YELLOW_0:6;
then f = "\/" ({},(MonMaps (S,T))) by A1, YELLOW_0:30;
hence Bottom (MonMaps (S,T)) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum
end;
theorem :: WAYBEL24:3
for S being non empty RelStr
for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T)
let T be non empty reflexive antisymmetric upper-bounded RelStr ; ::_thesis: Top (MonMaps (S,T)) = S --> (Top T)
set L = MonMaps (S,T);
reconsider f = S --> (Top T) as Element of (MonMaps (S,T)) by WAYBEL10:9;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (MonMaps (S,T)) st b is_<=_than {} holds
f >= b
proof
let b be Element of (MonMaps (S,T)); ::_thesis: ( b is_<=_than {} implies f >= b )
assume b is_<=_than {} ; ::_thesis: f >= b
reconsider b9 = b as Function of S,T by WAYBEL10:9;
reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:58;
for x being Element of S holds f9 . x >= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x >= b9 . x
f9 . x = ( the carrier of S --> (Top T)) . x
.= Top T by FUNCOP_1:7 ;
hence f9 . x >= b9 . x by YELLOW_0:45; ::_thesis: verum
end;
then f9 >= b9 by YELLOW_2:9;
then f99 >= b99 by WAYBEL10:11;
hence f >= b by YELLOW_0:60; ::_thesis: verum
end;
f is_<=_than {} by YELLOW_0:6;
then f = "/\" ({},(MonMaps (S,T))) by A1, YELLOW_0:31;
hence Top (MonMaps (S,T)) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum
end;
scheme :: WAYBEL24:sch 1
FuncFraenkelSL{ F1() -> non empty RelStr , F2() -> non empty RelStr , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } :
F4() .: { F3(x) where x is Element of F1() : P1[x] } = { (F4() . F3(x)) where x is Element of F1() : P1[x] }
provided
A1: the carrier of F2() c= dom F4()
proof
set f = F4();
thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } )
assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] }
then consider z being set such that
z in dom F4() and
A2: z in { F3(x) where x is Element of F1() : P1[x] } and
A3: y = F4() . z by FUNCT_1:def_6;
ex x being Element of F1() st
( z = F3(x) & P1[x] ) by A2;
hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } )
assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] }
then consider x being Element of F1() such that
A4: y = F4() . F3(x) and
A5: P1[x] ;
( F3(x) in the carrier of F2() & F3(x) in { F3(z) where z is Element of F1() : P1[z] } ) by A5;
hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A1, A4, FUNCT_1:def_6; ::_thesis: verum
end;
scheme :: WAYBEL24:sch 2
Fraenkel6A{ F1() -> LATTICE, F2( set ) -> set , P1[ set ], P2[ set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F2(v2) where v2 is Element of F1() : P2[v2] }
provided
A1: for v being Element of F1() holds
( P1[v] iff P2[v] )
proof
thus { F2(v1) where v1 is Element of F1() : P1[v1] } c= { F2(v2) where v2 is Element of F1() : P2[v2] } :: according to XBOOLE_0:def_10 ::_thesis: { F2(v2) where v2 is Element of F1() : P2[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F2(v1) where v1 is Element of F1() : P1[v1] } or a in { F2(v2) where v2 is Element of F1() : P2[v2] } )
assume a in { F2(v1) where v1 is Element of F1() : P1[v1] } ; ::_thesis: a in { F2(v2) where v2 is Element of F1() : P2[v2] }
then consider V1 being Element of F1() such that
A2: a = F2(V1) and
A3: P1[V1] ;
P2[V1] by A1, A3;
hence a in { F2(v2) where v2 is Element of F1() : P2[v2] } by A2; ::_thesis: verum
end;
thus { F2(v2) where v2 is Element of F1() : P2[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] } ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F2(v2) where v2 is Element of F1() : P2[v2] } or a in { F2(v1) where v1 is Element of F1() : P1[v1] } )
assume a in { F2(v1) where v1 is Element of F1() : P2[v1] } ; ::_thesis: a in { F2(v1) where v1 is Element of F1() : P1[v1] }
then consider V1 being Element of F1() such that
A4: a = F2(V1) and
A5: P2[V1] ;
P1[V1] by A1, A5;
hence a in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; ::_thesis: verum
end;
end;
theorem Th4: :: WAYBEL24:4
for S, T being complete LATTICE
for f being monotone Function of S,T
for x being Element of S holds f . x = sup (f .: (downarrow x))
proof
let S, T be complete LATTICE; ::_thesis: for f being monotone Function of S,T
for x being Element of S holds f . x = sup (f .: (downarrow x))
let f be monotone Function of S,T; ::_thesis: for x being Element of S holds f . x = sup (f .: (downarrow x))
let x be Element of S; ::_thesis: f . x = sup (f .: (downarrow x))
A1: for b being Element of T st b is_>=_than f .: (downarrow x) holds
f . x <= b
proof
let b be Element of T; ::_thesis: ( b is_>=_than f .: (downarrow x) implies f . x <= b )
x <= x ;
then ( dom f = the carrier of S & x in downarrow x ) by FUNCT_2:def_1, WAYBEL_0:17;
then A2: f . x in f .: (downarrow x) by FUNCT_1:def_6;
assume b is_>=_than f .: (downarrow x) ; ::_thesis: f . x <= b
hence f . x <= b by A2, LATTICE3:def_9; ::_thesis: verum
end;
( ex_sup_of downarrow x,S & sup (downarrow x) = x ) by WAYBEL_0:34;
then downarrow x is_<=_than x by YELLOW_0:30;
then f .: (downarrow x) is_<=_than f . x by YELLOW_2:14;
hence f . x = sup (f .: (downarrow x)) by A1, YELLOW_0:30; ::_thesis: verum
end;
theorem :: WAYBEL24:5
for S, T being lower-bounded complete LATTICE
for f being monotone Function of S,T
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
proof
let S, T be lower-bounded complete LATTICE; ::_thesis: for f being monotone Function of S,T
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
let f be monotone Function of S,T; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
let x be Element of S; ::_thesis: f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
deffunc H1( Element of S) -> Element of S = $1;
defpred S1[ Element of S] means $1 <= x;
defpred S2[ Element of S] means ex y1 being Element of S st
( $1 <= y1 & y1 in {x} );
A1: the carrier of S c= dom f by FUNCT_2:def_1;
A2: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL24:sch_1(A1);
A3: for x2 being Element of S holds
( S1[x2] iff S2[x2] )
proof
let x2 be Element of S; ::_thesis: ( S1[x2] iff S2[x2] )
hereby ::_thesis: ( S2[x2] implies S1[x2] )
A4: x in {x} by TARSKI:def_1;
assume x2 <= x ; ::_thesis: ex y1 being Element of S st
( x2 <= y1 & y1 in {x} )
hence ex y1 being Element of S st
( x2 <= y1 & y1 in {x} ) by A4; ::_thesis: verum
end;
given y1 being Element of S such that A5: ( x2 <= y1 & y1 in {x} ) ; ::_thesis: S1[x2]
thus S1[x2] by A5, TARSKI:def_1; ::_thesis: verum
end;
{ H1(w) where w is Element of S : S1[w] } = { H1(x1) where x1 is Element of S : S2[x1] } from WAYBEL24:sch_2(A3);
then A6: downarrow x = { w where w is Element of S : w <= x } by WAYBEL_0:14;
sup (f .: (downarrow x)) = f . x by Th4
.= f . (sup (downarrow x)) by WAYBEL_0:34 ;
hence f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T) by A2, A6, WAYBEL_0:34; ::_thesis: verum
end;
theorem Th6: :: WAYBEL24:6
for S being RelStr
for T being non empty RelStr
for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
proof
let S be RelStr ; ::_thesis: for T being non empty RelStr
for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
let T be non empty RelStr ; ::_thesis: for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
let F be Subset of (T |^ the carrier of S); ::_thesis: sup F is Function of S,T
set f = sup F;
sup F in the carrier of (T |^ the carrier of S) ;
then sup F in Funcs ( the carrier of S, the carrier of T) by YELLOW_1:28;
then ex f9 being Function st
( f9 = sup F & dom f9 = the carrier of S & rng f9 c= the carrier of T ) by FUNCT_2:def_2;
hence sup F is Function of S,T by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
begin
definition
let X1, X2, Y be non empty RelStr ;
let f be Function of [:X1,X2:],Y;
let x be Element of X1;
func Proj (f,x) -> Function of X2,Y equals :: WAYBEL24:def 1
(curry f) . x;
correctness
coherence
(curry f) . x is Function of X2,Y;
proof
[: the carrier of X1, the carrier of X2:] = the carrier of [:X1,X2:] by YELLOW_3:def_2;
then curry f is Function of the carrier of X1,(Funcs ( the carrier of X2, the carrier of Y)) by FUNCT_5:67;
hence (curry f) . x is Function of X2,Y by FUNCT_2:5, FUNCT_2:66; ::_thesis: verum
end;
end;
:: deftheorem defines Proj WAYBEL24:def_1_:_
for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for x being Element of X1 holds Proj (f,x) = (curry f) . x;
theorem Th7: :: WAYBEL24:7
for Y, X1, X2 being non empty RelStr
for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
proof
let Y, X1, X2 be non empty RelStr ; ::_thesis: for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
let f be Function of [:X1,X2:],Y; ::_thesis: for x being Element of X1
for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
let x be Element of X1; ::_thesis: for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
let y be Element of X2; ::_thesis: (Proj (f,x)) . y = f . (x,y)
dom f = the carrier of [:X1,X2:] by FUNCT_2:def_1
.= [: the carrier of X1, the carrier of X2:] by YELLOW_3:def_2 ;
then [x,y] in dom f by ZFMISC_1:87;
hence (Proj (f,x)) . y = f . (x,y) by FUNCT_5:20; ::_thesis: verum
end;
definition
let X1, X2, Y be non empty RelStr ;
let f be Function of [:X1,X2:],Y;
let y be Element of X2;
func Proj (f,y) -> Function of X1,Y equals :: WAYBEL24:def 2
(curry' f) . y;
correctness
coherence
(curry' f) . y is Function of X1,Y;
proof
[: the carrier of X1, the carrier of X2:] = the carrier of [:X1,X2:] by YELLOW_3:def_2;
then curry' f is Function of the carrier of X2,(Funcs ( the carrier of X1, the carrier of Y)) by FUNCT_5:68;
hence (curry' f) . y is Function of X1,Y by FUNCT_2:5, FUNCT_2:66; ::_thesis: verum
end;
end;
:: deftheorem defines Proj WAYBEL24:def_2_:_
for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2 holds Proj (f,y) = (curry' f) . y;
theorem Th8: :: WAYBEL24:8
for Y, X2, X1 being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2
for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
proof
let Y, X2, X1 be non empty RelStr ; ::_thesis: for f being Function of [:X1,X2:],Y
for y being Element of X2
for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
let f be Function of [:X1,X2:],Y; ::_thesis: for y being Element of X2
for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
let y be Element of X2; ::_thesis: for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
let x be Element of X1; ::_thesis: (Proj (f,y)) . x = f . (x,y)
dom f = the carrier of [:X1,X2:] by FUNCT_2:def_1
.= [: the carrier of X1, the carrier of X2:] by YELLOW_3:def_2 ;
then [x,y] in dom f by ZFMISC_1:87;
hence (Proj (f,y)) . x = f . (x,y) by FUNCT_5:22; ::_thesis: verum
end;
theorem Th9: :: WAYBEL24:9
for R, S, T being non empty RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
proof
let R, S, T be non empty RelStr ; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
let a be Element of R; ::_thesis: for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
let b be Element of S; ::_thesis: (Proj (f,a)) . b = (Proj (f,b)) . a
(Proj (f,a)) . b = f . (a,b) by Th7
.= (Proj (f,b)) . a by Th8 ;
hence (Proj (f,a)) . b = (Proj (f,b)) . a ; ::_thesis: verum
end;
registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total antitone for Element of bool [: the carrier of S, the carrier of T:];
existence
ex b1 being Function of S,T st b1 is antitone
proof
set c = the Element of T;
take f = S --> the Element of T; ::_thesis: f is antitone
let x, y be Element of S; :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b2 <= b1 ) )
assume [x,y] in the InternalRel of S ; :: according to ORDERS_2:def_5 ::_thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b2 <= b1 )
let a, b be Element of T; ::_thesis: ( not a = f . x or not b = f . y or b <= a )
assume that
A1: a = f . x and
A2: b = f . y ; ::_thesis: b <= a
a = the Element of T by A1, FUNCOP_1:7;
hence b <= a by A2, FUNCOP_1:7; ::_thesis: verum
end;
end;
theorem Th10: :: WAYBEL24:10
for R, S, T being non empty reflexive RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
proof
let R, S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
let a be Element of R; ::_thesis: for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
let b be Element of S; ::_thesis: ( f is monotone implies ( Proj (f,a) is monotone & Proj (f,b) is monotone ) )
reconsider a = a as Element of R ;
reconsider b = b as Element of S ;
set g = Proj (f,b);
set h = Proj (f,a);
assume A1: f is monotone ; ::_thesis: ( Proj (f,a) is monotone & Proj (f,b) is monotone )
A2: now__::_thesis:_for_x,_y_being_Element_of_R_st_x_<=_y_holds_
(Proj_(f,b))_._x_<=_(Proj_(f,b))_._y
let x, y be Element of R; ::_thesis: ( x <= y implies (Proj (f,b)) . x <= (Proj (f,b)) . y )
A3: b <= b ;
A4: ( (Proj (f,b)) . x = f . (x,b) & (Proj (f,b)) . y = f . (y,b) ) by Th8;
assume x <= y ; ::_thesis: (Proj (f,b)) . x <= (Proj (f,b)) . y
then [x,b] <= [y,b] by A3, YELLOW_3:11;
hence (Proj (f,b)) . x <= (Proj (f,b)) . y by A1, A4, WAYBEL_1:def_2; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
(Proj_(f,a))_._x_<=_(Proj_(f,a))_._y
let x, y be Element of S; ::_thesis: ( x <= y implies (Proj (f,a)) . x <= (Proj (f,a)) . y )
A5: a <= a ;
A6: ( (Proj (f,a)) . x = f . (a,x) & (Proj (f,a)) . y = f . (a,y) ) by Th7;
assume x <= y ; ::_thesis: (Proj (f,a)) . x <= (Proj (f,a)) . y
then [a,x] <= [a,y] by A5, YELLOW_3:11;
hence (Proj (f,a)) . x <= (Proj (f,a)) . y by A1, A6, WAYBEL_1:def_2; ::_thesis: verum
end;
hence ( Proj (f,a) is monotone & Proj (f,b) is monotone ) by A2, WAYBEL_1:def_2; ::_thesis: verum
end;
theorem Th11: :: WAYBEL24:11
for R, S, T being non empty reflexive RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
proof
let R, S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let a be Element of R; ::_thesis: for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let b be Element of S; ::_thesis: ( f is antitone implies ( Proj (f,a) is antitone & Proj (f,b) is antitone ) )
reconsider a9 = a as Element of R ;
set g = Proj (f,b);
set h = Proj (f,a);
assume A1: f is antitone ; ::_thesis: ( Proj (f,a) is antitone & Proj (f,b) is antitone )
A2: now__::_thesis:_for_x,_y_being_Element_of_R_st_x_<=_y_holds_
(Proj_(f,b))_._x_>=_(Proj_(f,b))_._y
reconsider b9 = b as Element of S ;
let x, y be Element of R; ::_thesis: ( x <= y implies (Proj (f,b)) . x >= (Proj (f,b)) . y )
A3: b9 <= b9 ;
A4: ( (Proj (f,b)) . x = f . (x,b) & (Proj (f,b)) . y = f . (y,b) ) by Th8;
assume x <= y ; ::_thesis: (Proj (f,b)) . x >= (Proj (f,b)) . y
then [x,b9] <= [y,b9] by A3, YELLOW_3:11;
hence (Proj (f,b)) . x >= (Proj (f,b)) . y by A1, A4, WAYBEL_0:def_5; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
(Proj_(f,a))_._x_>=_(Proj_(f,a))_._y
let x, y be Element of S; ::_thesis: ( x <= y implies (Proj (f,a)) . x >= (Proj (f,a)) . y )
A5: a9 <= a9 ;
A6: ( (Proj (f,a)) . x = f . (a,x) & (Proj (f,a)) . y = f . (a,y) ) by Th7;
assume x <= y ; ::_thesis: (Proj (f,a)) . x >= (Proj (f,a)) . y
then [a9,x] <= [a9,y] by A5, YELLOW_3:11;
hence (Proj (f,a)) . x >= (Proj (f,a)) . y by A1, A6, WAYBEL_0:def_5; ::_thesis: verum
end;
hence ( Proj (f,a) is antitone & Proj (f,b) is antitone ) by A2, WAYBEL_9:def_1; ::_thesis: verum
end;
registration
let R, S, T be non empty reflexive RelStr ;
let f be monotone Function of [:R,S:],T;
let a be Element of R;
cluster Proj (f,a) -> monotone ;
coherence
Proj (f,a) is monotone by Th10;
end;
registration
let R, S, T be non empty reflexive RelStr ;
let f be monotone Function of [:R,S:],T;
let b be Element of S;
cluster Proj (f,b) -> monotone ;
coherence
Proj (f,b) is monotone by Th10;
end;
registration
let R, S, T be non empty reflexive RelStr ;
let f be antitone Function of [:R,S:],T;
let a be Element of R;
cluster Proj (f,a) -> antitone ;
coherence
Proj (f,a) is antitone by Th11;
end;
registration
let R, S, T be non empty reflexive RelStr ;
let f be antitone Function of [:R,S:],T;
let b be Element of S;
cluster Proj (f,b) -> antitone ;
coherence
Proj (f,b) is antitone by Th11;
end;
theorem Th12: :: WAYBEL24:12
for R, S, T being LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds
f is monotone
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds
f is monotone
let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) implies f is monotone )
assume A1: for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ; ::_thesis: f is monotone
now__::_thesis:_for_x,_y_being_Element_of_[:R,S:]_st_x_<=_y_holds_
f_._x_<=_f_._y
let x, y be Element of [:R,S:]; ::_thesis: ( x <= y implies f . x <= f . y )
assume A2: x <= y ; ::_thesis: f . x <= f . y
then A3: x `1 <= y `1 by YELLOW_3:12;
A4: x `2 <= y `2 by A2, YELLOW_3:12;
A5: f . ((x `1),(y `2)) = (Proj (f,(x `1))) . (y `2) by Th7;
( Proj (f,(x `1)) is monotone & f . ((x `1),(x `2)) = (Proj (f,(x `1))) . (x `2) ) by A1, Th7;
then A6: f . [(x `1),(x `2)] <= f . [(x `1),(y `2)] by A4, A5, WAYBEL_1:def_2;
A7: f . ((y `1),(y `2)) = (Proj (f,(y `2))) . (y `1) by Th8;
( Proj (f,(y `2)) is monotone & f . ((x `1),(y `2)) = (Proj (f,(y `2))) . (x `1) ) by A1, Th8;
then f . [(x `1),(y `2)] <= f . [(y `1),(y `2)] by A3, A7, WAYBEL_1:def_2;
then A8: f . [(x `1),(x `2)] <= f . [(y `1),(y `2)] by A6, YELLOW_0:def_2;
A9: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then f . [(y `1),(y `2)] = f . y by MCART_1:21;
hence f . x <= f . y by A8, A9, MCART_1:21; ::_thesis: verum
end;
hence f is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;
theorem :: WAYBEL24:13
for R, S, T being LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds
f is antitone
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds
f is antitone
let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) implies f is antitone )
assume A1: for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ; ::_thesis: f is antitone
now__::_thesis:_for_x,_y_being_Element_of_[:R,S:]_st_x_<=_y_holds_
f_._x_>=_f_._y
let x, y be Element of [:R,S:]; ::_thesis: ( x <= y implies f . x >= f . y )
assume A2: x <= y ; ::_thesis: f . x >= f . y
then A3: x `1 <= y `1 by YELLOW_3:12;
A4: x `2 <= y `2 by A2, YELLOW_3:12;
A5: f . ((x `1),(y `2)) = (Proj (f,(x `1))) . (y `2) by Th7;
( Proj (f,(x `1)) is antitone & f . ((x `1),(x `2)) = (Proj (f,(x `1))) . (x `2) ) by A1, Th7;
then A6: f . [(x `1),(x `2)] >= f . [(x `1),(y `2)] by A4, A5, WAYBEL_9:def_1;
A7: f . ((y `1),(y `2)) = (Proj (f,(y `2))) . (y `1) by Th8;
( Proj (f,(y `2)) is antitone & f . ((x `1),(y `2)) = (Proj (f,(y `2))) . (x `1) ) by A1, Th8;
then f . [(x `1),(y `2)] >= f . [(y `1),(y `2)] by A3, A7, WAYBEL_9:def_1;
then A8: f . [(x `1),(x `2)] >= f . [(y `1),(y `2)] by A6, YELLOW_0:def_2;
A9: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then f . [(y `1),(y `2)] = f . y by MCART_1:21;
hence f . x >= f . y by A8, A9, MCART_1:21; ::_thesis: verum
end;
hence f is antitone by WAYBEL_9:def_1; ::_thesis: verum
end;
theorem Th14: :: WAYBEL24:14
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for b being Element of S
for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T
for b being Element of S
for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
let f be Function of [:R,S:],T; ::_thesis: for b being Element of S
for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
let b be Element of S; ::_thesis: for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
let X be Subset of R; ::_thesis: (Proj (f,b)) .: X = f .: [:X,{b}:]
A1: (Proj (f,b)) .: X c= f .: [:X,{b}:]
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in (Proj (f,b)) .: X or c in f .: [:X,{b}:] )
assume c in (Proj (f,b)) .: X ; ::_thesis: c in f .: [:X,{b}:]
then consider k being set such that
A2: k in dom (Proj (f,b)) and
A3: k in X and
A4: c = (Proj (f,b)) . k by FUNCT_1:def_6;
b in {b} by TARSKI:def_1;
then A5: [k,b] in [:X,{b}:] by A3, ZFMISC_1:87;
[: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then dom f = [: the carrier of R, the carrier of S:] by FUNCT_2:def_1;
then A6: [k,b] in dom f by A2, ZFMISC_1:87;
c = f . (k,b) by A2, A4, Th8;
hence c in f .: [:X,{b}:] by A5, A6, FUNCT_1:def_6; ::_thesis: verum
end;
f .: [:X,{b}:] c= (Proj (f,b)) .: X
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in f .: [:X,{b}:] or c in (Proj (f,b)) .: X )
assume c in f .: [:X,{b}:] ; ::_thesis: c in (Proj (f,b)) .: X
then consider k being set such that
k in dom f and
A7: k in [:X,{b}:] and
A8: c = f . k by FUNCT_1:def_6;
consider k1, k2 being set such that
A9: k1 in X and
A10: k2 in {b} and
A11: k = [k1,k2] by A7, ZFMISC_1:def_2;
A12: k2 = b by A10, TARSKI:def_1;
c = f . (k1,k2) by A8, A11;
then ( dom (Proj (f,b)) = the carrier of R & c = (Proj (f,b)) . k1 ) by A9, A12, Th8, FUNCT_2:def_1;
hence c in (Proj (f,b)) .: X by A9, FUNCT_1:def_6; ::_thesis: verum
end;
hence (Proj (f,b)) .: X = f .: [:X,{b}:] by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th15: :: WAYBEL24:15
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T
for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let f be Function of [:R,S:],T; ::_thesis: for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let b be Element of R; ::_thesis: for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let X be Subset of S; ::_thesis: (Proj (f,b)) .: X = f .: [:{b},X:]
A1: (Proj (f,b)) .: X c= f .: [:{b},X:]
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in (Proj (f,b)) .: X or c in f .: [:{b},X:] )
assume c in (Proj (f,b)) .: X ; ::_thesis: c in f .: [:{b},X:]
then consider k being set such that
A2: k in dom (Proj (f,b)) and
A3: k in X and
A4: c = (Proj (f,b)) . k by FUNCT_1:def_6;
b in {b} by TARSKI:def_1;
then A5: [b,k] in [:{b},X:] by A3, ZFMISC_1:87;
[: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then dom f = [: the carrier of R, the carrier of S:] by FUNCT_2:def_1;
then A6: [b,k] in dom f by A2, ZFMISC_1:87;
c = f . (b,k) by A2, A4, Th7;
hence c in f .: [:{b},X:] by A5, A6, FUNCT_1:def_6; ::_thesis: verum
end;
f .: [:{b},X:] c= (Proj (f,b)) .: X
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in f .: [:{b},X:] or c in (Proj (f,b)) .: X )
assume c in f .: [:{b},X:] ; ::_thesis: c in (Proj (f,b)) .: X
then consider k being set such that
k in dom f and
A7: k in [:{b},X:] and
A8: c = f . k by FUNCT_1:def_6;
consider k1, k2 being set such that
A9: k1 in {b} and
A10: k2 in X and
A11: k = [k1,k2] by A7, ZFMISC_1:def_2;
A12: k1 = b by A9, TARSKI:def_1;
c = f . (k1,k2) by A8, A11;
then ( dom (Proj (f,b)) = the carrier of S & c = (Proj (f,b)) . k2 ) by A10, A12, Th7, FUNCT_2:def_1;
hence c in (Proj (f,b)) .: X by A10, FUNCT_1:def_6; ::_thesis: verum
end;
hence (Proj (f,b)) .: X = f .: [:{b},X:] by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: WAYBEL24:16
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let a be Element of R; ::_thesis: for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let b be Element of S; ::_thesis: ( f is directed-sups-preserving implies ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) )
assume A1: f is directed-sups-preserving ; ::_thesis: ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
A2: for X being Subset of S st not X is empty & X is directed holds
Proj (f,a) preserves_sup_of X
proof
reconsider Y9 = {a} as non empty directed Subset of R by WAYBEL_0:5;
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies Proj (f,a) preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: Proj (f,a) preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of S ;
Proj (f,a) preserves_sup_of X
proof
A3: sup Y9 = a by YELLOW_0:39;
A4: f preserves_sup_of [:Y9,X9:] by A1, WAYBEL_0:def_37;
A5: (Proj (f,a)) .: X = f .: [:Y9,X9:] by Th15;
A6: ex_sup_of Y9,R by YELLOW_0:38;
assume A7: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) )
then A8: ex_sup_of [:Y9,X9:],[:R,S:] by A6, YELLOW_3:39;
sup ((Proj (f,a)) .: X) = sup (f .: [:Y9,X9:]) by Th15
.= f . (sup [:Y9,X9:]) by A8, A4, WAYBEL_0:def_31
.= f . ((sup Y9),(sup X9)) by A7, A6, YELLOW_3:43
.= (Proj (f,a)) . (sup X) by A3, Th7 ;
hence ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) ) by A8, A4, A5, WAYBEL_0:def_31; ::_thesis: verum
end;
hence Proj (f,a) preserves_sup_of X ; ::_thesis: verum
end;
for X being Subset of R st not X is empty & X is directed holds
Proj (f,b) preserves_sup_of X
proof
reconsider Y9 = {b} as non empty directed Subset of S by WAYBEL_0:5;
let X be Subset of R; ::_thesis: ( not X is empty & X is directed implies Proj (f,b) preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: Proj (f,b) preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of R ;
Proj (f,b) preserves_sup_of X
proof
A9: sup Y9 = b by YELLOW_0:39;
A10: f preserves_sup_of [:X9,Y9:] by A1, WAYBEL_0:def_37;
A11: (Proj (f,b)) .: X = f .: [:X9,Y9:] by Th14;
A12: ex_sup_of Y9,S by YELLOW_0:38;
assume A13: ex_sup_of X,R ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) )
then A14: ex_sup_of [:X9,Y9:],[:R,S:] by A12, YELLOW_3:39;
sup ((Proj (f,b)) .: X) = sup (f .: [:X9,Y9:]) by Th14
.= f . (sup [:X9,Y9:]) by A14, A10, WAYBEL_0:def_31
.= f . ((sup X9),(sup Y9)) by A13, A12, YELLOW_3:43
.= (Proj (f,b)) . (sup X) by A9, Th8 ;
hence ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) ) by A14, A10, A11, WAYBEL_0:def_31; ::_thesis: verum
end;
hence Proj (f,b) preserves_sup_of X ; ::_thesis: verum
end;
hence ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) by A2, WAYBEL_0:def_37; ::_thesis: verum
end;
theorem Th17: :: WAYBEL24:17
for R, S, T being LATTICE
for f being monotone Function of [:R,S:],T
for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
proof
let R, S, T be LATTICE; ::_thesis: for f being monotone Function of [:R,S:],T
for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let f be monotone Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let a be Element of R; ::_thesis: for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let b be Element of S; ::_thesis: for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let X be directed Subset of [:R,S:]; ::_thesis: ( ex_sup_of f .: X,T & a in proj1 X & b in proj2 X implies f . [a,b] <= sup (f .: X) )
assume that
A1: ex_sup_of f .: X,T and
A2: a in proj1 X and
A3: b in proj2 X ; ::_thesis: f . [a,b] <= sup (f .: X)
consider d being set such that
A4: [d,b] in X by A3, XTUPLE_0:def_13;
d in proj1 X by A4, XTUPLE_0:def_12;
then reconsider d = d as Element of R ;
consider c being set such that
A5: [a,c] in X by A2, XTUPLE_0:def_12;
c in proj2 X by A5, XTUPLE_0:def_13;
then reconsider c = c as Element of S ;
consider z being Element of [:R,S:] such that
A6: z in X and
A7: ( [a,c] <= z & [d,b] <= z ) by A5, A4, WAYBEL_0:def_1;
A8: f .: X is_<=_than sup (f .: X) by A1, YELLOW_0:30;
[a,c] "\/" [d,b] <= z "\/" z by A7, YELLOW_3:3;
then [a,c] "\/" [d,b] <= z by YELLOW_5:1;
then [(a "\/" d),(c "\/" b)] <= z by YELLOW10:16;
then A9: f . [(a "\/" d),(c "\/" b)] <= f . z by WAYBEL_1:def_2;
dom f = the carrier of [:R,S:] by FUNCT_2:def_1;
then f . z in f .: X by A6, FUNCT_1:def_6;
then A10: f . z <= sup (f .: X) by A8, LATTICE3:def_9;
( a <= a "\/" d & b <= c "\/" b ) by YELLOW_0:22;
then [a,b] <= [(a "\/" d),(c "\/" b)] by YELLOW_3:11;
then f . [a,b] <= f . [(a "\/" d),(c "\/" b)] by WAYBEL_1:def_2;
then f . [a,b] <= f . z by A9, YELLOW_0:def_2;
hence f . [a,b] <= sup (f .: X) by A10, YELLOW_0:def_2; ::_thesis: verum
end;
theorem :: WAYBEL24:18
for R, S, T being complete LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds
f is directed-sups-preserving
proof
let R, S, T be complete LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds
f is directed-sups-preserving
let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) implies f is directed-sups-preserving )
assume A1: for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ; ::_thesis: f is directed-sups-preserving
for X being Subset of [:R,S:] st not X is empty & X is directed holds
f preserves_sup_of X
proof
let X be Subset of [:R,S:]; ::_thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: f preserves_sup_of X
then reconsider X = X as non empty directed Subset of [:R,S:] ;
for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) by A1, WAYBEL17:3;
then A2: f is monotone by Th12;
f preserves_sup_of X
proof
( proj1 X is directed & not proj1 X is empty & Proj (f,("\/" ((proj2 X),S))) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22;
then A3: Proj (f,("\/" ((proj2 X),S))) preserves_sup_of proj1 X by WAYBEL_0:def_37;
A4: ex_sup_of (Proj (f,(sup (proj2 X)))) .: (proj1 X),T by YELLOW_0:17;
assume A5: ex_sup_of X,[:R,S:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,[:R,S:])) )
then A6: ex_sup_of proj1 X,R by YELLOW_3:41;
A7: ex_sup_of proj2 X,S by A5, YELLOW_3:41;
for b being Element of T st b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) holds
b <= sup (f .: X)
proof
let b be Element of T; ::_thesis: ( b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) implies b <= sup (f .: X) )
assume b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) ; ::_thesis: b <= sup (f .: X)
then consider b1 being set such that
A8: b1 in dom (Proj (f,(sup (proj2 X)))) and
A9: b1 in proj1 X and
A10: b = (Proj (f,(sup (proj2 X)))) . b1 by FUNCT_1:def_6;
reconsider b1 = b1 as Element of R by A8;
A11: (Proj (f,b1)) .: (proj2 X) is_<=_than sup (f .: X)
proof
let k be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not k in (Proj (f,b1)) .: (proj2 X) or k <= sup (f .: X) )
assume k in (Proj (f,b1)) .: (proj2 X) ; ::_thesis: k <= sup (f .: X)
then consider k1 being set such that
A12: k1 in dom (Proj (f,b1)) and
A13: k1 in proj2 X and
A14: k = (Proj (f,b1)) . k1 by FUNCT_1:def_6;
reconsider k1 = k1 as Element of S by A12;
k = f . (b1,k1) by A14, Th7;
hence k <= sup (f .: X) by A2, A9, A13, Th17, YELLOW_0:17; ::_thesis: verum
end;
( not proj2 X is empty & proj2 X is directed & Proj (f,b1) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22;
then A15: Proj (f,b1) preserves_sup_of proj2 X by WAYBEL_0:def_37;
A16: ex_sup_of (Proj (f,b1)) .: (proj2 X),T by YELLOW_0:17;
b = (Proj (f,b1)) . (sup (proj2 X)) by A10, Th9
.= sup ((Proj (f,b1)) .: (proj2 X)) by A7, A15, WAYBEL_0:def_31 ;
hence b <= sup (f .: X) by A16, A11, YELLOW_0:def_9; ::_thesis: verum
end;
then A17: (Proj (f,(sup (proj2 X)))) .: (proj1 X) is_<=_than sup (f .: X) by LATTICE3:def_9;
A18: sup (f .: X) <= f . (sup X) by A2, WAYBEL17:16;
f . (sup X) = f . ((sup (proj1 X)),(sup (proj2 X))) by YELLOW_3:46
.= (Proj (f,(sup (proj2 X)))) . (sup (proj1 X)) by Th8
.= sup ((Proj (f,(sup (proj2 X)))) .: (proj1 X)) by A6, A3, WAYBEL_0:def_31 ;
then f . (sup X) <= sup (f .: X) by A17, A4, YELLOW_0:def_9;
hence ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,[:R,S:])) ) by A18, YELLOW_0:17, YELLOW_0:def_3; ::_thesis: verum
end;
hence f preserves_sup_of X ; ::_thesis: verum
end;
hence f is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum
end;
theorem Th19: :: WAYBEL24:19
for S being set
for T being non empty RelStr
for f being set holds
( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
proof
let S be set ; ::_thesis: for T being non empty RelStr
for f being set holds
( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
let T be non empty RelStr ; ::_thesis: for f being set holds
( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
let f be set ; ::_thesis: ( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
hereby ::_thesis: ( f is Function of S, the carrier of T implies f is Element of (T |^ S) )
assume f is Element of (T |^ S) ; ::_thesis: f is Function of S, the carrier of T
then f in the carrier of (T |^ S) ;
then f in Funcs (S, the carrier of T) by YELLOW_1:28;
then ex a being Function st
( a = f & dom a = S & rng a c= the carrier of T ) by FUNCT_2:def_2;
hence f is Function of S, the carrier of T by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
assume f is Function of S, the carrier of T ; ::_thesis: f is Element of (T |^ S)
then f in Funcs (S, the carrier of T) by FUNCT_2:8;
hence f is Element of (T |^ S) by YELLOW_1:28; ::_thesis: verum
end;
begin
definition
let S be TopStruct ;
let T be non empty TopRelStr ;
func ContMaps (S,T) -> strict RelStr means :Def3: :: WAYBEL24:def 3
( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of it iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) );
existence
ex b1 being strict RelStr st
( b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) )
proof
defpred S1[ set ] means ex f being Function of S,T st
( $1 = f & f is continuous );
consider X being set such that
A1: for a being set holds
( a in X iff ( a in the carrier of (T |^ the carrier of S) & S1[a] ) ) from XBOOLE_0:sch_1();
X c= the carrier of (T |^ the carrier of S)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in the carrier of (T |^ the carrier of S) )
assume a in X ; ::_thesis: a in the carrier of (T |^ the carrier of S)
hence a in the carrier of (T |^ the carrier of S) by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of (T |^ the carrier of S) ;
take SX = subrelstr X; ::_thesis: ( SX is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of SX iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) )
thus SX is full SubRelStr of T |^ the carrier of S ; ::_thesis: for x being set holds
( x in the carrier of SX iff ex f being Function of S,T st
( x = f & f is continuous ) )
let f be set ; ::_thesis: ( f in the carrier of SX iff ex f being Function of S,T st
( f = f & f is continuous ) )
hereby ::_thesis: ( ex f being Function of S,T st
( f = f & f is continuous ) implies f in the carrier of SX )
assume f in the carrier of SX ; ::_thesis: ex f9 being Function of S,T st
( f9 = f & f9 is continuous )
then f in X by YELLOW_0:def_15;
then consider f9 being Function of S,T such that
A2: ( f9 = f & f9 is continuous ) by A1;
take f9 = f9; ::_thesis: ( f9 = f & f9 is continuous )
thus ( f9 = f & f9 is continuous ) by A2; ::_thesis: verum
end;
given f9 being Function of S,T such that A3: f = f9 and
A4: f9 is continuous ; ::_thesis: f in the carrier of SX
f in Funcs ( the carrier of S, the carrier of T) by A3, FUNCT_2:8;
then f in the carrier of (T |^ the carrier of S) by YELLOW_1:28;
then f in X by A1, A3, A4;
hence f in the carrier of SX by YELLOW_0:def_15; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict RelStr st b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) & b2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) holds
b1 = b2
proof
let A1, A2 be strict RelStr ; ::_thesis: ( A1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) & A2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) implies A1 = A2 )
assume that
A5: A1 is full SubRelStr of T |^ the carrier of S and
A6: for x being set holds
( x in the carrier of A1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) and
A7: A2 is full SubRelStr of T |^ the carrier of S and
A8: for x being set holds
( x in the carrier of A2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ; ::_thesis: A1 = A2
the carrier of A1 = the carrier of A2
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of A2 c= the carrier of A1
let x be set ; ::_thesis: ( x in the carrier of A1 implies x in the carrier of A2 )
assume x in the carrier of A1 ; ::_thesis: x in the carrier of A2
then ex f being Function of S,T st
( x = f & f is continuous ) by A6;
hence x in the carrier of A2 by A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A2 or x in the carrier of A1 )
assume x in the carrier of A2 ; ::_thesis: x in the carrier of A1
then ex f being Function of S,T st
( x = f & f is continuous ) by A8;
hence x in the carrier of A1 by A6; ::_thesis: verum
end;
hence A1 = A2 by A5, A7, YELLOW_0:57; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines ContMaps WAYBEL24:def_3_:_
for S being TopStruct
for T being non empty TopRelStr
for b3 being strict RelStr holds
( b3 = ContMaps (S,T) iff ( b3 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b3 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) ) );
registration
let S be non empty TopSpace;
let T be non empty TopSpace-like TopRelStr ;
cluster ContMaps (S,T) -> non empty strict ;
coherence
not ContMaps (S,T) is empty
proof
set f = the continuous Function of S,T;
the continuous Function of S,T in the carrier of (ContMaps (S,T)) by Def3;
hence not ContMaps (S,T) is empty ; ::_thesis: verum
end;
end;
registration
let S be non empty TopSpace;
let T be non empty TopSpace-like TopRelStr ;
cluster ContMaps (S,T) -> constituted-Functions strict ;
coherence
ContMaps (S,T) is constituted-Functions
proof
let a be Element of (ContMaps (S,T)); :: according to MONOID_0:def_1 ::_thesis: a is set
ex a9 being Function of S,T st
( a9 = a & a9 is continuous ) by Def3;
hence a is set ; ::_thesis: verum
end;
end;
theorem Th20: :: WAYBEL24:20
for S being non empty TopSpace
for T being non empty TopSpace-like reflexive TopRelStr
for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
proof
let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like reflexive TopRelStr
for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
let T be non empty TopSpace-like reflexive TopRelStr ; ::_thesis: for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
let x, y be Element of (ContMaps (S,T)); ::_thesis: ( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
A1: ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then reconsider x9 = x, y9 = y as Element of (T |^ the carrier of S) by YELLOW_0:58;
reconsider xa = x9, ya = y9 as Function of S,T by Th19;
hereby ::_thesis: ( ( for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) implies x <= y )
assume A2: x <= y ; ::_thesis: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T
let i be Element of S; ::_thesis: [(x . i),(y . i)] in the InternalRel of T
x9 <= y9 by A1, A2, YELLOW_0:59;
then xa <= ya by WAYBEL10:11;
then ex a, b being Element of T st
( a = xa . i & b = ya . i & a <= b ) by YELLOW_2:def_1;
hence [(x . i),(y . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;
assume A3: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ; ::_thesis: x <= y
now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_S_holds_
ex_a,_b_being_Element_of_T_st_
(_a_=_xa_._j_&_b_=_ya_._j_&_a_<=_b_)
let j be set ; ::_thesis: ( j in the carrier of S implies ex a, b being Element of T st
( a = xa . j & b = ya . j & a <= b ) )
assume j in the carrier of S ; ::_thesis: ex a, b being Element of T st
( a = xa . j & b = ya . j & a <= b )
then reconsider i = j as Element of S ;
reconsider a = xa . i, b = ya . i as Element of T ;
take a = a; ::_thesis: ex b being Element of T st
( a = xa . j & b = ya . j & a <= b )
take b = b; ::_thesis: ( a = xa . j & b = ya . j & a <= b )
thus ( a = xa . j & b = ya . j ) ; ::_thesis: a <= b
[a,b] in the InternalRel of T by A3;
hence a <= b by ORDERS_2:def_5; ::_thesis: verum
end;
then xa <= ya by YELLOW_2:def_1;
then x9 <= y9 by WAYBEL10:11;
hence x <= y by A1, YELLOW_0:60; ::_thesis: verum
end;
theorem Th21: :: WAYBEL24:21
for S being non empty TopSpace
for T being non empty TopSpace-like reflexive TopRelStr
for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
proof
let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like reflexive TopRelStr
for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
let T be non empty TopSpace-like reflexive TopRelStr ; ::_thesis: for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
let x be set ; ::_thesis: ( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
thus ( x is continuous Function of S,T implies x is Element of (ContMaps (S,T)) ) by Def3; ::_thesis: ( x is Element of (ContMaps (S,T)) implies x is continuous Function of S,T )
assume x is Element of (ContMaps (S,T)) ; ::_thesis: x is continuous Function of S,T
then ex f being Function of S,T st
( x = f & f is continuous ) by Def3;
hence x is continuous Function of S,T ; ::_thesis: verum
end;
registration
let S be non empty TopSpace;
let T be non empty TopSpace-like reflexive TopRelStr ;
cluster ContMaps (S,T) -> strict reflexive ;
coherence
ContMaps (S,T) is reflexive
proof
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
CS is reflexive ;
hence ContMaps (S,T) is reflexive ; ::_thesis: verum
end;
end;
registration
let S be non empty TopSpace;
let T be non empty TopSpace-like transitive TopRelStr ;
cluster ContMaps (S,T) -> strict transitive ;
coherence
ContMaps (S,T) is transitive
proof
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
CS is transitive ;
hence ContMaps (S,T) is transitive ; ::_thesis: verum
end;
end;
registration
let S be non empty TopSpace;
let T be non empty TopSpace-like antisymmetric TopRelStr ;
cluster ContMaps (S,T) -> strict antisymmetric ;
coherence
ContMaps (S,T) is antisymmetric
proof
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
CS is antisymmetric ;
hence ContMaps (S,T) is antisymmetric ; ::_thesis: verum
end;
end;
registration
let S be set ;
let T be non empty RelStr ;
clusterT |^ S -> constituted-Functions ;
coherence
T |^ S is constituted-Functions
proof
let a be Element of (T |^ S); :: according to MONOID_0:def_1 ::_thesis: a is set
thus a is set by Th19; ::_thesis: verum
end;
end;
theorem :: WAYBEL24:22
for S being non empty 1-sorted
for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
proof
let S be non empty 1-sorted ; ::_thesis: for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
let T be complete LATTICE; ::_thesis: for f, g, h being Function of S,T
for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
let f, g, h be Function of S,T; ::_thesis: for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
let i be Element of S; ::_thesis: ( h = "\/" ({f,g},(T |^ the carrier of S)) implies h . i = sup {(f . i),(g . i)} )
reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
A1: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:7;
reconsider f9 = f9, g9 = g9 as Element of (product SYT) by YELLOW_1:def_5;
reconsider DU = {f9,g9} as Subset of (product SYT) ;
assume h = "\/" ({f,g},(T |^ the carrier of S)) ; ::_thesis: h . i = sup {(f . i),(g . i)}
then h . i = (sup DU) . i by YELLOW_1:def_5
.= "\/" ((pi ({f,g},i)),(SYT . i)) by A1, WAYBEL_3:32
.= "\/" ((pi ({f,g},i)),T) by FUNCOP_1:7
.= sup {(f . i),(g . i)} by CARD_3:15 ;
hence h . i = sup {(f . i),(g . i)} ; ::_thesis: verum
end;
theorem Th23: :: WAYBEL24:23
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i)) )
assume A1: for i being Element of I holds J . i is complete LATTICE ; ::_thesis: for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
then reconsider L = product J as complete LATTICE by WAYBEL_3:31;
let X be Subset of (product J); ::_thesis: for i being Element of I holds (inf X) . i = inf (pi (X,i))
let i be Element of I; ::_thesis: (inf X) . i = inf (pi (X,i))
A2: L is complete ;
then A3: inf X is_<=_than X by YELLOW_0:33;
A4: (inf X) . i is_<=_than pi (X,i)
proof
let a be Element of (J . i); :: according to LATTICE3:def_8 ::_thesis: ( not a in pi (X,i) or (inf X) . i <= a )
assume a in pi (X,i) ; ::_thesis: (inf X) . i <= a
then consider f being Function such that
A5: f in X and
A6: a = f . i by CARD_3:def_6;
reconsider f = f as Element of (product J) by A5;
inf X <= f by A3, A5, LATTICE3:def_8;
hence (inf X) . i <= a by A6, WAYBEL_3:28; ::_thesis: verum
end;
A7: now__::_thesis:_for_a_being_Element_of_(J_._i)_st_a_is_<=_than_pi_(X,i)_holds_
(inf_X)_._i_>=_a
let a be Element of (J . i); ::_thesis: ( a is_<=_than pi (X,i) implies (inf X) . i >= a )
set f = (inf X) +* (i,a);
A8: dom ((inf X) +* (i,a)) = dom (inf X) by FUNCT_7:30;
A9: dom (inf X) = I by WAYBEL_3:27;
now__::_thesis:_for_j_being_Element_of_I_holds_((inf_X)_+*_(i,a))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: ((inf X) +* (i,a)) . j is Element of (J . j)
( j = i or j <> i ) ;
then ( ((inf X) +* (i,a)) . j = (inf X) . j or ( ((inf X) +* (i,a)) . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32;
hence ((inf X) +* (i,a)) . j is Element of (J . j) ; ::_thesis: verum
end;
then reconsider f = (inf X) +* (i,a) as Element of (product J) by A8, WAYBEL_3:27;
assume A10: a is_<=_than pi (X,i) ; ::_thesis: (inf X) . i >= a
f is_<=_than X
proof
let g be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not g in X or f <= g )
assume g in X ; ::_thesis: f <= g
then A11: ( g >= inf X & g . i in pi (X,i) ) by A2, CARD_3:def_6, YELLOW_2:22;
now__::_thesis:_for_j_being_Element_of_I_holds_f_._j_<=_g_._j
let j be Element of I; ::_thesis: f . j <= g . j
( j = i or j <> i ) ;
then ( f . j = (inf X) . j or ( f . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32;
hence f . j <= g . j by A10, A11, LATTICE3:def_8, WAYBEL_3:28; ::_thesis: verum
end;
hence f <= g by WAYBEL_3:28; ::_thesis: verum
end;
then A12: f <= inf X by A2, YELLOW_0:33;
f . i = a by A9, FUNCT_7:31;
hence (inf X) . i >= a by A12, WAYBEL_3:28; ::_thesis: verum
end;
J . i is complete LATTICE by A1;
hence (inf X) . i = inf (pi (X,i)) by A4, A7, YELLOW_0:33; ::_thesis: verum
end;
theorem :: WAYBEL24:24
for S being non empty 1-sorted
for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
proof
let S be non empty 1-sorted ; ::_thesis: for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let T be complete LATTICE; ::_thesis: for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let f, g, h be Function of S,T; ::_thesis: for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let i be Element of S; ::_thesis: ( h = "/\" ({f,g},(T |^ the carrier of S)) implies h . i = inf {(f . i),(g . i)} )
reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
A1: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:7;
reconsider f9 = f9, g9 = g9 as Element of (product SYT) by YELLOW_1:def_5;
reconsider DU = {f9,g9} as Subset of (product SYT) ;
assume h = "/\" ({f,g},(T |^ the carrier of S)) ; ::_thesis: h . i = inf {(f . i),(g . i)}
then h . i = (inf DU) . i by YELLOW_1:def_5
.= "/\" ((pi ({f,g},i)),(SYT . i)) by A1, Th23
.= "/\" ((pi ({f,g},i)),T) by FUNCOP_1:7
.= inf {(f . i),(g . i)} by CARD_3:15 ;
hence h . i = inf {(f . i),(g . i)} ; ::_thesis: verum
end;
theorem Th25: :: WAYBEL24:25
for S being non empty RelStr
for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
proof
let S be non empty RelStr ; ::_thesis: for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
let T be complete LATTICE; ::_thesis: for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
let F be non empty Subset of (T |^ the carrier of S); ::_thesis: for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
let i be Element of S; ::_thesis: (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
reconsider X = F as Subset of (product SYT) by YELLOW_1:def_5;
A1: pi (X,i) = { (f . i) where f is Element of (T |^ the carrier of S) : f in F }
proof
thus pi (X,i) c= { (f . i) where f is Element of (T |^ the carrier of S) : f in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (X,i) or a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } )
assume a in pi (X,i) ; ::_thesis: a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F }
then ex g being Function st
( g in X & a = g . i ) by CARD_3:def_6;
hence a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ; ::_thesis: verum
end;
thus { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i) ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } or a in pi (X,i) )
assume a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ; ::_thesis: a in pi (X,i)
then ex g being Element of (T |^ the carrier of S) st
( a = g . i & g in F ) ;
hence a in pi (X,i) by CARD_3:def_6; ::_thesis: verum
end;
end;
( T |^ the carrier of S = product SYT & ( for i being Element of S holds SYT . i is complete LATTICE ) ) by FUNCOP_1:7, YELLOW_1:def_5;
then (sup F) . i = "\/" ((pi (X,i)),(SYT . i)) by WAYBEL_3:32
.= "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A1, FUNCOP_1:7 ;
hence (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) ; ::_thesis: verum
end;
theorem Th26: :: WAYBEL24:26
for S, T being complete TopLattice
for F being non empty Subset of (ContMaps (S,T))
for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
proof
let S, T be complete TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
let i be Element of S; ::_thesis: ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then A1: F c= the carrier of (T |^ the carrier of S) by XBOOLE_1:1;
then reconsider X = F as Subset of (product SYT) by YELLOW_1:def_5;
A2: pi (X,i) = { (f . i) where f is Element of (T |^ the carrier of S) : f in F }
proof
thus pi (X,i) c= { (f . i) where f is Element of (T |^ the carrier of S) : f in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (X,i) or a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } )
assume a in pi (X,i) ; ::_thesis: a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F }
then ex g being Function st
( g in X & a = g . i ) by CARD_3:def_6;
hence a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } by A1; ::_thesis: verum
end;
thus { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i) ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } or a in pi (X,i) )
assume a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ; ::_thesis: a in pi (X,i)
then ex g being Element of (T |^ the carrier of S) st
( a = g . i & g in F ) ;
hence a in pi (X,i) by CARD_3:def_6; ::_thesis: verum
end;
end;
( T |^ the carrier of S = product SYT & ( for i being Element of S holds SYT . i is complete LATTICE ) ) by FUNCOP_1:7, YELLOW_1:def_5;
then ("\/" (F,(T |^ the carrier of S))) . i = "\/" ((pi (X,i)),(SYT . i)) by WAYBEL_3:32
.= "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, FUNCOP_1:7 ;
hence ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) ; ::_thesis: verum
end;
theorem Th27: :: WAYBEL24:27
for S being non empty RelStr
for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
proof
let S be non empty RelStr ; ::_thesis: for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
let T be complete LATTICE; ::_thesis: for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
let F be non empty Subset of (T |^ the carrier of S); ::_thesis: for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
let D be non empty Subset of S; ::_thesis: (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
thus (sup F) .: D c= { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= (sup F) .: D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (sup F) .: D or a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } )
assume a in (sup F) .: D ; ::_thesis: a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
then consider x being set such that
x in dom (sup F) and
A1: x in D and
A2: a = (sup F) . x by FUNCT_1:def_6;
reconsider x9 = x as Element of S by A1;
a = "\/" ( { (f . x9) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, Th25;
hence a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } by A1; ::_thesis: verum
end;
thus { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= (sup F) .: D ::_thesis: verum
proof
sup F is Function of S,T by Th6;
then A3: dom (sup F) = the carrier of S by FUNCT_2:def_1;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } or a in (sup F) .: D )
assume a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } ; ::_thesis: a in (sup F) .: D
then consider i1 being Element of S such that
A4: ( a = "\/" ( { (f . i1) where f is Element of (T |^ the carrier of S) : f in F } ,T) & i1 in D ) ;
a = (sup F) . i1 by A4, Th25;
hence a in (sup F) .: D by A4, A3, FUNCT_1:def_6; ::_thesis: verum
end;
end;
theorem Th28: :: WAYBEL24:28
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T))
for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
let D be non empty Subset of S; ::_thesis: ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
thus ("\/" (F,(T |^ the carrier of S))) .: D c= { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= ("\/" (F,(T |^ the carrier of S))) .: D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ("\/" (F,(T |^ the carrier of S))) .: D or a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } )
assume a in ("\/" (F,(T |^ the carrier of S))) .: D ; ::_thesis: a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D }
then consider x being set such that
x in dom ("\/" (F,(T |^ the carrier of S))) and
A1: x in D and
A2: a = ("\/" (F,(T |^ the carrier of S))) . x by FUNCT_1:def_6;
reconsider x9 = x as Element of S by A1;
a = "\/" ( { (f . x9) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, Th26;
hence a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } by A1; ::_thesis: verum
end;
thus { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= ("\/" (F,(T |^ the carrier of S))) .: D ::_thesis: verum
proof
"\/" (F,(T |^ the carrier of S)) is Function of S,T by Th19;
then A3: dom ("\/" (F,(T |^ the carrier of S))) = the carrier of S by FUNCT_2:def_1;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } or a in ("\/" (F,(T |^ the carrier of S))) .: D )
assume a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } ; ::_thesis: a in ("\/" (F,(T |^ the carrier of S))) .: D
then consider i1 being Element of S such that
A4: ( a = "\/" ( { (f . i1) where f is Element of (T |^ the carrier of S) : f in F } ,T) & i1 in D ) ;
a = ("\/" (F,(T |^ the carrier of S))) . i1 by A4, Th26;
hence a in ("\/" (F,(T |^ the carrier of S))) .: D by A4, A3, FUNCT_1:def_6; ::_thesis: verum
end;
end;
scheme :: WAYBEL24:sch 3
FraenkelF9RS{ F1() -> non empty TopRelStr , F2( set ) -> set , F3( set ) -> set , P1[ set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] }
provided
A1: for v being Element of F1() st P1[v] holds
F2(v) = F3(v)
proof
set X = { F2(v1) where v1 is Element of F1() : P1[v1] } ;
set Y = { F3(v2) where v2 is Element of F1() : P1[v2] } ;
A2: { F3(v2) where v2 is Element of F1() : P1[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(v2) where v2 is Element of F1() : P1[v2] } or x in { F2(v1) where v1 is Element of F1() : P1[v1] } )
assume x in { F3(v2) where v2 is Element of F1() : P1[v2] } ; ::_thesis: x in { F2(v1) where v1 is Element of F1() : P1[v1] }
then consider v1 being Element of F1() such that
A3: x = F3(v1) and
A4: P1[v1] ;
x = F2(v1) by A1, A3, A4;
hence x in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; ::_thesis: verum
end;
{ F2(v1) where v1 is Element of F1() : P1[v1] } c= { F3(v2) where v2 is Element of F1() : P1[v2] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F2(v1) where v1 is Element of F1() : P1[v1] } or x in { F3(v2) where v2 is Element of F1() : P1[v2] } )
assume x in { F2(v1) where v1 is Element of F1() : P1[v1] } ; ::_thesis: x in { F3(v2) where v2 is Element of F1() : P1[v2] }
then consider v1 being Element of F1() such that
A5: x = F2(v1) and
A6: P1[v1] ;
x = F3(v1) by A1, A5, A6;
hence x in { F3(v2) where v2 is Element of F1() : P1[v2] } by A6; ::_thesis: verum
end;
hence { F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
scheme :: WAYBEL24:sch 4
FraenkelF9RSS{ F1() -> non empty RelStr , F2( set ) -> set , F3( set ) -> set , P1[ set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] }
provided
A1: for v being Element of F1() st P1[v] holds
F2(v) = F3(v)
proof
set X = { F2(v1) where v1 is Element of F1() : P1[v1] } ;
set Y = { F3(v2) where v2 is Element of F1() : P1[v2] } ;
A2: { F3(v2) where v2 is Element of F1() : P1[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(v2) where v2 is Element of F1() : P1[v2] } or x in { F2(v1) where v1 is Element of F1() : P1[v1] } )
assume x in { F3(v2) where v2 is Element of F1() : P1[v2] } ; ::_thesis: x in { F2(v1) where v1 is Element of F1() : P1[v1] }
then consider v1 being Element of F1() such that
A3: x = F3(v1) and
A4: P1[v1] ;
x = F2(v1) by A1, A3, A4;
hence x in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; ::_thesis: verum
end;
{ F2(v1) where v1 is Element of F1() : P1[v1] } c= { F3(v2) where v2 is Element of F1() : P1[v2] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F2(v1) where v1 is Element of F1() : P1[v1] } or x in { F3(v2) where v2 is Element of F1() : P1[v2] } )
assume x in { F2(v1) where v1 is Element of F1() : P1[v1] } ; ::_thesis: x in { F3(v2) where v2 is Element of F1() : P1[v2] }
then consider v1 being Element of F1() such that
A5: x = F2(v1) and
A6: P1[v1] ;
x = F3(v1) by A1, A5, A6;
hence x in { F3(v2) where v2 is Element of F1() : P1[v2] } by A6; ::_thesis: verum
end;
hence { F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
scheme :: WAYBEL24:sch 5
FuncFraenkelS{ F1() -> non empty TopRelStr , F2() -> non empty TopRelStr , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } :
F4() .: { F3(x) where x is Element of F1() : P1[x] } = { (F4() . F3(x)) where x is Element of F1() : P1[x] }
provided
A1: the carrier of F2() c= dom F4()
proof
set f = F4();
thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } )
assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] }
then consider z being set such that
z in dom F4() and
A2: z in { F3(x) where x is Element of F1() : P1[x] } and
A3: y = F4() . z by FUNCT_1:def_6;
ex x being Element of F1() st
( z = F3(x) & P1[x] ) by A2;
hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } )
assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] }
then consider x being Element of F1() such that
A4: y = F4() . F3(x) and
A5: P1[x] ;
( F3(x) in the carrier of F2() & F3(x) in { F3(z) where z is Element of F1() : P1[z] } ) by A5;
hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A1, A4, FUNCT_1:def_6; ::_thesis: verum
end;
Lm1: for S being non empty RelStr
for D being non empty Subset of S holds D = { i where i is Element of S : i in D }
proof
let S be non empty RelStr ; ::_thesis: for D being non empty Subset of S holds D = { i where i is Element of S : i in D }
let D be non empty Subset of S; ::_thesis: D = { i where i is Element of S : i in D }
thus D c= { i where i is Element of S : i in D } :: according to XBOOLE_0:def_10 ::_thesis: { i where i is Element of S : i in D } c= D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in { i where i is Element of S : i in D } )
assume a in D ; ::_thesis: a in { i where i is Element of S : i in D }
hence a in { i where i is Element of S : i in D } ; ::_thesis: verum
end;
thus { i where i is Element of S : i in D } c= D ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of S : i in D } or a in D )
assume a in { i where i is Element of S : i in D } ; ::_thesis: a in D
then ex j being Element of S st
( j = a & j in D ) ;
hence a in D ; ::_thesis: verum
end;
end;
theorem Th29: :: WAYBEL24:29
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T
ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then reconsider F9 = F as Subset of (T |^ the carrier of S) by XBOOLE_1:1;
reconsider sF = sup F9 as Function of S,T by Th6;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
sF_._x_<=_sF_._y
let x, y be Element of S; ::_thesis: ( x <= y implies sF . x <= sF . y )
set G1 = { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ;
assume A1: x <= y ; ::_thesis: sF . x <= sF . y
A2: { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } is_<=_than sF . y
proof
let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } or a <= sF . y )
assume a in { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ; ::_thesis: a <= sF . y
then consider f9 being Element of (T |^ the carrier of S) such that
A3: a = f9 . x and
A4: f9 in F9 ;
reconsider f1 = f9 as continuous Function of S,T by A4, Th21;
reconsider f1 = f1 as monotone Function of S,T ;
f9 <= sup F9 by A4, YELLOW_2:22;
then f1 <= sF by WAYBEL10:11;
then A5: f1 . y <= sF . y by YELLOW_2:9;
f1 . x <= f1 . y by A1, WAYBEL_1:def_2;
hence a <= sF . y by A3, A5, YELLOW_0:def_2; ::_thesis: verum
end;
sF . x = "\/" ( { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ,T) by Th25;
hence sF . x <= sF . y by A2, YELLOW_0:32; ::_thesis: verum
end;
hence "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T by WAYBEL_1:def_2; ::_thesis: verum
end;
theorem Th30: :: WAYBEL24:30
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T)
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T)
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T)
let D be non empty directed Subset of S; ::_thesis: "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T)
reconsider sF = "\/" (F,(T |^ the carrier of S)) as Function of S,T by Th19;
set F9 = F;
set L = "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T);
set P = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T);
set L1 = { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ;
set P1 = { ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } ;
reconsider L = "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T), P = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) as Element of T ;
defpred S1[ set ] means $1 in F;
deffunc H1( Element of S) -> Element of S = $1;
defpred S2[ set ] means $1 in D;
deffunc H2( Element of (T |^ the carrier of S)) -> Element of the carrier of T = "\/" ( { ($1 . i4) where i4 is Element of S : i4 in D } ,T);
deffunc H3( Element of (T |^ the carrier of S)) -> set = $1 . (sup D);
A1: P = sup (sF .: D) by Th28;
{ ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } is_<=_than P
proof
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } or b <= P )
assume b in { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ; ::_thesis: b <= P
then consider g9 being Element of (T |^ the carrier of S) such that
A2: b = "\/" ( { (g9 . i) where i is Element of S : i in D } ,T) and
A3: g9 in F ;
reconsider g1 = g9 as continuous Function of S,T by A3, Th21;
g9 <= "\/" (F,(T |^ the carrier of S)) by A3, YELLOW_2:22;
then A4: g1 <= sF by WAYBEL10:11;
A5: g1 .: D is_<=_than sup (sF .: D)
proof
let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in g1 .: D or a <= sup (sF .: D) )
assume a in g1 .: D ; ::_thesis: a <= sup (sF .: D)
then consider x being set such that
A6: x in dom g1 and
A7: x in D and
A8: a = g1 . x by FUNCT_1:def_6;
reconsider x9 = x as Element of S by A6;
x in the carrier of S by A6;
then x9 in dom sF by FUNCT_2:def_1;
then sF . x9 in sF .: D by A7, FUNCT_1:def_6;
then A9: sF . x9 <= sup (sF .: D) by YELLOW_2:22;
g1 . x9 <= sF . x9 by A4, YELLOW_2:9;
hence a <= sup (sF .: D) by A8, A9, YELLOW_0:def_2; ::_thesis: verum
end;
the carrier of S c= dom g1 by FUNCT_2:def_1;
then A10: the carrier of S c= dom g9 ;
g9 .: { H1(i2) where i2 is Element of S : S2[i2] } = { (g9 . H1(i)) where i is Element of S : S2[i] } from WAYBEL24:sch_5(A10);
then b = "\/" ((g9 .: D),T) by A2, Lm1;
hence b <= P by A1, A5, YELLOW_0:32; ::_thesis: verum
end;
then A11: L <= P by YELLOW_0:32;
A12: for g8 being Element of (T |^ the carrier of S) st S1[g8] holds
H2(g8) = H3(g8)
proof
let g1 be Element of (T |^ the carrier of S); ::_thesis: ( S1[g1] implies H2(g1) = H3(g1) )
assume g1 in F ; ::_thesis: H2(g1) = H3(g1)
then reconsider g9 = g1 as continuous Function of S,T by Th21;
A13: ( g9 preserves_sup_of D & ex_sup_of D,S ) by WAYBEL_0:def_37, YELLOW_0:17;
the carrier of S c= dom g9 by FUNCT_2:def_1;
then A14: the carrier of S c= dom g1 ;
g1 .: { H1(i2) where i2 is Element of S : S2[i2] } = { (g1 . H1(i)) where i is Element of S : S2[i] } from WAYBEL24:sch_5(A14);
then "\/" ( { (g1 . i) where i is Element of S : i in D } ,T) = sup (g9 .: D) by Lm1
.= g1 . (sup D) by A13, WAYBEL_0:def_31 ;
hence H2(g1) = H3(g1) ; ::_thesis: verum
end;
{ H2(g3) where g3 is Element of (T |^ the carrier of S) : S1[g3] } = { H3(g4) where g4 is Element of (T |^ the carrier of S) : S1[g4] } from WAYBEL24:sch_4(A12);
then A15: L = sF . (sup D) by Th26;
{ ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } is_<=_than L
proof
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in { ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } or b <= L )
assume b in { ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } ; ::_thesis: b <= L
then consider i9 being Element of S such that
A16: b = "\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T) and
A17: i9 in D ;
i9 in the carrier of S ;
then A18: i9 in dom sF by FUNCT_2:def_1;
b = sF . i9 by A16, Th26;
then b in sF .: D by A17, A18, FUNCT_1:def_6;
then A19: b <= sup (sF .: D) by YELLOW_2:22;
sF is monotone by Th29;
then sup (sF .: D) <= L by A15, WAYBEL17:15;
hence b <= L by A19, YELLOW_0:def_2; ::_thesis: verum
end;
then P <= L by YELLOW_0:32;
hence "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) by A11, YELLOW_0:def_3; ::_thesis: verum
end;
theorem Th31: :: WAYBEL24:31
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
let D be non empty directed Subset of S; ::_thesis: "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then reconsider F9 = F as non empty Subset of (T |^ the carrier of S) by XBOOLE_1:1;
reconsider sF = sup F9 as Function of S,T by Th19;
set L = "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T);
set P = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T);
deffunc H1( Element of (T |^ the carrier of S)) -> Element of the carrier of T = "\/" ( { ($1 . i4) where i4 is Element of S : i4 in D } ,T);
deffunc H2( Element of (T |^ the carrier of S)) -> set = $1 . (sup D);
defpred S1[ set ] means $1 in F9;
A1: for g8 being Element of (T |^ the carrier of S) st S1[g8] holds
H1(g8) = H2(g8)
proof
deffunc H3( Element of S) -> Element of S = $1;
let g1 be Element of (T |^ the carrier of S); ::_thesis: ( S1[g1] implies H1(g1) = H2(g1) )
assume g1 in F9 ; ::_thesis: H1(g1) = H2(g1)
then reconsider g9 = g1 as continuous Function of S,T by Th21;
defpred S2[ set ] means $1 in D;
A2: ( g9 preserves_sup_of D & ex_sup_of D,S ) by WAYBEL_0:def_37, YELLOW_0:17;
the carrier of S c= dom g9 by FUNCT_2:def_1;
then A3: the carrier of S c= dom g1 ;
g1 .: { H3(i2) where i2 is Element of S : S2[i2] } = { (g1 . H3(i)) where i is Element of S : S2[i] } from WAYBEL24:sch_5(A3);
then "\/" ( { (g1 . i) where i is Element of S : i in D } ,T) = sup (g9 .: D) by Lm1
.= g1 . (sup D) by A2, WAYBEL_0:def_31 ;
hence H1(g1) = H2(g1) ; ::_thesis: verum
end;
{ H1(g3) where g3 is Element of (T |^ the carrier of S) : S1[g3] } = { H2(g4) where g4 is Element of (T |^ the carrier of S) : S1[g4] } from WAYBEL24:sch_4(A1);
then A4: "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = sF . (sup D) by Th25;
"\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) = sup (sF .: D) by Th27;
hence "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D) by A4, Th30; ::_thesis: verum
end;
theorem Th32: :: WAYBEL24:32
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))
reconsider Ex = "\/" (F,(T |^ the carrier of S)) as Function of S,T by Th19;
for X being Subset of S st not X is empty & X is directed holds
Ex preserves_sup_of X
proof
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies Ex preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: Ex preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of S ;
Ex preserves_sup_of X9
proof
assume ex_sup_of X9,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of Ex .: X9,T & "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) )
thus ex_sup_of Ex .: X9,T by YELLOW_0:17; ::_thesis: "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S))
thus "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) by Th31; ::_thesis: verum
end;
hence Ex preserves_sup_of X ; ::_thesis: verum
end;
then Ex is directed-sups-preserving by WAYBEL_0:def_37;
hence "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) by Def3; ::_thesis: verum
end;
theorem Th33: :: WAYBEL24:33
for S being non empty RelStr
for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)
let T be non empty antisymmetric lower-bounded RelStr ; ::_thesis: Bottom (T |^ the carrier of S) = S --> (Bottom T)
set L = T |^ the carrier of S;
reconsider f = S --> (Bottom T) as Element of (T |^ the carrier of S) by Th19;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (T |^ the carrier of S) st b is_>=_than {} holds
f <= b
proof
let b be Element of (T |^ the carrier of S); ::_thesis: ( b is_>=_than {} implies f <= b )
reconsider b9 = b as Function of S,T by Th19;
assume b is_>=_than {} ; ::_thesis: f <= b
for x being Element of S holds f9 . x <= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x <= b9 . x
f9 . x = ( the carrier of S --> (Bottom T)) . x
.= Bottom T by FUNCOP_1:7 ;
hence f9 . x <= b9 . x by YELLOW_0:44; ::_thesis: verum
end;
then f9 <= b9 by YELLOW_2:9;
hence f <= b by WAYBEL10:11; ::_thesis: verum
end;
f is_>=_than {} by YELLOW_0:6;
then f = "\/" ({},(T |^ the carrier of S)) by A1, YELLOW_0:30;
hence Bottom (T |^ the carrier of S) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum
end;
theorem :: WAYBEL24:34
for S being non empty RelStr
for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T)
let T be non empty antisymmetric upper-bounded RelStr ; ::_thesis: Top (T |^ the carrier of S) = S --> (Top T)
set L = T |^ the carrier of S;
reconsider f = S --> (Top T) as Element of (T |^ the carrier of S) by Th19;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (T |^ the carrier of S) st b is_<=_than {} holds
f >= b
proof
let b be Element of (T |^ the carrier of S); ::_thesis: ( b is_<=_than {} implies f >= b )
reconsider b9 = b as Function of S,T by Th19;
assume b is_<=_than {} ; ::_thesis: f >= b
for x being Element of S holds f9 . x >= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x >= b9 . x
f9 . x = ( the carrier of S --> (Top T)) . x
.= Top T by FUNCOP_1:7 ;
hence f9 . x >= b9 . x by YELLOW_0:45; ::_thesis: verum
end;
then f9 >= b9 by YELLOW_2:9;
hence f >= b by WAYBEL10:11; ::_thesis: verum
end;
f is_<=_than {} by YELLOW_0:6;
then f = "/\" ({},(T |^ the carrier of S)) by A1, YELLOW_0:31;
hence Top (T |^ the carrier of S) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum
end;
registration
let S be non empty reflexive RelStr ;
let T be complete LATTICE;
let a be Element of T;
clusterS --> a -> directed-sups-preserving ;
coherence
S --> a is directed-sups-preserving
proof
set f = S --> a;
for X being Subset of S st not X is empty & X is directed holds
S --> a preserves_sup_of X
proof
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies S --> a preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: S --> a preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of S ;
S --> a preserves_sup_of X
proof
assume ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (S --> a) .: X,T & "\/" (((S --> a) .: X),T) = (S --> a) . ("\/" (X,S)) )
thus ex_sup_of (S --> a) .: X,T by YELLOW_0:17; ::_thesis: "\/" (((S --> a) .: X),T) = (S --> a) . ("\/" (X,S))
A1: {a} c= (S --> a) .: X
proof
set n = the Element of X9;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in {a} or b in (S --> a) .: X )
A2: a = ( the carrier of S --> a) . the Element of X9 by FUNCOP_1:7
.= (S --> a) . the Element of X9 ;
assume b in {a} ; ::_thesis: b in (S --> a) .: X
then A3: b = a by TARSKI:def_1;
dom (S --> a) = the carrier of S by FUNCOP_1:13;
hence b in (S --> a) .: X by A3, A2, FUNCT_1:def_6; ::_thesis: verum
end;
(S --> a) .: X c= rng (S --> a) by RELAT_1:111;
then (S --> a) .: X c= {a} by FUNCOP_1:8;
hence sup ((S --> a) .: X) = sup {a} by A1, XBOOLE_0:def_10
.= a by YELLOW_0:39
.= ( the carrier of S --> a) . (sup X) by FUNCOP_1:7
.= (S --> a) . (sup X) ;
::_thesis: verum
end;
hence S --> a preserves_sup_of X ; ::_thesis: verum
end;
hence S --> a is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum
end;
end;
theorem Th35: :: WAYBEL24:35
for S, T being complete Scott TopLattice holds ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S
proof
let S, T be complete Scott TopLattice; ::_thesis: ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S
set L = T |^ the carrier of S;
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
now__::_thesis:_for_X_being_Subset_of_CS_st_ex_sup_of_X,T_|^_the_carrier_of_S_holds_
"\/"_(X,(T_|^_the_carrier_of_S))_in_the_carrier_of_CS
let X be Subset of CS; ::_thesis: ( ex_sup_of X,T |^ the carrier of S implies "\/" (b1,(T |^ the carrier of S)) in the carrier of CS )
assume ex_sup_of X,T |^ the carrier of S ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
percases ( not X is empty or X is empty ) ;
suppose not X is empty ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
hence "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Th32; ::_thesis: verum
end;
suppose X is empty ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
then "\/" (X,(T |^ the carrier of S)) = Bottom (T |^ the carrier of S) by YELLOW_0:def_11;
then "\/" (X,(T |^ the carrier of S)) = S --> (Bottom T) by Th33;
hence "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Def3; ::_thesis: verum
end;
end;
end;
hence ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S by YELLOW_0:def_19; ::_thesis: verum
end;
registration
let S, T be complete Scott TopLattice;
cluster ContMaps (S,T) -> strict complete ;
coherence
ContMaps (S,T) is complete
proof
ContMaps (S,T) is non empty full sups-inheriting SubRelStr of T |^ the carrier of S by Def3, Th35;
hence ContMaps (S,T) is complete by YELLOW_2:31; ::_thesis: verum
end;
end;
theorem :: WAYBEL24:36
for S, T being non empty complete Scott TopLattice holds Bottom (ContMaps (S,T)) = S --> (Bottom T)
proof
let S, T be non empty complete Scott TopLattice; ::_thesis: Bottom (ContMaps (S,T)) = S --> (Bottom T)
set L = ContMaps (S,T);
reconsider f = S --> (Bottom T) as Element of (ContMaps (S,T)) by Th21;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (ContMaps (S,T)) st b is_>=_than {} holds
f <= b
proof
let b be Element of (ContMaps (S,T)); ::_thesis: ( b is_>=_than {} implies f <= b )
reconsider b9 = b as Function of S,T by Th21;
assume b is_>=_than {} ; ::_thesis: f <= b
for i being Element of S holds [(f . i),(b . i)] in the InternalRel of T
proof
let i be Element of S; ::_thesis: [(f . i),(b . i)] in the InternalRel of T
f . i = ( the carrier of S --> (Bottom T)) . i
.= Bottom T by FUNCOP_1:7 ;
then f9 . i <= b9 . i by YELLOW_0:44;
hence [(f . i),(b . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;
hence f <= b by Th20; ::_thesis: verum
end;
f is_>=_than {} by YELLOW_0:6;
then f = "\/" ({},(ContMaps (S,T))) by A1, YELLOW_0:30;
hence Bottom (ContMaps (S,T)) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum
end;
theorem :: WAYBEL24:37
for S, T being non empty complete Scott TopLattice holds Top (ContMaps (S,T)) = S --> (Top T)
proof
let S, T be non empty complete Scott TopLattice; ::_thesis: Top (ContMaps (S,T)) = S --> (Top T)
set L = ContMaps (S,T);
reconsider f = S --> (Top T) as Element of (ContMaps (S,T)) by Th21;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (ContMaps (S,T)) st b is_<=_than {} holds
f >= b
proof
let b be Element of (ContMaps (S,T)); ::_thesis: ( b is_<=_than {} implies f >= b )
reconsider b9 = b as Function of S,T by Th21;
assume b is_<=_than {} ; ::_thesis: f >= b
for i being Element of S holds [(b . i),(f . i)] in the InternalRel of T
proof
let i be Element of S; ::_thesis: [(b . i),(f . i)] in the InternalRel of T
f . i = ( the carrier of S --> (Top T)) . i
.= Top T by FUNCOP_1:7 ;
then f9 . i >= b9 . i by YELLOW_0:45;
hence [(b . i),(f . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;
hence f >= b by Th20; ::_thesis: verum
end;
f is_<=_than {} by YELLOW_0:6;
then f = "/\" ({},(ContMaps (S,T))) by A1, YELLOW_0:31;
hence Top (ContMaps (S,T)) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum
end;
theorem :: WAYBEL24:38
for S, T being complete Scott TopLattice holds SCMaps (S,T) = ContMaps (S,T)
proof
let S, T be complete Scott TopLattice; ::_thesis: SCMaps (S,T) = ContMaps (S,T)
reconsider Sm = ContMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by Def3;
reconsider SC = SCMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by WAYBEL15:1;
A1: the carrier of SC c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13;
A2: the carrier of SC c= the carrier of Sm
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of SC or a in the carrier of Sm )
assume A3: a in the carrier of SC ; ::_thesis: a in the carrier of Sm
then reconsider f = a as Function of S,T by A1, WAYBEL10:9;
f is continuous Function of S,T by A3, WAYBEL17:def_2;
then a is Element of Sm by Th21;
hence a in the carrier of Sm ; ::_thesis: verum
end;
the carrier of Sm c= the carrier of SC
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of Sm or a in the carrier of SC )
assume a in the carrier of Sm ; ::_thesis: a in the carrier of SC
then a is continuous Function of S,T by Th21;
hence a in the carrier of SC by WAYBEL17:def_2; ::_thesis: verum
end;
then the carrier of SC = the carrier of Sm by A2, XBOOLE_0:def_10;
hence SCMaps (S,T) = ContMaps (S,T) by YELLOW_0:57; ::_thesis: verum
end;