:: WAYBEL17 semantic presentation
begin
definition
let S be non empty set ;
let a, b be Element of S;
func(a,b) ,... -> Function of NAT,S means :Def1: :: WAYBEL17:def 1
for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies it . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies it . i = b ) );
existence
ex b1 being Function of NAT,S st
for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b1 . i = b ) )
proof
defpred S1[ set ] means ex k being Element of NAT st $1 = 2 * k;
deffunc H1( set ) -> Element of S = b;
deffunc H2( set ) -> Element of S = a;
consider f being Function such that
A1: ( dom f = NAT & ( for x being set st x in NAT holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) ) ) from PARTFUN1:sch_1();
A2: rng f c= {a,b}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in {a,b} )
assume x in rng f ; ::_thesis: x in {a,b}
then consider y being set such that
A3: y in dom f and
A4: x = f . y by FUNCT_1:def_3;
percases ( S1[y] or not S1[y] ) ;
suppose S1[y] ; ::_thesis: x in {a,b}
then f . y = a by A1;
hence x in {a,b} by A4, TARSKI:def_2; ::_thesis: verum
end;
suppose not S1[y] ; ::_thesis: x in {a,b}
then f . y = b by A1, A3;
hence x in {a,b} by A4, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
for y being set st y in {a,b} holds
ex x being set st
( x in dom f & y = f . x )
proof
let y be set ; ::_thesis: ( y in {a,b} implies ex x being set st
( x in dom f & y = f . x ) )
assume A5: y in {a,b} ; ::_thesis: ex x being set st
( x in dom f & y = f . x )
percases ( y = a or y = b ) by A5, TARSKI:def_2;
supposeA6: y = a ; ::_thesis: ex x being set st
( x in dom f & y = f . x )
take 2 ; ::_thesis: ( 2 in dom f & y = f . 2 )
S1[2]
proof
take 1 ; ::_thesis: 2 = 2 * 1
thus 2 = 2 * 1 ; ::_thesis: verum
end;
hence ( 2 in dom f & y = f . 2 ) by A1, A6; ::_thesis: verum
end;
supposeA7: y = b ; ::_thesis: ex x being set st
( x in dom f & y = f . x )
take 1 ; ::_thesis: ( 1 in dom f & y = f . 1 )
for k being Element of NAT holds 1 <> 2 * k by NAT_1:15;
hence ( 1 in dom f & y = f . 1 ) by A1, A7; ::_thesis: verum
end;
end;
end;
then {a,b} c= rng f by FUNCT_1:9;
then rng f = {a,b} by A2, XBOOLE_0:def_10;
then reconsider f = f as Function of NAT,S by A1, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) )
let i be Element of NAT ; ::_thesis: ( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) )
thus ( ( ex k being Element of NAT st i = 2 * k implies f . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f . i = b ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of NAT,S st ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b1 . i = b ) ) ) & ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b2 . i = b ) ) ) holds
b1 = b2
proof
let f1, f2 be Function of NAT,S; ::_thesis: ( ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f1 . i = b ) ) ) & ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f2 . i = b ) ) ) implies f1 = f2 )
A8: dom f1 = NAT by FUNCT_2:def_1;
A9: dom f2 = NAT by FUNCT_2:def_1;
assume that
A10: for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f1 . i = b ) ) and
A11: for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f2 . i = b ) ) ; ::_thesis: f1 = f2
for k being set st k in NAT holds
f1 . k = f2 . k
proof
let k be set ; ::_thesis: ( k in NAT implies f1 . k = f2 . k )
assume k in NAT ; ::_thesis: f1 . k = f2 . k
then reconsider k9 = k as Element of NAT ;
percases ( ex l being Element of NAT st k = 2 * l or for l being Element of NAT holds not k = 2 * l ) ;
supposeA12: ex l being Element of NAT st k = 2 * l ; ::_thesis: f1 . k = f2 . k
then f1 . k = a by A10
.= f2 . k by A11, A12 ;
hence f1 . k = f2 . k ; ::_thesis: verum
end;
supposeA13: for l being Element of NAT holds not k = 2 * l ; ::_thesis: f1 . k = f2 . k
then f1 . k9 = b by A10
.= f2 . k9 by A11, A13 ;
hence f1 . k = f2 . k ; ::_thesis: verum
end;
end;
end;
hence f1 = f2 by A8, A9, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines ,... WAYBEL17:def_1_:_
for S being non empty set
for a, b being Element of S
for b4 being Function of NAT,S holds
( b4 = (a,b) ,... iff for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies b4 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies b4 . i = b ) ) );
scheme :: WAYBEL17:sch 1
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] ;
A6: 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, A6, FUNCT_1:def_6; ::_thesis: verum
end;
scheme :: WAYBEL17:sch 2
FuncFraenkelSL{ F1() -> LATTICE, F2() -> LATTICE, 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] ;
A6: 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, A6, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th1: :: WAYBEL17:1
for S, T being non empty reflexive RelStr
for f being Function of S,T
for P being lower Subset of T st f is monotone holds
f " P is lower
proof
let S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of S,T
for P being lower Subset of T st f is monotone holds
f " P is lower
let f be Function of S,T; ::_thesis: for P being lower Subset of T st f is monotone holds
f " P is lower
let P be lower Subset of T; ::_thesis: ( f is monotone implies f " P is lower )
assume A1: f is monotone ; ::_thesis: f " P is lower
for x, y being Element of S st x in f " P & y <= x holds
y in f " P
proof
let x, y be Element of S; ::_thesis: ( x in f " P & y <= x implies y in f " P )
assume that
A2: x in f " P and
A3: y <= x ; ::_thesis: y in f " P
A4: f . y <= f . x by A1, A3, WAYBEL_1:def_2;
reconsider fy = f . y, fx = f . x as Element of T ;
fx in P by A2, FUNCT_2:38;
then fy in P by A4, WAYBEL_0:def_19;
hence y in f " P by FUNCT_2:38; ::_thesis: verum
end;
hence f " P is lower by WAYBEL_0:def_19; ::_thesis: verum
end;
theorem :: WAYBEL17:2
for S, T being non empty reflexive RelStr
for f being Function of S,T
for P being upper Subset of T st f is monotone holds
f " P is upper
proof
let S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of S,T
for P being upper Subset of T st f is monotone holds
f " P is upper
let f be Function of S,T; ::_thesis: for P being upper Subset of T st f is monotone holds
f " P is upper
let P be upper Subset of T; ::_thesis: ( f is monotone implies f " P is upper )
assume A1: f is monotone ; ::_thesis: f " P is upper
for x, y being Element of S st x in f " P & y >= x holds
y in f " P
proof
let x, y be Element of S; ::_thesis: ( x in f " P & y >= x implies y in f " P )
assume that
A2: x in f " P and
A3: y >= x ; ::_thesis: y in f " P
A4: f . y >= f . x by A1, A3, WAYBEL_1:def_2;
reconsider fy = f . y, fx = f . x as Element of T ;
fx in P by A2, FUNCT_2:38;
then fy in P by A4, WAYBEL_0:def_20;
hence y in f " P by FUNCT_2:38; ::_thesis: verum
end;
hence f " P is upper by WAYBEL_0:def_20; ::_thesis: verum
end;
Lm1: for T being up-complete LATTICE
for x being Element of T holds downarrow x is directly_closed
proof
let T be up-complete LATTICE; ::_thesis: for x being Element of T holds downarrow x is directly_closed
let x be Element of T; ::_thesis: downarrow x is directly_closed
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( not D c= downarrow x or "\/" (D,T) in downarrow x )
assume A1: D c= downarrow x ; ::_thesis: "\/" (D,T) in downarrow x
A2: ex_sup_of D,T by WAYBEL_0:75;
x is_>=_than D
proof
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in D or b <= x )
assume b in D ; ::_thesis: b <= x
hence b <= x by A1, WAYBEL_0:17; ::_thesis: verum
end;
then sup D <= x by A2, YELLOW_0:30;
hence "\/" (D,T) in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
Lm2: for T being up-complete Scott TopLattice
for x being Element of T holds Cl {x} = downarrow x
proof
let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T holds Cl {x} = downarrow x
let x be Element of T; ::_thesis: Cl {x} = downarrow x
downarrow x is directly_closed by Lm1;
then A1: downarrow x is closed by WAYBEL11:7;
x <= x ;
then x in downarrow x by WAYBEL_0:17;
then A2: {x} c= downarrow x by ZFMISC_1:31;
now__::_thesis:_for_C_being_Subset_of_T_st_{x}_c=_C_&_C_is_closed_holds_
downarrow_x_c=_C
let C be Subset of T; ::_thesis: ( {x} c= C & C is closed implies downarrow x c= C )
assume A3: {x} c= C ; ::_thesis: ( C is closed implies downarrow x c= C )
reconsider D = C as Subset of T ;
assume C is closed ; ::_thesis: downarrow x c= C
then A4: D is lower by WAYBEL11:7;
x in C by A3, ZFMISC_1:31;
hence downarrow x c= C by A4, WAYBEL11:6; ::_thesis: verum
end;
hence Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum
end;
Lm3: for T being up-complete Scott TopLattice
for x being Element of T holds downarrow x is closed
proof
let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T holds downarrow x is closed
let x be Element of T; ::_thesis: downarrow x is closed
Cl {x} = downarrow x by Lm2;
hence downarrow x is closed ; ::_thesis: verum
end;
theorem Th3: :: WAYBEL17:3
for S, T being non empty reflexive antisymmetric RelStr
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
proof
let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies f is monotone )
assume A1: f is directed-sups-preserving ; ::_thesis: f is monotone
let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y )
assume A2: x <= y ; ::_thesis: f . x <= f . y
y <= y ;
then A3: {x,y} is_<=_than y by A2, YELLOW_0:8;
A4: for b being Element of S st {x,y} is_<=_than b holds
y <= b by YELLOW_0:8;
then A5: y = sup {x,y} by A3, YELLOW_0:30;
A6: ex_sup_of {x,y},S by A3, A4, YELLOW_0:30;
for a, b being Element of S st a in {x,y} & b in {x,y} holds
ex z being Element of S st
( z in {x,y} & a <= z & b <= z )
proof
let a, b be Element of S; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of S st
( z in {x,y} & a <= z & b <= z ) )
assume that
A7: a in {x,y} and
A8: b in {x,y} ; ::_thesis: ex z being Element of S st
( z in {x,y} & a <= z & b <= z )
take y ; ::_thesis: ( y in {x,y} & a <= y & b <= y )
thus y in {x,y} by TARSKI:def_2; ::_thesis: ( a <= y & b <= y )
thus ( a <= y & b <= y ) by A2, A7, A8, TARSKI:def_2; ::_thesis: verum
end;
then ( {x,y} is directed & not {x,y} is empty ) by WAYBEL_0:def_1;
then A9: f preserves_sup_of {x,y} by A1, WAYBEL_0:def_37;
then A10: sup (f .: {x,y}) = f . y by A5, A6, WAYBEL_0:def_31;
A11: dom f = the carrier of S by FUNCT_2:def_1;
then A12: f . y = sup {(f . x),(f . y)} by A10, FUNCT_1:60;
f .: {x,y} = {(f . x),(f . y)} by A11, FUNCT_1:60;
then ex_sup_of {(f . x),(f . y)},T by A6, A9, WAYBEL_0:def_31;
then {(f . x),(f . y)} is_<=_than f . y by A12, YELLOW_0:def_9;
hence f . x <= f . y by YELLOW_0:8; ::_thesis: verum
end;
registration
let S, T be non empty reflexive antisymmetric RelStr ;
cluster Function-like quasi_total directed-sups-preserving -> monotone for Element of K32(K33( the carrier of S, the carrier of T));
coherence
for b1 being Function of S,T st b1 is directed-sups-preserving holds
b1 is monotone by Th3;
end;
theorem Th4: :: WAYBEL17:4
for S, T being up-complete Scott TopLattice
for f being Function of S,T st f is continuous holds
f is monotone
proof
let S, T be up-complete Scott TopLattice; ::_thesis: for f being Function of S,T st f is continuous holds
f is monotone
let f be Function of S,T; ::_thesis: ( f is continuous implies f is monotone )
assume A1: f is continuous ; ::_thesis: f is monotone
let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y )
A2: dom f = the carrier of S by FUNCT_2:def_1;
assume A3: x <= y ; ::_thesis: f . x <= f . y
A4: [#] T <> {} ;
f . x <= f . y
proof
set V = (downarrow (f . y)) ` ;
set U1 = f " ((downarrow (f . y)) `);
assume not f . x <= f . y ; ::_thesis: contradiction
then not f . x in downarrow (f . y) by WAYBEL_0:17;
then A5: f . x in (downarrow (f . y)) ` by XBOOLE_0:def_5;
f . y <= f . y ;
then A6: f . y in downarrow (f . y) by WAYBEL_0:17;
downarrow (f . y) is closed by Lm3;
then f " ((downarrow (f . y)) `) is open by A1, A4, TOPS_2:43;
then reconsider U1 = f " ((downarrow (f . y)) `) as upper Subset of S by WAYBEL11:def_4;
x in U1 by A2, A5, FUNCT_1:def_7;
then y in U1 by A3, WAYBEL_0:def_20;
then f . y in (downarrow (f . y)) ` by FUNCT_1:def_7;
hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
hence f . x <= f . y ; ::_thesis: verum
end;
registration
let S, T be up-complete Scott TopLattice;
cluster Function-like quasi_total continuous -> monotone for Element of K32(K33( the carrier of S, the carrier of T));
correctness
coherence
for b1 being Function of S,T st b1 is continuous holds
b1 is monotone ;
by Th4;
end;
Lm4: for S, T being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
for f being Function of S,T st f is directed-sups-preserving holds
f is continuous
proof
let S, T be non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for f being Function of S,T st f is directed-sups-preserving holds
f is continuous
let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies f is continuous )
assume A1: f is directed-sups-preserving ; ::_thesis: f is continuous
thus f is continuous ::_thesis: verum
proof
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed )
reconsider P19 = P1 as Subset of T ;
assume P1 is closed ; ::_thesis: f " P1 is closed
then A2: ( P19 is directly_closed & P19 is lower ) by WAYBEL11:7;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_S_st_D_c=_f_"_P1_holds_
sup_D_in_f_"_P1
let D be non empty directed Subset of S; ::_thesis: ( D c= f " P1 implies sup D in f " P1 )
assume A3: D c= f " P1 ; ::_thesis: sup D in f " P1
A4: f preserves_sup_of D by A1, WAYBEL_0:def_37;
ex_sup_of D,S by WAYBEL_0:75;
then A5: sup (f .: D) = f . (sup D) by A4, WAYBEL_0:def_31;
reconsider fD = f .: D as directed Subset of T by A1, YELLOW_2:15;
fD c= P1 by A3, EQREL_1:46;
then sup fD in P19 by A2, WAYBEL11:def_2;
hence sup D in f " P1 by A5, FUNCT_2:38; ::_thesis: verum
end;
then ( f " P1 is directly_closed & f " P1 is lower ) by A1, A2, Th1, WAYBEL11:def_2;
hence f " P1 is closed by WAYBEL11:7; ::_thesis: verum
end;
end;
begin
registration
let S be set ;
let T be reflexive RelStr ;
clusterS --> T -> reflexive-yielding ;
coherence
S --> T is reflexive-yielding
proof
set f = S --> T;
let W be RelStr ; :: according to WAYBEL_3:def_8 ::_thesis: ( not W in rng (S --> T) or W is reflexive )
assume W in rng (S --> T) ; ::_thesis: W is reflexive
hence W is reflexive by TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let S be non empty set ;
let T be complete LATTICE;
clusterT |^ S -> complete ;
coherence
T |^ S is complete
proof
A1: T |^ S = product (S --> T) by YELLOW_1:def_5;
for i being Element of S holds (S --> T) . i is complete LATTICE by FUNCOP_1:7;
hence T |^ S is complete by A1, WAYBEL_3:31; ::_thesis: verum
end;
end;
definition
let S, T be up-complete Scott TopLattice;
func SCMaps (S,T) -> strict full SubRelStr of MonMaps (S,T) means :Def2: :: WAYBEL17:def 2
for f being Function of S,T holds
( f in the carrier of it iff f is continuous );
existence
ex b1 being strict full SubRelStr of MonMaps (S,T) st
for f being Function of S,T holds
( f in the carrier of b1 iff 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 (MonMaps (S,T)) & S1[a] ) ) from XBOOLE_0:sch_1();
X c= the carrier of (MonMaps (S,T))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in the carrier of (MonMaps (S,T)) )
assume a in X ; ::_thesis: a in the carrier of (MonMaps (S,T))
hence a in the carrier of (MonMaps (S,T)) by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of (MonMaps (S,T)) ;
take SX = subrelstr X; ::_thesis: for f being Function of S,T holds
( f in the carrier of SX iff f is continuous )
let f be Function of S,T; ::_thesis: ( f in the carrier of SX iff f is continuous )
hereby ::_thesis: ( f is continuous implies f in the carrier of SX )
assume f in the carrier of SX ; ::_thesis: f is continuous
then f in X by YELLOW_0:def_15;
then ex f9 being Function of S,T st
( f9 = f & f9 is continuous ) by A1;
hence f is continuous ; ::_thesis: verum
end;
assume A2: f is continuous ; ::_thesis: f in the carrier of SX
f in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8;
then f in the carrier of (MonMaps (S,T)) by A2, YELLOW_1:def_6;
then f in X by A1, A2;
hence f in the carrier of SX by YELLOW_0:def_15; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict full SubRelStr of MonMaps (S,T) st ( for f being Function of S,T holds
( f in the carrier of b1 iff f is continuous ) ) & ( for f being Function of S,T holds
( f in the carrier of b2 iff f is continuous ) ) holds
b1 = b2
proof
let A1, A2 be strict full SubRelStr of MonMaps (S,T); ::_thesis: ( ( for f being Function of S,T holds
( f in the carrier of A1 iff f is continuous ) ) & ( for f being Function of S,T holds
( f in the carrier of A2 iff f is continuous ) ) implies A1 = A2 )
assume that
A3: for f being Function of S,T holds
( f in the carrier of A1 iff f is continuous ) and
A4: for f being Function of S,T holds
( f in the carrier of A2 iff f is continuous ) ; ::_thesis: A1 = A2
A5: the carrier of A1 c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13;
A6: the carrier of A2 c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13;
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 A7: x in the carrier of A1 ; ::_thesis: x in the carrier of A2
then reconsider y = x as Element of A1 ;
reconsider y = y as Function of S,T by A5, A7, WAYBEL10:9;
y is continuous by A3, A7;
hence x in the carrier of A2 by A4; ::_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 A8: x in the carrier of A2 ; ::_thesis: x in the carrier of A1
then reconsider y = x as Element of A2 ;
reconsider y = y as Function of S,T by A6, A8, WAYBEL10:9;
y is continuous by A4, A8;
hence x in the carrier of A1 by A3; ::_thesis: verum
end;
hence A1 = A2 by YELLOW_0:57; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines SCMaps WAYBEL17:def_2_:_
for S, T being up-complete Scott TopLattice
for b3 being strict full SubRelStr of MonMaps (S,T) holds
( b3 = SCMaps (S,T) iff for f being Function of S,T holds
( f in the carrier of b3 iff f is continuous ) );
registration
let S, T be up-complete Scott TopLattice;
cluster SCMaps (S,T) -> non empty strict full ;
coherence
not SCMaps (S,T) is empty
proof
set f = the continuous Function of S,T;
the continuous Function of S,T in the carrier of (SCMaps (S,T)) by Def2;
hence not SCMaps (S,T) is empty ; ::_thesis: verum
end;
end;
begin
definition
let S be non empty RelStr ;
let a, b be Element of S;
func Net-Str (a,b) -> non empty strict NetStr over S means :Def3: :: WAYBEL17:def 3
( the carrier of it = NAT & the mapping of it = (a,b) ,... & ( for i, j being Element of it
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) );
existence
ex b1 being non empty strict NetStr over S st
( the carrier of b1 = NAT & the mapping of b1 = (a,b) ,... & ( for i, j being Element of b1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) )
proof
defpred S1[ set , set ] means for i, j being Element of NAT st i = $1 & j = $2 holds
i <= j;
consider R being Relation of NAT,NAT such that
A1: for x, y being Element of NAT holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
reconsider R = R as Relation of NAT ;
take N = NetStr(# NAT,R,((a,b) ,...) #); ::_thesis: ( the carrier of N = NAT & the mapping of N = (a,b) ,... & ( for i, j being Element of N
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) )
thus the carrier of N = NAT ; ::_thesis: ( the mapping of N = (a,b) ,... & ( for i, j being Element of N
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) )
thus the mapping of N = (a,b) ,... ; ::_thesis: for i, j being Element of N
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 )
let i, j be Element of N; ::_thesis: for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 )
let i9, j9 be Element of NAT ; ::_thesis: ( i = i9 & j = j9 implies ( i <= j iff i9 <= j9 ) )
assume that
A2: i = i9 and
A3: j = j9 ; ::_thesis: ( i <= j iff i9 <= j9 )
reconsider x = i, y = j as Element of NAT ;
( [x,y] in the InternalRel of N iff S1[x,y] ) by A1;
hence ( i <= j iff i9 <= j9 ) by A2, A3, ORDERS_2:def_5; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict NetStr over S st the carrier of b1 = NAT & the mapping of b1 = (a,b) ,... & ( for i, j being Element of b1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) & the carrier of b2 = NAT & the mapping of b2 = (a,b) ,... & ( for i, j being Element of b2
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) holds
b1 = b2
proof
let it1, it2 be non empty strict NetStr over S; ::_thesis: ( the carrier of it1 = NAT & the mapping of it1 = (a,b) ,... & ( for i, j being Element of it1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) & the carrier of it2 = NAT & the mapping of it2 = (a,b) ,... & ( for i, j being Element of it2
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) implies it1 = it2 )
assume that
A4: the carrier of it1 = NAT and
A5: the mapping of it1 = (a,b) ,... and
A6: for i, j being Element of it1
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) and
A7: the carrier of it2 = NAT and
A8: the mapping of it2 = (a,b) ,... and
A9: for i, j being Element of it2
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ; ::_thesis: it1 = it2
the InternalRel of it1 = the InternalRel of it2
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of it1 or [x,y] in the InternalRel of it2 ) & ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 ) )
hereby ::_thesis: ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 )
assume A10: [x,y] in the InternalRel of it1 ; ::_thesis: [x,y] in the InternalRel of it2
then reconsider i = x, j = y as Element of it1 by ZFMISC_1:87;
reconsider i1 = i, i2 = j as Element of NAT by A4;
reconsider i9 = x, j9 = y as Element of it2 by A4, A7, A10, ZFMISC_1:87;
i <= j by A10, ORDERS_2:def_5;
then i1 <= i2 by A6;
then i9 <= j9 by A9;
hence [x,y] in the InternalRel of it2 by ORDERS_2:def_5; ::_thesis: verum
end;
assume A11: [x,y] in the InternalRel of it2 ; ::_thesis: [x,y] in the InternalRel of it1
then reconsider i = x, j = y as Element of it2 by ZFMISC_1:87;
reconsider i9 = x, j9 = y as Element of it1 by A4, A7, A11, ZFMISC_1:87;
reconsider i1 = i, i2 = j as Element of NAT by A7;
i <= j by A11, ORDERS_2:def_5;
then i1 <= i2 by A9;
then i9 <= j9 by A6;
hence [x,y] in the InternalRel of it1 by ORDERS_2:def_5; ::_thesis: verum
end;
hence it1 = it2 by A4, A5, A7, A8; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Net-Str WAYBEL17:def_3_:_
for S being non empty RelStr
for a, b being Element of S
for b4 being non empty strict NetStr over S holds
( b4 = Net-Str (a,b) iff ( the carrier of b4 = NAT & the mapping of b4 = (a,b) ,... & ( for i, j being Element of b4
for i9, j9 being Element of NAT st i = i9 & j = j9 holds
( i <= j iff i9 <= j9 ) ) ) );
registration
let S be non empty RelStr ;
let a, b be Element of S;
cluster Net-Str (a,b) -> non empty reflexive transitive antisymmetric strict directed ;
coherence
( Net-Str (a,b) is reflexive & Net-Str (a,b) is transitive & Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )
proof
set L = Net-Str (a,b);
thus Net-Str (a,b) is reflexive ::_thesis: ( Net-Str (a,b) is transitive & Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )
proof
let x be Element of (Net-Str (a,b)); :: according to YELLOW_0:def_1 ::_thesis: x <= x
reconsider x9 = x as Element of NAT by Def3;
x9 <= x9 ;
hence x <= x by Def3; ::_thesis: verum
end;
thus Net-Str (a,b) is transitive ::_thesis: ( Net-Str (a,b) is directed & Net-Str (a,b) is antisymmetric )
proof
let x, y, z be Element of (Net-Str (a,b)); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= z
reconsider x9 = x, y9 = y, z9 = z as Element of NAT by Def3;
A3: x9 <= y9 by A1, Def3;
y9 <= z9 by A2, Def3;
then x9 <= z9 by A3, XXREAL_0:2;
hence x <= z by Def3; ::_thesis: verum
end;
[#] (Net-Str (a,b)) is directed
proof
let x, y be Element of (Net-Str (a,b)); :: according to WAYBEL_0:def_1 ::_thesis: ( not x in [#] (Net-Str (a,b)) or not y in [#] (Net-Str (a,b)) or ex b1 being Element of the carrier of (Net-Str (a,b)) st
( b1 in [#] (Net-Str (a,b)) & x <= b1 & y <= b1 ) )
assume that
x in [#] (Net-Str (a,b)) and
y in [#] (Net-Str (a,b)) ; ::_thesis: ex b1 being Element of the carrier of (Net-Str (a,b)) st
( b1 in [#] (Net-Str (a,b)) & x <= b1 & y <= b1 )
reconsider x9 = x, y9 = y as Element of NAT by Def3;
set z9 = x9 + y9;
reconsider z = x9 + y9 as Element of (Net-Str (a,b)) by Def3;
reconsider z = z as Element of (Net-Str (a,b)) ;
take z ; ::_thesis: ( z in [#] (Net-Str (a,b)) & x <= z & y <= z )
A4: x9 <= x9 + y9 by NAT_1:11;
y9 <= x9 + y9 by NAT_1:11;
hence ( z in [#] (Net-Str (a,b)) & x <= z & y <= z ) by A4, Def3; ::_thesis: verum
end;
hence Net-Str (a,b) is directed by WAYBEL_0:def_6; ::_thesis: Net-Str (a,b) is antisymmetric
thus Net-Str (a,b) is antisymmetric ::_thesis: verum
proof
let x, y be Element of (Net-Str (a,b)); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
reconsider x9 = x, y9 = y as Element of NAT by Def3;
assume that
A5: x <= y and
A6: y <= x ; ::_thesis: x = y
A7: x9 <= y9 by A5, Def3;
y9 <= x9 by A6, Def3;
hence x = y by A7, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
theorem Th5: :: WAYBEL17:5
for S being non empty RelStr
for a, b being Element of S
for i being Element of (Net-Str (a,b)) holds
( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )
proof
let S be non empty RelStr ; ::_thesis: for a, b being Element of S
for i being Element of (Net-Str (a,b)) holds
( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )
let a, b be Element of S; ::_thesis: for i being Element of (Net-Str (a,b)) holds
( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )
let i be Element of (Net-Str (a,b)); ::_thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )
set N = Net-Str (a,b);
reconsider I = i as Element of NAT by Def3;
A1: (Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3;
defpred S1[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;
percases ( S1[I] or not S1[I] ) ;
suppose S1[I] ; ::_thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )
hence ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) by A1, Def1; ::_thesis: verum
end;
suppose not S1[I] ; ::_thesis: ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b )
hence ( (Net-Str (a,b)) . i = a or (Net-Str (a,b)) . i = b ) by A1, Def1; ::_thesis: verum
end;
end;
end;
theorem Th6: :: WAYBEL17:6
for S being non empty RelStr
for a, b being Element of S
for i, j being Element of (Net-Str (a,b))
for i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds
( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
proof
let S be non empty RelStr ; ::_thesis: for a, b being Element of S
for i, j being Element of (Net-Str (a,b))
for i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds
( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
let a, b be Element of S; ::_thesis: for i, j being Element of (Net-Str (a,b))
for i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds
( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
let i, j be Element of (Net-Str (a,b)); ::_thesis: for i9, j9 being Element of NAT st i9 = i & j9 = i9 + 1 & j9 = j holds
( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
let i9, j9 be Element of NAT ; ::_thesis: ( i9 = i & j9 = i9 + 1 & j9 = j implies ( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) ) )
assume that
A1: i9 = i and
A2: j9 = i9 + 1 and
A3: j9 = j ; ::_thesis: ( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
percases ( a <> b or a = b ) ;
supposeA4: a <> b ; ::_thesis: ( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
defpred S1[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;
thus ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) ::_thesis: ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a )
proof
assume A5: (Net-Str (a,b)) . i = a ; ::_thesis: (Net-Str (a,b)) . j = b
S1[i9]
proof
assume A6: not S1[i9] ; ::_thesis: contradiction
(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3
.= b by A1, A6, Def1 ;
hence contradiction by A4, A5; ::_thesis: verum
end;
then A7: for k being Element of NAT holds j9 <> 2 * k by A2;
(Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= b by A3, A7, Def1 ;
hence (Net-Str (a,b)) . j = b ; ::_thesis: verum
end;
assume A8: (Net-Str (a,b)) . i = b ; ::_thesis: (Net-Str (a,b)) . j = a
A9: not S1[i9]
proof
assume A10: S1[i9] ; ::_thesis: contradiction
(Net-Str (a,b)) . i = ((a,b) ,...) . i by Def3
.= a by A1, A10, Def1 ;
hence contradiction by A4, A8; ::_thesis: verum
end;
A11: S1[j9]
proof
assume not S1[j9] ; ::_thesis: contradiction
then ex kl being Element of NAT st j9 = (2 * kl) + 1 by SCHEME1:1;
hence contradiction by A2, A9; ::_thesis: verum
end;
(Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= a by A3, A11, Def1 ;
hence (Net-Str (a,b)) . j = a ; ::_thesis: verum
end;
suppose a = b ; ::_thesis: ( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) )
hence ( ( (Net-Str (a,b)) . i = a implies (Net-Str (a,b)) . j = b ) & ( (Net-Str (a,b)) . i = b implies (Net-Str (a,b)) . j = a ) ) by Th5; ::_thesis: verum
end;
end;
end;
theorem Th7: :: WAYBEL17:7
for S being with_infima Poset
for a, b being Element of S holds lim_inf (Net-Str (a,b)) = a "/\" b
proof
let S be with_infima Poset; ::_thesis: for a, b being Element of S holds lim_inf (Net-Str (a,b)) = a "/\" b
let a, b be Element of S; ::_thesis: lim_inf (Net-Str (a,b)) = a "/\" b
set N = Net-Str (a,b);
A1: for j being Element of (Net-Str (a,b)) holds { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } = {a,b}
proof
let j be Element of (Net-Str (a,b)); ::_thesis: { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } = {a,b}
thus { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } c= {a,b} :: according to XBOOLE_0:def_10 ::_thesis: {a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } or x in {a,b} )
assume x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ; ::_thesis: x in {a,b}
then consider i1 being Element of (Net-Str (a,b)) such that
A2: x = (Net-Str (a,b)) . i1 and
i1 >= j ;
( (Net-Str (a,b)) . i1 = a or (Net-Str (a,b)) . i1 = b ) by Th5;
hence x in {a,b} by A2, TARSKI:def_2; ::_thesis: verum
end;
thus {a,b} c= { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a,b} or x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } )
assume A3: x in {a,b} ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
reconsider J = j as Element of NAT by Def3;
defpred S1[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;
percases ( x = a or x = b ) by A3, TARSKI:def_2;
supposeA4: x = a ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
now__::_thesis:_x_in__{__((Net-Str_(a,b))_._i)_where_i_is_Element_of_(Net-Str_(a,b))_:_i_>=_j__}_
percases ( S1[J] or not S1[J] ) ;
supposeA5: S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
A6: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= a by A5, Def1 ;
j <= j ;
hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A4, A6; ::_thesis: verum
end;
supposeA7: not S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
A8: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= b by A7, Def1 ;
reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3;
A9: (Net-Str (a,b)) . k = a by A8, Th6;
J + 1 >= J by NAT_1:11;
then k >= j by Def3;
hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A4, A9; ::_thesis: verum
end;
end;
end;
hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ; ::_thesis: verum
end;
supposeA10: x = b ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
now__::_thesis:_x_in__{__((Net-Str_(a,b))_._i)_where_i_is_Element_of_(Net-Str_(a,b))_:_i_>=_j__}_
percases ( not S1[J] or S1[J] ) ;
supposeA11: not S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
A12: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= b by A11, Def1 ;
j <= j ;
hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A10, A12; ::_thesis: verum
end;
supposeA13: S1[J] ; ::_thesis: x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j }
A14: (Net-Str (a,b)) . j = ((a,b) ,...) . j by Def3
.= a by A13, Def1 ;
reconsider k = J + 1 as Element of (Net-Str (a,b)) by Def3;
A15: (Net-Str (a,b)) . k = b by A14, Th6;
J + 1 >= J by NAT_1:11;
then k >= j by Def3;
hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } by A10, A15; ::_thesis: verum
end;
end;
end;
hence x in { ((Net-Str (a,b)) . i) where i is Element of (Net-Str (a,b)) : i >= j } ; ::_thesis: verum
end;
end;
end;
end;
defpred S1[ Element of (Net-Str (a,b)), Element of (Net-Str (a,b))] means $1 >= $2;
deffunc H1( Element of (Net-Str (a,b))) -> set = { ((Net-Str (a,b)) . i1) where i1 is Element of (Net-Str (a,b)) : S1[i1,$1] } ;
defpred S2[ set ] means verum;
deffunc H2( Element of (Net-Str (a,b))) -> Element of K32( the carrier of S) = {a,b};
deffunc H3( Element of (Net-Str (a,b))) -> Element of the carrier of S = "/\" (H1($1),S);
deffunc H4( Element of (Net-Str (a,b))) -> Element of the carrier of S = "/\" (H2($1),S);
deffunc H5( set ) -> Element of the carrier of S = a "/\" b;
A16: for jj being Element of (Net-Str (a,b)) holds H3(jj) = H5(jj)
proof
let jj be Element of (Net-Str (a,b)); ::_thesis: H3(jj) = H5(jj)
H3(jj) = H4(jj) by A1
.= a "/\" b by YELLOW_0:40 ;
hence H3(jj) = H5(jj) ; ::_thesis: verum
end;
A17: { H3(j3) where j3 is Element of (Net-Str (a,b)) : S2[j3] } = { H5(j4) where j4 is Element of (Net-Str (a,b)) : S2[j4] } from FRAENKEL:sch_5(A16);
A18: { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } c= {(a "/\" b)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } or x in {(a "/\" b)} )
assume x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } ; ::_thesis: x in {(a "/\" b)}
then ex q being Element of (Net-Str (a,b)) st
( x = a "/\" b & S2[q] ) ;
hence x in {(a "/\" b)} by TARSKI:def_1; ::_thesis: verum
end;
{(a "/\" b)} c= { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(a "/\" b)} or x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } )
assume x in {(a "/\" b)} ; ::_thesis: x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] }
then x = a "/\" b by TARSKI:def_1;
hence x in { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } ; ::_thesis: verum
end;
then { (a "/\" b) where j4 is Element of (Net-Str (a,b)) : S2[j4] } = {(a "/\" b)} by A18, XBOOLE_0:def_10;
hence lim_inf (Net-Str (a,b)) = a "/\" b by A17, YELLOW_0:39; ::_thesis: verum
end;
Lm5: for S being with_infima Poset
for a, b being Element of S st a <= b holds
lim_inf (Net-Str (a,b)) = a
proof
let S be with_infima Poset; ::_thesis: for a, b being Element of S st a <= b holds
lim_inf (Net-Str (a,b)) = a
let a, b be Element of S; ::_thesis: ( a <= b implies lim_inf (Net-Str (a,b)) = a )
assume A1: a <= b ; ::_thesis: lim_inf (Net-Str (a,b)) = a
reconsider a9 = a, b9 = b as Element of S ;
lim_inf (Net-Str (a,b)) = a9 "/\" b9 by Th7
.= a9 by A1, YELLOW_0:25 ;
hence lim_inf (Net-Str (a,b)) = a ; ::_thesis: verum
end;
theorem Th8: :: WAYBEL17:8
for S, T being with_infima Poset
for a, b being Element of S
for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
proof
let S, T be with_infima Poset; ::_thesis: for a, b being Element of S
for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
let a, b be Element of S; ::_thesis: for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
let f be Function of S,T; ::_thesis: lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)
set N = Net-Str (a,b);
set fN = f * (Net-Str (a,b));
A1: RelStr(# the carrier of (f * (Net-Str (a,b))), the InternalRel of (f * (Net-Str (a,b))) #) = RelStr(# the carrier of (Net-Str (a,b)), the InternalRel of (Net-Str (a,b)) #) by WAYBEL_9:def_8;
A2: for j being Element of (f * (Net-Str (a,b))) holds { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } = {(f . a),(f . b)}
proof
let j be Element of (f * (Net-Str (a,b))); ::_thesis: { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } = {(f . a),(f . b)}
reconsider jj = j as Element of (Net-Str (a,b)) by A1;
thus { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } c= {(f . a),(f . b)} :: according to XBOOLE_0:def_10 ::_thesis: {(f . a),(f . b)} c= { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } or x in {(f . a),(f . b)} )
assume x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ; ::_thesis: x in {(f . a),(f . b)}
then consider i1 being Element of (f * (Net-Str (a,b))) such that
A3: x = (f * (Net-Str (a,b))) . i1 and
i1 >= j ;
reconsider I1 = i1 as Element of (Net-Str (a,b)) by A1;
i1 in the carrier of (Net-Str (a,b)) by A1;
then A4: i1 in dom the mapping of (Net-Str (a,b)) by FUNCT_2:def_1;
(f * (Net-Str (a,b))) . i1 = (f * the mapping of (Net-Str (a,b))) . i1 by WAYBEL_9:def_8
.= f . ((Net-Str (a,b)) . I1) by A4, FUNCT_1:13 ;
then ( (f * (Net-Str (a,b))) . i1 = f . a or (f * (Net-Str (a,b))) . i1 = f . b ) by Th5;
hence x in {(f . a),(f . b)} by A3, TARSKI:def_2; ::_thesis: verum
end;
thus {(f . a),(f . b)} c= { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(f . a),(f . b)} or x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } )
assume A5: x in {(f . a),(f . b)} ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
A6: j in the carrier of (Net-Str (a,b)) by A1;
reconsider J = j as Element of NAT by A1, Def3;
A7: j in dom the mapping of (Net-Str (a,b)) by A6, FUNCT_2:def_1;
defpred S1[ Element of NAT ] means ex k being Element of NAT st $1 = 2 * k;
percases ( x = f . a or x = f . b ) by A5, TARSKI:def_2;
supposeA8: x = f . a ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
reconsider jj = j as Element of (Net-Str (a,b)) by A1;
now__::_thesis:_x_in__{__((f_*_(Net-Str_(a,b)))_._i)_where_i_is_Element_of_(f_*_(Net-Str_(a,b)))_:_i_>=_j__}_
percases ( S1[J] or not S1[J] ) ;
supposeA9: S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
A10: (f * (Net-Str (a,b))) . j = (f * the mapping of (Net-Str (a,b))) . j by WAYBEL_9:def_8
.= f . ( the mapping of (Net-Str (a,b)) . j) by A7, FUNCT_1:13
.= f . (((a,b) ,...) . j) by Def3
.= f . a by A9, Def1 ;
j <= j ;
hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A8, A10; ::_thesis: verum
end;
supposeA11: not S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
A12: (Net-Str (a,b)) . jj = ((a,b) ,...) . jj by Def3
.= b by A11, Def1 ;
reconsider k = J + 1 as Element of (f * (Net-Str (a,b))) by A1, Def3;
reconsider kk = k as Element of (Net-Str (a,b)) by A1;
kk in the carrier of (Net-Str (a,b)) ;
then A13: kk in dom the mapping of (Net-Str (a,b)) by FUNCT_2:def_1;
A14: (f * (Net-Str (a,b))) . k = (f * the mapping of (Net-Str (a,b))) . k by WAYBEL_9:def_8
.= f . ((Net-Str (a,b)) . kk) by A13, FUNCT_1:13
.= f . a by A12, Th6 ;
J + 1 >= J by NAT_1:11;
then kk >= jj by Def3;
then [jj,kk] in the InternalRel of (Net-Str (a,b)) by ORDERS_2:def_5;
then k >= j by A1, ORDERS_2:def_5;
hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A8, A14; ::_thesis: verum
end;
end;
end;
hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ; ::_thesis: verum
end;
supposeA15: x = f . b ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
now__::_thesis:_x_in__{__((f_*_(Net-Str_(a,b)))_._i)_where_i_is_Element_of_(f_*_(Net-Str_(a,b)))_:_i_>=_j__}_
percases ( not S1[J] or S1[J] ) ;
supposeA16: not S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
A17: (f * (Net-Str (a,b))) . j = (f * the mapping of (Net-Str (a,b))) . j by WAYBEL_9:def_8
.= f . ( the mapping of (Net-Str (a,b)) . j) by A7, FUNCT_1:13
.= f . (((a,b) ,...) . j) by Def3
.= f . b by A16, Def1 ;
j <= j ;
hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A15, A17; ::_thesis: verum
end;
supposeA18: S1[J] ; ::_thesis: x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j }
A19: (Net-Str (a,b)) . jj = ((a,b) ,...) . j by Def3
.= a by A18, Def1 ;
reconsider k = J + 1 as Element of (f * (Net-Str (a,b))) by A1, Def3;
reconsider kk = k as Element of (Net-Str (a,b)) by Def3;
kk in the carrier of (Net-Str (a,b)) ;
then A20: kk in dom the mapping of (Net-Str (a,b)) by FUNCT_2:def_1;
A21: (f * (Net-Str (a,b))) . k = (f * the mapping of (Net-Str (a,b))) . k by WAYBEL_9:def_8
.= f . ((Net-Str (a,b)) . kk) by A20, FUNCT_1:13
.= f . b by A19, Th6 ;
J + 1 >= J by NAT_1:11;
then kk >= jj by Def3;
then [jj,kk] in the InternalRel of (Net-Str (a,b)) by ORDERS_2:def_5;
then k >= j by A1, ORDERS_2:def_5;
hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } by A15, A21; ::_thesis: verum
end;
end;
end;
hence x in { ((f * (Net-Str (a,b))) . i) where i is Element of (f * (Net-Str (a,b))) : i >= j } ; ::_thesis: verum
end;
end;
end;
end;
defpred S1[ Element of (f * (Net-Str (a,b))), Element of (f * (Net-Str (a,b)))] means $1 >= $2;
deffunc H1( Element of (f * (Net-Str (a,b)))) -> set = { ((f * (Net-Str (a,b))) . i1) where i1 is Element of (f * (Net-Str (a,b))) : S1[i1,$1] } ;
defpred S2[ set ] means verum;
deffunc H2( Element of (f * (Net-Str (a,b)))) -> Element of K32( the carrier of T) = {(f . a),(f . b)};
deffunc H3( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H1($1),T);
deffunc H4( Element of (f * (Net-Str (a,b)))) -> Element of the carrier of T = "/\" (H2($1),T);
deffunc H5( set ) -> Element of the carrier of T = (f . a) "/\" (f . b);
A22: for jj being Element of (f * (Net-Str (a,b))) holds H3(jj) = H5(jj)
proof
let jj be Element of (f * (Net-Str (a,b))); ::_thesis: H3(jj) = H5(jj)
H3(jj) = H4(jj) by A2
.= (f . a) "/\" (f . b) by YELLOW_0:40 ;
hence H3(jj) = H5(jj) ; ::_thesis: verum
end;
A23: { H3(j3) where j3 is Element of (f * (Net-Str (a,b))) : S2[j3] } = { H5(j4) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } from FRAENKEL:sch_5(A22);
A24: { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } c= {((f . a) "/\" (f . b))}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } or x in {((f . a) "/\" (f . b))} )
assume x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } ; ::_thesis: x in {((f . a) "/\" (f . b))}
then ex q being Element of (f * (Net-Str (a,b))) st
( x = (f . a) "/\" (f . b) & S2[q] ) ;
hence x in {((f . a) "/\" (f . b))} by TARSKI:def_1; ::_thesis: verum
end;
{((f . a) "/\" (f . b))} c= { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {((f . a) "/\" (f . b))} or x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } )
assume x in {((f . a) "/\" (f . b))} ; ::_thesis: x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] }
then x = (f . a) "/\" (f . b) by TARSKI:def_1;
hence x in { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } ; ::_thesis: verum
end;
then { ((f . a) "/\" (f . b)) where j4 is Element of (f * (Net-Str (a,b))) : S2[j4] } = {((f . a) "/\" (f . b))} by A24, XBOOLE_0:def_10;
hence lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by A23, YELLOW_0:39; ::_thesis: verum
end;
definition
let S be non empty RelStr ;
let D be non empty Subset of S;
func Net-Str D -> strict NetStr over S equals :: WAYBEL17:def 4
NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #);
correctness
coherence
NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #) is strict NetStr over S;
;
end;
:: deftheorem defines Net-Str WAYBEL17:def_4_:_
for S being non empty RelStr
for D being non empty Subset of S holds Net-Str D = NetStr(# D,( the InternalRel of S |_2 D),((id the carrier of S) | D) #);
theorem Th9: :: WAYBEL17:9
for S being non empty reflexive RelStr
for D being non empty Subset of S holds Net-Str D = Net-Str (D,((id the carrier of S) | D))
proof
let S be non empty reflexive RelStr ; ::_thesis: for D being non empty Subset of S holds Net-Str D = Net-Str (D,((id the carrier of S) | D))
let D be non empty Subset of S; ::_thesis: Net-Str D = Net-Str (D,((id the carrier of S) | D))
set M = Net-Str (D,((id the carrier of S) | D));
A1: D = the carrier of (Net-Str (D,((id the carrier of S) | D))) by WAYBEL11:def_10;
A2: (id the carrier of S) | D = the mapping of (Net-Str (D,((id the carrier of S) | D))) by WAYBEL11:def_10;
A3: (id the carrier of S) | D = id D by FUNCT_3:1;
A4: the InternalRel of S |_2 D c= the InternalRel of S by XBOOLE_1:17;
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_the_InternalRel_of_S_|_2_D_implies_[x,y]_in_the_InternalRel_of_(Net-Str_(D,((id_the_carrier_of_S)_|_D)))_)_&_(_[x,y]_in_the_InternalRel_of_(Net-Str_(D,((id_the_carrier_of_S)_|_D)))_implies_[x,y]_in_the_InternalRel_of_S_|_2_D_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in the InternalRel of S |_2 D implies [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) ) & ( [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) implies [x,y] in the InternalRel of S |_2 D ) )
hereby ::_thesis: ( [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) implies [x,y] in the InternalRel of S |_2 D )
assume A5: [x,y] in the InternalRel of S |_2 D ; ::_thesis: [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D)))
then A6: x in D by ZFMISC_1:87;
A7: y in D by A5, ZFMISC_1:87;
reconsider x9 = x, y9 = y as Element of (Net-Str (D,((id the carrier of S) | D))) by A1, A5, ZFMISC_1:87;
A8: x9 = ((id the carrier of S) | D) . x9 by A3, A6, FUNCT_1:18;
y9 = ((id the carrier of S) | D) . y9 by A3, A7, FUNCT_1:18;
then (Net-Str (D,((id the carrier of S) | D))) . x9 <= (Net-Str (D,((id the carrier of S) | D))) . y9 by A2, A4, A5, A8, ORDERS_2:def_5;
then x9 <= y9 by WAYBEL11:def_10;
hence [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) by ORDERS_2:def_5; ::_thesis: verum
end;
assume A9: [x,y] in the InternalRel of (Net-Str (D,((id the carrier of S) | D))) ; ::_thesis: [x,y] in the InternalRel of S |_2 D
then reconsider x9 = x, y9 = y as Element of (Net-Str (D,((id the carrier of S) | D))) by ZFMISC_1:87;
x9 <= y9 by A9, ORDERS_2:def_5;
then (Net-Str (D,((id the carrier of S) | D))) . x9 <= (Net-Str (D,((id the carrier of S) | D))) . y9 by WAYBEL11:def_10;
then A10: [((Net-Str (D,((id the carrier of S) | D))) . x9),((Net-Str (D,((id the carrier of S) | D))) . y9)] in the InternalRel of S by ORDERS_2:def_5;
A11: x9 = ((id the carrier of S) | D) . x9 by A1, A3, FUNCT_1:18;
y9 = ((id the carrier of S) | D) . y9 by A1, A3, FUNCT_1:18;
hence [x,y] in the InternalRel of S |_2 D by A1, A2, A9, A10, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence Net-Str D = Net-Str (D,((id the carrier of S) | D)) by A1, A2, RELAT_1:def_2; ::_thesis: verum
end;
registration
let S be non empty reflexive RelStr ;
let D be non empty directed Subset of S;
cluster Net-Str D -> non empty reflexive strict directed ;
coherence
( not Net-Str D is empty & Net-Str D is directed & Net-Str D is reflexive )
proof
Net-Str D = Net-Str (D,((id the carrier of S) | D)) by Th9;
hence ( not Net-Str D is empty & Net-Str D is directed & Net-Str D is reflexive ) ; ::_thesis: verum
end;
end;
registration
let S be non empty reflexive transitive RelStr ;
let D be non empty directed Subset of S;
cluster Net-Str D -> transitive strict ;
coherence
Net-Str D is transitive ;
end;
registration
let S be non empty reflexive RelStr ;
let D be non empty directed Subset of S;
cluster Net-Str D -> strict monotone ;
coherence
Net-Str D is monotone
proof
Net-Str D = Net-Str (D,((id the carrier of S) | D)) by Th9;
hence Net-Str D is monotone ; ::_thesis: verum
end;
end;
Lm6: for R being up-complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
proof
let R be up-complete LATTICE; ::_thesis: for N being reflexive monotone net of R holds lim_inf N = sup N
let N be reflexive monotone net of R; ::_thesis: lim_inf N = sup N
defpred S1[ set ] means verum;
deffunc H1( Element of N) -> Element of the carrier of R = N . $1;
deffunc H2( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,R);
A1: for j being Element of N holds H1(j) = H2(j)
proof
let j be Element of N; ::_thesis: H1(j) = H2(j)
set Y = { (N . i) where i is Element of N : i >= j } ;
A2: N . j is_<=_than { (N . i) where i is Element of N : i >= j }
proof
let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in { (N . i) where i is Element of N : i >= j } or N . j <= y )
assume y in { (N . i) where i is Element of N : i >= j } ; ::_thesis: N . j <= y
then ex i being Element of N st
( y = N . i & j <= i ) ;
hence N . j <= y by WAYBEL11:def_9; ::_thesis: verum
end;
for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= j } holds
N . j >= b
proof
let b be Element of R; ::_thesis: ( b is_<=_than { (N . i) where i is Element of N : i >= j } implies N . j >= b )
assume A3: b is_<=_than { (N . i) where i is Element of N : i >= j } ; ::_thesis: N . j >= b
reconsider j9 = j as Element of N ;
j9 <= j9 ;
then N . j9 in { (N . i) where i is Element of N : i >= j } ;
hence N . j >= b by A3, LATTICE3:def_8; ::_thesis: verum
end;
hence H1(j) = H2(j) by A2, YELLOW_0:31; ::_thesis: verum
end;
rng the mapping of N = { H1(j) where j is Element of N : S1[j] } by WAYBEL11:19
.= { H2(j) where j is Element of N : S1[j] } from FRAENKEL:sch_5(A1) ;
hence lim_inf N = Sup by YELLOW_2:def_5
.= sup N by WAYBEL_2:def_1 ;
::_thesis: verum
end;
theorem Th10: :: WAYBEL17:10
for S being up-complete LATTICE
for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D
proof
let S be up-complete LATTICE; ::_thesis: for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D
let D be non empty directed Subset of S; ::_thesis: lim_inf (Net-Str D) = sup D
set F = (id the carrier of S) | D;
A1: (id the carrier of S) | D = id D by FUNCT_3:1;
lim_inf (Net-Str D) = sup (Net-Str D) by Lm6
.= Sup by WAYBEL_2:def_1
.= "\/" ((rng ((id the carrier of S) | D)),S) by YELLOW_2:def_5
.= sup D by A1, RELAT_1:45 ;
hence lim_inf (Net-Str D) = sup D ; ::_thesis: verum
end;
begin
theorem Th11: :: WAYBEL17:11
for S, T being LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is monotone
proof
let S, T be LATTICE; ::_thesis: for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is monotone
let f be Function of S,T; ::_thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies f is monotone )
assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: f is monotone
now__::_thesis:_for_a,_b_being_Element_of_S_st_a_<=_b_holds_
f_._a_<=_f_._b
let a, b be Element of S; ::_thesis: ( a <= b implies f . a <= f . b )
assume A2: a <= b ; ::_thesis: f . a <= f . b
set N = Net-Str (a,b);
A3: f . (lim_inf (Net-Str (a,b))) = f . a by A2, Lm5;
lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b) by Th8;
then A4: f . a <= (f . a) "/\" (f . b) by A1, A3;
f . a >= (f . a) "/\" (f . b) by YELLOW_0:23;
then f . a = (f . a) "/\" (f . b) by A4, ORDERS_2:2;
hence f . a <= f . b by YELLOW_0:25; ::_thesis: verum
end;
hence f is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;
scheme :: WAYBEL17:sch 3
NetFraenkelS{ F1() -> non empty TopRelStr , F2() -> non empty TopRelStr , F3() -> non empty TopRelStr , F4( set ) -> Element of F3(), F5() -> Function, P1[ set ] } :
F5() .: { F4(x) where x is Element of F1() : P1[x] } = { (F5() . F4(x)) where x is Element of F2() : P1[x] }
provided
A1: the carrier of F3() c= dom F5() and
A2: the carrier of F1() = the carrier of F2()
proof
set f = F5();
thus F5() .: { F4(x) where x is Element of F1() : P1[x] } c= { (F5() . F4(x)) where x is Element of F2() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F5() . F4(x)) where x is Element of F2() : P1[x] } c= F5() .: { F4(x) where x is Element of F1() : P1[x] }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F5() .: { F4(x) where x is Element of F1() : P1[x] } or y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } )
assume y in F5() .: { F4(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F5() . F4(x)) where x is Element of F2() : P1[x] }
then consider z being set such that
z in dom F5() and
A3: z in { F4(x) where x is Element of F1() : P1[x] } and
A4: y = F5() . z by FUNCT_1:def_6;
consider x being Element of F1() such that
A5: z = F4(x) and
A6: P1[x] by A3;
reconsider x = x as Element of F2() by A2;
y = F5() . F4(x) by A4, A5;
hence y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } by A6; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } or y in F5() .: { F4(x) where x is Element of F1() : P1[x] } )
assume y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } ; ::_thesis: y in F5() .: { F4(x) where x is Element of F1() : P1[x] }
then consider x being Element of F2() such that
A7: y = F5() . F4(x) and
A8: P1[x] ;
reconsider x = x as Element of F1() by A2;
A9: F4(x) in the carrier of F3() ;
F4(x) in { F4(z) where z is Element of F1() : P1[z] } by A8;
hence y in F5() .: { F4(x) where x is Element of F1() : P1[x] } by A1, A7, A9, FUNCT_1:def_6; ::_thesis: verum
end;
theorem Th12: :: WAYBEL17:12
for S, T being lower-bounded continuous LATTICE
for f being Function of S,T st f is directed-sups-preserving holds
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 continuous LATTICE; ::_thesis: for f being Function of S,T st f is directed-sups-preserving holds
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)
let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )
assume A1: f is directed-sups-preserving ; ::_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)
defpred S1[ Element of S] means $1 << x;
deffunc H1( Element of S) -> Element of S = $1;
A2: f preserves_sup_of waybelow x by A1, WAYBEL_0:def_37;
A3: ex_sup_of waybelow x,S by YELLOW_0:17;
A4: the carrier of S c= dom f by FUNCT_2:def_1;
A5: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A4);
f . x = f . (sup (waybelow x)) by WAYBEL_3:def_5
.= "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A2, A3, A5, WAYBEL_0:def_31 ;
hence f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: verum
end;
theorem Th13: :: WAYBEL17:13
for S being LATTICE
for T being lower-bounded up-complete LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
f is monotone
proof
let S be LATTICE; ::_thesis: for T being lower-bounded up-complete LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
f is monotone
let T be lower-bounded up-complete LATTICE; ::_thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
f is monotone
let f be 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) ) implies f is monotone )
assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: f is monotone
let X, Y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not X <= Y or f . X <= f . Y )
deffunc H1( Element of S) -> Element of S = $1;
defpred S1[ Element of S] means $1 << X;
defpred S2[ Element of S] means $1 << Y;
assume X <= Y ; ::_thesis: f . X <= f . Y
then A2: waybelow X c= waybelow Y by WAYBEL_3:12;
A3: f . X = "\/" ( { (f . w) where w is Element of S : w << X } ,T) by A1;
A4: the carrier of S c= dom f by FUNCT_2:def_1;
A5: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A4);
f .: { H1(w) where w is Element of S : S2[w] } = { (f . H1(w)) where w is Element of S : S2[w] } from WAYBEL17:sch_2(A4);
then A6: f . Y = "\/" ((f .: (waybelow Y)),T) by A1;
A7: ex_sup_of f .: (waybelow X),T by YELLOW_0:17;
ex_sup_of f .: (waybelow Y),T by YELLOW_0:17;
hence f . X <= f . Y by A2, A3, A5, A6, A7, RELAT_1:123, YELLOW_0:34; ::_thesis: verum
end;
theorem Th14: :: WAYBEL17:14
for S being lower-bounded up-complete LATTICE
for T being lower-bounded continuous LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
proof
let S be lower-bounded up-complete LATTICE; ::_thesis: for T being lower-bounded continuous LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let T be lower-bounded continuous LATTICE; ::_thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let f be 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) ) implies for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
then A2: f is monotone by Th13;
let x be Element of S; ::_thesis: for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let y be Element of T; ::_thesis: ( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
hereby ::_thesis: ( ex w being Element of S st
( w << x & y << f . w ) implies y << f . x )
assume A3: y << f . x ; ::_thesis: ex v being Element of S st
( v << x & y << f . v )
reconsider D = f .: (waybelow x) as non empty directed Subset of T by A1, Th13, YELLOW_2:15;
A4: f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A1;
A5: the carrier of S c= dom f by FUNCT_2:def_1;
defpred S1[ Element of S] means $1 << x;
deffunc H1( Element of S) -> Element of S = $1;
f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A5);
then consider w being Element of T such that
A6: w in D and
A7: y << w by A3, A4, WAYBEL_4:53;
consider v being set such that
A8: v in the carrier of S and
A9: v in waybelow x and
A10: w = f . v by A6, FUNCT_2:64;
reconsider v = v as Element of S by A8;
take v = v; ::_thesis: ( v << x & y << f . v )
thus ( v << x & y << f . v ) by A7, A9, A10, WAYBEL_3:7; ::_thesis: verum
end;
given w being Element of S such that A11: w << x and
A12: y << f . w ; ::_thesis: y << f . x
w <= x by A11, WAYBEL_3:1;
then f . w <= f . x by A2, WAYBEL_1:def_2;
hence y << f . x by A12, WAYBEL_3:2; ::_thesis: verum
end;
theorem Th15: :: WAYBEL17:15
for S, T being non empty RelStr
for D being Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
proof
let S, T be non empty RelStr ; ::_thesis: for D being Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
let D be Subset of S; ::_thesis: for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
let f be Function of S,T; ::_thesis: ( ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone implies sup (f .: D) <= f . (sup D) )
assume A1: ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) ; ::_thesis: ( not f is monotone or sup (f .: D) <= f . (sup D) )
A2: ex_sup_of D,S by A1, YELLOW_0:17;
A3: ex_sup_of f .: D,T by A1, YELLOW_0:17;
assume A4: f is monotone ; ::_thesis: sup (f .: D) <= f . (sup D)
D is_<=_than sup D by A2, YELLOW_0:def_9;
then f .: D is_<=_than f . (sup D) by A4, YELLOW_2:14;
hence sup (f .: D) <= f . (sup D) by A3, YELLOW_0:def_9; ::_thesis: verum
end;
theorem Th16: :: WAYBEL17:16
for S, T being non empty reflexive antisymmetric RelStr
for D being non empty directed Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
proof
let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: for D being non empty directed Subset of S
for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
let D be non empty directed Subset of S; ::_thesis: for f being Function of S,T st ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone holds
sup (f .: D) <= f . (sup D)
let f be Function of S,T; ::_thesis: ( ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) & f is monotone implies sup (f .: D) <= f . (sup D) )
assume A1: ( ( ex_sup_of D,S & ex_sup_of f .: D,T ) or ( S is up-complete & T is up-complete ) ) ; ::_thesis: ( not f is monotone or sup (f .: D) <= f . (sup D) )
assume A2: f is monotone ; ::_thesis: sup (f .: D) <= f . (sup D)
then reconsider fD = f .: D as non empty directed Subset of T by YELLOW_2:15;
A3: ex_sup_of fD,T by A1, WAYBEL_0:75;
ex_sup_of D,S by A1, WAYBEL_0:75;
then D is_<=_than sup D by YELLOW_0:30;
then f .: D is_<=_than f . (sup D) by A2, YELLOW_2:14;
hence sup (f .: D) <= f . (sup D) by A3, YELLOW_0:30; ::_thesis: verum
end;
theorem :: WAYBEL17:17
for S, T being non empty RelStr
for D being Subset of S
for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
f . (inf D) <= inf (f .: D)
proof
let S, T be non empty RelStr ; ::_thesis: for D being Subset of S
for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
f . (inf D) <= inf (f .: D)
let D be Subset of S; ::_thesis: for f being Function of S,T st ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone holds
f . (inf D) <= inf (f .: D)
let f be Function of S,T; ::_thesis: ( ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) & f is monotone implies f . (inf D) <= inf (f .: D) )
assume A1: ( ( ex_inf_of D,S & ex_inf_of f .: D,T ) or ( S is complete & S is antisymmetric & T is complete & T is antisymmetric ) ) ; ::_thesis: ( not f is monotone or f . (inf D) <= inf (f .: D) )
A2: ex_inf_of D,S by A1, YELLOW_0:17;
A3: ex_inf_of f .: D,T by A1, YELLOW_0:17;
assume A4: f is monotone ; ::_thesis: f . (inf D) <= inf (f .: D)
inf D is_<=_than D by A2, YELLOW_0:def_10;
then f . (inf D) is_<=_than f .: D by A4, YELLOW_2:13;
hence f . (inf D) <= inf (f .: D) by A3, YELLOW_0:def_10; ::_thesis: verum
end;
Lm7: for S, T being complete LATTICE
for D being Subset of S
for f being Function of S,T st f is monotone holds
f . ("/\" (D,S)) <= inf (f .: D)
proof
let S, T be complete LATTICE; ::_thesis: for D being Subset of S
for f being Function of S,T st f is monotone holds
f . ("/\" (D,S)) <= inf (f .: D)
let D be Subset of S; ::_thesis: for f being Function of S,T st f is monotone holds
f . ("/\" (D,S)) <= inf (f .: D)
let f be Function of S,T; ::_thesis: ( f is monotone implies f . ("/\" (D,S)) <= inf (f .: D) )
reconsider D9 = D as Subset of S ;
set infD = "/\" (D,S);
assume A1: f is monotone ; ::_thesis: f . ("/\" (D,S)) <= inf (f .: D)
"/\" (D,S) is_<=_than D by YELLOW_0:33;
then f . ("/\" (D,S)) is_<=_than f .: D9 by A1, YELLOW_2:13;
hence f . ("/\" (D,S)) <= inf (f .: D) by YELLOW_0:33; ::_thesis: verum
end;
theorem Th18: :: WAYBEL17:18
for S, T being up-complete LATTICE
for f being Function of S,T
for N being non empty monotone NetStr over S st f is monotone holds
f * N is monotone
proof
let S, T be up-complete LATTICE; ::_thesis: for f being Function of S,T
for N being non empty monotone NetStr over S st f is monotone holds
f * N is monotone
let f be Function of S,T; ::_thesis: for N being non empty monotone NetStr over S st f is monotone holds
f * N is monotone
let N be non empty monotone NetStr over S; ::_thesis: ( f is monotone implies f * N is monotone )
assume A1: f is monotone ; ::_thesis: f * N is monotone
A2: netmap (N,S) is monotone by WAYBEL_0:def_9;
A3: netmap ((f * N),T) = f * (netmap (N,S)) by WAYBEL_9:def_8;
set g = netmap ((f * N),T);
now__::_thesis:_for_x,_y_being_Element_of_(f_*_N)_st_x_<=_y_holds_
(netmap_((f_*_N),T))_._x_<=_(netmap_((f_*_N),T))_._y
let x, y be Element of (f * N); ::_thesis: ( x <= y implies (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y )
assume A4: x <= y ; ::_thesis: (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y
A5: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) by WAYBEL_9:def_8;
then reconsider x9 = x, y9 = y as Element of N ;
A6: dom (netmap (N,S)) = the carrier of (f * N) by A5, FUNCT_2:def_1;
then A7: (netmap ((f * N),T)) . x = f . ((netmap (N,S)) . x) by A3, FUNCT_1:13;
A8: (netmap ((f * N),T)) . y = f . ((netmap (N,S)) . y) by A3, A6, FUNCT_1:13;
[x,y] in the InternalRel of (f * N) by A4, ORDERS_2:def_5;
then x9 <= y9 by A5, ORDERS_2:def_5;
then (netmap (N,S)) . x9 <= (netmap (N,S)) . y9 by A2, WAYBEL_1:def_2;
hence (netmap ((f * N),T)) . x <= (netmap ((f * N),T)) . y by A1, A7, A8, WAYBEL_1:def_2; ::_thesis: verum
end;
then netmap ((f * N),T) is monotone by WAYBEL_1:def_2;
hence f * N is monotone by WAYBEL_0:def_9; ::_thesis: verum
end;
registration
let S, T be up-complete LATTICE;
let f be monotone Function of S,T;
let N be non empty monotone NetStr over S;
clusterf * N -> monotone ;
coherence
f * N is monotone by Th18;
end;
theorem :: WAYBEL17:19
for S, T being up-complete LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)
proof
let S, T be up-complete LATTICE; ::_thesis: for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)
let f be Function of S,T; ::_thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D) )
assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: for D being non empty directed Subset of S holds sup (f .: D) = f . (sup D)
let D be non empty directed Subset of S; ::_thesis: sup (f .: D) = f . (sup D)
A2: f is monotone by A1, Th11;
then A3: sup (f .: D) <= f . (sup D) by Th16;
f . (sup D) <= sup (f .: D)
proof
sup D = lim_inf (Net-Str D) by Th10;
then A4: f . (sup D) <= lim_inf (f * (Net-Str D)) by A1;
reconsider fN = f * (Net-Str D) as reflexive monotone net of T by A2;
A5: sup fN = Sup by WAYBEL_2:def_1
.= Sup by WAYBEL_9:def_8
.= sup (rng (f * ((id the carrier of S) | D))) by YELLOW_2:def_5 ;
rng (f * ((id the carrier of S) | D)) = rng (f * (id D)) by FUNCT_3:1
.= rng (f | D) by RELAT_1:65
.= f .: D by RELAT_1:115 ;
hence f . (sup D) <= sup (f .: D) by A4, A5, Lm6; ::_thesis: verum
end;
hence sup (f .: D) = f . (sup D) by A3, ORDERS_2:2; ::_thesis: verum
end;
Lm8: for S, T being complete LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is directed-sups-preserving
proof
let S, T be complete LATTICE; ::_thesis: for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is directed-sups-preserving
let f be Function of S,T; ::_thesis: ( ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) implies f is directed-sups-preserving )
assume A1: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: f is directed-sups-preserving
thus f is directed-sups-preserving ::_thesis: verum
proof
let D be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( D is empty or not D is directed or f preserves_sup_of D )
assume ( not D is empty & D is directed ) ; ::_thesis: f preserves_sup_of D
then reconsider D = D as non empty directed Subset of S ;
A2: f is monotone by A1, Th11;
then A3: sup (f .: D) <= f . (sup D) by Th15;
A4: f . (sup D) <= sup (f .: D)
proof
sup D = lim_inf (Net-Str D) by Th10;
then A5: f . (sup D) <= lim_inf (f * (Net-Str D)) by A1;
reconsider fN = f * (Net-Str D) as reflexive monotone net of T by A2;
A6: sup fN = Sup by WAYBEL_2:def_1
.= Sup by WAYBEL_9:def_8
.= sup (rng (f * ((id the carrier of S) | D))) by YELLOW_2:def_5 ;
rng (f * ((id the carrier of S) | D)) = rng (f * (id D)) by FUNCT_3:1
.= rng (f | D) by RELAT_1:65
.= f .: D by RELAT_1:115 ;
hence f . (sup D) <= sup (f .: D) by A5, A6, WAYBEL11:22; ::_thesis: verum
end;
f preserves_sup_of D
proof
assume ex_sup_of D,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: D,T & "\/" ((f .: D),T) = f . ("\/" (D,S)) )
thus ( ex_sup_of f .: D,T & "\/" ((f .: D),T) = f . ("\/" (D,S)) ) by A3, A4, ORDERS_2:2, YELLOW_0:17; ::_thesis: verum
end;
hence f preserves_sup_of D ; ::_thesis: verum
end;
end;
theorem Th20: :: WAYBEL17:20
for S, T being complete LATTICE
for f being Function of S,T
for N being net of S
for j being Element of N
for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
proof
let S, T be complete LATTICE; ::_thesis: for f being Function of S,T
for N being net of S
for j being Element of N
for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let f be Function of S,T; ::_thesis: for N being net of S
for j being Element of N
for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let N be net of S; ::_thesis: for j being Element of N
for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let j be Element of N; ::_thesis: for j9 being Element of (f * N) st j9 = j & f is monotone holds
f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
let j9 be Element of (f * N); ::_thesis: ( j9 = j & f is monotone implies f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T) )
assume A1: j9 = j ; ::_thesis: ( not f is monotone or f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T) )
assume A2: f is monotone ; ::_thesis: f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T)
A3: dom f = the carrier of S by FUNCT_2:def_1;
A4: RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def_8;
A5: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
A6: { ((f * N) . l) where l is Element of (f * N) : l >= j9 } c= f .: { (N . l1) where l1 is Element of N : l1 >= j }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } or s in f .: { (N . l1) where l1 is Element of N : l1 >= j } )
assume s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ; ::_thesis: s in f .: { (N . l1) where l1 is Element of N : l1 >= j }
then consider x being Element of (f * N) such that
A7: s = (f * N) . x and
A8: x >= j9 ;
reconsider x = x as Element of N by A4;
[j9,x] in the InternalRel of (f * N) by A8, ORDERS_2:def_5;
then A9: x >= j by A1, A4, ORDERS_2:def_5;
A10: s = (f * the mapping of N) . x by A7, WAYBEL_9:def_8
.= f . (N . x) by A5, FUNCT_1:13 ;
N . x in { (N . z) where z is Element of N : z >= j } by A9;
hence s in f .: { (N . l1) where l1 is Element of N : l1 >= j } by A3, A10, FUNCT_1:def_6; ::_thesis: verum
end;
A11: f .: { (N . l1) where l1 is Element of N : l1 >= j } c= { ((f * N) . l) where l is Element of (f * N) : l >= j9 }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in f .: { (N . l1) where l1 is Element of N : l1 >= j } or s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } )
assume s in f .: { (N . l1) where l1 is Element of N : l1 >= j } ; ::_thesis: s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 }
then consider x being set such that
x in dom f and
A12: x in { (N . l1) where l1 is Element of N : l1 >= j } and
A13: s = f . x by FUNCT_1:def_6;
consider l2 being Element of N such that
A14: x = N . l2 and
A15: l2 >= j by A12;
reconsider l29 = l2 as Element of (f * N) by A4;
A16: s = (f * the mapping of N) . l2 by A5, A13, A14, FUNCT_1:13
.= (f * N) . l29 by WAYBEL_9:def_8 ;
[j,l2] in the InternalRel of N by A15, ORDERS_2:def_5;
then l29 >= j9 by A1, A4, ORDERS_2:def_5;
hence s in { ((f * N) . l) where l is Element of (f * N) : l >= j9 } by A16; ::_thesis: verum
end;
set K = { (N . k) where k is Element of N : k >= j } ;
{ (N . k) where k is Element of N : k >= j } c= the carrier of S
proof
let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in { (N . k) where k is Element of N : k >= j } or r in the carrier of S )
assume r in { (N . k) where k is Element of N : k >= j } ; ::_thesis: r in the carrier of S
then ex f being Element of N st
( r = N . f & f >= j ) ;
hence r in the carrier of S ; ::_thesis: verum
end;
then reconsider K = { (N . k) where k is Element of N : k >= j } as Subset of S ;
{ ((f * N) . l) where l is Element of (f * N) : l >= j9 } = f .: K by A6, A11, XBOOLE_0:def_10;
hence f . ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) <= "/\" ( { ((f * N) . l) where l is Element of (f * N) : l >= j9 } ,T) by A2, Lm7; ::_thesis: verum
end;
Lm9: for S, T being complete Scott TopLattice
for f being continuous Function of S,T
for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
proof
let S, T be complete Scott TopLattice; ::_thesis: for f being continuous Function of S,T
for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
let f be continuous Function of S,T; ::_thesis: for N being net of S holds f . (lim_inf N) <= lim_inf (f * N)
let N be net of S; ::_thesis: f . (lim_inf N) <= lim_inf (f * N)
set x = lim_inf N;
set t = lim_inf (f * N);
A1: [#] T <> {} ;
assume not f . (lim_inf N) <= lim_inf (f * N) ; ::_thesis: contradiction
then not f . (lim_inf N) in downarrow (lim_inf (f * N)) by WAYBEL_0:17;
then A2: f . (lim_inf N) in (downarrow (lim_inf (f * N))) ` by XBOOLE_0:def_5;
A3: downarrow (lim_inf (f * N)) is closed by Lm3;
set U1 = f " ((downarrow (lim_inf (f * N))) `);
A4: f " ((downarrow (lim_inf (f * N))) `) is open by A1, A3, TOPS_2:43;
set D = { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } ;
now__::_thesis:_for_f_being_set_st_f_in__{__("/\"_(_{__(N_._k)_where_k_is_Element_of_N_:_k_>=_j__}__,S))_where_j_is_Element_of_N_:_verum__}__holds_
f_in_the_carrier_of_S
let f be set ; ::_thesis: ( f in { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } implies f in the carrier of S )
assume f in { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } ; ::_thesis: f in the carrier of S
then ex j being Element of N st f = "/\" ( { (N . k) where k is Element of N : k >= j } ,S) ;
hence f in the carrier of S ; ::_thesis: verum
end;
then reconsider D = { ("/\" ( { (N . k) where k is Element of N : k >= j } ,S)) where j is Element of N : verum } as Subset of S by TARSKI:def_3;
reconsider D = D as non empty directed Subset of S by WAYBEL11:30;
A5: lim_inf N in f " ((downarrow (lim_inf (f * N))) `) by A2, FUNCT_2:38;
f " ((downarrow (lim_inf (f * N))) `) is property(S) by A4, WAYBEL11:15;
then consider y being Element of S such that
A6: y in D and
A7: for x being Element of S st x in D & x >= y holds
x in f " ((downarrow (lim_inf (f * N))) `) by A5, WAYBEL11:def_3;
consider j being Element of N such that
A8: y = "/\" ( { (N . k) where k is Element of N : k >= j } ,S) by A6;
y <= y ;
then A9: y in f " ((downarrow (lim_inf (f * N))) `) by A6, A7;
RelStr(# the carrier of (f * N), the InternalRel of (f * N) #) = RelStr(# the carrier of N, the InternalRel of N #) by WAYBEL_9:def_8;
then reconsider j9 = j as Element of (f * N) ;
A10: dom f = the carrier of S by FUNCT_2:def_1;
set fy = "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T);
set fD = { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } ;
now__::_thesis:_for_g_being_set_st_g_in__{__("/\"_(_{__((f_*_N)_._k)_where_k_is_Element_of_(f_*_N)_:_k_>=_j1__}__,T))_where_j1_is_Element_of_(f_*_N)_:_verum__}__holds_
g_in_the_carrier_of_T
let g be set ; ::_thesis: ( g in { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } implies g in the carrier of T )
assume g in { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } ; ::_thesis: g in the carrier of T
then ex j being Element of (f * N) st g = "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j } ,T) ;
hence g in the carrier of T ; ::_thesis: verum
end;
then reconsider fD = { ("/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j1 } ,T)) where j1 is Element of (f * N) : verum } as Subset of T by TARSKI:def_3;
A11: f . y <= "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) by A8, Th20;
"/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) in fD ;
then "/\" ( { ((f * N) . k) where k is Element of (f * N) : k >= j9 } ,T) <= sup fD by YELLOW_2:22;
then f . y <= lim_inf (f * N) by A11, ORDERS_2:3;
then f . y in downarrow (lim_inf (f * N)) by WAYBEL_0:17;
then A12: y in f " (downarrow (lim_inf (f * N))) by A10, FUNCT_1:def_7;
f " ((downarrow (lim_inf (f * N))) `) = (f " ([#] T)) \ (f " (downarrow (lim_inf (f * N)))) by FUNCT_1:69
.= ([#] S) \ (f " (downarrow (lim_inf (f * N)))) by TOPS_2:41
.= (f " (downarrow (lim_inf (f * N)))) ` ;
then A13: y in (f " ((downarrow (lim_inf (f * N))) `)) /\ ((f " ((downarrow (lim_inf (f * N))) `)) `) by A9, A12, XBOOLE_0:def_4;
f " ((downarrow (lim_inf (f * N))) `) misses (f " ((downarrow (lim_inf (f * N))) `)) ` by XBOOLE_1:79;
hence contradiction by A13, XBOOLE_0:4; ::_thesis: verum
end;
Lm10: for L being continuous Scott TopLattice
for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
proof
let L be continuous Scott TopLattice; ::_thesis: for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
let p be Element of L; ::_thesis: for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
let S be Subset of L; ::_thesis: ( S is open & p in S implies ex q being Element of L st
( q << p & q in S ) )
assume that
A1: S is open and
A2: p in S ; ::_thesis: ex q being Element of L st
( q << p & q in S )
A3: S is inaccessible by A1, WAYBEL11:def_4;
sup (waybelow p) = p by WAYBEL_3:def_5;
then waybelow p meets S by A2, A3, WAYBEL11:def_1;
then (waybelow p) /\ S <> {} by XBOOLE_0:def_7;
then consider u being set such that
A4: u in (waybelow p) /\ S by XBOOLE_0:def_1;
A5: u in waybelow p by A4, XBOOLE_0:def_4;
reconsider u = u as Element of L by A4;
take u ; ::_thesis: ( u << p & u in S )
thus u << p by A5, WAYBEL_3:7; ::_thesis: u in S
thus u in S by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
Lm11: for L being lower-bounded continuous Scott TopLattice
for x being Element of L holds wayabove x is open
proof
let L be lower-bounded continuous Scott TopLattice; ::_thesis: for x being Element of L holds wayabove x is open
let x be Element of L; ::_thesis: wayabove x is open
set W = wayabove x;
wayabove x is inaccessible
proof
let D be non empty directed Subset of L; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,L) in wayabove x or not D misses wayabove x )
assume sup D in wayabove x ; ::_thesis: not D misses wayabove x
then x << sup D by WAYBEL_3:8;
then consider d being Element of L such that
A1: d in D and
A2: x << d by WAYBEL_4:53;
d in wayabove x by A2;
hence not D misses wayabove x by A1, XBOOLE_0:3; ::_thesis: verum
end;
hence wayabove x is open by WAYBEL11:def_4; ::_thesis: verum
end;
Lm12: for L being lower-bounded continuous Scott TopLattice
for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of
proof
let L be lower-bounded continuous Scott TopLattice; ::_thesis: for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of
let p be Element of L; ::_thesis: { (wayabove q) where q is Element of L : q << p } is Basis of
set X = { (wayabove q) where q is Element of L : q << p } ;
{ (wayabove q) where q is Element of L : q << p } c= bool the carrier of L
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove q) where q is Element of L : q << p } or e in bool the carrier of L )
assume e in { (wayabove q) where q is Element of L : q << p } ; ::_thesis: e in bool the carrier of L
then ex q being Element of L st
( e = wayabove q & q << p ) ;
hence e in bool the carrier of L ; ::_thesis: verum
end;
then reconsider X = { (wayabove q) where q is Element of L : q << p } as Subset-Family of L ;
X is Basis of
proof
A1: X is open
proof
let e be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not e in X or e is open )
assume e in X ; ::_thesis: e is open
then consider q being Element of L such that
A2: e = wayabove q and
q << p ;
wayabove q is open by Lm11;
hence e is open by A2; ::_thesis: verum
end;
X is p -quasi_basis
proof
for Y being set st Y in X holds
p in Y
proof
let e be set ; ::_thesis: ( e in X implies p in e )
assume e in X ; ::_thesis: p in e
then ex q being Element of L st
( e = wayabove q & q << p ) ;
hence p in e ; ::_thesis: verum
end;
hence p in Intersect X by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of K32( the carrier of L) holds
( not b1 is open or not p in b1 or ex b2 being Element of K32( the carrier of L) st
( b2 in X & b2 c= b1 ) )
let S be Subset of L; ::_thesis: ( not S is open or not p in S or ex b1 being Element of K32( the carrier of L) st
( b1 in X & b1 c= S ) )
assume that
A3: S is open and
A4: p in S ; ::_thesis: ex b1 being Element of K32( the carrier of L) st
( b1 in X & b1 c= S )
consider u being Element of L such that
A5: u << p and
A6: u in S by A3, A4, Lm10;
take V = wayabove u; ::_thesis: ( V in X & V c= S )
thus V in X by A5; ::_thesis: V c= S
A7: S is upper by A3, WAYBEL11:def_4;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
uparrow u c= S by A6, A7, WAYBEL11:42;
hence V c= S by A8, XBOOLE_1:1; ::_thesis: verum
end;
hence X is Basis of by A1; ::_thesis: verum
end;
hence { (wayabove q) where q is Element of L : q << p } is Basis of ; ::_thesis: verum
end;
Lm13: for T being lower-bounded continuous Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T
proof
let T be lower-bounded continuous Scott TopLattice; ::_thesis: { (wayabove x) where x is Element of T : verum } is Basis of T
set B = { (wayabove x) where x is Element of T : verum } ;
A1: { (wayabove x) where x is Element of T : verum } c= the topology of T
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove x) where x is Element of T : verum } or e in the topology of T )
assume e in { (wayabove x) where x is Element of T : verum } ; ::_thesis: e in the topology of T
then consider x being Element of T such that
A2: e = wayabove x ;
wayabove x is open by Lm11;
hence e in the topology of T by A2, PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider P = { (wayabove x) where x is Element of T : verum } as Subset-Family of T by XBOOLE_1:1;
for x being Point of T ex B being Basis of st B c= P
proof
let x be Point of T; ::_thesis: ex B being Basis of st B c= P
reconsider p = x as Element of T ;
reconsider A = { (wayabove q) where q is Element of T : q << p } as Basis of by Lm12;
take A ; ::_thesis: A c= P
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in A or u in P )
assume u in A ; ::_thesis: u in P
then ex q being Element of T st
( u = wayabove q & q << p ) ;
hence u in P ; ::_thesis: verum
end;
hence { (wayabove x) where x is Element of T : verum } is Basis of T by A1, YELLOW_8:14; ::_thesis: verum
end;
Lm14: for T being lower-bounded continuous Scott TopLattice
for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }
proof
let T be lower-bounded continuous Scott TopLattice; ::_thesis: for S being Subset of T holds Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }
let S be Subset of T; ::_thesis: Int S = union { (wayabove x) where x is Element of T : wayabove x c= S }
set B = { (wayabove x) where x is Element of T : verum } ;
set I = { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ;
set P = { (wayabove x) where x is Element of T : wayabove x c= S } ;
A1: { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } = { (wayabove x) where x is Element of T : wayabove x c= S }
proof
thus { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } c= { (wayabove x) where x is Element of T : wayabove x c= S } :: according to XBOOLE_0:def_10 ::_thesis: { (wayabove x) where x is Element of T : wayabove x c= S } c= { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } or e in { (wayabove x) where x is Element of T : wayabove x c= S } )
assume e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } ; ::_thesis: e in { (wayabove x) where x is Element of T : wayabove x c= S }
then consider G being Subset of T such that
A2: e = G and
A3: G in { (wayabove x) where x is Element of T : verum } and
A4: G c= S ;
ex x being Element of T st G = wayabove x by A3;
hence e in { (wayabove x) where x is Element of T : wayabove x c= S } by A2, A4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (wayabove x) where x is Element of T : wayabove x c= S } or e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } )
assume e in { (wayabove x) where x is Element of T : wayabove x c= S } ; ::_thesis: e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) }
then consider x being Element of T such that
A5: e = wayabove x and
A6: wayabove x c= S ;
wayabove x in { (wayabove x) where x is Element of T : verum } ;
hence e in { G where G is Subset of T : ( G in { (wayabove x) where x is Element of T : verum } & G c= S ) } by A5, A6; ::_thesis: verum
end;
{ (wayabove x) where x is Element of T : verum } is Basis of T by Lm13;
hence Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } by A1, YELLOW_8:11; ::_thesis: verum
end;
Lm15: for S, T being lower-bounded continuous Scott TopLattice
for f being Function of S,T st ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
f is continuous
proof
let S, T be lower-bounded continuous Scott TopLattice; ::_thesis: for f being Function of S,T st ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
f is continuous
let f be Function of S,T; ::_thesis: ( ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) implies f is continuous )
assume A1: for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ; ::_thesis: f is continuous
A2: [#] T <> {} ;
now__::_thesis:_for_U1_being_Subset_of_T_st_U1_is_open_holds_
f_"_U1_is_open
let U1 be Subset of T; ::_thesis: ( U1 is open implies f " U1 is open )
assume A3: U1 is open ; ::_thesis: f " U1 is open
set U19 = U1;
A4: U1 is upper by A3, WAYBEL11:def_4;
reconsider fU = f " U1 as Subset of S ;
A5: Int fU c= fU by TOPS_1:16;
fU c= Int fU
proof
let xx be set ; :: according to TARSKI:def_3 ::_thesis: ( not xx in fU or xx in Int fU )
assume A6: xx in fU ; ::_thesis: xx in Int fU
then reconsider x = xx as Element of S ;
A7: f . x in U1 by A6, FUNCT_1:def_7;
reconsider p = f . x as Element of T ;
consider u being Element of T such that
A8: u << p and
A9: u in U1 by A3, A7, Lm10;
consider w being Element of S such that
A10: w << x and
A11: u << f . w by A1, A8;
f .: (wayabove w) c= U1
proof
let h be set ; :: according to TARSKI:def_3 ::_thesis: ( not h in f .: (wayabove w) or h in U1 )
assume h in f .: (wayabove w) ; ::_thesis: h in U1
then consider z being set such that
A12: z in dom f and
A13: z in wayabove w and
A14: h = f . z by FUNCT_1:def_6;
reconsider z = z as Element of S by A12;
w << z by A13, WAYBEL_3:8;
then u << f . z by A1, A11;
then u <= f . z by WAYBEL_3:1;
hence h in U1 by A4, A9, A14, WAYBEL_0:def_20; ::_thesis: verum
end;
then A15: f " (f .: (wayabove w)) c= f " U1 by RELAT_1:143;
wayabove w c= f " (f .: (wayabove w)) by FUNCT_2:42;
then A16: wayabove w c= f " U1 by A15, XBOOLE_1:1;
A17: Int fU = union { (wayabove g) where g is Element of S : wayabove g c= fU } by Lm14;
A18: x in wayabove w by A10;
wayabove w in { (wayabove g) where g is Element of S : wayabove g c= fU } by A16;
hence xx in Int fU by A17, A18, TARSKI:def_4; ::_thesis: verum
end;
hence f " U1 is open by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
hence f is continuous by A2, TOPS_2:43; ::_thesis: verum
end;
begin
theorem :: WAYBEL17:21
for S, T being complete Scott TopLattice
for f being Function of S,T holds
( f is continuous iff for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) by Lm4, Lm8, Lm9;
theorem Th22: :: WAYBEL17:22
for S, T being complete Scott TopLattice
for f being Function of S,T holds
( f is continuous iff f is directed-sups-preserving )
proof
let S, T be complete Scott TopLattice; ::_thesis: for f being Function of S,T holds
( f is continuous iff f is directed-sups-preserving )
let f be Function of S,T; ::_thesis: ( f is continuous iff f is directed-sups-preserving )
thus ( f is continuous implies f is directed-sups-preserving ) ::_thesis: ( f is directed-sups-preserving implies f is continuous )
proof
assume f is continuous ; ::_thesis: f is directed-sups-preserving
then for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) by Lm9;
hence f is directed-sups-preserving by Lm8; ::_thesis: verum
end;
thus ( f is directed-sups-preserving implies f is continuous ) by Lm4; ::_thesis: verum
end;
registration
let S, T be complete Scott TopLattice;
cluster Function-like quasi_total continuous -> directed-sups-preserving for Element of K32(K33( the carrier of S, the carrier of T));
coherence
for b1 being Function of S,T st b1 is continuous holds
b1 is directed-sups-preserving by Th22;
cluster Function-like quasi_total directed-sups-preserving -> continuous for Element of K32(K33( the carrier of S, the carrier of T));
coherence
for b1 being Function of S,T st b1 is directed-sups-preserving holds
b1 is continuous by Th22;
end;
Lm16: for S, T being complete continuous Scott TopLattice
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
f is directed-sups-preserving
proof
let S, T be complete continuous Scott TopLattice; ::_thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
f is directed-sups-preserving
let f be 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) ) implies f is directed-sups-preserving )
assume for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: f is directed-sups-preserving
then for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) by Th14;
then f is continuous by Lm15;
hence f is directed-sups-preserving ; ::_thesis: verum
end;
theorem Th23: :: WAYBEL17:23
for S, T being complete continuous Scott TopLattice
for f being Function of S,T holds
( f is continuous iff for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
proof
let S, T be complete continuous Scott TopLattice; ::_thesis: for f being Function of S,T holds
( f is continuous iff for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
let f be Function of S,T; ::_thesis: ( f is continuous iff for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
hereby ::_thesis: ( ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) implies f is continuous )
assume f is continuous ; ::_thesis: for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by Th12;
hence for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) by Th14; ::_thesis: verum
end;
thus ( ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) implies f is continuous ) by Lm15; ::_thesis: verum
end;
theorem Th24: :: WAYBEL17:24
for S, T being complete continuous Scott TopLattice
for f being Function of S,T holds
( f is continuous iff 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 complete continuous Scott TopLattice; ::_thesis: for f being Function of S,T holds
( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )
let f be Function of S,T; ::_thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )
thus ( f is continuous implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) by Th12; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is continuous )
assume for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: f is continuous
then f is directed-sups-preserving by Lm16;
hence f is continuous ; ::_thesis: verum
end;
Lm17: for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
proof
let S, T be complete Scott TopLattice; ::_thesis: for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) holds
for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
let f be Function of S,T; ::_thesis: ( S is algebraic & T is algebraic & ( for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ) implies for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
assume that
A1: S is algebraic and
A2: T is algebraic ; ::_thesis: ( ex x being Element of S ex y being Element of T st
( ( y << f . x implies ex w being Element of S st
( w << x & y << f . w ) ) implies ( ex w being Element of S st
( w << x & y << f . w ) & not y << f . x ) ) or for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
A3: S is continuous by A1, WAYBEL_8:7;
A4: T is continuous by A2, WAYBEL_8:7;
assume A5: for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) ; ::_thesis: for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
then A6: f is continuous by A3, A4, Th23;
let x be Element of S; ::_thesis: for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
let k be Element of T; ::_thesis: ( k in the carrier of (CompactSublatt T) implies ( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
assume A7: k in the carrier of (CompactSublatt T) ; ::_thesis: ( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
hereby ::_thesis: ( ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) implies k <= f . x )
assume k <= f . x ; ::_thesis: ex w1 being Element of S st
( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 )
then k << f . x by A7, WAYBEL_8:1;
then consider w being Element of S such that
A8: w << x and
A9: k << f . w by A5;
consider w1 being Element of S such that
A10: w1 in the carrier of (CompactSublatt S) and
A11: w <= w1 and
A12: w1 <= x by A1, A8, WAYBEL_8:7;
A13: k <= f . w by A9, WAYBEL_3:1;
take w1 = w1; ::_thesis: ( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 )
thus w1 in the carrier of (CompactSublatt S) by A10; ::_thesis: ( w1 <= x & k <= f . w1 )
thus w1 <= x by A12; ::_thesis: k <= f . w1
f . w <= f . w1 by A6, A11, WAYBEL_1:def_2;
hence k <= f . w1 by A13, ORDERS_2:3; ::_thesis: verum
end;
given j being Element of S such that j in the carrier of (CompactSublatt S) and
A14: j <= x and
A15: k <= f . j ; ::_thesis: k <= f . x
f is continuous by A3, A4, A5, Lm15;
then f . j <= f . x by A14, WAYBEL_1:def_2;
hence k <= f . x by A15, ORDERS_2:3; ::_thesis: verum
end;
Lm18: for S, T being complete Scott TopLattice
for f being Function of S,T st T is algebraic & ( for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
proof
let S, T be complete Scott TopLattice; ::_thesis: for f being Function of S,T st T is algebraic & ( for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let f be Function of S,T; ::_thesis: ( T is algebraic & ( for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) implies for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
assume A1: T is algebraic ; ::_thesis: ( ex x being Element of S ex k being Element of T st
( k in the carrier of (CompactSublatt T) & not ( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) or for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
assume A2: for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ; ::_thesis: for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let x be Element of S; ::_thesis: for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let y be Element of T; ::_thesis: ( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
hereby ::_thesis: ( ex w being Element of S st
( w << x & y << f . w ) implies y << f . x )
assume y << f . x ; ::_thesis: ex j being Element of S st
( j << x & y << f . j )
then consider w being Element of T such that
A3: w in the carrier of (CompactSublatt T) and
A4: y <= w and
A5: w <= f . x by A1, WAYBEL_8:7;
consider j being Element of S such that
A6: j in the carrier of (CompactSublatt S) and
A7: j <= x and
A8: w <= f . j by A2, A3, A5;
take j = j; ::_thesis: ( j << x & y << f . j )
thus j << x by A6, A7, WAYBEL_8:1; ::_thesis: y << f . j
thus y << f . j by A3, A4, A8, WAYBEL_8:1; ::_thesis: verum
end;
given w being Element of S such that A9: w << x and
A10: y << f . w ; ::_thesis: y << f . x
consider h being Element of T such that
A11: h in the carrier of (CompactSublatt T) and
A12: y <= h and
A13: h <= f . w by A1, A10, WAYBEL_8:7;
consider j being Element of S such that
A14: j in the carrier of (CompactSublatt S) and
A15: j <= w and
A16: h <= f . j by A2, A11, A13;
j << x by A9, A15, WAYBEL_3:2;
then j <= x by WAYBEL_3:1;
then h <= f . x by A2, A11, A14, A16;
hence y << f . x by A11, A12, WAYBEL_8:1; ::_thesis: verum
end;
Lm19: for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
proof
let S, T be complete Scott TopLattice; ::_thesis: for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
let f be Function of S,T; ::_thesis: ( S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )
assume that
A1: S is algebraic and
A2: T is algebraic ; ::_thesis: ( ex x being Element of S st not f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) or for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )
A3: S is continuous by A1, WAYBEL_8:7;
A4: T is continuous by A2, WAYBEL_8:7;
assume A5: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
let x be Element of S; ::_thesis: f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
A6: the carrier of S c= dom f by FUNCT_2:def_1;
defpred S1[ Element of S] means ( $1 <= x & $1 is compact );
deffunc H1( Element of S) -> Element of S = $1;
A7: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_1(A6);
A8: f .: { w where w is Element of S : ( w <= x & w is compact ) } = f .: (compactbelow x) by WAYBEL_8:def_2;
reconsider D = compactbelow x as non empty directed Subset of S by A1, WAYBEL_8:def_4;
f is directed-sups-preserving by A3, A4, A5, Lm16;
then A9: f preserves_sup_of D by WAYBEL_0:def_37;
A10: ex_sup_of D,S by YELLOW_0:17;
S is satisfying_axiom_K by A1, WAYBEL_8:def_4;
then f . x = f . (sup D) by WAYBEL_8:def_3
.= "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A7, A8, A9, A10, WAYBEL_0:def_31 ;
hence f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: verum
end;
theorem Th25: :: WAYBEL17:25
for S being LATTICE
for T being complete LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds
f is monotone
proof
let S be LATTICE; ::_thesis: for T being complete LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds
f is monotone
let T be complete LATTICE; ::_thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds
f is monotone
let f be Function of S,T; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) implies f is monotone )
assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: f is monotone
thus f is monotone ::_thesis: verum
proof
let X, Y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not X <= Y or f . X <= f . Y )
assume X <= Y ; ::_thesis: f . X <= f . Y
then A2: compactbelow X c= compactbelow Y by WAYBEL13:1;
A3: f . X = "\/" ( { (f . w) where w is Element of S : ( w <= X & w is compact ) } ,T) by A1;
A4: f . Y = "\/" ( { (f . w) where w is Element of S : ( w <= Y & w is compact ) } ,T) by A1;
A5: the carrier of S c= dom f by FUNCT_2:def_1;
defpred S1[ Element of S] means ( $1 <= X & $1 is compact );
defpred S2[ Element of S] means ( $1 <= Y & $1 is compact );
deffunc H1( Element of S) -> Element of S = $1;
f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL17:sch_2(A5);
then A6: f . X = "\/" ((f .: (compactbelow X)),T) by A3, WAYBEL_8:def_2;
f .: { H1(w) where w is Element of S : S2[w] } = { (f . H1(w)) where w is Element of S : S2[w] } from WAYBEL17:sch_2(A5);
then A7: f . Y = "\/" ((f .: (compactbelow Y)),T) by A4, WAYBEL_8:def_2;
A8: ex_sup_of f .: (compactbelow X),T by YELLOW_0:17;
ex_sup_of f .: (compactbelow Y),T by YELLOW_0:17;
hence f . X <= f . Y by A2, A6, A7, A8, RELAT_1:123, YELLOW_0:34; ::_thesis: verum
end;
end;
theorem Th26: :: WAYBEL17:26
for S, T being complete Scott TopLattice
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds
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 complete Scott TopLattice; ::_thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) holds
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)
let f be Function of S,T; ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )
assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)
then A2: f is monotone by Th25;
let x be Element of S; ::_thesis: f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)
A3: f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A1;
set FW = { (f . w) where w is Element of S : ( w <= x & w is compact ) } ;
set FX = { (f . w) where w is Element of S : w << x } ;
set fx = f . x;
A4: { (f . w) where w is Element of S : ( w <= x & w is compact ) } c= { (f . w) where w is Element of S : w << x }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f . w) where w is Element of S : ( w <= x & w is compact ) } or a in { (f . w) where w is Element of S : w << x } )
assume a in { (f . w) where w is Element of S : ( w <= x & w is compact ) } ; ::_thesis: a in { (f . w) where w is Element of S : w << x }
then consider w being Element of S such that
A5: a = f . w and
A6: w <= x and
A7: w is compact ;
w << w by A7, WAYBEL_3:def_2;
then w << x by A6, WAYBEL_3:2;
hence a in { (f . w) where w is Element of S : w << x } by A5; ::_thesis: verum
end;
A8: f . x is_>=_than { (f . w) where w is Element of S : w << x }
proof
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in { (f . w) where w is Element of S : w << x } or b <= f . x )
assume b in { (f . w) where w is Element of S : w << x } ; ::_thesis: b <= f . x
then consider ww being Element of S such that
A9: b = f . ww and
A10: ww << x ;
ww <= x by A10, WAYBEL_3:1;
hence b <= f . x by A2, A9, WAYBEL_1:def_2; ::_thesis: verum
end;
for b being Element of T st b is_>=_than { (f . w) where w is Element of S : w << x } holds
f . x <= b
proof
let b be Element of T; ::_thesis: ( b is_>=_than { (f . w) where w is Element of S : w << x } implies f . x <= b )
assume b is_>=_than { (f . w) where w is Element of S : w << x } ; ::_thesis: f . x <= b
then b is_>=_than { (f . w) where w is Element of S : ( w <= x & w is compact ) } by A4, YELLOW_0:9;
hence f . x <= b by A3, YELLOW_0:32; ::_thesis: verum
end;
hence f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A8, YELLOW_0:30; ::_thesis: verum
end;
theorem :: WAYBEL17:27
for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic & T is algebraic holds
( f is continuous iff for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
proof
let S, T be complete Scott TopLattice; ::_thesis: for f being Function of S,T st S is algebraic & T is algebraic holds
( f is continuous iff for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
let f be Function of S,T; ::_thesis: ( S is algebraic & T is algebraic implies ( f is continuous iff for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) )
assume that
A1: S is algebraic and
A2: T is algebraic ; ::_thesis: ( f is continuous iff for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )
A3: S is continuous by A1, WAYBEL_8:7;
A4: T is continuous by A2, WAYBEL_8:7;
hereby ::_thesis: ( ( for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) implies f is continuous )
assume f is continuous ; ::_thesis: for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )
then for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) by A3, A4, Th23;
hence for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) by A1, A2, Lm17; ::_thesis: verum
end;
assume for x being Element of S
for k being Element of T st k in the carrier of (CompactSublatt T) holds
( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ; ::_thesis: f is continuous
then for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) by A2, Lm18;
hence f is continuous by A3, A4, Th23; ::_thesis: verum
end;
theorem :: WAYBEL17:28
for S, T being complete Scott TopLattice
for f being Function of S,T st S is algebraic & T is algebraic holds
( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )
proof
let S, T be complete Scott TopLattice; ::_thesis: for f being Function of S,T st S is algebraic & T is algebraic holds
( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )
let f be Function of S,T; ::_thesis: ( S is algebraic & T is algebraic implies ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) )
assume that
A1: S is algebraic and
A2: T is algebraic ; ::_thesis: ( f is continuous iff for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )
A3: S is continuous by A1, WAYBEL_8:7;
A4: T is continuous by A2, WAYBEL_8:7;
hereby ::_thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ) implies f is continuous )
assume f is continuous ; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)
then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A3, A4, Th24;
hence for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A1, A2, Lm19; ::_thesis: verum
end;
assume for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; ::_thesis: f is continuous
then for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by Th26;
hence f is continuous by A3, A4, Th24; ::_thesis: verum
end;
theorem :: WAYBEL17:29
for S, T being non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott TopRelStr
for f being Function of S,T st f is directed-sups-preserving holds
f is continuous by Lm4;