:: WAYBEL11 semantic presentation
begin
Lm1: for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
proof
let R, S be RelStr ; ::_thesis: for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p, q be Element of R; ::_thesis: for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p9, q9 be Element of S; ::_thesis: ( p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q implies p9 <= q9 )
assume that
A1: p = p9 and
A2: q = q9 and
A3: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) ; ::_thesis: ( not p <= q or p9 <= q9 )
assume p <= q ; ::_thesis: p9 <= q9
then [p9,q9] in the InternalRel of S by A1, A2, A3, ORDERS_2:def_5;
hence p9 <= q9 by ORDERS_2:def_5; ::_thesis: verum
end;
scheme :: WAYBEL11:sch 1
Irrel{ F1() -> non empty set , F2() -> non empty set , P1[ set ], F3( set ) -> set , F4( set , set ) -> set } :
{ F3(u) where u is Element of F1() : P1[u] } = { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] }
provided
A1: for i being Element of F2()
for u being Element of F1() holds F3(u) = F4(i,u)
proof
set A = { F3(u) where u is Element of F1() : P1[u] } ;
set B = { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } ;
thus { F3(u) where u is Element of F1() : P1[u] } c= { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } :: according to XBOOLE_0:def_10 ::_thesis: { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } c= { F3(u) where u is Element of F1() : P1[u] }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { F3(u) where u is Element of F1() : P1[u] } or e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } )
set i = the Element of F2();
assume e in { F3(u) where u is Element of F1() : P1[u] } ; ::_thesis: e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] }
then consider u being Element of F1() such that
A2: e = F3(u) and
A3: P1[u] ;
e = F4( the Element of F2(),u) by A1, A2;
hence e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } by A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } or e in { F3(u) where u is Element of F1() : P1[u] } )
assume e in { F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v] } ; ::_thesis: e in { F3(u) where u is Element of F1() : P1[u] }
then consider i being Element of F2(), u being Element of F1() such that
A4: e = F4(i,u) and
A5: P1[u] ;
e = F3(u) by A1, A4;
hence e in { F3(u) where u is Element of F1() : P1[u] } by A5; ::_thesis: verum
end;
theorem Th1: :: WAYBEL11:1
for L being complete LATTICE
for X, Y being Subset of L st Y is_coarser_than X holds
"/\" (X,L) <= "/\" (Y,L)
proof
let L be complete LATTICE; ::_thesis: for X, Y being Subset of L st Y is_coarser_than X holds
"/\" (X,L) <= "/\" (Y,L)
let X, Y be Subset of L; ::_thesis: ( Y is_coarser_than X implies "/\" (X,L) <= "/\" (Y,L) )
assume A1: Y is_coarser_than X ; ::_thesis: "/\" (X,L) <= "/\" (Y,L)
"/\" (X,L) is_<=_than Y
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in Y or "/\" (X,L) <= y )
assume y in Y ; ::_thesis: "/\" (X,L) <= y
then consider x being Element of L such that
A2: x in X and
A3: x <= y by A1, YELLOW_4:def_2;
"/\" (X,L) <= x by A2, YELLOW_2:22;
hence "/\" (X,L) <= y by A3, YELLOW_0:def_2; ::_thesis: verum
end;
hence "/\" (X,L) <= "/\" (Y,L) by YELLOW_0:33; ::_thesis: verum
end;
theorem Th2: :: WAYBEL11:2
for L being complete LATTICE
for X, Y being Subset of L st X is_finer_than Y holds
"\/" (X,L) <= "\/" (Y,L)
proof
let L be complete LATTICE; ::_thesis: for X, Y being Subset of L st X is_finer_than Y holds
"\/" (X,L) <= "\/" (Y,L)
let X, Y be Subset of L; ::_thesis: ( X is_finer_than Y implies "\/" (X,L) <= "\/" (Y,L) )
assume A1: X is_finer_than Y ; ::_thesis: "\/" (X,L) <= "\/" (Y,L)
"\/" (Y,L) is_>=_than X
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= "\/" (Y,L) )
assume x in X ; ::_thesis: x <= "\/" (Y,L)
then consider y being Element of L such that
A2: y in Y and
A3: x <= y by A1, YELLOW_4:def_1;
"\/" (Y,L) >= y by A2, YELLOW_2:22;
hence x <= "\/" (Y,L) by A3, YELLOW_0:def_2; ::_thesis: verum
end;
hence "\/" (X,L) <= "\/" (Y,L) by YELLOW_0:32; ::_thesis: verum
end;
theorem :: WAYBEL11:3
for T being RelStr
for A being upper Subset of T
for B being directed Subset of T holds A /\ B is directed
proof
let T be RelStr ; ::_thesis: for A being upper Subset of T
for B being directed Subset of T holds A /\ B is directed
let A be upper Subset of T; ::_thesis: for B being directed Subset of T holds A /\ B is directed
let B be directed Subset of T; ::_thesis: A /\ B is directed
let x, y be Element of T; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in A /\ B or not y in A /\ B or ex b1 being Element of the carrier of T st
( b1 in A /\ B & x <= b1 & y <= b1 ) )
assume that
A1: x in A /\ B and
A2: y in A /\ B ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in A /\ B & x <= b1 & y <= b1 )
A3: x in B by A1, XBOOLE_0:def_4;
y in B by A2, XBOOLE_0:def_4;
then consider z being Element of T such that
A4: z in B and
A5: x <= z and
A6: y <= z by A3, WAYBEL_0:def_1;
take z ; ::_thesis: ( z in A /\ B & x <= z & y <= z )
x in A by A1, XBOOLE_0:def_4;
then z in A by A5, WAYBEL_0:def_20;
hence z in A /\ B by A4, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A5, A6; ::_thesis: verum
end;
registration
let T be non empty reflexive RelStr ;
cluster non empty finite directed for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is directed & b1 is finite )
proof
set x = the Element of T;
take { the Element of T} ; ::_thesis: ( not { the Element of T} is empty & { the Element of T} is directed & { the Element of T} is finite )
thus ( not { the Element of T} is empty & { the Element of T} is directed & { the Element of T} is finite ) by WAYBEL_0:5; ::_thesis: verum
end;
end;
theorem Th4: :: WAYBEL11:4
for T being with_suprema Poset
for D being non empty finite directed Subset of T holds sup D in D
proof
let T be reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for D being non empty finite directed Subset of T holds sup D in D
let D be non empty finite directed Subset of T; ::_thesis: sup D in D
D c= D ;
then reconsider E = D as finite Subset of D ;
consider x being Element of T such that
A1: x in D and
A2: x is_>=_than E by WAYBEL_0:1;
A3: for b being Element of T st D is_<=_than b holds
b >= x by A1, LATTICE3:def_9;
for c being Element of T st D is_<=_than c & ( for b being Element of T st D is_<=_than b holds
b >= c ) holds
c = x
proof
let c be Element of T; ::_thesis: ( D is_<=_than c & ( for b being Element of T st D is_<=_than b holds
b >= c ) implies c = x )
assume that
A4: D is_<=_than c and
A5: for b being Element of T st D is_<=_than b holds
b >= c ; ::_thesis: c = x
A6: x >= c by A2, A5;
c >= x by A1, A4, LATTICE3:def_9;
hence c = x by A6, ORDERS_2:2; ::_thesis: verum
end;
then ex_sup_of D,T by A2, A3, YELLOW_0:def_7;
hence sup D in D by A1, A2, A3, YELLOW_0:def_9; ::_thesis: verum
end;
registration
cluster finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;
existence
ex b1 being RelStr st
( b1 is reflexive & b1 is transitive & b1 is 1 -element & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & b1 is finite & b1 is strict )
proof
0 in {0} by TARSKI:def_1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
reconsider T = RelStr(# {0},r #) as non empty RelStr ;
take T ; ::_thesis: ( T is reflexive & T is transitive & T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
thus T is reflexive ::_thesis: ( T is transitive & T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
proof
let x be Element of T; :: according to YELLOW_0:def_1 ::_thesis: x <= x
x = 0 by TARSKI:def_1;
then [x,x] in {[0,0]} by TARSKI:def_1;
hence x <= x by ORDERS_2:def_5; ::_thesis: verum
end;
then reconsider T9 = T as 1 -element reflexive RelStr ;
T9 is transitive ;
hence T is transitive ; ::_thesis: ( T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
thus T is 1 -element ; ::_thesis: ( T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
T9 is antisymmetric ;
hence T is antisymmetric ; ::_thesis: ( T is with_suprema & T is with_infima & T is finite & T is strict )
T9 is with_suprema ;
hence T is with_suprema ; ::_thesis: ( T is with_infima & T is finite & T is strict )
T9 is with_infima ;
hence T is with_infima ; ::_thesis: ( T is finite & T is strict )
thus T is finite ; ::_thesis: T is strict
thus T is strict ; ::_thesis: verum
end;
end;
registration
let T be finite 1-sorted ;
cluster -> finite for Element of bool the carrier of T;
coherence
for b1 being Subset of T holds b1 is finite ;
end;
registration
let R be RelStr ;
cluster empty -> lower upper for Element of bool the carrier of R;
coherence
for b1 being Subset of R st b1 is empty holds
( b1 is lower & b1 is upper )
proof
let S be Subset of R; ::_thesis: ( S is empty implies ( S is lower & S is upper ) )
assume S is empty ; ::_thesis: ( S is lower & S is upper )
then A1: S = {} R ;
hence for x, y being Element of R st x in S & y <= x holds
y in S ; :: according to WAYBEL_0:def_19 ::_thesis: S is upper
thus for x, y being Element of R st x in S & x <= y holds
y in S by A1; :: according to WAYBEL_0:def_20 ::_thesis: verum
end;
end;
registration
let R be 1 -element RelStr ;
cluster -> upper for Element of bool the carrier of R;
coherence
for b1 being Subset of R holds b1 is upper
proof
let S be Subset of R; ::_thesis: S is upper
ex x being Element of R st the carrier of R = {x} by TEX_1:def_1;
then ( S = {} R or S = [#] R ) by ZFMISC_1:33;
hence S is upper ; ::_thesis: verum
end;
end;
theorem Th5: :: WAYBEL11:5
for T being non empty RelStr
for x being Element of T
for A being upper Subset of T st not x in A holds
A misses downarrow x
proof
let T be non empty RelStr ; ::_thesis: for x being Element of T
for A being upper Subset of T st not x in A holds
A misses downarrow x
let x be Element of T; ::_thesis: for A being upper Subset of T st not x in A holds
A misses downarrow x
let A be upper Subset of T; ::_thesis: ( not x in A implies A misses downarrow x )
assume A1: not x in A ; ::_thesis: A misses downarrow x
assume A meets downarrow x ; ::_thesis: contradiction
then consider y being set such that
A2: y in A and
A3: y in downarrow x by XBOOLE_0:3;
reconsider y = y as Element of T by A2;
y <= x by A3, WAYBEL_0:17;
hence contradiction by A1, A2, WAYBEL_0:def_20; ::_thesis: verum
end;
theorem Th6: :: WAYBEL11:6
for T being non empty RelStr
for x being Element of T
for A being lower Subset of T st x in A holds
downarrow x c= A
proof
let T be non empty RelStr ; ::_thesis: for x being Element of T
for A being lower Subset of T st x in A holds
downarrow x c= A
let x be Element of T; ::_thesis: for A being lower Subset of T st x in A holds
downarrow x c= A
let A be lower Subset of T; ::_thesis: ( x in A implies downarrow x c= A )
assume x in A ; ::_thesis: downarrow x c= A
then not x in A ` by XBOOLE_0:def_5;
then A ` misses downarrow x by Th5;
then A ` c= (downarrow x) ` by SUBSET_1:23;
hence downarrow x c= A by SUBSET_1:12; ::_thesis: verum
end;
begin
definition
let T be non empty reflexive RelStr ;
let S be Subset of T;
attrS is inaccessible_by_directed_joins means :Def1: :: WAYBEL11:def 1
for D being non empty directed Subset of T st sup D in S holds
D meets S;
attrS is closed_under_directed_sups means :Def2: :: WAYBEL11:def 2
for D being non empty directed Subset of T st D c= S holds
sup D in S;
attrS is property(S) means :Def3: :: WAYBEL11:def 3
for D being non empty directed Subset of T st sup D in S holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) );
end;
:: deftheorem Def1 defines inaccessible_by_directed_joins WAYBEL11:def_1_:_
for T being non empty reflexive RelStr
for S being Subset of T holds
( S is inaccessible_by_directed_joins iff for D being non empty directed Subset of T st sup D in S holds
D meets S );
:: deftheorem Def2 defines closed_under_directed_sups WAYBEL11:def_2_:_
for T being non empty reflexive RelStr
for S being Subset of T holds
( S is closed_under_directed_sups iff for D being non empty directed Subset of T st D c= S holds
sup D in S );
:: deftheorem Def3 defines property(S) WAYBEL11:def_3_:_
for T being non empty reflexive RelStr
for S being Subset of T holds
( S is property(S) iff for D being non empty directed Subset of T st sup D in S holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) );
notation
let T be non empty reflexive RelStr ;
let S be Subset of T;
synonym inaccessible S for inaccessible_by_directed_joins ;
synonym directly_closed S for closed_under_directed_sups ;
end;
registration
let T be non empty reflexive RelStr ;
cluster empty -> directly_closed property(S) for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is empty holds
( b1 is property(S) & b1 is directly_closed )
proof
let S be Subset of T; ::_thesis: ( S is empty implies ( S is property(S) & S is directly_closed ) )
assume S is empty ; ::_thesis: ( S is property(S) & S is directly_closed )
then A1: S = {} T ;
for D being non empty directed Subset of T st sup D in {} T holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in {} T ) ) ;
hence S is property(S) by A1, Def3; ::_thesis: S is directly_closed
thus for D being non empty directed Subset of T st D c= S holds
sup D in S by A1; :: according to WAYBEL11:def_2 ::_thesis: verum
end;
end;
registration
let T be non empty reflexive RelStr ;
cluster directly_closed property(S) for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is property(S) & b1 is directly_closed )
proof
take {} T ; ::_thesis: ( {} T is property(S) & {} T is directly_closed )
thus ( {} T is property(S) & {} T is directly_closed ) ; ::_thesis: verum
end;
end;
registration
let T be non empty reflexive RelStr ;
let S be property(S) Subset of T;
clusterS ` -> directly_closed ;
coherence
S ` is closed_under_directed_sups
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= S ` implies sup D in S ` )
assume A1: D c= S ` ; ::_thesis: sup D in S `
assume not sup D in S ` ; ::_thesis: contradiction
then sup D in S by XBOOLE_0:def_5;
then consider y being Element of T such that
A2: y in D and
A3: for x being Element of T st x in D & x >= y holds
x in S by Def3;
y <= y ;
then y in S by A2, A3;
then D /\ S <> {} by A2, XBOOLE_0:def_4;
then D meets S by XBOOLE_0:def_7;
hence contradiction by A1, SUBSET_1:23; ::_thesis: verum
end;
end;
definition
let T be non empty reflexive TopRelStr ;
attrT is Scott means :Def4: :: WAYBEL11:def 4
for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) );
end;
:: deftheorem Def4 defines Scott WAYBEL11:def_4_:_
for T being non empty reflexive TopRelStr holds
( T is Scott iff for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) ) );
registration
let T be non empty finite reflexive transitive antisymmetric with_suprema RelStr ;
cluster -> inaccessible for Element of bool the carrier of T;
coherence
for b1 being Subset of T holds b1 is inaccessible
proof
let S be Subset of T; ::_thesis: S is inaccessible
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume A1: sup D in S ; ::_thesis: D meets S
sup D in D by Th4;
hence D meets S by A1, XBOOLE_0:3; ::_thesis: verum
end;
end;
definition
let T be non empty finite reflexive transitive antisymmetric with_suprema TopRelStr ;
redefine attr T is Scott means :: WAYBEL11:def 5
for S being Subset of T holds
( S is open iff S is upper );
compatibility
( T is Scott iff for S being Subset of T holds
( S is open iff S is upper ) )
proof
thus ( T is Scott implies for S being Subset of T holds
( S is open iff S is upper ) ) by Def4; ::_thesis: ( ( for S being Subset of T holds
( S is open iff S is upper ) ) implies T is Scott )
assume A1: for S being Subset of T holds
( S is open iff S is upper ) ; ::_thesis: T is Scott
let S be Subset of T; :: according to WAYBEL11:def_4 ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) )
thus ( S is open iff ( S is inaccessible & S is upper ) ) by A1; ::_thesis: verum
end;
end;
:: deftheorem defines Scott WAYBEL11:def_5_:_
for T being non empty finite reflexive transitive antisymmetric with_suprema TopRelStr holds
( T is Scott iff for S being Subset of T holds
( S is open iff S is upper ) );
registration
cluster non empty 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is complete & b1 is strict & b1 is 1 -element & b1 is Scott )
proof
set T = the finite 1 -element discrete reflexive strict TopRelStr ;
take the finite 1 -element discrete reflexive strict TopRelStr ; ::_thesis: ( the finite 1 -element discrete reflexive strict TopRelStr is complete & the finite 1 -element discrete reflexive strict TopRelStr is strict & the finite 1 -element discrete reflexive strict TopRelStr is 1 -element & the finite 1 -element discrete reflexive strict TopRelStr is Scott )
thus ( the finite 1 -element discrete reflexive strict TopRelStr is complete & the finite 1 -element discrete reflexive strict TopRelStr is strict & the finite 1 -element discrete reflexive strict TopRelStr is 1 -element ) ; ::_thesis: the finite 1 -element discrete reflexive strict TopRelStr is Scott
let S be Subset of the finite 1 -element discrete reflexive strict TopRelStr ; :: according to WAYBEL11:def_5 ::_thesis: ( S is open iff S is upper )
thus ( S is open iff S is upper ) by TDLAT_3:15; ::_thesis: verum
end;
end;
registration
let T be non empty reflexive RelStr ;
cluster [#] T -> inaccessible directly_closed ;
coherence
( [#] T is closed_under_directed_sups & [#] T is inaccessible_by_directed_joins )
proof
thus [#] T is directly_closed ::_thesis: [#] T is inaccessible_by_directed_joins
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= [#] T implies sup D in [#] T )
assume D c= [#] T ; ::_thesis: sup D in [#] T
thus sup D in [#] T ; ::_thesis: verum
end;
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in [#] T implies D meets [#] T )
assume sup D in [#] T ; ::_thesis: D meets [#] T
ex p being Element of T st p in D by SUBSET_1:4;
hence D meets [#] T by XBOOLE_0:3; ::_thesis: verum
end;
end;
registration
let T be non empty reflexive RelStr ;
cluster lower upper inaccessible directly_closed for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( b1 is directly_closed & b1 is lower & b1 is inaccessible & b1 is upper )
proof
take [#] T ; ::_thesis: ( [#] T is directly_closed & [#] T is lower & [#] T is inaccessible & [#] T is upper )
thus ( [#] T is directly_closed & [#] T is lower & [#] T is inaccessible & [#] T is upper ) ; ::_thesis: verum
end;
end;
registration
let T be non empty reflexive RelStr ;
let S be inaccessible Subset of T;
clusterS ` -> directly_closed ;
coherence
S ` is closed_under_directed_sups
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= S ` implies sup D in S ` )
assume D c= S ` ; ::_thesis: sup D in S `
then D misses S by SUBSET_1:23;
then not sup D in S by Def1;
hence sup D in S ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
registration
let T be non empty reflexive RelStr ;
let S be directly_closed Subset of T;
clusterS ` -> inaccessible ;
coherence
S ` is inaccessible_by_directed_joins
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S ` implies D meets S ` )
assume sup D in S ` ; ::_thesis: D meets S `
then not sup D in S by XBOOLE_0:def_5;
then not D c= (S `) ` by Def2;
hence D meets S ` by SUBSET_1:23; ::_thesis: verum
end;
end;
theorem Th7: :: WAYBEL11:7
for T being non empty reflexive transitive up-complete Scott TopRelStr
for S being Subset of T holds
( S is closed iff ( S is directly_closed & S is lower ) )
proof
let T be non empty reflexive transitive up-complete Scott TopRelStr ; ::_thesis: for S being Subset of T holds
( S is closed iff ( S is directly_closed & S is lower ) )
let S be Subset of T; ::_thesis: ( S is closed iff ( S is directly_closed & S is lower ) )
hereby ::_thesis: ( S is directly_closed & S is lower implies S is closed )
assume S is closed ; ::_thesis: ( S is directly_closed & S is lower )
then S ` is open by TOPS_1:3;
then reconsider A = S ` as upper inaccessible Subset of T by Def4;
( A ` is directly_closed & A ` is lower ) ;
hence ( S is directly_closed & S is lower ) ; ::_thesis: verum
end;
assume ( S is directly_closed & S is lower ) ; ::_thesis: S is closed
then reconsider S = S as lower directly_closed Subset of T ;
S ` is open by Def4;
hence S is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th8: :: WAYBEL11:8
for T being non empty reflexive transitive antisymmetric up-complete TopRelStr
for x being Element of T holds downarrow x is directly_closed
proof
let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_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
downarrow x is directly_closed
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= downarrow x implies sup D in downarrow x )
assume A1: D c= downarrow x ; ::_thesis: sup D in downarrow x
ex a being Element of T st
( a is_>=_than D & ( for b being Element of T st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def_39;
then A2: ex_sup_of D,T by YELLOW_0:15;
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 sup D in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
hence downarrow x is directly_closed ; ::_thesis: verum
end;
theorem Th9: :: WAYBEL11:9
for T being complete Scott TopLattice
for x being Element of T holds Cl {x} = downarrow x
proof
let T be 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 Th8;
then A1: downarrow x is closed by Th7;
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 Th7;
x in C by A3, ZFMISC_1:31;
hence downarrow x c= C by A4, Th6; ::_thesis: verum
end;
hence Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum
end;
theorem :: WAYBEL11:10
for T being complete Scott TopLattice holds T is T_0-TopSpace
proof
let T be complete Scott TopLattice; ::_thesis: T is T_0-TopSpace
now__::_thesis:_for_x,_y_being_Point_of_T_st_x_<>_y_holds_
Cl_{x}_<>_Cl_{y}
let x, y be Point of T; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} )
reconsider x9 = x, y9 = y as Element of T ;
A1: Cl {x9} = downarrow x9 by Th9;
A2: Cl {y9} = downarrow y9 by Th9;
assume x <> y ; ::_thesis: Cl {x} <> Cl {y}
hence Cl {x} <> Cl {y} by A1, A2, WAYBEL_0:19; ::_thesis: verum
end;
hence T is T_0-TopSpace by TSP_1:def_5; ::_thesis: verum
end;
theorem Th11: :: WAYBEL11:11
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds downarrow x is closed
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for x being Element of T holds downarrow x is closed
let x be Element of T; ::_thesis: downarrow x is closed
( downarrow x is directly_closed & downarrow x is lower ) by Th8;
hence downarrow x is closed by Th7; ::_thesis: verum
end;
theorem Th12: :: WAYBEL11:12
for T being up-complete Scott TopLattice
for x being Element of T holds (downarrow x) ` is open
proof
let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T holds (downarrow x) ` is open
let x be Element of T; ::_thesis: (downarrow x) ` is open
downarrow x is closed by Th11;
hence (downarrow x) ` is open ; ::_thesis: verum
end;
theorem Th13: :: WAYBEL11:13
for T being up-complete Scott TopLattice
for x being Element of T
for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
proof
let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T
for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
let x be Element of T; ::_thesis: for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
let A be upper Subset of T; ::_thesis: ( not x in A implies (downarrow x) ` is a_neighborhood of A )
assume A1: not x in A ; ::_thesis: (downarrow x) ` is a_neighborhood of A
(downarrow x) ` is open by Th12;
then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23;
A misses downarrow x by A1, Th5;
then A c= (downarrow x) ` by SUBSET_1:23;
hence (downarrow x) ` is a_neighborhood of A by A2, CONNSP_2:def_2; ::_thesis: verum
end;
theorem :: WAYBEL11:14
for T being complete Scott TopLattice
for S being upper Subset of T ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
proof
let T be complete Scott TopLattice; ::_thesis: for S being upper Subset of T ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
let S be upper Subset of T; ::_thesis: ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
defpred S1[ set ] means $1 is a_neighborhood of S;
set F = { X where X is Subset of T : S1[X] } ;
{ X where X is Subset of T : S1[X] } is Subset-Family of T from DOMAIN_1:sch_7();
then reconsider F = { X where X is Subset of T : S1[X] } as Subset-Family of T ;
take F ; ::_thesis: ( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
thus S = meet F ::_thesis: for X being Subset of T st X in F holds
X is a_neighborhood of S
proof
[#] T is a_neighborhood of S by CONNSP_2:28;
then A1: [#] T in F ;
now__::_thesis:_for_Z1_being_set_st_Z1_in_F_holds_
S_c=_Z1
let Z1 be set ; ::_thesis: ( Z1 in F implies S c= Z1 )
assume Z1 in F ; ::_thesis: S c= Z1
then ex X being Subset of T st
( Z1 = X & X is a_neighborhood of S ) ;
hence S c= Z1 by CONNSP_2:29; ::_thesis: verum
end;
hence S c= meet F by A1, SETFAM_1:5; :: according to XBOOLE_0:def_10 ::_thesis: meet F c= S
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F or x in S )
assume that
A2: x in meet F and
A3: not x in S ; ::_thesis: contradiction
reconsider p = x as Element of T by A2;
(downarrow p) ` is a_neighborhood of S by A3, Th13;
then (downarrow p) ` in F ;
then A4: meet F c= (downarrow p) ` by SETFAM_1:3;
p <= p ;
then p in downarrow p by WAYBEL_0:17;
hence contradiction by A2, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
let X be Subset of T; ::_thesis: ( X in F implies X is a_neighborhood of S )
assume X in F ; ::_thesis: X is a_neighborhood of S
then ex Y being Subset of T st
( X = Y & Y is a_neighborhood of S ) ;
hence X is a_neighborhood of S ; ::_thesis: verum
end;
theorem :: WAYBEL11:15
for T being Scott TopLattice
for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
proof
let T be Scott TopLattice; ::_thesis: for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
let S be Subset of T; ::_thesis: ( S is open iff ( S is upper & S is property(S) ) )
hereby ::_thesis: ( S is upper & S is property(S) implies S is open )
assume A1: S is open ; ::_thesis: ( S is upper & S is property(S) )
hence A2: S is upper by Def4; ::_thesis: S is property(S)
thus S is property(S) ::_thesis: verum
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in S implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) )
assume A3: sup D in S ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
S is inaccessible by A1, Def4;
then S meets D by A3, Def1;
then consider y being set such that
A4: y in S and
A5: y in D by XBOOLE_0:3;
reconsider y = y as Element of T by A4;
take y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
thus ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) by A2, A4, A5, WAYBEL_0:def_20; ::_thesis: verum
end;
end;
assume that
A6: S is upper and
A7: S is property(S) ; ::_thesis: S is open
S is inaccessible
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume sup D in S ; ::_thesis: D meets S
then consider y being Element of T such that
A8: y in D and
A9: for x being Element of T st x in D & x >= y holds
x in S by A7, Def3;
y >= y by YELLOW_0:def_1;
then y in S by A8, A9;
hence D meets S by A8, XBOOLE_0:3; ::_thesis: verum
end;
hence S is open by A6, Def4; ::_thesis: verum
end;
registration
let T be complete TopLattice;
cluster lower -> property(S) for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is lower holds
b1 is property(S)
proof
let S be Subset of T; ::_thesis: ( S is lower implies S is property(S) )
assume A1: S is lower ; ::_thesis: S is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in S implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) )
assume A2: sup D in S ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
consider y being Element of T such that
A3: y in D by SUBSET_1:4;
take y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
thus y in D by A3; ::_thesis: for x being Element of T st x in D & x >= y holds
x in S
let x be Element of T; ::_thesis: ( x in D & x >= y implies x in S )
assume that
A4: x in D and
x >= y ; ::_thesis: x in S
x <= sup D by A4, YELLOW_2:22;
hence x in S by A1, A2, WAYBEL_0:def_19; ::_thesis: verum
end;
end;
Lm2: for T being non empty reflexive TopRelStr holds [#] T is property(S)
proof
let T be non empty reflexive TopRelStr ; ::_thesis: [#] T is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in [#] T implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in [#] T ) ) )
assume sup D in [#] T ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in [#] T ) )
consider y being Element of T such that
A1: y in D by SUBSET_1:4;
take y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in [#] T ) )
thus y in D by A1; ::_thesis: for x being Element of T st x in D & x >= y holds
x in [#] T
let x be Element of T; ::_thesis: ( x in D & x >= y implies x in [#] T )
assume that
x in D and
x >= y ; ::_thesis: x in [#] T
thus x in [#] T ; ::_thesis: verum
end;
theorem :: WAYBEL11:16
for T being non empty reflexive transitive TopRelStr st the topology of T = { S where S is Subset of T : S is property(S) } holds
T is TopSpace-like
proof
let T be non empty reflexive transitive TopRelStr ; ::_thesis: ( the topology of T = { S where S is Subset of T : S is property(S) } implies T is TopSpace-like )
assume A1: the topology of T = { S where S is Subset of T : S is property(S) } ; ::_thesis: T is TopSpace-like
[#] T is property(S) by Lm2;
hence the carrier of T in the topology of T by A1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T) holds
( not b1 c= the topology of T or union b1 in the topology of T ) ) & ( for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) ) )
hereby ::_thesis: for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T )
let a be Subset-Family of T; ::_thesis: ( a c= the topology of T implies union a in the topology of T )
assume A2: a c= the topology of T ; ::_thesis: union a in the topology of T
union a is property(S)
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in union a implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in union a ) ) )
assume sup D in union a ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in union a ) )
then consider x being set such that
A3: sup D in x and
A4: x in a by TARSKI:def_4;
x in the topology of T by A2, A4;
then consider X being Subset of T such that
A5: x = X and
A6: X is property(S) by A1;
consider y being Element of T such that
A7: y in D and
A8: for x being Element of T st x in D & x >= y holds
x in X by A3, A5, A6, Def3;
take y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in union a ) )
thus y in D by A7; ::_thesis: for x being Element of T st x in D & x >= y holds
x in union a
let u be Element of T; ::_thesis: ( u in D & u >= y implies u in union a )
assume that
A9: u in D and
A10: u >= y ; ::_thesis: u in union a
u in X by A8, A9, A10;
hence u in union a by A4, A5, TARSKI:def_4; ::_thesis: verum
end;
hence union a in the topology of T by A1; ::_thesis: verum
end;
let a, b be Subset of T; ::_thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )
assume a in the topology of T ; ::_thesis: ( not b in the topology of T or a /\ b in the topology of T )
then consider A being Subset of T such that
A11: a = A and
A12: A is property(S) by A1;
assume b in the topology of T ; ::_thesis: a /\ b in the topology of T
then consider B being Subset of T such that
A13: b = B and
A14: B is property(S) by A1;
A /\ B is property(S)
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in A /\ B implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A /\ B ) ) )
assume A15: sup D in A /\ B ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A /\ B ) )
then sup D in A by XBOOLE_0:def_4;
then consider x being Element of T such that
A16: x in D and
A17: for z being Element of T st z in D & z >= x holds
z in A by A12, Def3;
sup D in B by A15, XBOOLE_0:def_4;
then consider y being Element of T such that
A18: y in D and
A19: for z being Element of T st z in D & z >= y holds
z in B by A14, Def3;
consider z being Element of T such that
A20: z in D and
A21: x <= z and
A22: y <= z by A16, A18, WAYBEL_0:def_1;
take z ; ::_thesis: ( z in D & ( for x being Element of T st x in D & x >= z holds
x in A /\ B ) )
thus z in D by A20; ::_thesis: for x being Element of T st x in D & x >= z holds
x in A /\ B
let u be Element of T; ::_thesis: ( u in D & u >= z implies u in A /\ B )
assume A23: u in D ; ::_thesis: ( not u >= z or u in A /\ B )
assume A24: u >= z ; ::_thesis: u in A /\ B
then u >= x by A21, YELLOW_0:def_2;
then A25: u in A by A17, A23;
u >= y by A22, A24, YELLOW_0:def_2;
then u in B by A19, A23;
hence u in A /\ B by A25, XBOOLE_0:def_4; ::_thesis: verum
end;
hence a /\ b in the topology of T by A1, A11, A13; ::_thesis: verum
end;
begin
definition
let R be non empty RelStr ;
let N be net of R;
func lim_inf N -> Element of R equals :: WAYBEL11:def 6
"\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R);
correctness
coherence
"\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R) is Element of R;
;
end;
:: deftheorem defines lim_inf WAYBEL11:def_6_:_
for R being non empty RelStr
for N being net of R holds lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R);
definition
let R be non empty reflexive RelStr ;
let N be net of R;
let p be Element of R;
predp is_S-limit_of N means :Def7: :: WAYBEL11:def 7
p <= lim_inf N;
end;
:: deftheorem Def7 defines is_S-limit_of WAYBEL11:def_7_:_
for R being non empty reflexive RelStr
for N being net of R
for p being Element of R holds
( p is_S-limit_of N iff p <= lim_inf N );
definition
let R be non empty reflexive RelStr ;
func Scott-Convergence R -> Convergence-Class of R means :Def8: :: WAYBEL11:def 8
for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it iff p is_S-limit_of N );
existence
ex b1 being Convergence-Class of R st
for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b1 iff p is_S-limit_of N )
proof
defpred S1[ set , Element of R] means ex N being strict net of R st
( N = $1 & $2 is_S-limit_of N );
consider C being Relation of (NetUniv R), the carrier of R such that
A1: for x being Element of NetUniv R
for y being Element of R holds
( [x,y] in C iff S1[x,y] ) from RELSET_1:sch_2();
reconsider C = C as Convergence-Class of R by YELLOW_6:def_18;
take C ; ::_thesis: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N )
let N be strict net of R; ::_thesis: ( N in NetUniv R implies for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N ) )
assume A2: N in NetUniv R ; ::_thesis: for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N )
let p be Element of R; ::_thesis: ( [N,p] in C iff p is_S-limit_of N )
hereby ::_thesis: ( p is_S-limit_of N implies [N,p] in C )
assume [N,p] in C ; ::_thesis: p is_S-limit_of N
then ex M being strict net of R st
( M = N & p is_S-limit_of M ) by A1, A2;
hence p is_S-limit_of N ; ::_thesis: verum
end;
thus ( p is_S-limit_of N implies [N,p] in C ) by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Convergence-Class of R st ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b2 iff p is_S-limit_of N ) ) holds
b1 = b2
proof
let it1, it2 be Convergence-Class of R; ::_thesis: ( ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it2 iff p is_S-limit_of N ) ) implies it1 = it2 )
assume that
A3: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it1 iff p is_S-limit_of N ) and
A4: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it2 iff p is_S-limit_of N ) ; ::_thesis: it1 = it2
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in it1 or [x,y] in it2 ) & ( not [x,y] in it2 or [x,y] in it1 ) )
A5: it1 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
A6: it2 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
hereby ::_thesis: ( not [x,y] in it2 or [x,y] in it1 )
assume A7: [x,y] in it1 ; ::_thesis: [x,y] in it2
then A8: x in NetUniv R by A5, ZFMISC_1:87;
then consider N being strict net of R such that
A9: N = x and
the carrier of N in the_universe_of the carrier of R by YELLOW_6:def_11;
reconsider p = y as Element of R by A5, A7, ZFMISC_1:87;
p is_S-limit_of N by A3, A7, A8, A9;
hence [x,y] in it2 by A4, A8, A9; ::_thesis: verum
end;
assume A10: [x,y] in it2 ; ::_thesis: [x,y] in it1
then A11: x in NetUniv R by A6, ZFMISC_1:87;
then consider N being strict net of R such that
A12: N = x and
the carrier of N in the_universe_of the carrier of R by YELLOW_6:def_11;
reconsider p = y as Element of R by A6, A10, ZFMISC_1:87;
p is_S-limit_of N by A4, A10, A11, A12;
hence [x,y] in it1 by A3, A11, A12; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines Scott-Convergence WAYBEL11:def_8_:_
for R being non empty reflexive RelStr
for b2 being Convergence-Class of R holds
( b2 = Scott-Convergence R iff for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b2 iff p is_S-limit_of N ) );
theorem :: WAYBEL11:17
for R being complete LATTICE
for N being net of R
for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
proof
let R be complete LATTICE; ::_thesis: for N being net of R
for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
let N be net of R; ::_thesis: for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
let p, q be Element of R; ::_thesis: ( p is_S-limit_of N & N is_eventually_in downarrow q implies p <= q )
assume that
A1: p <= lim_inf N and
A2: N is_eventually_in downarrow q ; :: according to WAYBEL11:def_7 ::_thesis: p <= q
consider j0 being Element of N such that
A3: for i being Element of N st j0 <= i holds
N . i in downarrow q by A2, WAYBEL_0:def_11;
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
reconsider q9 = q as Element of R ;
q9 is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }
proof
let x be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } or x <= q9 )
assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: x <= q9
then consider j1 being Element of N such that
A4: x = "/\" ( { (N . i) where i is Element of N : i >= j1 } ,R) ;
set Y = { (N . i) where i is Element of N : i >= j1 } ;
reconsider j1 = j1 as Element of N ;
consider j2 being Element of N such that
A5: j2 >= j0 and
A6: j2 >= j1 by YELLOW_6:def_3;
N . j2 in { (N . i) where i is Element of N : i >= j1 } by A6;
then A7: x <= N . j2 by A4, YELLOW_2:22;
N . j2 in downarrow q by A3, A5;
then N . j2 <= q9 by WAYBEL_0:17;
hence x <= q9 by A7, YELLOW_0:def_2; ::_thesis: verum
end;
then lim_inf N <= q9 by YELLOW_0:32;
hence p <= q by A1, YELLOW_0:def_2; ::_thesis: verum
end;
theorem Th18: :: WAYBEL11:18
for R being complete LATTICE
for N being net of R
for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
proof
let R be complete LATTICE; ::_thesis: for N being net of R
for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
let N be net of R; ::_thesis: for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
let p, q be Element of R; ::_thesis: ( N is_eventually_in uparrow q implies lim_inf N >= q )
assume N is_eventually_in uparrow q ; ::_thesis: lim_inf N >= q
then consider j0 being Element of N such that
A1: for i being Element of N st j0 <= i holds
N . i in uparrow q by WAYBEL_0:def_11;
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
set Y = { (N . i) where i is Element of N : i >= j0 } ;
reconsider q9 = q as Element of R ;
"/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
then A2: lim_inf N >= "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) by YELLOW_2:22;
q9 is_<=_than { (N . i) where i is Element of N : i >= j0 }
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 >= j0 } or q9 <= y )
assume y in { (N . i) where i is Element of N : i >= j0 } ; ::_thesis: q9 <= y
then consider i1 being Element of N such that
A3: y = N . i1 and
A4: i1 >= j0 ;
reconsider i19 = i1 as Element of N ;
N . i19 in uparrow q by A1, A4;
hence q9 <= y by A3, WAYBEL_0:18; ::_thesis: verum
end;
then "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) >= q9 by YELLOW_0:33;
hence lim_inf N >= q by A2, YELLOW_0:def_2; ::_thesis: verum
end;
definition
let R be non empty reflexive RelStr ;
let N be non empty NetStr over R;
redefine attr N is monotone means :Def9: :: WAYBEL11:def 9
for i, j being Element of N st i <= j holds
N . i <= N . j;
compatibility
( N is monotone iff for i, j being Element of N st i <= j holds
N . i <= N . j )
proof
hereby ::_thesis: ( ( for i, j being Element of N st i <= j holds
N . i <= N . j ) implies N is monotone )
assume N is monotone ; ::_thesis: for i, j being Element of N st i <= j holds
N . i <= N . j
then A1: netmap (N,R) is monotone by WAYBEL_0:def_9;
let i, j be Element of N; ::_thesis: ( i <= j implies N . i <= N . j )
assume i <= j ; ::_thesis: N . i <= N . j
hence N . i <= N . j by A1, WAYBEL_1:def_2; ::_thesis: verum
end;
assume A2: for i, j being Element of N st i <= j holds
N . i <= N . j ; ::_thesis: N is monotone
netmap (N,R) is monotone
proof
let x, y be Element of N; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (netmap (N,R)) . x <= (netmap (N,R)) . y )
A3: (netmap (N,R)) . x = N . x ;
A4: (netmap (N,R)) . y = N . y ;
assume x <= y ; ::_thesis: (netmap (N,R)) . x <= (netmap (N,R)) . y
hence (netmap (N,R)) . x <= (netmap (N,R)) . y by A2, A3, A4; ::_thesis: verum
end;
hence N is monotone by WAYBEL_0:def_9; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines monotone WAYBEL11:def_9_:_
for R being non empty reflexive RelStr
for N being non empty NetStr over R holds
( N is monotone iff for i, j being Element of N st i <= j holds
N . i <= N . j );
definition
let R be non empty RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
func Net-Str (S,f) -> non empty strict NetStr over R means :Def10: :: WAYBEL11:def 10
( the carrier of it = S & the mapping of it = f & ( for i, j being Element of it holds
( i <= j iff it . i <= it . j ) ) );
existence
ex b1 being non empty strict NetStr over R st
( the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds
( i <= j iff b1 . i <= b1 . j ) ) )
proof
defpred S1[ Element of S, Element of S] means f . $1 <= f . $2;
consider R being Relation of S,S such that
A1: for x, y being Element of S holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
take N = NetStr(# S,R,f #); ::_thesis: ( the carrier of N = S & the mapping of N = f & ( for i, j being Element of N holds
( i <= j iff N . i <= N . j ) ) )
thus the carrier of N = S ; ::_thesis: ( the mapping of N = f & ( for i, j being Element of N holds
( i <= j iff N . i <= N . j ) ) )
thus the mapping of N = f ; ::_thesis: for i, j being Element of N holds
( i <= j iff N . i <= N . j )
let i, j be Element of N; ::_thesis: ( i <= j iff N . i <= N . j )
reconsider x = i, y = j as Element of S ;
( [x,y] in the InternalRel of N iff f . x <= f . y ) by A1;
hence ( i <= j iff N . i <= N . j ) by ORDERS_2:def_5; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict NetStr over R st the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds
( i <= j iff b1 . i <= b1 . j ) ) & the carrier of b2 = S & the mapping of b2 = f & ( for i, j being Element of b2 holds
( i <= j iff b2 . i <= b2 . j ) ) holds
b1 = b2
proof
let it1, it2 be non empty strict NetStr over R; ::_thesis: ( the carrier of it1 = S & the mapping of it1 = f & ( for i, j being Element of it1 holds
( i <= j iff it1 . i <= it1 . j ) ) & the carrier of it2 = S & the mapping of it2 = f & ( for i, j being Element of it2 holds
( i <= j iff it2 . i <= it2 . j ) ) implies it1 = it2 )
assume that
A2: the carrier of it1 = S and
A3: the mapping of it1 = f and
A4: for i, j being Element of it1 holds
( i <= j iff it1 . i <= it1 . j ) and
A5: the carrier of it2 = S and
A6: the mapping of it2 = f and
A7: for i, j being Element of it2 holds
( i <= j iff it2 . i <= it2 . j ) ; ::_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 A8: [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 i9 = x, j9 = y as Element of it2 by A2, A5, A8, ZFMISC_1:87;
A9: it1 . i = it2 . i9 by A3, A6;
A10: it1 . j = it2 . j9 by A3, A6;
i <= j by A8, ORDERS_2:def_5;
then it2 . i9 <= it2 . j9 by A4, A9, A10;
then i9 <= j9 by A7;
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 A2, A5, A11, ZFMISC_1:87;
A12: it2 . i = it1 . i9 by A3, A6;
A13: it2 . j = it1 . j9 by A3, A6;
i <= j by A11, ORDERS_2:def_5;
then it1 . i9 <= it1 . j9 by A7, A12, A13;
then i9 <= j9 by A4;
hence [x,y] in the InternalRel of it1 by ORDERS_2:def_5; ::_thesis: verum
end;
hence it1 = it2 by A2, A3, A5, A6; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines Net-Str WAYBEL11:def_10_:_
for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R
for b4 being non empty strict NetStr over R holds
( b4 = Net-Str (S,f) iff ( the carrier of b4 = S & the mapping of b4 = f & ( for i, j being Element of b4 holds
( i <= j iff b4 . i <= b4 . j ) ) ) );
theorem Th19: :: WAYBEL11:19
for L being non empty 1-sorted
for N being non empty NetStr over L holds rng the mapping of N = { (N . i) where i is Element of N : verum }
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L holds rng the mapping of N = { (N . i) where i is Element of N : verum }
let N be non empty NetStr over L; ::_thesis: rng the mapping of N = { (N . i) where i is Element of N : verum }
set X = { (N . i) where i is Element of N : verum } ;
A1: the carrier of N = dom the mapping of N by FUNCT_2:def_1;
thus rng the mapping of N c= { (N . i) where i is Element of N : verum } :: according to XBOOLE_0:def_10 ::_thesis: { (N . i) where i is Element of N : verum } c= rng the mapping of N
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng the mapping of N or e in { (N . i) where i is Element of N : verum } )
assume e in rng the mapping of N ; ::_thesis: e in { (N . i) where i is Element of N : verum }
then consider u being set such that
A2: u in dom the mapping of N and
A3: e = the mapping of N . u by FUNCT_1:def_3;
reconsider u = u as Element of N by A2;
e = N . u by A3;
hence e in { (N . i) where i is Element of N : verum } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (N . i) where i is Element of N : verum } or e in rng the mapping of N )
assume e in { (N . i) where i is Element of N : verum } ; ::_thesis: e in rng the mapping of N
then ex i being Element of N st e = N . i ;
hence e in rng the mapping of N by A1, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th20: :: WAYBEL11:20
for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
proof
let R be non empty RelStr ; ::_thesis: for S being non empty set
for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
let S be non empty set ; ::_thesis: for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
let f be Function of S, the carrier of R; ::_thesis: ( rng f is directed implies Net-Str (S,f) is directed )
assume A1: rng f is directed ; ::_thesis: Net-Str (S,f) is directed
set N = Net-Str (S,f);
let x, y be Element of (Net-Str (S,f)); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of (Net-Str (S,f)) st
( x <= b1 & y <= b1 )
f = the mapping of (Net-Str (S,f)) by Def10;
then A2: rng f = { ((Net-Str (S,f)) . i) where i is Element of (Net-Str (S,f)) : verum } by Th19;
then A3: (Net-Str (S,f)) . x in rng f ;
(Net-Str (S,f)) . y in rng f by A2;
then consider p being Element of R such that
A4: p in rng f and
A5: (Net-Str (S,f)) . x <= p and
A6: (Net-Str (S,f)) . y <= p by A1, A3, WAYBEL_0:def_1;
consider z being set such that
A7: z in dom f and
A8: p = f . z by A4, FUNCT_1:def_3;
reconsider z = z as Element of (Net-Str (S,f)) by A7, Def10;
take z ; ::_thesis: ( x <= z & y <= z )
p = (Net-Str (S,f)) . z by A8, Def10;
hence ( x <= z & y <= z ) by A5, A6, Def10; ::_thesis: verum
end;
registration
let R be non empty RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) -> non empty strict monotone ;
coherence
Net-Str (S,f) is monotone
proof
set N = Net-Str (S,f);
netmap ((Net-Str (S,f)),R) is monotone
proof
let x, y be Element of (Net-Str (S,f)); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y )
A1: (netmap ((Net-Str (S,f)),R)) . x = (Net-Str (S,f)) . x ;
A2: (netmap ((Net-Str (S,f)),R)) . y = (Net-Str (S,f)) . y ;
assume x <= y ; ::_thesis: (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y
hence (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y by A1, A2, Def10; ::_thesis: verum
end;
hence Net-Str (S,f) is monotone by WAYBEL_0:def_9; ::_thesis: verum
end;
end;
registration
let R be non empty transitive RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) -> non empty transitive strict ;
coherence
Net-Str (S,f) is transitive
proof
set N = Net-Str (S,f);
let x, y, z be Element of (Net-Str (S,f)); :: 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
A3: (Net-Str (S,f)) . x <= (Net-Str (S,f)) . y by A1, Def10;
(Net-Str (S,f)) . y <= (Net-Str (S,f)) . z by A2, Def10;
then (Net-Str (S,f)) . x <= (Net-Str (S,f)) . z by A3, YELLOW_0:def_2;
hence x <= z by Def10; ::_thesis: verum
end;
end;
registration
let R be non empty reflexive RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) -> non empty reflexive strict ;
coherence
Net-Str (S,f) is reflexive
proof
let x be Element of (Net-Str (S,f)); :: according to YELLOW_0:def_1 ::_thesis: x <= x
(Net-Str (S,f)) . x <= (Net-Str (S,f)) . x ;
hence x <= x by Def10; ::_thesis: verum
end;
end;
theorem Th21: :: WAYBEL11:21
for R being non empty transitive RelStr
for S being non empty set
for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
proof
let R be non empty transitive RelStr ; ::_thesis: for S being non empty set
for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
let S be non empty set ; ::_thesis: for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
let f be Function of S, the carrier of R; ::_thesis: ( S c= the carrier of R & Net-Str (S,f) is directed implies Net-Str (S,f) in NetUniv R )
assume that
A1: S c= the carrier of R and
A2: Net-Str (S,f) is directed ; ::_thesis: Net-Str (S,f) in NetUniv R
reconsider N = Net-Str (S,f) as strict net of R by A2;
set UN = the_universe_of the carrier of R;
reconsider UN = the_universe_of the carrier of R as universal set ;
the_transitive-closure_of the carrier of R in UN by CLASSES1:2;
then the carrier of R in UN by CLASSES1:3, CLASSES1:52;
then A3: S in UN by A1, CLASSES1:def_1;
the carrier of N = S by Def10;
hence Net-Str (S,f) in NetUniv R by A3, YELLOW_6:def_11; ::_thesis: verum
end;
registration
let R be LATTICE;
cluster non empty reflexive transitive strict directed monotone for NetStr over R;
existence
ex b1 being net of R st
( b1 is monotone & b1 is reflexive & b1 is strict )
proof
reconsider f = id the carrier of R as Function of the carrier of R, the carrier of R ;
rng f = [#] R by RELAT_1:45;
then reconsider N = Net-Str ( the carrier of R,f) as reflexive strict net of R by Th20;
take N ; ::_thesis: ( N is monotone & N is reflexive & N is strict )
thus ( N is monotone & N is reflexive & N is strict ) ; ::_thesis: verum
end;
end;
theorem Th22: :: WAYBEL11:22
for R being complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
proof
let R be 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 . i) where i is Element of N : i >= $1 } ,R);
set X = { H1(j) where j is Element of N : S1[j] } ;
deffunc H2( Element of N) -> Element of the carrier of R = N . $1;
A1: for j being Element of N holds H2(j) = H1(j)
proof
let j be Element of N; ::_thesis: H2(j) = H1(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 Def9; ::_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 H2(j) = H1(j) by A2, YELLOW_0:33; ::_thesis: verum
end;
rng the mapping of N = { H2(j) where j is Element of N : S1[j] } by Th19
.= { H1(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 Th23: :: WAYBEL11:23
for R being complete LATTICE
for N being constant net of R holds the_value_of N = lim_inf N
proof
let R be complete LATTICE; ::_thesis: for N being constant net of R holds the_value_of N = lim_inf N
let N be constant net of R; ::_thesis: the_value_of N = lim_inf N
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
set j = the Element of N;
A1: N . the Element of N is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }
proof
let b be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not b in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } or b <= N . the Element of N )
assume b in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: b <= N . the Element of N
then consider j0 being Element of N such that
A2: b = "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) ;
reconsider j0 = j0 as Element of N ;
consider i0 being Element of N such that
A3: i0 >= j0 and
i0 >= j0 by YELLOW_6:def_3;
A4: N . i0 in { (N . i) where i is Element of N : i >= j0 } by A3;
N . i0 = the_value_of N by YELLOW_6:16
.= N . the Element of N by YELLOW_6:16 ;
hence b <= N . the Element of N by A2, A4, YELLOW_2:22; ::_thesis: verum
end;
A5: for b being Element of R st b is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } holds
N . the Element of N <= b
proof
let b be Element of R; ::_thesis: ( b is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } implies N . the Element of N <= b )
set Y = { (N . i) where i is Element of N : i >= the Element of N } ;
A6: "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,R) in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
assume b is_>=_than { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: N . the Element of N <= b
then A7: b >= "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,R) by A6, LATTICE3:def_9;
A8: N . the Element of N is_<=_than { (N . i) where i is Element of N : i >= the Element of N }
proof
let c be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not c in { (N . i) where i is Element of N : i >= the Element of N } or N . the Element of N <= c )
assume c in { (N . i) where i is Element of N : i >= the Element of N } ; ::_thesis: N . the Element of N <= c
then consider i0 being Element of N such that
A9: c = N . i0 and
i0 >= the Element of N ;
N . the Element of N = the_value_of N by YELLOW_6:16
.= N . i0 by YELLOW_6:16 ;
hence N . the Element of N <= c by A9; ::_thesis: verum
end;
for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= the Element of N } holds
N . the Element of N >= b
proof
let c be Element of R; ::_thesis: ( c is_<=_than { (N . i) where i is Element of N : i >= the Element of N } implies N . the Element of N >= c )
consider i0 being Element of N such that
A10: i0 >= the Element of N and
i0 >= the Element of N by YELLOW_6:def_3;
A11: N . i0 in { (N . i) where i is Element of N : i >= the Element of N } by A10;
assume A12: c is_<=_than { (N . i) where i is Element of N : i >= the Element of N } ; ::_thesis: N . the Element of N >= c
N . the Element of N = the_value_of N by YELLOW_6:16
.= N . i0 by YELLOW_6:16 ;
hence N . the Element of N >= c by A11, A12, LATTICE3:def_8; ::_thesis: verum
end;
hence N . the Element of N <= b by A7, A8, YELLOW_0:33; ::_thesis: verum
end;
thus the_value_of N = N . the Element of N by YELLOW_6:16
.= lim_inf N by A1, A5, YELLOW_0:32 ; ::_thesis: verum
end;
theorem Th24: :: WAYBEL11:24
for R being complete LATTICE
for N being constant net of R holds the_value_of N is_S-limit_of N
proof
let R be complete LATTICE; ::_thesis: for N being constant net of R holds the_value_of N is_S-limit_of N
let N be constant net of R; ::_thesis: the_value_of N is_S-limit_of N
the_value_of N <= lim_inf N by Th23;
hence the_value_of N is_S-limit_of N by Def7; ::_thesis: verum
end;
definition
let S be non empty 1-sorted ;
let e be Element of S;
func Net-Str e -> strict NetStr over S means :Def11: :: WAYBEL11:def 11
( the carrier of it = {e} & the InternalRel of it = {[e,e]} & the mapping of it = id {e} );
existence
ex b1 being strict NetStr over S st
( the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} )
proof
e in {e} by TARSKI:def_1;
then reconsider r = {[e,e]} as Relation of {e} by RELSET_1:3;
A1: dom (id {e}) = {e} by RELAT_1:45;
rng (id {e}) = {e} by RELAT_1:45;
then reconsider f = id {e} as Function of {e}, the carrier of S by A1, RELSET_1:4;
take NetStr(# {e},r,f #) ; ::_thesis: ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} )
thus ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict NetStr over S st the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} & the carrier of b2 = {e} & the InternalRel of b2 = {[e,e]} & the mapping of b2 = id {e} holds
b1 = b2 ;
end;
:: deftheorem Def11 defines Net-Str WAYBEL11:def_11_:_
for S being non empty 1-sorted
for e being Element of S
for b3 being strict NetStr over S holds
( b3 = Net-Str e iff ( the carrier of b3 = {e} & the InternalRel of b3 = {[e,e]} & the mapping of b3 = id {e} ) );
registration
let S be non empty 1-sorted ;
let e be Element of S;
cluster Net-Str e -> non empty strict ;
coherence
not Net-Str e is empty
proof
set N = Net-Str e;
the carrier of (Net-Str e) = {e} by Def11;
hence not the carrier of (Net-Str e) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
theorem Th25: :: WAYBEL11:25
for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds x = e
proof
let S be non empty 1-sorted ; ::_thesis: for e being Element of S
for x being Element of (Net-Str e) holds x = e
let e be Element of S; ::_thesis: for x being Element of (Net-Str e) holds x = e
let x be Element of (Net-Str e); ::_thesis: x = e
the carrier of (Net-Str e) = {e} by Def11;
hence x = e by TARSKI:def_1; ::_thesis: verum
end;
theorem Th26: :: WAYBEL11:26
for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds (Net-Str e) . x = e
proof
let S be non empty 1-sorted ; ::_thesis: for e being Element of S
for x being Element of (Net-Str e) holds (Net-Str e) . x = e
let e be Element of S; ::_thesis: for x being Element of (Net-Str e) holds (Net-Str e) . x = e
let x be Element of (Net-Str e); ::_thesis: (Net-Str e) . x = e
set N = Net-Str e;
A1: the carrier of (Net-Str e) = {e} by Def11;
then A2: x = e by TARSKI:def_1;
thus (Net-Str e) . x = (id {e}) . x by Def11
.= e by A1, A2, FUNCT_1:18 ; ::_thesis: verum
end;
registration
let S be non empty 1-sorted ;
let e be Element of S;
cluster Net-Str e -> reflexive transitive antisymmetric strict directed ;
coherence
( Net-Str e is reflexive & Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )
proof
set N = Net-Str e;
the carrier of (Net-Str e) = {e} by Def11;
then reconsider e = e as Element of (Net-Str e) by TARSKI:def_1;
the InternalRel of (Net-Str e) = {[e,e]} by Def11;
then A1: [e,e] in the InternalRel of (Net-Str e) by TARSKI:def_1;
thus Net-Str e is reflexive ::_thesis: ( Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )
proof
let x be Element of (Net-Str e); :: according to YELLOW_0:def_1 ::_thesis: x <= x
x = e by Th25;
hence x <= x by A1, ORDERS_2:def_5; ::_thesis: verum
end;
thus Net-Str e is transitive ::_thesis: ( Net-Str e is directed & Net-Str e is antisymmetric )
proof
let x, y, z be Element of (Net-Str e); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
x <= y and
y <= z ; ::_thesis: x <= z
A2: x = e by Th25;
z = e by Th25;
hence x <= z by A1, A2, ORDERS_2:def_5; ::_thesis: verum
end;
thus Net-Str e is directed ::_thesis: Net-Str e is antisymmetric
proof
let x, y be Element of (Net-Str e); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of (Net-Str e) st
( x <= b1 & y <= b1 )
take e ; ::_thesis: ( x <= e & y <= e )
A3: x = e by Th25;
y = e by Th25;
hence ( x <= e & y <= e ) by A1, A3, ORDERS_2:def_5; ::_thesis: verum
end;
let x, y be Element of (Net-Str e); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
assume that
x <= y and
y <= x ; ::_thesis: x = y
x = e by Th25;
hence x = y by Th25; ::_thesis: verum
end;
end;
theorem Th27: :: WAYBEL11:27
for S being non empty 1-sorted
for e being Element of S
for X being set holds
( Net-Str e is_eventually_in X iff e in X )
proof
let S be non empty 1-sorted ; ::_thesis: for e being Element of S
for X being set holds
( Net-Str e is_eventually_in X iff e in X )
let e be Element of S; ::_thesis: for X being set holds
( Net-Str e is_eventually_in X iff e in X )
let X be set ; ::_thesis: ( Net-Str e is_eventually_in X iff e in X )
set N = Net-Str e;
the carrier of (Net-Str e) = {e} by Def11;
then reconsider d = e as Element of (Net-Str e) by TARSKI:def_1;
hereby ::_thesis: ( e in X implies Net-Str e is_eventually_in X )
assume Net-Str e is_eventually_in X ; ::_thesis: e in X
then consider x being Element of (Net-Str e) such that
A1: for y being Element of (Net-Str e) st x <= y holds
(Net-Str e) . y in X by WAYBEL_0:def_11;
(Net-Str e) . x in X by A1;
hence e in X by Th26; ::_thesis: verum
end;
assume A2: e in X ; ::_thesis: Net-Str e is_eventually_in X
take d ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (Net-Str e) holds
( not d <= b1 or (Net-Str e) . b1 in X )
let j be Element of (Net-Str e); ::_thesis: ( not d <= j or (Net-Str e) . j in X )
assume d <= j ; ::_thesis: (Net-Str e) . j in X
thus (Net-Str e) . j in X by A2, Th26; ::_thesis: verum
end;
theorem Th28: :: WAYBEL11:28
for S being non empty reflexive antisymmetric RelStr
for e being Element of S holds e = lim_inf (Net-Str e)
proof
let S be non empty reflexive antisymmetric RelStr ; ::_thesis: for e being Element of S holds e = lim_inf (Net-Str e)
let e be Element of S; ::_thesis: e = lim_inf (Net-Str e)
set N = Net-Str e;
set X = { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ;
reconsider e9 = e as Element of S ;
A1: { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } c= {e9}
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } or u in {e9} )
assume u in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ; ::_thesis: u in {e9}
then consider j being Element of (Net-Str e) such that
A2: u = "/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S) ;
set Y = { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ;
A3: { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } c= {e9}
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } or v in {e9} )
assume v in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ; ::_thesis: v in {e9}
then consider i being Element of (Net-Str e) such that
A4: v = (Net-Str e) . i and
i >= j ;
reconsider i9 = i as Element of (Net-Str e) ;
(Net-Str e) . i9 = e by Th26;
hence v in {e9} by A4, TARSKI:def_1; ::_thesis: verum
end;
reconsider j9 = j as Element of (Net-Str e) ;
j9 <= j9 ;
then (Net-Str e) . j in { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ;
then { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } = {e9} by A3, ZFMISC_1:33;
then u = e9 by A2, YELLOW_0:39;
hence u in {e9} by TARSKI:def_1; ::_thesis: verum
end;
set j = the Element of (Net-Str e);
"/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= the Element of (Net-Str e) } ,S) in { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } ;
then { ("/\" ( { ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j } ,S)) where j is Element of (Net-Str e) : verum } = {e9} by A1, ZFMISC_1:33;
hence e = lim_inf (Net-Str e) by YELLOW_0:39; ::_thesis: verum
end;
theorem Th29: :: WAYBEL11:29
for S being non empty reflexive RelStr
for e being Element of S holds Net-Str e in NetUniv S
proof
let S be non empty reflexive RelStr ; ::_thesis: for e being Element of S holds Net-Str e in NetUniv S
let e be Element of S; ::_thesis: Net-Str e in NetUniv S
set N = Net-Str e;
set UN = the_universe_of the carrier of S;
A1: the carrier of (Net-Str e) = {e} by Def11;
reconsider UN = the_universe_of the carrier of S as universal set ;
the_transitive-closure_of the carrier of S in UN by CLASSES1:2;
then the carrier of S in UN by CLASSES1:3, CLASSES1:52;
then the carrier of (Net-Str e) in the_universe_of the carrier of S by A1, CLASSES1:def_1;
hence Net-Str e in NetUniv S by YELLOW_6:def_11; ::_thesis: verum
end;
theorem Th30: :: WAYBEL11:30
for R being complete LATTICE
for Z being net of R
for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds
( not D is empty & D is directed )
proof
let R be complete LATTICE; ::_thesis: for Z being net of R
for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds
( not D is empty & D is directed )
let Z be net of R; ::_thesis: for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds
( not D is empty & D is directed )
let D be Subset of R; ::_thesis: ( D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } implies ( not D is empty & D is directed ) )
assume A1: D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } ; ::_thesis: ( not D is empty & D is directed )
set j = the Element of Z;
"/\" ( { (Z . k) where k is Element of Z : k >= the Element of Z } ,R) in D by A1;
hence not D is empty ; ::_thesis: D is directed
let x, y be Element of R; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in D or not y in D or ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 ) )
assume x in D ; ::_thesis: ( not y in D or ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 ) )
then consider jx being Element of Z such that
A2: x = "/\" ( { (Z . k) where k is Element of Z : k >= jx } ,R) by A1;
assume y in D ; ::_thesis: ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 )
then consider jy being Element of Z such that
A3: y = "/\" ( { (Z . k) where k is Element of Z : k >= jy } ,R) by A1;
reconsider jx = jx, jy = jy as Element of Z ;
consider j being Element of Z such that
A4: j >= jx and
A5: j >= jy by YELLOW_6:def_3;
set E1 = { (Z . k) where k is Element of Z : k >= jx } ;
set Ey = { (Z . k) where k is Element of Z : k >= jy } ;
set E = { (Z . k) where k is Element of Z : k >= j } ;
take z = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R); ::_thesis: ( z in D & x <= z & y <= z )
thus z in D by A1; ::_thesis: ( x <= z & y <= z )
{ (Z . k) where k is Element of Z : k >= j } c= { (Z . k) where k is Element of Z : k >= jx }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (Z . k) where k is Element of Z : k >= j } or e in { (Z . k) where k is Element of Z : k >= jx } )
assume e in { (Z . k) where k is Element of Z : k >= j } ; ::_thesis: e in { (Z . k) where k is Element of Z : k >= jx }
then consider k being Element of Z such that
A6: e = Z . k and
A7: k >= j ;
reconsider k = k as Element of Z ;
k >= jx by A4, A7, YELLOW_0:def_2;
hence e in { (Z . k) where k is Element of Z : k >= jx } by A6; ::_thesis: verum
end;
hence x <= z by A2, WAYBEL_7:1; ::_thesis: y <= z
{ (Z . k) where k is Element of Z : k >= j } c= { (Z . k) where k is Element of Z : k >= jy }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (Z . k) where k is Element of Z : k >= j } or e in { (Z . k) where k is Element of Z : k >= jy } )
assume e in { (Z . k) where k is Element of Z : k >= j } ; ::_thesis: e in { (Z . k) where k is Element of Z : k >= jy }
then consider k being Element of Z such that
A8: e = Z . k and
A9: k >= j ;
reconsider k = k as Element of Z ;
k >= jy by A5, A9, YELLOW_0:def_2;
hence e in { (Z . k) where k is Element of Z : k >= jy } by A8; ::_thesis: verum
end;
hence y <= z by A3, WAYBEL_7:1; ::_thesis: verum
end;
theorem Th31: :: WAYBEL11:31
for L being complete LATTICE
for S being Subset of L holds
( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
proof
let L be complete LATTICE; ::_thesis: for S being Subset of L holds
( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
set SC = Scott-Convergence L;
set T = ConvergenceSpace (Scott-Convergence L);
A1: the topology of (ConvergenceSpace (Scott-Convergence L)) = { V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in V } by YELLOW_6:def_24;
let S be Subset of L; ::_thesis: ( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
hereby ::_thesis: ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence L)) )
assume S in the topology of (ConvergenceSpace (Scott-Convergence L)) ; ::_thesis: ( S is inaccessible & S is upper )
then A2: ex V being Subset of L st
( S = V & ( for p being Element of L st p in V holds
for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in V ) ) by A1;
thus S is inaccessible ::_thesis: S is upper
proof
let D be non empty directed Subset of L; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume A3: sup D in S ; ::_thesis: D meets S
A4: dom (id D) = D by RELAT_1:45;
A5: rng (id D) = D by RELAT_1:45;
then reconsider f = id D as Function of D, the carrier of L by A4, RELSET_1:4;
reconsider N = Net-Str (D,f) as reflexive strict monotone net of L by A5, Th20;
A6: N in NetUniv L by Th21;
lim_inf N = sup N by Th22
.= Sup by WAYBEL_2:def_1
.= "\/" ((rng the mapping of N),L) by YELLOW_2:def_5
.= "\/" ((rng f),L) by Def10
.= sup D by RELAT_1:45 ;
then sup D is_S-limit_of N by Def7;
then [N,(sup D)] in Scott-Convergence L by A6, Def8;
then N is_eventually_in S by A2, A3;
then consider i0 being Element of N such that
A7: for j being Element of N st i0 <= j holds
N . j in S by WAYBEL_0:def_11;
consider j0 being Element of N such that
A8: j0 >= i0 and
j0 >= i0 by YELLOW_6:def_3;
A9: N . j0 in S by A7, A8;
A10: D = the carrier of N by Def10;
N . j0 = (id D) . j0 by Def10
.= j0 by A10, FUNCT_1:18 ;
hence D meets S by A9, A10, XBOOLE_0:3; ::_thesis: verum
end;
thus S is upper ::_thesis: verum
proof
let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in S or not x <= y or y in S )
assume that
A11: x in S and
A12: x <= y ; ::_thesis: y in S
A13: Net-Str y in NetUniv L by Th29;
y = lim_inf (Net-Str y) by Th28;
then x is_S-limit_of Net-Str y by A12, Def7;
then [(Net-Str y),x] in Scott-Convergence L by A13, Def8;
then Net-Str y is_eventually_in S by A2, A11;
hence y in S by Th27; ::_thesis: verum
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper ; ::_thesis: S in the topology of (ConvergenceSpace (Scott-Convergence L))
for p being Element of L st p in S holds
for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S
proof
let p be Element of L; ::_thesis: ( p in S implies for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S )
assume A16: p in S ; ::_thesis: for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S
reconsider p9 = p as Element of L ;
let N be net of L; ::_thesis: ( [N,p] in Scott-Convergence L implies N is_eventually_in S )
assume A17: [N,p] in Scott-Convergence L ; ::_thesis: N is_eventually_in S
Scott-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
then A18: N in NetUniv L by A17, ZFMISC_1:87;
then ex N9 being strict net of L st
( N9 = N & the carrier of N9 in the_universe_of the carrier of L ) by YELLOW_6:def_11;
then p is_S-limit_of N by A17, A18, Def8;
then A19: p9 <= lim_inf N by Def7;
defpred S1[ set ] means verum;
deffunc H1( Element of N) -> Element of the carrier of L = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,L);
set X = { H1(j) where j is Element of N : S1[j] } ;
{ H1(j) where j is Element of N : S1[j] } is Subset of L from DOMAIN_1:sch_8();
then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of L ;
reconsider D = D as non empty directed Subset of L by Th30;
sup D in S by A15, A16, A19, WAYBEL_0:def_20;
then D meets S by A14, Def1;
then D /\ S <> {} by XBOOLE_0:def_7;
then consider d being Element of L such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d = d as Element of L ;
d in D by A20, XBOOLE_0:def_4;
then consider j being Element of N such that
A21: d = "/\" ( { (N . i) where i is Element of N : i >= j } ,L) ;
reconsider j = j as Element of N ;
take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in S )
let i0 be Element of N; ::_thesis: ( not j <= i0 or N . i0 in S )
A22: d in S by A20, XBOOLE_0:def_4;
assume j <= i0 ; ::_thesis: N . i0 in S
then N . i0 in { (N . i) where i is Element of N : i >= j } ;
then d <= N . i0 by A21, YELLOW_2:22;
hence N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum
end;
hence S in the topology of (ConvergenceSpace (Scott-Convergence L)) by A1; ::_thesis: verum
end;
theorem Th32: :: WAYBEL11:32
for T being complete Scott TopLattice holds TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T)
proof
let T be complete Scott TopLattice; ::_thesis: TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T)
set CSC = ConvergenceSpace (Scott-Convergence T);
the topology of T = the topology of (ConvergenceSpace (Scott-Convergence T))
proof
thus the topology of T c= the topology of (ConvergenceSpace (Scott-Convergence T)) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (ConvergenceSpace (Scott-Convergence T)) c= the topology of T
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of T or e in the topology of (ConvergenceSpace (Scott-Convergence T)) )
assume A1: e in the topology of T ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence T))
then reconsider A = e as Subset of T ;
A is open by A1, PRE_TOPC:def_2;
then ( A is inaccessible & A is upper ) by Def4;
hence e in the topology of (ConvergenceSpace (Scott-Convergence T)) by Th31; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence T)) or e in the topology of T )
assume A2: e in the topology of (ConvergenceSpace (Scott-Convergence T)) ; ::_thesis: e in the topology of T
then reconsider A = e as Subset of T by YELLOW_6:def_24;
( A is inaccessible & A is upper ) by A2, Th31;
then A is open by Def4;
hence e in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
hence TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by YELLOW_6:def_24; ::_thesis: verum
end;
theorem Th33: :: WAYBEL11:33
for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds
for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) )
proof
let T be complete TopLattice; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) ) )
set SC = Scott-Convergence T;
assume TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) ; ::_thesis: for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) )
then A1: the topology of T = { V where V is Subset of T : for p being Element of T st p in V holds
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in V } by YELLOW_6:def_24;
let S be Subset of T; ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) )
hereby ::_thesis: ( S is inaccessible & S is upper implies S is open )
assume S is open ; ::_thesis: ( S is inaccessible & S is upper )
then S in the topology of T by PRE_TOPC:def_2;
then A2: ex V being Subset of T st
( S = V & ( for p being Element of T st p in V holds
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in V ) ) by A1;
thus S is inaccessible ::_thesis: S is upper
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume A3: sup D in S ; ::_thesis: D meets S
A4: dom (id D) = D by RELAT_1:45;
A5: rng (id D) = D by RELAT_1:45;
then reconsider f = id D as Function of D, the carrier of T by A4, RELSET_1:4;
reconsider N = Net-Str (D,f) as reflexive strict monotone net of T by A5, Th20;
A6: N in NetUniv T by Th21;
lim_inf N = sup N by Th22
.= Sup by WAYBEL_2:def_1
.= "\/" ((rng the mapping of N),T) by YELLOW_2:def_5
.= "\/" ((rng f),T) by Def10
.= sup D by RELAT_1:45 ;
then sup D is_S-limit_of N by Def7;
then [N,(sup D)] in Scott-Convergence T by A6, Def8;
then N is_eventually_in S by A2, A3;
then consider i0 being Element of N such that
A7: for j being Element of N st i0 <= j holds
N . j in S by WAYBEL_0:def_11;
consider j0 being Element of N such that
A8: j0 >= i0 and
j0 >= i0 by YELLOW_6:def_3;
A9: N . j0 in S by A7, A8;
A10: D = the carrier of N by Def10;
N . j0 = (id D) . j0 by Def10
.= j0 by A10, FUNCT_1:18 ;
hence D meets S by A9, A10, XBOOLE_0:3; ::_thesis: verum
end;
thus S is upper ::_thesis: verum
proof
let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in S or not x <= y or y in S )
assume that
A11: x in S and
A12: x <= y ; ::_thesis: y in S
A13: Net-Str y in NetUniv T by Th29;
y = lim_inf (Net-Str y) by Th28;
then x is_S-limit_of Net-Str y by A12, Def7;
then [(Net-Str y),x] in Scott-Convergence T by A13, Def8;
then Net-Str y is_eventually_in S by A2, A11;
hence y in S by Th27; ::_thesis: verum
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper ; ::_thesis: S is open
for p being Element of T st p in S holds
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S
proof
let p be Element of T; ::_thesis: ( p in S implies for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S )
assume A16: p in S ; ::_thesis: for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S
reconsider p9 = p as Element of T ;
let N be net of T; ::_thesis: ( [N,p] in Scott-Convergence T implies N is_eventually_in S )
assume A17: [N,p] in Scott-Convergence T ; ::_thesis: N is_eventually_in S
Scott-Convergence T c= [:(NetUniv T), the carrier of T:] by YELLOW_6:def_18;
then A18: N in NetUniv T by A17, ZFMISC_1:87;
then ex N9 being strict net of T st
( N9 = N & the carrier of N9 in the_universe_of the carrier of T ) by YELLOW_6:def_11;
then p is_S-limit_of N by A17, A18, Def8;
then A19: p9 <= lim_inf N by Def7;
defpred S1[ set ] means verum;
deffunc H1( Element of N) -> Element of the carrier of T = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,T);
set X = { H1(j) where j is Element of N : S1[j] } ;
{ H1(j) where j is Element of N : S1[j] } is Subset of T from DOMAIN_1:sch_8();
then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of T ;
reconsider D = D as non empty directed Subset of T by Th30;
sup D in S by A15, A16, A19, WAYBEL_0:def_20;
then D meets S by A14, Def1;
then D /\ S <> {} by XBOOLE_0:def_7;
then consider d being Element of T such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d = d as Element of T ;
d in D by A20, XBOOLE_0:def_4;
then consider j being Element of N such that
A21: d = "/\" ( { (N . i) where i is Element of N : i >= j } ,T) ;
reconsider j = j as Element of N ;
take j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in S )
let i0 be Element of N; ::_thesis: ( not j <= i0 or N . i0 in S )
A22: d in S by A20, XBOOLE_0:def_4;
assume j <= i0 ; ::_thesis: N . i0 in S
then N . i0 in { (N . i) where i is Element of N : i >= j } ;
then d <= N . i0 by A21, YELLOW_2:22;
hence N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum
end;
then S in the topology of T by A1;
hence S is open by PRE_TOPC:def_2; ::_thesis: verum
end;
theorem Th34: :: WAYBEL11:34
for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds
T is Scott
proof
let T be complete TopLattice; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies T is Scott )
assume TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) ; ::_thesis: T is Scott
hence for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) ) by Th33; :: according to WAYBEL11:def_4 ::_thesis: verum
end;
registration
let R be complete LATTICE;
cluster Scott-Convergence R -> (CONSTANTS) ;
coherence
Scott-Convergence R is (CONSTANTS)
proof
let N be constant net of R; :: according to YELLOW_6:def_20 ::_thesis: ( not N in NetUniv R or [N,(the_value_of N)] in Scott-Convergence R )
assume A1: N in NetUniv R ; ::_thesis: [N,(the_value_of N)] in Scott-Convergence R
then consider M being strict net of R such that
A2: M = N and
the carrier of M in the_universe_of the carrier of R by YELLOW_6:def_11;
the_value_of M is_S-limit_of M by A2, Th24;
hence [N,(the_value_of N)] in Scott-Convergence R by A1, A2, Def8; ::_thesis: verum
end;
end;
registration
let R be complete LATTICE;
cluster Scott-Convergence R -> (SUBNETS) ;
coherence
Scott-Convergence R is (SUBNETS)
proof
set S = Scott-Convergence R;
let N be net of R; :: according to YELLOW_6:def_21 ::_thesis: for b1 being subnet of N holds
( not b1 in NetUniv R or for b2 being Element of the carrier of R holds
( not [N,b2] in Scott-Convergence R or [b1,b2] in Scott-Convergence R ) )
let Y be subnet of N; ::_thesis: ( not Y in NetUniv R or for b1 being Element of the carrier of R holds
( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence R ) )
A1: Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
assume A2: Y in NetUniv R ; ::_thesis: for b1 being Element of the carrier of R holds
( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence R )
then consider Y9 being strict net of R such that
A3: Y9 = Y and
the carrier of Y9 in the_universe_of the carrier of R by YELLOW_6:def_11;
let p be Element of R; ::_thesis: ( not [N,p] in Scott-Convergence R or [Y,p] in Scott-Convergence R )
assume A4: [N,p] in Scott-Convergence R ; ::_thesis: [Y,p] in Scott-Convergence R
then A5: N in NetUniv R by A1, ZFMISC_1:87;
then consider N9 being strict net of R such that
A6: N9 = N and
the carrier of N9 in the_universe_of the carrier of R by YELLOW_6:def_11;
deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= R } ,R);
defpred S1[ set ] means verum;
reconsider X1 = { H1(j) where j is Element of N : S1[j] } as Subset of R from DOMAIN_1:sch_8();
deffunc H2( Element of Y) -> Element of the carrier of R = "/\" ( { (Y . i) where i is Element of Y : i >= R } ,R);
reconsider X2 = { H2(j) where j is Element of Y : S1[j] } as Subset of R from DOMAIN_1:sch_8();
p is_S-limit_of N9 by A4, A5, A6, Def8;
then A7: p <= lim_inf N by A6, Def7;
consider f being Function of Y,N such that
A8: the mapping of Y = the mapping of N * f and
A9: for m being Element of N ex n being Element of Y st
for p being Element of Y st n <= p holds
m <= f . p by YELLOW_6:def_9;
X1 is_finer_than X2
proof
let a be Element of R; :: according to YELLOW_4:def_1 ::_thesis: ( not a in X1 or ex b1 being Element of the carrier of R st
( b1 in X2 & a <= b1 ) )
assume a in X1 ; ::_thesis: ex b1 being Element of the carrier of R st
( b1 in X2 & a <= b1 )
then consider j being Element of N such that
A10: a = "/\" ( { (N . i) where i is Element of N : i >= j } ,R) ;
reconsider j = j as Element of N ;
consider n being Element of Y such that
A11: for p being Element of Y st n <= p holds
j <= f . p by A9;
set X3 = { (Y . i) where i is Element of Y : i >= n } ;
set X4 = { (N . i) where i is Element of N : i >= j } ;
take b = "/\" ( { (Y . i) where i is Element of Y : i >= n } ,R); ::_thesis: ( b in X2 & a <= b )
thus b in X2 ; ::_thesis: a <= b
{ (Y . i) where i is Element of Y : i >= n } c= { (N . i) where i is Element of N : i >= j }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (Y . i) where i is Element of Y : i >= n } or u in { (N . i) where i is Element of N : i >= j } )
assume u in { (Y . i) where i is Element of Y : i >= n } ; ::_thesis: u in { (N . i) where i is Element of N : i >= j }
then consider m being Element of Y such that
A12: u = Y . m and
A13: m >= n ;
reconsider m = m as Element of Y ;
A14: f . m >= j by A11, A13;
u = N . (f . m) by A8, A12, FUNCT_2:15;
hence u in { (N . i) where i is Element of N : i >= j } by A14; ::_thesis: verum
end;
hence a <= b by A10, WAYBEL_7:1; ::_thesis: verum
end;
then "\/" (X1,R) <= "\/" (X2,R) by Th2;
then p <= lim_inf Y by A7, YELLOW_0:def_2;
then p is_S-limit_of Y9 by A3, Def7;
hence [Y,p] in Scott-Convergence R by A2, A3, Def8; ::_thesis: verum
end;
end;
theorem Th35: :: WAYBEL11:35
for S being non empty 1-sorted
for N being net of S
for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let N be net of S; ::_thesis: for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let X be set ; ::_thesis: for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let M be subnet of N; ::_thesis: ( M = N " X implies for i being Element of M holds M . i in X )
assume A1: M = N " X ; ::_thesis: for i being Element of M holds M . i in X
let j be Element of M; ::_thesis: M . j in X
j in the carrier of M ;
then j in the mapping of N " X by A1, YELLOW_6:def_10;
then A2: the mapping of N . j in X by FUNCT_1:def_7;
the mapping of M = the mapping of N | the carrier of M by A1, YELLOW_6:def_6;
hence M . j in X by A2, FUNCT_1:49; ::_thesis: verum
end;
definition
let L be non empty reflexive RelStr ;
func sigma L -> Subset-Family of L equals :: WAYBEL11:def 12
the topology of (ConvergenceSpace (Scott-Convergence L));
coherence
the topology of (ConvergenceSpace (Scott-Convergence L)) is Subset-Family of L by YELLOW_6:def_24;
end;
:: deftheorem defines sigma WAYBEL11:def_12_:_
for L being non empty reflexive RelStr holds sigma L = the topology of (ConvergenceSpace (Scott-Convergence L));
theorem Th36: :: WAYBEL11:36
for L being complete continuous Scott TopLattice
for x being Element of L holds wayabove x is open
proof
let L be complete 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: ( sup D in wayabove x implies D meets wayabove x )
assume sup D in wayabove x ; ::_thesis: D meets 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 D meets wayabove x by A1, XBOOLE_0:3; ::_thesis: verum
end;
hence wayabove x is open by Def4; ::_thesis: verum
end;
theorem Th37: :: WAYBEL11:37
for T being complete TopLattice st the topology of T = sigma T holds
T is Scott
proof
let T be complete TopLattice; ::_thesis: ( the topology of T = sigma T implies T is Scott )
set CSC = ConvergenceSpace (Scott-Convergence T);
assume the topology of T = sigma T ; ::_thesis: T is Scott
then TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (ConvergenceSpace (Scott-Convergence T)), the topology of (ConvergenceSpace (Scott-Convergence T)) #) by YELLOW_6:def_24;
hence T is Scott by Th34; ::_thesis: verum
end;
Lm3: for T1, T2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like holds
T2 is TopSpace-like
proof
let T1, T2 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like implies T2 is TopSpace-like )
assume that
A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) and
A2: T1 is TopSpace-like ; ::_thesis: T2 is TopSpace-like
thus the carrier of T2 in the topology of T2 by A1, A2, PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T2) holds
( not b1 c= the topology of T2 or union b1 in the topology of T2 ) ) & ( for b1, b2 being Element of bool the carrier of T2 holds
( not b1 in the topology of T2 or not b2 in the topology of T2 or b1 /\ b2 in the topology of T2 ) ) )
thus ( ( for b1 being Element of bool (bool the carrier of T2) holds
( not b1 c= the topology of T2 or union b1 in the topology of T2 ) ) & ( for b1, b2 being Element of bool the carrier of T2 holds
( not b1 in the topology of T2 or not b2 in the topology of T2 or b1 /\ b2 in the topology of T2 ) ) ) by A1, A2, PRE_TOPC:def_1; ::_thesis: verum
end;
Lm4: for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being strict net of S1 holds N is strict net of S2
;
Lm5: for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
proof
let S1, S2 be non empty 1-sorted ; ::_thesis: ( the carrier of S1 = the carrier of S2 implies NetUniv S1 = NetUniv S2 )
assume A1: the carrier of S1 = the carrier of S2 ; ::_thesis: NetUniv S1 = NetUniv S2
defpred S1[ set ] means ex N being strict net of S2 st
( N = $1 & the carrier of N in the_universe_of the carrier of S2 );
A2: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_NetUniv_S1_implies_S1[x]_)_&_(_S1[x]_implies_x_in_NetUniv_S1_)_)
let x be set ; ::_thesis: ( ( x in NetUniv S1 implies S1[x] ) & ( S1[x] implies x in NetUniv S1 ) )
hereby ::_thesis: ( S1[x] implies x in NetUniv S1 )
assume x in NetUniv S1 ; ::_thesis: S1[x]
then consider N being strict net of S1 such that
A3: N = x and
A4: the carrier of N in the_universe_of the carrier of S1 by YELLOW_6:def_11;
reconsider N = N as strict net of S2 by A1;
thus S1[x] ::_thesis: verum
proof
take N ; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S2 )
thus ( N = x & the carrier of N in the_universe_of the carrier of S2 ) by A1, A3, A4; ::_thesis: verum
end;
end;
assume S1[x] ; ::_thesis: x in NetUniv S1
then consider N being strict net of S2 such that
A5: N = x and
A6: the carrier of N in the_universe_of the carrier of S2 ;
reconsider N = N as strict net of S1 by A1;
now__::_thesis:_ex_N_being_strict_net_of_S1_st_
(_N_=_x_&_the_carrier_of_N_in_the_universe_of_the_carrier_of_S1_)
take N = N; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S1 )
thus ( N = x & the carrier of N in the_universe_of the carrier of S1 ) by A1, A5, A6; ::_thesis: verum
end;
hence x in NetUniv S1 by YELLOW_6:def_11; ::_thesis: verum
end;
A7: for x being set holds
( x in NetUniv S2 iff S1[x] ) by YELLOW_6:def_11;
thus NetUniv S1 = NetUniv S2 from XBOOLE_0:sch_2(A2, A7); ::_thesis: verum
end;
Lm6: for T1, T2 being non empty 1-sorted
for X being set
for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
proof
let T1, T2 be non empty 1-sorted ; ::_thesis: for X being set
for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let X be set ; ::_thesis: for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let N1 be net of T1; ::_thesis: for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let N2 be net of T2; ::_thesis: ( N1 = N2 & N1 is_eventually_in X implies N2 is_eventually_in X )
assume A1: N1 = N2 ; ::_thesis: ( not N1 is_eventually_in X or N2 is_eventually_in X )
assume N1 is_eventually_in X ; ::_thesis: N2 is_eventually_in X
then consider i being Element of N1 such that
A2: for j being Element of N1 st i <= j holds
N1 . j in X by WAYBEL_0:def_11;
reconsider ii = i as Element of N2 by A1;
take ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds
( not ii <= b1 or N2 . b1 in X )
let jj be Element of N2; ::_thesis: ( not ii <= jj or N2 . jj in X )
reconsider j = jj as Element of N1 by A1;
assume A3: ii <= jj ; ::_thesis: N2 . jj in X
N2 . jj = N1 . j by A1;
hence N2 . jj in X by A1, A2, A3; ::_thesis: verum
end;
Lm7: for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
proof
let T1, T2 be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2 )
assume A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; ::_thesis: for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let N1 be net of T1; ::_thesis: for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let N2 be net of T2; ::_thesis: ( N1 = N2 implies for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2 )
assume A2: N1 = N2 ; ::_thesis: for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let p1 be Point of T1; ::_thesis: for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let p2 be Point of T2; ::_thesis: ( p1 = p2 & p1 in Lim N1 implies p2 in Lim N2 )
assume that
A3: p1 = p2 and
A4: p1 in Lim N1 ; ::_thesis: p2 in Lim N2
for V being a_neighborhood of p2 holds N2 is_eventually_in V
proof
let V be a_neighborhood of p2; ::_thesis: N2 is_eventually_in V
reconsider W = V as Subset of T1 by A1;
p2 in Int V by CONNSP_2:def_1;
then consider G being Subset of T2 such that
A5: G is open and
A6: G c= V and
A7: p2 in G by TOPS_1:22;
reconsider H = G as Subset of T1 by A1;
G in the topology of T2 by A5, PRE_TOPC:def_2;
then H is open by A1, PRE_TOPC:def_2;
then p1 in Int W by A3, A6, A7, TOPS_1:22;
then reconsider W = V as a_neighborhood of p1 by CONNSP_2:def_1;
thus N2 is_eventually_in V ::_thesis: verum
proof
N1 is_eventually_in W by A4, YELLOW_6:def_15;
then consider i being Element of N1 such that
A8: for j being Element of N1 st i <= j holds
N1 . j in W by WAYBEL_0:def_11;
reconsider ii = i as Element of N2 by A2;
take ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds
( not ii <= b1 or N2 . b1 in V )
let jj be Element of N2; ::_thesis: ( not ii <= jj or N2 . jj in V )
reconsider j = jj as Element of N1 by A2;
assume A9: ii <= jj ; ::_thesis: N2 . jj in V
N2 . jj = N1 . j by A2;
hence N2 . jj in V by A2, A8, A9; ::_thesis: verum
end;
end;
hence p2 in Lim N2 by YELLOW_6:def_15; ::_thesis: verum
end;
Lm8: for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
Convergence T1 = Convergence T2
proof
let T1, T2 be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies Convergence T1 = Convergence T2 )
assume A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; ::_thesis: Convergence T1 = Convergence T2
A2: Convergence T1 c= [:(NetUniv T1), the carrier of T1:] by YELLOW_6:def_18;
A3: Convergence T2 c= [:(NetUniv T2), the carrier of T2:] by YELLOW_6:def_18;
let u1, u2 be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [u1,u2] in Convergence T1 or [u1,u2] in Convergence T2 ) & ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 ) )
hereby ::_thesis: ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 )
assume A4: [u1,u2] in Convergence T1 ; ::_thesis: [u1,u2] in Convergence T2
then consider N1 being Element of NetUniv T1, p1 being Point of T1 such that
A5: [u1,u2] = [N1,p1] by A2, DOMAIN_1:1;
A6: N1 in NetUniv T1 ;
ex N being strict net of T1 st
( N = N1 & the carrier of N in the_universe_of the carrier of T1 ) by YELLOW_6:def_11;
then reconsider N1 = N1 as net of T1 ;
A7: p1 in Lim N1 by A4, A5, YELLOW_6:def_19;
reconsider N2 = N1 as net of T2 by A1;
reconsider p2 = p1 as Point of T2 by A1;
A8: N2 in NetUniv T2 by A1, A6, Lm5;
p2 in Lim N2 by A1, A7, Lm7;
hence [u1,u2] in Convergence T2 by A5, A8, YELLOW_6:def_19; ::_thesis: verum
end;
assume A9: [u1,u2] in Convergence T2 ; ::_thesis: [u1,u2] in Convergence T1
then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that
A10: [u1,u2] = [N1,p1] by A3, DOMAIN_1:1;
A11: N1 in NetUniv T2 ;
ex N being strict net of T2 st
( N = N1 & the carrier of N in the_universe_of the carrier of T2 ) by YELLOW_6:def_11;
then reconsider N1 = N1 as net of T2 ;
A12: p1 in Lim N1 by A9, A10, YELLOW_6:def_19;
reconsider N2 = N1 as net of T1 by A1;
reconsider p2 = p1 as Point of T1 by A1;
A13: N2 in NetUniv T1 by A1, A11, Lm5;
p2 in Lim N2 by A1, A12, Lm7;
hence [u1,u2] in Convergence T1 by A10, A13, YELLOW_6:def_19; ::_thesis: verum
end;
Lm9: for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE holds
R2 is LATTICE
proof
let R1, R2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE implies R2 is LATTICE )
assume that
A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and
A2: R1 is LATTICE ; ::_thesis: R2 is LATTICE
A3: R2 is with_infima
proof
let x, y be Element of R2; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of R2 st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of R2 holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
reconsider x9 = x, y9 = y as Element of R1 by A1;
consider z9 being Element of R1 such that
A4: z9 <= x9 and
A5: z9 <= y9 and
A6: for w9 being Element of R1 st w9 <= x9 & w9 <= y9 holds
w9 <= z9 by A2, LATTICE3:def_11;
reconsider z = z9 as Element of R2 by A1;
take z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of R2 holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
thus ( z <= x & z <= y ) by A1, A4, A5, Lm1; ::_thesis: for b1 being Element of the carrier of R2 holds
( not b1 <= x or not b1 <= y or b1 <= z )
let w be Element of R2; ::_thesis: ( not w <= x or not w <= y or w <= z )
reconsider w9 = w as Element of R1 by A1;
assume that
A7: w <= x and
A8: w <= y ; ::_thesis: w <= z
A9: w9 <= x9 by A1, A7, Lm1;
w9 <= y9 by A1, A8, Lm1;
then w9 <= z9 by A6, A9;
hence w <= z by A1, Lm1; ::_thesis: verum
end;
A10: R2 is with_suprema
proof
let x, y be Element of R2; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of R2 st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of R2 holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
reconsider x9 = x, y9 = y as Element of R1 by A1;
consider z9 being Element of R1 such that
A11: z9 >= x9 and
A12: z9 >= y9 and
A13: for w9 being Element of R1 st w9 >= x9 & w9 >= y9 holds
w9 >= z9 by A2, LATTICE3:def_10;
reconsider z = z9 as Element of R2 by A1;
take z ; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of R2 holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
thus ( z >= x & z >= y ) by A1, A11, A12, Lm1; ::_thesis: for b1 being Element of the carrier of R2 holds
( not x <= b1 or not y <= b1 or z <= b1 )
let w be Element of R2; ::_thesis: ( not x <= w or not y <= w or z <= w )
reconsider w9 = w as Element of R1 by A1;
assume that
A14: w >= x and
A15: w >= y ; ::_thesis: z <= w
A16: w9 >= x9 by A1, A14, Lm1;
w9 >= y9 by A1, A15, Lm1;
then w9 >= z9 by A13, A16;
hence z <= w by A1, Lm1; ::_thesis: verum
end;
A17: R2 is reflexive
proof
let x be Element of R2; :: according to YELLOW_0:def_1 ::_thesis: x <= x
reconsider x9 = x as Element of R1 by A1;
x9 <= x9 by A2, YELLOW_0:def_1;
hence x <= x by A1, Lm1; ::_thesis: verum
end;
A18: R2 is transitive
proof
let x, y, z be Element of R2; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
reconsider x9 = x, y9 = y, z9 = z as Element of R1 by A1;
assume that
A19: x <= y and
A20: y <= z ; ::_thesis: x <= z
A21: x9 <= y9 by A1, A19, Lm1;
y9 <= z9 by A1, A20, Lm1;
then x9 <= z9 by A2, A21, YELLOW_0:def_2;
hence x <= z by A1, Lm1; ::_thesis: verum
end;
R2 is antisymmetric
proof
let x, y be Element of R2; :: 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 R1 by A1;
assume that
A22: x <= y and
A23: y <= x ; ::_thesis: x = y
A24: x9 <= y9 by A1, A22, Lm1;
y9 <= x9 by A1, A23, Lm1;
hence x = y by A2, A24, YELLOW_0:def_3; ::_thesis: verum
end;
hence R2 is LATTICE by A3, A10, A17, A18; ::_thesis: verum
end;
Lm10: for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
proof
let R1, R2 be LATTICE; ::_thesis: for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
let X be set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
let p1 be Element of R1; ::_thesis: for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
let p2 be Element of R2; ::_thesis: ( p1 = p2 & X is_<=_than p1 implies X is_<=_than p2 )
assume that
A2: p1 = p2 and
A3: X is_<=_than p1 ; ::_thesis: X is_<=_than p2
let b2 be Element of R2; :: according to LATTICE3:def_9 ::_thesis: ( not b2 in X or b2 <= p2 )
reconsider b1 = b2 as Element of R1 by A1;
assume b2 in X ; ::_thesis: b2 <= p2
then p1 >= b1 by A3, LATTICE3:def_9;
hence b2 <= p2 by A1, A2, Lm1; ::_thesis: verum
end;
Lm11: for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
proof
let R1, R2 be LATTICE; ::_thesis: for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let X be set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let p1 be Element of R1; ::_thesis: for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let p2 be Element of R2; ::_thesis: ( p1 = p2 & X is_>=_than p1 implies X is_>=_than p2 )
assume that
A2: p1 = p2 and
A3: X is_>=_than p1 ; ::_thesis: X is_>=_than p2
let b2 be Element of R2; :: according to LATTICE3:def_8 ::_thesis: ( not b2 in X or p2 <= b2 )
reconsider b1 = b2 as Element of R1 by A1;
assume b2 in X ; ::_thesis: p2 <= b2
then p1 <= b1 by A3, LATTICE3:def_8;
hence p2 <= b2 by A1, A2, Lm1; ::_thesis: verum
end;
Lm12: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "\/" (D,R1) = "\/" (D,R2)
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being set holds "\/" (D,R1) = "\/" (D,R2) )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being set holds "\/" (D,R1) = "\/" (D,R2)
let D be set ; ::_thesis: "\/" (D,R1) = "\/" (D,R2)
reconsider b = "\/" (D,R1) as Element of R2 by A1;
A2: ex_sup_of D,R2 by YELLOW_0:17;
A3: ex_sup_of D,R1 by YELLOW_0:17;
then D is_<=_than "\/" (D,R1) by YELLOW_0:def_9;
then A4: D is_<=_than b by A1, Lm10;
for a being Element of R2 st D is_<=_than a holds
a >= b
proof
let a be Element of R2; ::_thesis: ( D is_<=_than a implies a >= b )
reconsider a9 = a as Element of R1 by A1;
assume D is_<=_than a ; ::_thesis: a >= b
then D is_<=_than a9 by A1, Lm10;
then a9 >= "\/" (D,R1) by A3, YELLOW_0:def_9;
hence a >= b by A1, Lm1; ::_thesis: verum
end;
hence "\/" (D,R1) = "\/" (D,R2) by A2, A4, YELLOW_0:def_9; ::_thesis: verum
end;
Lm13: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "/\" (D,R1) = "/\" (D,R2)
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being set holds "/\" (D,R1) = "/\" (D,R2) )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being set holds "/\" (D,R1) = "/\" (D,R2)
let D be set ; ::_thesis: "/\" (D,R1) = "/\" (D,R2)
reconsider b = "/\" (D,R1) as Element of R2 by A1;
A2: ex_inf_of D,R2 by YELLOW_0:17;
A3: ex_inf_of D,R1 by YELLOW_0:17;
then D is_>=_than "/\" (D,R1) by YELLOW_0:def_10;
then A4: D is_>=_than b by A1, Lm11;
for a being Element of R2 st D is_>=_than a holds
a <= b
proof
let a be Element of R2; ::_thesis: ( D is_>=_than a implies a <= b )
reconsider a9 = a as Element of R1 by A1;
assume D is_>=_than a ; ::_thesis: a <= b
then D is_>=_than a9 by A1, Lm11;
then a9 <= "/\" (D,R1) by A3, YELLOW_0:def_10;
hence a <= b by A1, Lm1; ::_thesis: verum
end;
hence "/\" (D,R1) = "/\" (D,R2) by A2, A4, YELLOW_0:def_10; ::_thesis: verum
end;
Lm14: for R1, R2 being non empty reflexive RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
proof
let R1, R2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
let D be Subset of R1; ::_thesis: for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
let D9 be Subset of R2; ::_thesis: ( D = D9 & D is directed implies D9 is directed )
assume that
A2: D = D9 and
A3: D is directed ; ::_thesis: D9 is directed
let x2, y2 be Element of R2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x2 in D9 or not y2 in D9 or ex b1 being Element of the carrier of R2 st
( b1 in D9 & x2 <= b1 & y2 <= b1 ) )
assume that
A4: x2 in D9 and
A5: y2 in D9 ; ::_thesis: ex b1 being Element of the carrier of R2 st
( b1 in D9 & x2 <= b1 & y2 <= b1 )
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
consider z1 being Element of R1 such that
A6: z1 in D and
A7: x1 <= z1 and
A8: y1 <= z1 by A2, A3, A4, A5, WAYBEL_0:def_1;
reconsider z2 = z1 as Element of R2 by A1;
take z2 ; ::_thesis: ( z2 in D9 & x2 <= z2 & y2 <= z2 )
thus z2 in D9 by A2, A6; ::_thesis: ( x2 <= z2 & y2 <= z2 )
thus ( x2 <= z2 & y2 <= z2 ) by A1, A7, A8, Lm1; ::_thesis: verum
end;
Lm15: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
let p, q be Element of R1; ::_thesis: ( p << q implies for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9 )
assume A2: p << q ; ::_thesis: for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
let p9, q9 be Element of R2; ::_thesis: ( p = p9 & q = q9 implies p9 << q9 )
assume that
A3: p = p9 and
A4: q = q9 ; ::_thesis: p9 << q9
let D9 be non empty directed Subset of R2; :: according to WAYBEL_3:def_1 ::_thesis: ( not q9 <= "\/" (D9,R2) or ex b1 being Element of the carrier of R2 st
( b1 in D9 & p9 <= b1 ) )
assume A5: q9 <= sup D9 ; ::_thesis: ex b1 being Element of the carrier of R2 st
( b1 in D9 & p9 <= b1 )
reconsider D = D9 as non empty Subset of R1 by A1;
reconsider D = D as non empty directed Subset of R1 by A1, Lm14;
sup D = sup D9 by A1, Lm12;
then q <= sup D by A1, A4, A5, Lm1;
then consider d being Element of R1 such that
A6: d in D and
A7: p <= d by A2, WAYBEL_3:def_1;
reconsider d9 = d as Element of R2 by A1;
take d9 ; ::_thesis: ( d9 in D9 & p9 <= d9 )
thus d9 in D9 by A6; ::_thesis: p9 <= d9
thus p9 <= d9 by A1, A3, A7, Lm1; ::_thesis: verum
end;
Lm16: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
let N2 be net of R2; ::_thesis: ( N1 = N2 implies lim_inf N1 = lim_inf N2 )
assume A2: N1 = N2 ; ::_thesis: lim_inf N1 = lim_inf N2
set X1 = { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ;
set X2 = { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ;
{ ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } = { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum }
proof
thus { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } c= { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } :: according to XBOOLE_0:def_10 ::_thesis: { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } c= { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } or e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } )
assume e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ; ::_thesis: e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum }
then consider j1 being Element of N1 such that
A3: e = "/\" ( { (N1 . i) where i is Element of N1 : i >= j1 } ,R1) ;
reconsider j2 = j1 as Element of N2 by A2;
set Y1 = { (N1 . i) where i is Element of N1 : i >= j1 } ;
set Y2 = { (N2 . i) where i is Element of N2 : i >= j2 } ;
{ (N1 . i) where i is Element of N1 : i >= j1 } = { (N2 . i) where i is Element of N2 : i >= j2 }
proof
thus { (N1 . i) where i is Element of N1 : i >= j1 } c= { (N2 . i) where i is Element of N2 : i >= j2 } :: according to XBOOLE_0:def_10 ::_thesis: { (N2 . i) where i is Element of N2 : i >= j2 } c= { (N1 . i) where i is Element of N1 : i >= j1 }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N1 . i) where i is Element of N1 : i >= j1 } or u in { (N2 . i) where i is Element of N2 : i >= j2 } )
assume u in { (N1 . i) where i is Element of N1 : i >= j1 } ; ::_thesis: u in { (N2 . i) where i is Element of N2 : i >= j2 }
then consider i1 being Element of N1 such that
A4: u = N1 . i1 and
A5: j1 <= i1 ;
reconsider i2 = i1 as Element of N2 by A2;
N2 . i2 = u by A2, A4;
hence u in { (N2 . i) where i is Element of N2 : i >= j2 } by A2, A5; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N2 . i) where i is Element of N2 : i >= j2 } or u in { (N1 . i) where i is Element of N1 : i >= j1 } )
assume u in { (N2 . i) where i is Element of N2 : i >= j2 } ; ::_thesis: u in { (N1 . i) where i is Element of N1 : i >= j1 }
then consider i2 being Element of N2 such that
A6: u = N2 . i2 and
A7: j2 <= i2 ;
reconsider i1 = i2 as Element of N1 by A2;
N1 . i1 = u by A2, A6;
hence u in { (N1 . i) where i is Element of N1 : i >= j1 } by A2, A7; ::_thesis: verum
end;
then e = "/\" ( { (N2 . i) where i is Element of N2 : i >= j2 } ,R2) by A1, A3, Lm13;
hence e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } or e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } )
assume e in { ("/\" ( { (N2 . i) where i is Element of N2 : i >= j } ,R2)) where j is Element of N2 : verum } ; ::_thesis: e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum }
then consider j1 being Element of N2 such that
A8: e = "/\" ( { (N2 . i) where i is Element of N2 : i >= j1 } ,R2) ;
reconsider j2 = j1 as Element of N1 by A2;
set Y1 = { (N2 . i) where i is Element of N2 : i >= j1 } ;
set Y2 = { (N1 . i) where i is Element of N1 : i >= j2 } ;
{ (N2 . i) where i is Element of N2 : i >= j1 } = { (N1 . i) where i is Element of N1 : i >= j2 }
proof
thus { (N2 . i) where i is Element of N2 : i >= j1 } c= { (N1 . i) where i is Element of N1 : i >= j2 } :: according to XBOOLE_0:def_10 ::_thesis: { (N1 . i) where i is Element of N1 : i >= j2 } c= { (N2 . i) where i is Element of N2 : i >= j1 }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N2 . i) where i is Element of N2 : i >= j1 } or u in { (N1 . i) where i is Element of N1 : i >= j2 } )
assume u in { (N2 . i) where i is Element of N2 : i >= j1 } ; ::_thesis: u in { (N1 . i) where i is Element of N1 : i >= j2 }
then consider i1 being Element of N2 such that
A9: u = N2 . i1 and
A10: j1 <= i1 ;
reconsider i2 = i1 as Element of N1 by A2;
N1 . i2 = u by A2, A9;
hence u in { (N1 . i) where i is Element of N1 : i >= j2 } by A2, A10; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (N1 . i) where i is Element of N1 : i >= j2 } or u in { (N2 . i) where i is Element of N2 : i >= j1 } )
assume u in { (N1 . i) where i is Element of N1 : i >= j2 } ; ::_thesis: u in { (N2 . i) where i is Element of N2 : i >= j1 }
then consider i2 being Element of N1 such that
A11: u = N1 . i2 and
A12: j2 <= i2 ;
reconsider i1 = i2 as Element of N2 by A2;
N2 . i1 = u by A2, A11;
hence u in { (N2 . i) where i is Element of N2 : i >= j1 } by A2, A12; ::_thesis: verum
end;
then e = "/\" ( { (N1 . i) where i is Element of N1 : i >= j2 } ,R1) by A1, A8, Lm13;
hence e in { ("/\" ( { (N1 . i) where i is Element of N1 : i >= j } ,R1)) where j is Element of N1 : verum } ; ::_thesis: verum
end;
hence lim_inf N1 = lim_inf N2 by A1, Lm12; ::_thesis: verum
end;
Lm17: for R1, R2 being non empty reflexive RelStr
for X being non empty set
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
proof
let R1, R2 be non empty reflexive RelStr ; ::_thesis: for X being non empty set
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let X be non empty set ; ::_thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let N2 be net of R2; ::_thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2 )
assume A1: N1 = N2 ; ::_thesis: for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let J1 be net_set of the carrier of N1,R1; ::_thesis: for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let J2 be net_set of the carrier of N2,R2; ::_thesis: ( J1 = J2 implies Iterated J1 = Iterated J2 )
assume A2: J1 = J2 ; ::_thesis: Iterated J1 = Iterated J2
A3: RelStr(# the carrier of (Iterated J1), the InternalRel of (Iterated J1) #) = [:N1,(product J1):] by YELLOW_6:def_13;
A4: RelStr(# the carrier of (Iterated J2), the InternalRel of (Iterated J2) #) = [:N2,(product J2):] by YELLOW_6:def_13;
set f = the mapping of (Iterated J1);
set g = the mapping of (Iterated J2);
A5: dom the mapping of (Iterated J1) = the carrier of (Iterated J2) by A1, A2, A3, A4, FUNCT_2:def_1
.= dom the mapping of (Iterated J2) by FUNCT_2:def_1 ;
for x being set st x in dom the mapping of (Iterated J1) holds
the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x
proof
let x be set ; ::_thesis: ( x in dom the mapping of (Iterated J1) implies the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x )
assume x in dom the mapping of (Iterated J1) ; ::_thesis: the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x
then x in the carrier of (Iterated J1) ;
then x in [: the carrier of N1, the carrier of (product J1):] by A3, YELLOW_3:def_2;
then consider x1 being Element of N1, x2 being Element of (product J1) such that
A6: x = [x1,x2] by DOMAIN_1:1;
reconsider y1 = x1 as Element of N2 by A1;
reconsider y2 = x2 as Element of (product J2) by A1, A2;
thus the mapping of (Iterated J1) . x = the mapping of (Iterated J1) . (x1,x2) by A6
.= the mapping of (J1 . x1) . (x2 . x1) by YELLOW_6:def_13
.= the mapping of (J2 . y1) . (y2 . y1) by A2
.= the mapping of (Iterated J2) . (y1,y2) by YELLOW_6:def_13
.= the mapping of (Iterated J2) . x by A6 ; ::_thesis: verum
end;
then the mapping of (Iterated J1) = the mapping of (Iterated J2) by A5, FUNCT_1:2;
hence Iterated J1 = Iterated J2 by A1, A2, A3, A4; ::_thesis: verum
end;
Lm18: for R1, R2 being non empty reflexive RelStr
for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
proof
let R1, R2 be non empty reflexive RelStr ; ::_thesis: for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let X be non empty set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let N2 be net of R2; ::_thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 )
assume A2: N1 = N2 ; ::_thesis: for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let J1 be net_set of the carrier of N1,R1; ::_thesis: J1 is net_set of the carrier of N2,R2
reconsider J2 = J1 as ManySortedSet of the carrier of N2 by A2;
for i being set st i in rng J2 holds
i is net of R2
proof
let i be set ; ::_thesis: ( i in rng J2 implies i is net of R2 )
assume i in rng J2 ; ::_thesis: i is net of R2
then reconsider N = i as net of R1 by YELLOW_6:def_12;
N is NetStr over R2 by A1;
hence i is net of R2 ; ::_thesis: verum
end;
hence J1 is net_set of the carrier of N2,R2 by YELLOW_6:def_12; ::_thesis: verum
end;
Lm19: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 c= Scott-Convergence R2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies Scott-Convergence R1 c= Scott-Convergence R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: Scott-Convergence R1 c= Scott-Convergence R2
A2: Scott-Convergence R1 c= [:(NetUniv R1), the carrier of R1:] by YELLOW_6:def_18;
for e being set st e in Scott-Convergence R1 holds
e in Scott-Convergence R2
proof
let e be set ; ::_thesis: ( e in Scott-Convergence R1 implies e in Scott-Convergence R2 )
assume A3: e in Scott-Convergence R1 ; ::_thesis: e in Scott-Convergence R2
then consider N1 being Element of NetUniv R1, p1 being Element of R1 such that
A4: e = [N1,p1] by A2, DOMAIN_1:1;
A5: N1 in NetUniv R1 ;
A6: ex N being strict net of R1 st
( N1 = N & the carrier of N in the_universe_of the carrier of R1 ) by YELLOW_6:def_11;
then reconsider N2 = N1 as strict net of R2 by A1, Lm4;
reconsider N1 = N1 as strict net of R1 by A6;
reconsider p2 = p1 as Element of R2 by A1;
A7: N2 in NetUniv R2 by A1, A5, Lm5;
A8: lim_inf N1 = lim_inf N2 by A1, Lm16;
p1 is_S-limit_of N1 by A3, A4, Def8;
then p1 <= lim_inf N1 by Def7;
then p2 <= lim_inf N2 by A1, A8, Lm1;
then p2 is_S-limit_of N2 by Def7;
hence e in Scott-Convergence R2 by A4, A7, Def8; ::_thesis: verum
end;
hence Scott-Convergence R1 c= Scott-Convergence R2 by TARSKI:def_3; ::_thesis: verum
end;
Lm20: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 = Scott-Convergence R2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies Scott-Convergence R1 = Scott-Convergence R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: Scott-Convergence R1 = Scott-Convergence R2
then A2: Scott-Convergence R1 c= Scott-Convergence R2 by Lm19;
Scott-Convergence R2 c= Scott-Convergence R1 by A1, Lm19;
hence Scott-Convergence R1 = Scott-Convergence R2 by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm21: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
sigma R1 = sigma R2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies sigma R1 = sigma R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: sigma R1 = sigma R2
set T1 = ConvergenceSpace (Scott-Convergence R1);
set T2 = ConvergenceSpace (Scott-Convergence R2);
A2: the topology of (ConvergenceSpace (Scott-Convergence R1)) = { V where V is Subset of R1 : for p being Element of R1 st p in V holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V } by YELLOW_6:def_24;
A3: the topology of (ConvergenceSpace (Scott-Convergence R2)) = { V where V is Subset of R2 : for p being Element of R2 st p in V holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V } by YELLOW_6:def_24;
the topology of (ConvergenceSpace (Scott-Convergence R1)) = the topology of (ConvergenceSpace (Scott-Convergence R2))
proof
thus the topology of (ConvergenceSpace (Scott-Convergence R1)) c= the topology of (ConvergenceSpace (Scott-Convergence R2)) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (ConvergenceSpace (Scott-Convergence R2)) c= the topology of (ConvergenceSpace (Scott-Convergence R1))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R1)) or e in the topology of (ConvergenceSpace (Scott-Convergence R2)) )
assume e in the topology of (ConvergenceSpace (Scott-Convergence R1)) ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R2))
then consider V1 being Subset of R1 such that
A4: e = V1 and
A5: for p being Element of R1 st p in V1 holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V1 by A2;
reconsider V2 = V1 as Subset of R2 by A1;
for p being Element of R2 st p in V2 holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V2
proof
let p2 be Element of R2; ::_thesis: ( p2 in V2 implies for N being net of R2 st [N,p2] in Scott-Convergence R2 holds
N is_eventually_in V2 )
assume A6: p2 in V2 ; ::_thesis: for N being net of R2 st [N,p2] in Scott-Convergence R2 holds
N is_eventually_in V2
reconsider p1 = p2 as Element of R1 by A1;
let N2 be net of R2; ::_thesis: ( [N2,p2] in Scott-Convergence R2 implies N2 is_eventually_in V2 )
reconsider N1 = N2 as net of R1 by A1;
assume [N2,p2] in Scott-Convergence R2 ; ::_thesis: N2 is_eventually_in V2
then [N1,p1] in Scott-Convergence R1 by A1, Lm20;
hence N2 is_eventually_in V2 by A5, A6, Lm6; ::_thesis: verum
end;
hence e in the topology of (ConvergenceSpace (Scott-Convergence R2)) by A3, A4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R2)) or e in the topology of (ConvergenceSpace (Scott-Convergence R1)) )
assume e in the topology of (ConvergenceSpace (Scott-Convergence R2)) ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R1))
then consider V1 being Subset of R2 such that
A7: e = V1 and
A8: for p being Element of R2 st p in V1 holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V1 by A3;
reconsider V2 = V1 as Subset of R1 by A1;
for p being Element of R1 st p in V2 holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V2
proof
let p2 be Element of R1; ::_thesis: ( p2 in V2 implies for N being net of R1 st [N,p2] in Scott-Convergence R1 holds
N is_eventually_in V2 )
assume A9: p2 in V2 ; ::_thesis: for N being net of R1 st [N,p2] in Scott-Convergence R1 holds
N is_eventually_in V2
reconsider p1 = p2 as Element of R2 by A1;
let N2 be net of R1; ::_thesis: ( [N2,p2] in Scott-Convergence R1 implies N2 is_eventually_in V2 )
reconsider N1 = N2 as net of R2 by A1;
assume [N2,p2] in Scott-Convergence R1 ; ::_thesis: N2 is_eventually_in V2
then [N1,p1] in Scott-Convergence R2 by A1, Lm20;
hence N2 is_eventually_in V2 by A8, A9, Lm6; ::_thesis: verum
end;
hence e in the topology of (ConvergenceSpace (Scott-Convergence R1)) by A2, A7; ::_thesis: verum
end;
hence sigma R1 = sigma R2 ; ::_thesis: verum
end;
Lm22: for R1, R2 being LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete holds
R2 is complete
proof
let R1, R2 be LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete implies R2 is complete )
assume that
A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and
A2: R1 is complete ; ::_thesis: R2 is complete
let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of R2 st
( X is_<=_than b1 & ( for b2 being Element of the carrier of R2 holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
consider a1 being Element of R1 such that
A3: X is_<=_than a1 and
A4: for b being Element of R1 st X is_<=_than b holds
a1 <= b by A2, LATTICE3:def_12;
reconsider a2 = a1 as Element of R2 by A1;
take a2 ; ::_thesis: ( X is_<=_than a2 & ( for b1 being Element of the carrier of R2 holds
( not X is_<=_than b1 or a2 <= b1 ) ) )
thus X is_<=_than a2 by A1, A3, Lm10; ::_thesis: for b1 being Element of the carrier of R2 holds
( not X is_<=_than b1 or a2 <= b1 )
let b2 be Element of R2; ::_thesis: ( not X is_<=_than b2 or a2 <= b2 )
reconsider b1 = b2 as Element of R1 by A1;
assume X is_<=_than b2 ; ::_thesis: a2 <= b2
then X is_<=_than b1 by A1, Lm10;
hence a2 <= b2 by A1, A4, Lm1; ::_thesis: verum
end;
Lm23: for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous holds
R2 is continuous
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous implies R2 is continuous )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: ( not R1 is continuous or R2 is continuous )
assume A2: R1 is continuous ; ::_thesis: R2 is continuous
thus A3: for x being Element of R2 holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( R2 is up-complete & R2 is satisfying_axiom_of_approximation )
thus R2 is up-complete ; ::_thesis: R2 is satisfying_axiom_of_approximation
A4: for x being Element of R1 holds
( not waybelow x is empty & waybelow x is directed ) ;
for x, y being Element of R2 st not x <= y holds
ex u being Element of R2 st
( u << x & not u <= y )
proof
let x2, y2 be Element of R2; ::_thesis: ( not x2 <= y2 implies ex u being Element of R2 st
( u << x2 & not u <= y2 ) )
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
assume not x2 <= y2 ; ::_thesis: ex u being Element of R2 st
( u << x2 & not u <= y2 )
then not x1 <= y1 by A1, Lm1;
then consider u1 being Element of R1 such that
A5: u1 << x1 and
A6: not u1 <= y1 by A2, A4, WAYBEL_3:24;
reconsider u2 = u1 as Element of R2 by A1;
take u2 ; ::_thesis: ( u2 << x2 & not u2 <= y2 )
thus u2 << x2 by A1, A5, Lm15; ::_thesis: not u2 <= y2
thus not u2 <= y2 by A1, A6, Lm1; ::_thesis: verum
end;
hence R2 is satisfying_axiom_of_approximation by A3, WAYBEL_3:24; ::_thesis: verum
end;
registration
let R be complete continuous LATTICE;
cluster Scott-Convergence R -> topological ;
coherence
Scott-Convergence R is topological
proof
set C = Scott-Convergence R;
thus ( Scott-Convergence R is (CONSTANTS) & Scott-Convergence R is (SUBNETS) ) ; :: according to YELLOW_6:def_25 ::_thesis: ( Scott-Convergence R is (DIVERGENCE) & Scott-Convergence R is (ITERATED_LIMITS) )
thus Scott-Convergence R is (DIVERGENCE) ::_thesis: Scott-Convergence R is (ITERATED_LIMITS)
proof
let X be net of R; :: according to YELLOW_6:def_22 ::_thesis: for b1 being Element of the carrier of R holds
( not X in NetUniv R or [X,b1] in Scott-Convergence R or ex b2 being subnet of X st
( b2 in NetUniv R & ( for b3 being subnet of b2 holds not [b3,b1] in Scott-Convergence R ) ) )
let p be Element of R; ::_thesis: ( not X in NetUniv R or [X,p] in Scott-Convergence R or ex b1 being subnet of X st
( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) ) )
assume that
A1: X in NetUniv R and
A2: not [X,p] in Scott-Convergence R ; ::_thesis: ex b1 being subnet of X st
( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) )
A3: for x being Element of R holds
( not waybelow x is empty & waybelow x is directed ) ;
reconsider p9 = p as Element of R ;
consider N being strict net of R such that
A4: N = X and
the carrier of N in the_universe_of the carrier of R by A1, YELLOW_6:def_11;
not p is_S-limit_of N by A1, A2, A4, Def8;
then not p <= lim_inf X by A4, Def7;
then consider u being Element of R such that
A5: u << p9 and
A6: not u <= lim_inf X by A3, WAYBEL_3:24;
set A = { a where a is Element of R : not a >= u } ;
X is_often_in { a where a is Element of R : not a >= u }
proof
let i be Element of X; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of X st
( i <= b1 & X . b1 in { a where a is Element of R : not a >= u } )
set B = { (X . j) where j is Element of X : j >= i } ;
set C = { ("/\" ( { (X . k) where k is Element of X : k >= j } ,R)) where j is Element of X : verum } ;
"/\" ( { (X . j) where j is Element of X : j >= i } ,R) in { ("/\" ( { (X . k) where k is Element of X : k >= j } ,R)) where j is Element of X : verum } ;
then "/\" ( { (X . j) where j is Element of X : j >= i } ,R) <= lim_inf X by YELLOW_2:22;
then not u <= "/\" ( { (X . j) where j is Element of X : j >= i } ,R) by A6, YELLOW_0:def_2;
then not u is_<=_than { (X . j) where j is Element of X : j >= i } by YELLOW_0:33;
then consider b being Element of R such that
A7: b in { (X . j) where j is Element of X : j >= i } and
A8: not u <= b by LATTICE3:def_8;
consider j being Element of X such that
A9: b = X . j and
A10: j >= i by A7;
take j ; ::_thesis: ( i <= j & X . j in { a where a is Element of R : not a >= u } )
thus i <= j by A10; ::_thesis: X . j in { a where a is Element of R : not a >= u }
thus X . j in { a where a is Element of R : not a >= u } by A8, A9; ::_thesis: verum
end;
then reconsider Y = X " { a where a is Element of R : not a >= u } as subnet of X by YELLOW_6:22;
take Y ; ::_thesis: ( Y in NetUniv R & ( for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R ) )
reconsider UN = the_universe_of the carrier of R as universal set ;
A11: ex N being strict net of R st
( X = N & the carrier of N in UN ) by A1, YELLOW_6:def_11;
X " { a where a is Element of R : not a >= u } is SubRelStr of X by YELLOW_6:def_6;
then the carrier of (X " { a where a is Element of R : not a >= u } ) c= the carrier of X by YELLOW_0:def_13;
then the carrier of Y in UN by A11, CLASSES1:def_1;
hence Y in NetUniv R by YELLOW_6:def_11; ::_thesis: for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R
let Z be subnet of Y; ::_thesis: not [Z,p] in Scott-Convergence R
assume A12: [Z,p] in Scott-Convergence R ; ::_thesis: contradiction
Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
then A13: Z in NetUniv R by A12, ZFMISC_1:87;
then consider ZZ being strict net of R such that
A14: ZZ = Z and
the carrier of ZZ in UN by YELLOW_6:def_11;
deffunc H1( Element of Z) -> Element of the carrier of R = "/\" ( { (Z . i) where i is Element of Z : i >= R } ,R);
defpred S1[ set ] means verum;
set D = { H1(j) where j is Element of Z : S1[j] } ;
{ H1(j) where j is Element of Z : S1[j] } is Subset of R from DOMAIN_1:sch_8();
then reconsider D = { H1(j) where j is Element of Z : S1[j] } as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th30;
p is_S-limit_of ZZ by A12, A13, A14, Def8;
then p <= lim_inf Z by A14, Def7;
then consider d being Element of R such that
A15: d in D and
A16: u <= d by A5, WAYBEL_3:def_1;
consider j being Element of Z such that
A17: d = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R) by A15;
reconsider j9 = j as Element of Z ;
consider i being Element of Z such that
A18: i >= j9 and
i >= j9 by YELLOW_6:def_3;
consider f being Function of Z,Y such that
A19: the mapping of Z = the mapping of Y * f and
for m being Element of Y ex n being Element of Z st
for p being Element of Z st n <= p holds
m <= f . p by YELLOW_6:def_9;
Z . i in { (Z . k) where k is Element of Z : k >= j } by A18;
then A20: d <= Z . i by A17, YELLOW_2:22;
Y . (f . i) = Z . i by A19, FUNCT_2:15;
then Z . i in { a where a is Element of R : not a >= u } by Th35;
then ex a being Element of R st
( a = Z . i & not a >= u ) ;
hence contradiction by A16, A20, YELLOW_0:def_2; ::_thesis: verum
end;
thus Scott-Convergence R is (ITERATED_LIMITS) ::_thesis: verum
proof
let X be net of R; :: according to YELLOW_6:def_23 ::_thesis: for b1 being Element of the carrier of R holds
( not [X,b1] in Scott-Convergence R or for b2 being net_set of the carrier of X,R holds
( ex b3 being Element of the carrier of X st not [(b2 . b3),(X . b3)] in Scott-Convergence R or [(Iterated b2),b1] in Scott-Convergence R ) )
let p be Element of R; ::_thesis: ( not [X,p] in Scott-Convergence R or for b1 being net_set of the carrier of X,R holds
( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R ) )
assume A21: [X,p] in Scott-Convergence R ; ::_thesis: for b1 being net_set of the carrier of X,R holds
( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R )
let J be net_set of the carrier of X,R; ::_thesis: ( ex b1 being Element of the carrier of X st not [(J . b1),(X . b1)] in Scott-Convergence R or [(Iterated J),p] in Scott-Convergence R )
assume A22: for i being Element of X holds [(J . i),(X . i)] in Scott-Convergence R ; ::_thesis: [(Iterated J),p] in Scott-Convergence R
A23: Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
then A24: X in NetUniv R by A21, ZFMISC_1:87;
for i being Element of X holds J . i in NetUniv R
proof
let i be Element of X; ::_thesis: J . i in NetUniv R
[(J . i),(X . i)] in Scott-Convergence R by A22;
hence J . i in NetUniv R by A23, ZFMISC_1:87; ::_thesis: verum
end;
then A25: Iterated J in NetUniv R by A24, YELLOW_6:25;
reconsider p9 = p as Element of R ;
set q = lim_inf (Iterated J);
lim_inf (Iterated J) is_>=_than waybelow p9
proof
let u be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not u in waybelow p9 or u <= lim_inf (Iterated J) )
assume u in waybelow p9 ; ::_thesis: u <= lim_inf (Iterated J)
then A26: u << p9 by WAYBEL_3:7;
set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #);
A27: RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) #) = RelStr(# the carrier of R, the InternalRel of R #) ;
A28: the carrier of R = the carrier of (ConvergenceSpace (Scott-Convergence R)) by YELLOW_6:def_24;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopLattice by A27, Lm3, Lm9;
reconsider T = T as complete TopLattice by A27, Lm22;
reconsider T = T as complete continuous TopLattice by A27, Lm23;
the topology of T = sigma T by A27, Lm21;
then reconsider T = T as complete continuous Scott TopLattice by Th37;
reconsider XX = X as net of T ;
reconsider JJ = J as net_set of the carrier of XX,T by A27, Lm18;
reconsider uu = u, qq = lim_inf (Iterated J), pp = p9 as Element of T ;
set N = Iterated JJ;
set CC = Convergence T;
Convergence T = Convergence (ConvergenceSpace (Scott-Convergence R)) by A28, Lm8;
then A29: Scott-Convergence R c= Convergence T by YELLOW_6:40;
A30: uu << pp by A26, A27, Lm15;
A31: qq = lim_inf (Iterated JJ) by A27, Lm16, Lm17;
for i being Element of XX holds [(JJ . i),(XX . i)] in Convergence T
proof
let i be Element of XX; ::_thesis: [(JJ . i),(XX . i)] in Convergence T
reconsider ii = i as Element of X ;
[(J . ii),(X . ii)] in Scott-Convergence R by A22;
hence [(JJ . i),(XX . i)] in Convergence T by A29; ::_thesis: verum
end;
then [(Iterated JJ),pp] in Convergence T by A21, A29, YELLOW_6:def_23;
then A32: pp in Lim (Iterated JJ) by YELLOW_6:def_19;
pp in wayabove uu by A30;
then wayabove uu is a_neighborhood of pp by Th36, CONNSP_2:3;
then A33: Iterated JJ is_eventually_in wayabove uu by A32, YELLOW_6:def_15;
wayabove uu c= uparrow uu by WAYBEL_3:11;
then Iterated JJ is_eventually_in uparrow uu by A33, WAYBEL_0:8;
hence u <= lim_inf (Iterated J) by A27, A31, Lm1, Th18; ::_thesis: verum
end;
then sup (waybelow p9) <= lim_inf (Iterated J) by YELLOW_0:32;
then p <= lim_inf (Iterated J) by WAYBEL_3:def_5;
then p is_S-limit_of Iterated J by Def7;
hence [(Iterated J),p] in Scott-Convergence R by A25, Def8; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL11:38
for T being complete continuous Scott TopLattice
for x being Element of T
for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
proof
let T be complete continuous Scott TopLattice; ::_thesis: for x being Element of T
for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
let x be Element of T; ::_thesis: for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
let N be net of T; ::_thesis: ( N in NetUniv T implies ( x is_S-limit_of N iff x in Lim N ) )
assume A1: N in NetUniv T ; ::_thesis: ( x is_S-limit_of N iff x in Lim N )
A2: Convergence (ConvergenceSpace (Scott-Convergence T)) = Scott-Convergence T by YELLOW_6:44;
consider M being strict net of T such that
A3: M = N and
the carrier of M in the_universe_of the carrier of T by A1, YELLOW_6:def_11;
TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32;
then A4: Convergence T = Convergence (ConvergenceSpace (Scott-Convergence T)) by Lm8;
thus ( x is_S-limit_of N implies x in Lim N ) ::_thesis: ( x in Lim N implies x is_S-limit_of N )
proof
assume x is_S-limit_of N ; ::_thesis: x in Lim N
then [N,x] in Convergence T by A1, A2, A3, A4, Def8;
hence x in Lim N by YELLOW_6:def_19; ::_thesis: verum
end;
assume x in Lim N ; ::_thesis: x is_S-limit_of N
then [M,x] in Scott-Convergence T by A1, A2, A3, A4, YELLOW_6:def_19;
hence x is_S-limit_of N by A1, A3, Def8; ::_thesis: verum
end;
theorem Th39: :: WAYBEL11:39
for L being non empty complete Poset st Scott-Convergence L is (ITERATED_LIMITS) holds
L is continuous
proof
let L be non empty complete Poset; ::_thesis: ( Scott-Convergence L is (ITERATED_LIMITS) implies L is continuous )
assume A1: Scott-Convergence L is (ITERATED_LIMITS) ; ::_thesis: L is continuous
set C = Scott-Convergence L;
now__::_thesis:_for_I_being_non_empty_set_st_I_in_the_universe_of_the_carrier_of_L_holds_
for_K_being_V8()_ManySortedSet_of_I_st_(_for_j_being_Element_of_I_holds_K_._j_in_the_universe_of_the_carrier_of_L_)_holds_
for_F_being_DoubleIndexedSet_of_K,L_st_(_for_j_being_Element_of_I_holds_rng_(F_._j)_is_directed_)_holds_
Inf_=_Sup
let I be non empty set ; ::_thesis: ( I in the_universe_of the carrier of L implies for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup )
assume A2: I in the_universe_of the carrier of L ; ::_thesis: for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup
let K be V8() ManySortedSet of I; ::_thesis: ( ( for j being Element of I holds K . j in the_universe_of the carrier of L ) implies for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup )
assume A3: for j being Element of I holds K . j in the_universe_of the carrier of L ; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup
let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of I holds rng (F . j) is directed ) implies Inf = Sup )
assume A4: for j being Element of I holds rng (F . j) is directed ; ::_thesis: Inf = Sup
set x = Inf ;
A5: Inf >= Sup by WAYBEL_5:16;
[:I,I:] c= [:I,I:] ;
then reconsider r = [:I,I:] as Relation of I ;
dom F = I by PARTFUN1:def_2;
then reconsider f = Sups as Function of I, the carrier of L ;
set X = NetStr(# I,r,f #);
A6: for i, j being Element of NetStr(# I,r,f #) holds i <= j
proof
let i, j be Element of NetStr(# I,r,f #); ::_thesis: i <= j
[i,j] in the InternalRel of NetStr(# I,r,f #) by ZFMISC_1:87;
hence i <= j by ORDERS_2:def_5; ::_thesis: verum
end;
A7: NetStr(# I,r,f #) is transitive
proof
let x, y, z be Element of NetStr(# I,r,f #); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
x <= y and
y <= z ; ::_thesis: x <= z
thus x <= z by A6; ::_thesis: verum
end;
NetStr(# I,r,f #) is directed
proof
let x, y be Element of NetStr(# I,r,f #); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of NetStr(# I,r,f #) st
( x <= b1 & y <= b1 )
take x ; ::_thesis: ( x <= x & y <= x )
thus ( x <= x & y <= x ) by A6; ::_thesis: verum
end;
then reconsider X = NetStr(# I,r,f #) as strict net of L by A7;
deffunc H1( Element of I) -> non empty strict NetStr over L = Net-Str ((K . $1),(F . $1));
consider J being ManySortedSet of I such that
A8: for i being Element of I holds J . i = H1(i) from PBOOLE:sch_5();
for i being set st i in the carrier of X holds
J . i is net of L
proof
let i be set ; ::_thesis: ( i in the carrier of X implies J . i is net of L )
assume i in the carrier of X ; ::_thesis: J . i is net of L
then reconsider i9 = i as Element of I ;
reconsider rFi = rng (F . i9) as Subset of L ;
A9: rFi is directed by A4;
J . i9 = Net-Str ((K . i9),(F . i9)) by A8;
hence J . i is net of L by A9, Th20; ::_thesis: verum
end;
then reconsider J = J as net_set of the carrier of X,L by YELLOW_6:24;
A10: for j being set st j in I holds
ex R being 1-sorted st
( R = J . j & K . j = the carrier of R )
proof
let i be set ; ::_thesis: ( i in I implies ex R being 1-sorted st
( R = J . i & K . i = the carrier of R ) )
assume i in I ; ::_thesis: ex R being 1-sorted st
( R = J . i & K . i = the carrier of R )
then reconsider i9 = i as Element of I ;
take R = Net-Str ((K . i9),(F . i9)); ::_thesis: ( R = J . i & K . i = the carrier of R )
thus R = J . i by A8; ::_thesis: K . i = the carrier of R
thus K . i = the carrier of R by Def10; ::_thesis: verum
end;
A11: doms F = K by YELLOW_7:45
.= Carrier J by A10, PRALG_1:def_13 ;
A12: dom (Frege F) = product (doms F) by PARTFUN1:def_2;
then A13: dom (Infs ) = product (doms F) by FUNCT_2:def_1;
A14: for i being Element of X holds J . i in NetUniv L
proof
let i be Element of X; ::_thesis: J . i in NetUniv L
reconsider i9 = i as Element of I ;
A15: J . i = Net-Str ((K . i9),(F . i9)) by A8;
then reconsider Ji = J . i as strict net of L ;
K . i9 in the_universe_of the carrier of L by A3;
then the carrier of Ji in the_universe_of the carrier of L by A15, Def10;
hence J . i in NetUniv L by YELLOW_6:def_11; ::_thesis: verum
end;
A16: for i being Element of X holds [(J . i),(X . i)] in Scott-Convergence L
proof
let i be Element of X; ::_thesis: [(J . i),(X . i)] in Scott-Convergence L
reconsider i9 = i as Element of I ;
A17: J . i = Net-Str ((K . i9),(F . i9)) by A8;
then reconsider Ji = J . i as reflexive monotone net of L ;
A18: J . i in NetUniv L by A14;
i in I ;
then i9 in dom F by PARTFUN1:def_2;
then X . i = Sup by WAYBEL_5:def_1
.= Sup by A17, Def10
.= sup Ji by WAYBEL_2:def_1
.= lim_inf Ji by Th22 ;
then X . i is_S-limit_of J . i by Def7;
hence [(J . i),(X . i)] in Scott-Convergence L by A17, A18, Def8; ::_thesis: verum
end;
A19: X in NetUniv L by A2, YELLOW_6:def_11;
then A20: Iterated J in NetUniv L by A14, YELLOW_6:25;
deffunc H2( Element of (Iterated J)) -> set = { ((Iterated J) . p) where p is Element of (Iterated J) : p >= $1 } ;
the carrier of (Iterated J) = [: the carrier of X,(product (Carrier J)):] by YELLOW_6:26;
then reconsider G = the mapping of (Iterated J) as Function of [: the carrier of X,(product (doms F)):], the carrier of L by A11;
deffunc H3( Element of X, Element of product (doms F)) -> set = { (G . (i,$2)) where i is Element of X : i >= $1 } ;
defpred S1[ set ] means verum;
deffunc H4( Element of product (doms F)) -> Element of the carrier of L = "/\" ((rng ((Frege F) . $1)),L);
deffunc H5( Element of X, Element of product (doms F)) -> Element of the carrier of L = "/\" (H3($1,$2),L);
set D = { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } ;
set D9 = { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ;
set E9 = { H4(g) where g is Element of product (doms F) : S1[g] } ;
A21: for i being Element of X
for g being Element of product (doms F) holds H4(g) = H5(i,g)
proof
let j be Element of X; ::_thesis: for g being Element of product (doms F) holds H4(g) = H5(j,g)
let g be Element of product (doms F); ::_thesis: H4(g) = H5(j,g)
for y being set holds
( y in H3(j,g) iff ex x being set st
( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) )
proof
let y be set ; ::_thesis: ( y in H3(j,g) iff ex x being set st
( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) )
g in product (Carrier J) by A11;
then A22: g in the carrier of (product J) by YELLOW_1:def_4;
hereby ::_thesis: ( ex x being set st
( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) implies y in H3(j,g) )
assume y in H3(j,g) ; ::_thesis: ex x being set st
( x in dom ((Frege F) . g) & ((Frege F) . g) . x = y )
then consider i being Element of X such that
A23: y = G . (i,g) and
i >= j ;
reconsider x = i as set ;
take x = x; ::_thesis: ( x in dom ((Frege F) . g) & ((Frege F) . g) . x = y )
reconsider i9 = i as Element of I ;
A24: i in I ;
then A25: i9 in dom F by PARTFUN1:def_2;
thus x in dom ((Frege F) . g) by A24, PARTFUN1:def_2; ::_thesis: ((Frege F) . g) . x = y
thus ((Frege F) . g) . x = (F . i9) . (g . i) by A12, A25, WAYBEL_5:9
.= the mapping of (Net-Str ((K . i9),(F . i9))) . (g . i) by Def10
.= the mapping of (J . i) . (g . i) by A8
.= y by A22, A23, YELLOW_6:def_13 ; ::_thesis: verum
end;
given x being set such that A26: x in dom ((Frege F) . g) and
A27: y = ((Frege F) . g) . x ; ::_thesis: y in H3(j,g)
A28: x in dom F by A12, A26, WAYBEL_5:8;
reconsider i9 = x as Element of I by A26;
reconsider i = i9 as Element of X ;
A29: i >= j by A6;
y = (F . x) . (g . x) by A12, A27, A28, WAYBEL_5:9
.= the mapping of (Net-Str ((K . i9),(F . i9))) . (g . i) by Def10
.= the mapping of (J . i) . (g . i) by A8
.= G . (i,g) by A22, YELLOW_6:def_13 ;
hence y in H3(j,g) by A29; ::_thesis: verum
end;
hence H4(g) = H5(j,g) by FUNCT_1:def_3; ::_thesis: verum
end;
A30: { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } = { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
proof
A31: the carrier of (Iterated J) = [: the carrier of X,(product (Carrier J)):] by YELLOW_6:26;
A32: for p being Element of (Iterated J)
for i being Element of X
for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)
proof
let p be Element of (Iterated J); ::_thesis: for i being Element of X
for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)
let i be Element of X; ::_thesis: for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)
let g be Element of product (doms F); ::_thesis: ( p = [i,g] implies "/\" (H2(p),L) = "/\" (H3(i,g),L) )
assume A33: p = [i,g] ; ::_thesis: "/\" (H2(p),L) = "/\" (H3(i,g),L)
A34: RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = RelStr(# the carrier of [:X,(product J):], the InternalRel of [:X,(product J):] #) by YELLOW_6:def_13;
reconsider g9 = g as Element of (product J) by A11, YELLOW_1:def_4;
g9 in the carrier of (product J) ;
then A35: g9 in product (Carrier J) by YELLOW_1:def_4;
reconsider i9 = i as Element of X ;
for i being set st i in the carrier of X holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in the carrier of X implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi ) )
assume i in the carrier of X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
then reconsider ii = i as Element of X ;
reconsider i9 = ii as Element of I ;
A36: J . i = Net-Str ((K . i9),(F . i9)) by A8;
set R = Net-Str ((K . i9),(F . i9));
g9 . ii in the carrier of (Net-Str ((K . i9),(F . i9))) by A36;
then reconsider x = g9 . i as Element of (Net-Str ((K . i9),(F . i9))) ;
take Net-Str ((K . i9),(F . i9)) ; ::_thesis: ex xi, yi being Element of (Net-Str ((K . i9),(F . i9))) st
( Net-Str ((K . i9),(F . i9)) = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
take x ; ::_thesis: ex yi being Element of (Net-Str ((K . i9),(F . i9))) st
( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & yi = g9 . i & x <= yi )
take x ; ::_thesis: ( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & x = g9 . i & x <= x )
x <= x ;
hence ( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & x = g9 . i & x <= x ) by A8; ::_thesis: verum
end;
then A37: g9 <= g9 by A35, YELLOW_1:def_4;
H3(i,g) c= H2(p)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in H3(i,g) or u in H2(p) )
assume u in H3(i,g) ; ::_thesis: u in H2(p)
then consider j being Element of X such that
A38: u = the mapping of (Iterated J) . (j,g) and
A39: j >= i ;
reconsider j9 = j as Element of X ;
reconsider q = [j,g] as Element of (Iterated J) by A11, YELLOW_6:26;
[j9,g9] >= [i9,g9] by A37, A39, YELLOW_3:11;
then A40: q >= p by A33, A34, Lm1;
u = (Iterated J) . q by A38;
hence u in H2(p) by A40; ::_thesis: verum
end;
then A41: "/\" (H2(p),L) <= "/\" (H3(i,g),L) by WAYBEL_7:1;
defpred S2[ Element of X] means $1 >= i;
deffunc H6( Element of X) -> Element of the carrier of L = G . ($1,g);
{ H6(k) where k is Element of X : S2[k] } is Subset of L from DOMAIN_1:sch_8();
then reconsider A = H3(i,g) as Subset of L ;
defpred S3[ Element of (Iterated J)] means $1 >= p;
deffunc H7( Element of (Iterated J)) -> Element of the carrier of L = (Iterated J) . $1;
{ H7(z) where z is Element of (Iterated J) : S3[z] } is Subset of L from DOMAIN_1:sch_8();
then reconsider B = H2(p) as Subset of L ;
B is_coarser_than A
proof
let b be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not b in B or ex b1 being Element of the carrier of L st
( b1 in A & b1 <= b ) )
assume b in B ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in A & b1 <= b )
then consider q being Element of (Iterated J) such that
A42: b = (Iterated J) . q and
A43: p <= q ;
consider k being Element of X, f being Element of product (Carrier J) such that
A44: q = [k,f] by A31, DOMAIN_1:1;
reconsider k9 = k as Element of X ;
set a = the mapping of (Iterated J) . (k,g);
the mapping of (Iterated J) . (k,g) = G . (k,g) ;
then reconsider a = the mapping of (Iterated J) . (k,g) as Element of L ;
take a ; ::_thesis: ( a in A & a <= b )
reconsider f9 = f as Element of (product J) by YELLOW_1:def_4;
A45: [k9,f9] >= [i9,g9] by A33, A34, A43, A44, Lm1;
then i <= k by YELLOW_3:11;
hence a in A ; ::_thesis: a <= b
reconsider k9 = k as Element of I ;
set N = Net-Str ((K . k9),(F . k9));
A46: J . k = Net-Str ((K . k9),(F . k9)) by A8;
reconsider g9k = g9 . k, f9k = f9 . k as Element of (Net-Str ((K . k9),(F . k9))) by A8;
A47: b = (Net-Str ((K . k9),(F . k9))) . f9k by A42, A44, A46, YELLOW_6:27;
reconsider kg = [k,g] as Element of (Iterated J) by A11, YELLOW_6:26;
A48: a = (Iterated J) . kg
.= (Net-Str ((K . k9),(F . k9))) . g9k by A46, YELLOW_6:27 ;
g9 <= f9 by A45, YELLOW_3:11;
then g9 . k <= f9 . k by WAYBEL_3:28;
hence a <= b by A46, A47, A48, Def10; ::_thesis: verum
end;
then "/\" (H3(i,g),L) <= "/\" (H2(p),L) by Th1;
hence "/\" (H2(p),L) = "/\" (H3(i,g),L) by A41, YELLOW_0:def_3; ::_thesis: verum
end;
thus { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } c= { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } :: according to XBOOLE_0:def_10 ::_thesis: { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } c= { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } or e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } )
assume e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } ; ::_thesis: e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] }
then consider p being Element of (Iterated J) such that
A49: e = "/\" (H2(p),L) ;
consider j being Element of X, g being Element of product (doms F) such that
A50: p = [j,g] by A11, A31, DOMAIN_1:1;
e = "/\" (H3(j,g),L) by A32, A49, A50;
hence e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } or e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } )
assume e in { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } ; ::_thesis: e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum }
then consider i being Element of X, g being Element of product (doms F) such that
A51: e = "/\" (H3(i,g),L) ;
reconsider j = [i,g] as Element of (Iterated J) by A11, YELLOW_6:26;
e = "/\" (H2(j),L) by A32, A51;
hence e in { ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum } ; ::_thesis: verum
end;
A52: { H4(g) where g is Element of product (doms F) : S1[g] } = { H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g] } from WAYBEL11:sch_1(A21);
for y being set holds
( y in { H4(g) where g is Element of product (doms F) : S1[g] } iff ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) )
proof
let y be set ; ::_thesis: ( y in { H4(g) where g is Element of product (doms F) : S1[g] } iff ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) )
thus ( y in { H4(g) where g is Element of product (doms F) : S1[g] } implies ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) ) ::_thesis: ( ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) implies y in { H4(g) where g is Element of product (doms F) : S1[g] } )
proof
assume y in { H4(g) where g is Element of product (doms F) : S1[g] } ; ::_thesis: ex x being set st
( x in dom (Infs ) & y = (Infs ) . x )
then consider g being Element of product (doms F) such that
A53: y = "/\" ((rng ((Frege F) . g)),L) ;
take g ; ::_thesis: ( g in dom (Infs ) & y = (Infs ) . g )
thus A54: g in dom (Infs ) by A13; ::_thesis: y = (Infs ) . g
thus y = //\ (((Frege F) . g),L) by A53, YELLOW_2:def_6
.= (Infs ) . g by A54, WAYBEL_5:def_2 ; ::_thesis: verum
end;
given x being set such that A55: x in dom (Infs ) and
A56: y = (Infs ) . x ; ::_thesis: y in { H4(g) where g is Element of product (doms F) : S1[g] }
reconsider x = x as Element of product (doms F) by A55, PARTFUN1:def_2;
y = //\ (((Frege F) . x),L) by A55, A56, WAYBEL_5:def_2
.= "/\" ((rng ((Frege F) . x)),L) by YELLOW_2:def_6 ;
hence y in { H4(g) where g is Element of product (doms F) : S1[g] } ; ::_thesis: verum
end;
then rng (Infs ) = { H4(g) where g is Element of product (doms F) : S1[g] } by FUNCT_1:def_3;
then A57: Sup = lim_inf (Iterated J) by A30, A52, YELLOW_2:def_5;
reconsider x9 = Inf as Element of L ;
set X1 = { (Inf ) where j9 is Element of X : verum } ;
set X2 = { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ;
A58: { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } = { (Inf ) where j9 is Element of X : verum }
proof
A59: for j being Element of X holds Inf = "/\" ( { (X . i) where i is Element of X : i >= j } ,L)
proof
let j be Element of X; ::_thesis: Inf = "/\" ( { (X . i) where i is Element of X : i >= j } ,L)
set X3 = { (X . i) where i is Element of X : i >= j } ;
for e being set holds
( e in { (X . i) where i is Element of X : i >= j } iff ex u being set st
( u in dom (Sups ) & e = (Sups ) . u ) )
proof
let e be set ; ::_thesis: ( e in { (X . i) where i is Element of X : i >= j } iff ex u being set st
( u in dom (Sups ) & e = (Sups ) . u ) )
hereby ::_thesis: ( ex u being set st
( u in dom (Sups ) & e = (Sups ) . u ) implies e in { (X . i) where i is Element of X : i >= j } )
assume e in { (X . i) where i is Element of X : i >= j } ; ::_thesis: ex u being set st
( u in dom (Sups ) & e = (Sups ) . u )
then consider i being Element of X such that
A60: e = X . i and
i >= j ;
reconsider u = i as set ;
take u = u; ::_thesis: ( u in dom (Sups ) & e = (Sups ) . u )
u in I ;
hence u in dom (Sups ) by FUNCT_2:def_1; ::_thesis: e = (Sups ) . u
thus e = (Sups ) . u by A60; ::_thesis: verum
end;
given u being set such that A61: u in dom (Sups ) and
A62: e = (Sups ) . u ; ::_thesis: e in { (X . i) where i is Element of X : i >= j }
reconsider i = u as Element of X by A61, FUNCT_2:def_1;
A63: i >= j by A6;
e = X . i by A62;
hence e in { (X . i) where i is Element of X : i >= j } by A63; ::_thesis: verum
end;
then rng (Sups ) = { (X . i) where i is Element of X : i >= j } by FUNCT_1:def_3;
hence Inf = "/\" ( { (X . i) where i is Element of X : i >= j } ,L) by YELLOW_2:def_6; ::_thesis: verum
end;
thus { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } c= { (Inf ) where j9 is Element of X : verum } :: according to XBOOLE_0:def_10 ::_thesis: { (Inf ) where j9 is Element of X : verum } c= { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } or u in { (Inf ) where j9 is Element of X : verum } )
assume u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ; ::_thesis: u in { (Inf ) where j9 is Element of X : verum }
then ex j being Element of X st u = "/\" ( { (X . i) where i is Element of X : i >= j } ,L) ;
then u = Inf by A59;
hence u in { (Inf ) where j9 is Element of X : verum } ; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { (Inf ) where j9 is Element of X : verum } or u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } )
set j = the Element of X;
assume u in { (Inf ) where j9 is Element of X : verum } ; ::_thesis: u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum }
then ex j being Element of X st u = Inf ;
then u = "/\" ( { (X . i) where i is Element of X : i >= the Element of X } ,L) by A59;
hence u in { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ; ::_thesis: verum
end;
now__::_thesis:_for_u_being_set_holds_
(_u_in__{__(Inf_)_where_j9_is_Element_of_X_:_verum__}__iff_u_in_{(Inf_)}_)
let u be set ; ::_thesis: ( u in { (Inf ) where j9 is Element of X : verum } iff u in {(Inf )} )
( u in { (Inf ) where j9 is Element of X : verum } iff ex j9 being Element of X st u = Inf ) ;
then ( u in { (Inf ) where j9 is Element of X : verum } iff u = Inf ) ;
hence ( u in { (Inf ) where j9 is Element of X : verum } iff u in {(Inf )} ) by TARSKI:def_1; ::_thesis: verum
end;
then "\/" ( { ("/\" ( { (X . i) where i is Element of X : i >= j } ,L)) where j is Element of X : verum } ,L) = sup {x9} by A58, TARSKI:1
.= Inf by YELLOW_0:39 ;
then Inf <= lim_inf X ;
then Inf is_S-limit_of X by Def7;
then [X,(Inf )] in Scott-Convergence L by A19, Def8;
then [(Iterated J),(Inf )] in Scott-Convergence L by A1, A16, YELLOW_6:def_23;
then Inf is_S-limit_of Iterated J by A20, Def8;
then Inf <= Sup by A57, Def7;
hence Inf = Sup by A5, ORDERS_2:2; ::_thesis: verum
end;
hence L is continuous by WAYBEL_5:18; ::_thesis: verum
end;
theorem :: WAYBEL11:40
for T being complete Scott TopLattice holds
( T is continuous iff Convergence T = Scott-Convergence T )
proof
let T be complete Scott TopLattice; ::_thesis: ( T is continuous iff Convergence T = Scott-Convergence T )
hereby ::_thesis: ( Convergence T = Scott-Convergence T implies T is continuous )
assume T is continuous ; ::_thesis: Convergence T = Scott-Convergence T
then reconsider L = T as complete continuous Scott TopLattice ;
TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32;
hence Convergence T = Convergence (ConvergenceSpace (Scott-Convergence L)) by Lm8
.= Scott-Convergence T by YELLOW_6:44 ;
::_thesis: verum
end;
thus ( Convergence T = Scott-Convergence T implies T is continuous ) by Th39; ::_thesis: verum
end;
theorem Th41: :: WAYBEL11:41
for T being complete Scott TopLattice
for S being upper Subset of T st S is Open holds
S is open
proof
let T be complete Scott TopLattice; ::_thesis: for S being upper Subset of T st S is Open holds
S is open
let S be upper Subset of T; ::_thesis: ( S is Open implies S is open )
assume A1: for x being Element of T st x in S holds
ex y being Element of T st
( y in S & y << x ) ; :: according to WAYBEL_6:def_1 ::_thesis: S is open
S is inaccessible
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume sup D in S ; ::_thesis: D meets S
then consider y being Element of T such that
A2: y in S and
A3: y << sup D by A1;
consider d being Element of T such that
A4: d in D and
A5: y <= d by A3, WAYBEL_3:def_1;
d in S by A2, A5, WAYBEL_0:def_20;
hence D meets S by A4, XBOOLE_0:3; ::_thesis: verum
end;
hence S is open by Def4; ::_thesis: verum
end;
theorem Th42: :: WAYBEL11:42
for L being non empty RelStr
for S being upper Subset of L
for x being Element of L st x in S holds
uparrow x c= S
proof
let L be non empty RelStr ; ::_thesis: for S being upper Subset of L
for x being Element of L st x in S holds
uparrow x c= S
let S be upper Subset of L; ::_thesis: for x being Element of L st x in S holds
uparrow x c= S
let x be Element of L; ::_thesis: ( x in S implies uparrow x c= S )
assume A1: x in S ; ::_thesis: uparrow x c= S
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in uparrow x or e in S )
assume A2: e in uparrow x ; ::_thesis: e in S
then reconsider y = e as Element of L ;
x <= y by A2, WAYBEL_0:18;
hence e in S by A1, WAYBEL_0:def_20; ::_thesis: verum
end;
theorem Th43: :: WAYBEL11:43
for L being complete 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 complete 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, Def4;
sup (waybelow p) = p by WAYBEL_3:def_5;
then waybelow p meets S by A2, A3, Def1;
then (waybelow p) /\ S <> {} by XBOOLE_0:def_7;
then consider u being Element of L such that
A4: u in (waybelow p) /\ S by SUBSET_1:4;
reconsider u = u as Element of L ;
take u ; ::_thesis: ( u << p & u in S )
u in waybelow p by A4, XBOOLE_0:def_4;
hence u << p by WAYBEL_3:7; ::_thesis: u in S
thus u in S by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th44: :: WAYBEL11:44
for L being complete 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 complete 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 Th36;
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 bool the carrier of L holds
( not b1 is open or not p in b1 or ex b2 being Element of bool 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 bool 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 bool 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, Th43;
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, Def4;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
uparrow u c= S by A6, A7, Th42;
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;
theorem Th45: :: WAYBEL11:45
for T being complete continuous Scott TopLattice holds { (wayabove x) where x is Element of T : verum } is Basis of T
proof
let T be complete 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 Th36;
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 Th44;
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;
theorem :: WAYBEL11:46
for T being complete continuous Scott TopLattice
for S being upper Subset of T holds
( S is open iff S is Open )
proof
let T be complete continuous Scott TopLattice; ::_thesis: for S being upper Subset of T holds
( S is open iff S is Open )
let S be upper Subset of T; ::_thesis: ( S is open iff S is Open )
thus ( S is open implies S is Open ) ::_thesis: ( S is Open implies S is open )
proof
assume A1: S is open ; ::_thesis: S is Open
let x be Element of T; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in S or ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x ) )
assume x in S ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x )
then ex y being Element of T st
( y << x & y in S ) by A1, Th43;
hence ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x ) ; ::_thesis: verum
end;
thus ( S is Open implies S is open ) by Th41; ::_thesis: verum
end;
theorem :: WAYBEL11:47
for T being complete continuous Scott TopLattice
for p being Element of T holds Int (uparrow p) = wayabove p
proof
let T be complete continuous Scott TopLattice; ::_thesis: for p being Element of T holds Int (uparrow p) = wayabove p
let p be Element of T; ::_thesis: Int (uparrow p) = wayabove p
thus Int (uparrow p) c= wayabove p :: according to XBOOLE_0:def_10 ::_thesis: wayabove p c= Int (uparrow p)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Int (uparrow p) or y in wayabove p )
assume A1: y in Int (uparrow p) ; ::_thesis: y in wayabove p
then reconsider q = y as Element of T ;
reconsider S = Int (uparrow p) as Subset of T ;
consider u being Element of T such that
A2: u << q and
A3: u in S by A1, Th43;
S c= uparrow p by TOPS_1:16;
then p <= u by A3, WAYBEL_0:18;
then p << q by A2, WAYBEL_3:2;
hence y in wayabove p ; ::_thesis: verum
end;
wayabove p c= uparrow p by WAYBEL_3:11;
hence wayabove p c= Int (uparrow p) by Th36, TOPS_1:24; ::_thesis: verum
end;
theorem :: WAYBEL11:48
for T being complete 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 complete 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 Th45;
hence Int S = union { (wayabove x) where x is Element of T : wayabove x c= S } by A1, YELLOW_8:11; ::_thesis: verum
end;