:: WAYBEL32 semantic presentation
begin
definition
let T be non empty TopRelStr ;
attrT is upper means :Def1: :: WAYBEL32:def 1
{ ((downarrow x) `) where x is Element of T : verum } is prebasis of T;
end;
:: deftheorem Def1 defines upper WAYBEL32:def_1_:_
for T being non empty TopRelStr holds
( T is upper iff { ((downarrow x) `) where x is Element of T : verum } is prebasis of T );
registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict Scott for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is Scott & b1 is up-complete & b1 is strict )
proof
set R = the complete LATTICE;
set T = the correct strict Scott TopAugmentation of the complete LATTICE;
take the correct strict Scott TopAugmentation of the complete LATTICE ; ::_thesis: ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is up-complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict )
thus ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is up-complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) ; ::_thesis: verum
end;
end;
definition
let T be non empty TopSpace-like reflexive TopRelStr ;
attrT is order_consistent means :Def2: :: WAYBEL32:def 2
for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) );
end;
:: deftheorem Def2 defines order_consistent WAYBEL32:def_2_:_
for T being non empty TopSpace-like reflexive TopRelStr holds
( T is order_consistent iff for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) ) );
registration
cluster1 -element TopSpace-like reflexive -> 1 -element TopSpace-like reflexive upper for TopRelStr ;
coherence
for b1 being 1 -element TopSpace-like reflexive TopRelStr holds b1 is upper
proof
let T be 1 -element TopSpace-like reflexive TopRelStr ; ::_thesis: T is upper
set BB = { ((downarrow x) `) where x is Element of T : verum } ;
{ ((downarrow x) `) where x is Element of T : verum } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((downarrow x) `) where x is Element of T : verum } or a in bool the carrier of T )
assume a in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: a in bool the carrier of T
then ex x being Element of T st a = (downarrow x) ` ;
hence a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider C = { ((downarrow x) `) where x is Element of T : verum } as Subset-Family of T ;
reconsider C = C as Subset-Family of T ;
A1: { ((downarrow x) `) where x is Element of T : verum } c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((downarrow x) `) where x is Element of T : verum } or a in the topology of T )
assume a in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: a in the topology of T
then consider x being Element of T such that
A2: a = (downarrow x) ` ;
a c= {}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in {} )
assume A3: y in a ; ::_thesis: y in {}
A4: x <= x ;
A5: y = x by A2, A3, STRUCT_0:def_10;
x in downarrow x by A4, WAYBEL_0:17;
then A6: x in (downarrow x) /\ a by A3, A5, XBOOLE_0:def_4;
downarrow x misses a by A2, XBOOLE_1:79;
hence y in {} by A6, XBOOLE_0:def_7; ::_thesis: verum
end;
then a = {} ;
hence a in the topology of T by PRE_TOPC:1; ::_thesis: verum
end;
reconsider F = { the carrier of T} as Basis of T by YELLOW_9:10;
{ ((downarrow x) `) where x is Element of T : verum } = {{}}
proof
thus { ((downarrow x) `) where x is Element of T : verum } c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= { ((downarrow x) `) where x is Element of T : verum }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((downarrow x) `) where x is Element of T : verum } or a in {{}} )
assume a in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: a in {{}}
then consider x being Element of T such that
A7: a = (downarrow x) ` ;
A8: x <= x ;
A9: the carrier of T = {x} by YELLOW_9:9;
x in downarrow x by A8, WAYBEL_0:17;
then ( a = {} or ( a = the carrier of T & not x in a ) ) by A7, A9, XBOOLE_0:def_5, ZFMISC_1:33;
hence a in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set x = the Element of T;
A10: the Element of T <= the Element of T ;
A11: the carrier of T = { the Element of T} by YELLOW_9:9;
the Element of T in downarrow the Element of T by A10, WAYBEL_0:17;
then ( (downarrow the Element of T) ` = {} or ( (downarrow the Element of T) ` = the carrier of T & not the Element of T in (downarrow the Element of T) ` ) ) by A11, XBOOLE_0:def_5, ZFMISC_1:33;
then {} in { ((downarrow x) `) where x is Element of T : verum } ;
hence {{}} c= { ((downarrow x) `) where x is Element of T : verum } by ZFMISC_1:31; ::_thesis: verum
end;
then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11;
then F c= FinMeetCl C by ZFMISC_1:7;
hence { ((downarrow x) `) where x is Element of T : verum } is prebasis of T by A1, CANTOR_1:def_4, TOPS_2:64; :: according to WAYBEL32:def_1 ::_thesis: verum
end;
end;
registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict upper for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is upper & b1 is trivial & b1 is up-complete & b1 is strict )
proof
set T = the 1 -element up-complete strict TopLattice;
take the 1 -element up-complete strict TopLattice ; ::_thesis: ( the 1 -element up-complete strict TopLattice is upper & the 1 -element up-complete strict TopLattice is trivial & the 1 -element up-complete strict TopLattice is up-complete & the 1 -element up-complete strict TopLattice is strict )
thus ( the 1 -element up-complete strict TopLattice is upper & the 1 -element up-complete strict TopLattice is trivial & the 1 -element up-complete strict TopLattice is up-complete & the 1 -element up-complete strict TopLattice is strict ) ; ::_thesis: verum
end;
end;
theorem Th1: :: WAYBEL32:1
for T being non empty up-complete upper TopPoset
for A being Subset of T st A is open holds
A is upper
proof
let T be non empty up-complete upper TopPoset; ::_thesis: for A being Subset of T st A is open holds
A is upper
let A be Subset of T; ::_thesis: ( A is open implies A is upper )
assume A is open ; ::_thesis: A is upper
then A1: A in the topology of T by PRE_TOPC:def_2;
reconsider BB = { ((downarrow x) `) where x is Element of T : verum } as prebasis of T by Def1;
consider F being Basis of T such that
A2: F c= FinMeetCl BB by CANTOR_1:def_4;
the topology of T c= UniCl F by CANTOR_1:def_2;
then consider Y being Subset-Family of T such that
A3: Y c= F and
A4: A = union Y by A1, CANTOR_1:def_1;
let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A )
assume x in A ; ::_thesis: ( not x <= y or y in A )
then consider Z being set such that
A5: x in Z and
A6: Z in Y by A4, TARSKI:def_4;
Z in F by A3, A6;
then consider X being Subset-Family of T such that
A7: X c= BB and
X is finite and
A8: Z = Intersect X by A2, CANTOR_1:def_3;
assume A9: x <= y ; ::_thesis: y in A
now__::_thesis:_for_Q_being_set_st_Q_in_X_holds_
y_in_Q
let Q be set ; ::_thesis: ( Q in X implies y in Q )
assume A10: Q in X ; ::_thesis: y in Q
then Q in BB by A7;
then consider z being Element of T such that
A11: Q = (downarrow z) ` ;
A12: x in Q by A5, A8, A10, SETFAM_1:43;
downarrow z misses Q by A11, XBOOLE_1:79;
then not x in downarrow z by A12, XBOOLE_0:3;
then not x <= z by WAYBEL_0:17;
then not y <= z by A9, ORDERS_2:3;
then not y in downarrow z by WAYBEL_0:17;
hence y in Q by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then y in Z by A8, SETFAM_1:43;
hence y in A by A4, A6, TARSKI:def_4; ::_thesis: verum
end;
theorem :: WAYBEL32:2
for T being non empty up-complete TopPoset st T is upper holds
T is order_consistent
proof
let T be non empty up-complete TopPoset; ::_thesis: ( T is upper implies T is order_consistent )
assume A1: T is upper ; ::_thesis: T is order_consistent
then reconsider BB = { ((downarrow x) `) where x is Element of T : verum } as prebasis of T by Def1;
for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
proof
let x be Element of T; ::_thesis: ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
A2: downarrow x c= Cl {x}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in Cl {x} )
assume A3: a in downarrow x ; ::_thesis: a in Cl {x}
then reconsider a9 = a as Point of T ;
for G being Subset of T st G is open & a9 in G holds
{x} meets G
proof
let G be Subset of T; ::_thesis: ( G is open & a9 in G implies {x} meets G )
assume A4: G is open ; ::_thesis: ( not a9 in G or {x} meets G )
assume A5: a9 in G ; ::_thesis: {x} meets G
reconsider v = a9 as Element of T ;
A6: v <= x by A3, WAYBEL_0:17;
G is upper by A1, A4, Th1;
then A7: x in G by A5, A6, WAYBEL_0:def_20;
x in {x} by TARSKI:def_1;
hence {x} meets G by A7, XBOOLE_0:3; ::_thesis: verum
end;
hence a in Cl {x} by PRE_TOPC:24; ::_thesis: verum
end;
Cl {x} c= downarrow x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl {x} or a in downarrow x )
assume A8: a in Cl {x} ; ::_thesis: a in downarrow x
reconsider BB = BB as Subset-Family of T ;
(downarrow x) ` in BB ;
then A9: (downarrow x) ` is open by TOPS_2:def_1;
(downarrow x) ` = ([#] T) \ (downarrow x) ;
then A10: downarrow x is closed by A9, PRE_TOPC:def_3;
x <= x ;
then x in downarrow x by WAYBEL_0:17;
then {x} c= downarrow x by ZFMISC_1:31;
hence a in downarrow x by A8, A10, PRE_TOPC:15; ::_thesis: verum
end;
hence downarrow x = Cl {x} by A2, XBOOLE_0:def_10; ::_thesis: for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V
thus for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ::_thesis: verum
proof
let N be eventually-directed net of T; ::_thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V )
assume x = sup N ; ::_thesis: for V being a_neighborhood of x holds N is_eventually_in V
then A11: x = Sup by WAYBEL_2:def_1
.= sup (rng (netmap (N,T))) by YELLOW_2:def_5 ;
let V be a_neighborhood of x; ::_thesis: N is_eventually_in V
A12: x in Int V by CONNSP_2:def_1;
FinMeetCl BB is Basis of T by YELLOW_9:23;
then A13: the topology of T = UniCl (FinMeetCl BB) by YELLOW_9:22;
Int V in the topology of T by PRE_TOPC:def_2;
then consider Y being Subset-Family of T such that
A14: Y c= FinMeetCl BB and
A15: Int V = union Y by A13, CANTOR_1:def_1;
consider Y1 being set such that
A16: x in Y1 and
A17: Y1 in Y by A12, A15, TARSKI:def_4;
consider Z being Subset-Family of T such that
A18: Z c= BB and
A19: Z is finite and
A20: Y1 = Intersect Z by A14, A17, CANTOR_1:def_3;
reconsider rngN = rng (netmap (N,T)) as Subset of T ;
rngN is directed by WAYBEL_2:18;
then ex a being Element of T st
( a is_>=_than rngN & ( for b being Element of T st b is_>=_than rngN holds
a <= b ) ) by WAYBEL_0:def_39;
then A21: ex_sup_of rngN,T by YELLOW_0:15;
defpred S1[ set , set ] means for i, j being Element of N st i = $2 & j >= i holds
N . j in $1;
A22: for Q being set st Q in Z holds
ex b being set st
( b in the carrier of N & S1[Q,b] )
proof
let Q be set ; ::_thesis: ( Q in Z implies ex b being set st
( b in the carrier of N & S1[Q,b] ) )
assume A23: Q in Z ; ::_thesis: ex b being set st
( b in the carrier of N & S1[Q,b] )
then Q in BB by A18;
then consider v1 being Element of T such that
A24: Q = (downarrow v1) ` ;
x in (downarrow v1) ` by A16, A20, A23, A24, SETFAM_1:43;
then not x in downarrow v1 by XBOOLE_0:def_5;
then A25: not x <= v1 by WAYBEL_0:17;
not rngN c= downarrow v1
proof
assume A26: rngN c= downarrow v1 ; ::_thesis: contradiction
ex_sup_of downarrow v1,T by WAYBEL_0:34;
then sup rngN <= sup (downarrow v1) by A21, A26, YELLOW_0:34;
hence contradiction by A11, A25, WAYBEL_0:34; ::_thesis: verum
end;
then consider w being set such that
A27: w in rngN and
A28: not w in downarrow v1 by TARSKI:def_3;
reconsider w9 = w as Element of T by A27;
consider i being set such that
A29: i in dom the mapping of N and
A30: w9 = the mapping of N . i by A27, FUNCT_1:def_3;
reconsider i = i as Element of N by A29;
consider b being Element of N such that
A31: for l being Element of N st b <= l holds
N . i <= N . l by WAYBEL_0:11;
take b ; ::_thesis: ( b in the carrier of N & S1[Q,b] )
thus b in the carrier of N ; ::_thesis: S1[Q,b]
thus for j, k being Element of N st j = b & k >= j holds
N . k in Q ::_thesis: verum
proof
let j, k be Element of N; ::_thesis: ( j = b & k >= j implies N . k in Q )
assume that
A32: j = b and
A33: k >= j ; ::_thesis: N . k in Q
A34: N . i <= N . k by A31, A32, A33;
not N . i <= v1 by A28, A30, WAYBEL_0:17;
then not N . k <= v1 by A34, ORDERS_2:3;
then not N . k in downarrow v1 by WAYBEL_0:17;
hence N . k in Q by A24, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
consider f being Function such that
A35: ( dom f = Z & rng f c= the carrier of N ) and
A36: for Q being set st Q in Z holds
S1[Q,f . Q] from FUNCT_1:sch_5(A22);
reconsider rngf = rng f as finite Subset of ([#] N) by A19, A35, FINSET_1:8;
[#] N is directed by WAYBEL_0:def_6;
then consider k being Element of N such that
k in [#] N and
A37: k is_>=_than rngf by WAYBEL_0:1;
take k ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not k <= b1 or N . b1 in V )
let k1 be Element of N; ::_thesis: ( not k <= k1 or N . k1 in V )
assume A38: k <= k1 ; ::_thesis: N . k1 in V
now__::_thesis:_for_Q_being_set_st_Q_in_Z_holds_
N_._k1_in_Q
let Q be set ; ::_thesis: ( Q in Z implies N . k1 in Q )
assume A39: Q in Z ; ::_thesis: N . k1 in Q
then A40: f . Q in rngf by A35, FUNCT_1:def_3;
then reconsider j = f . Q as Element of N ;
j <= k by A37, A40, LATTICE3:def_9;
hence N . k1 in Q by A36, A38, A39, ORDERS_2:3; ::_thesis: verum
end;
then A41: N . k1 in Y1 by A20, SETFAM_1:43;
Y1 c= union Y by A17, ZFMISC_1:74;
then A42: N . k1 in Int V by A15, A41;
Int V c= V by TOPS_1:16;
hence N . k1 in V by A42; ::_thesis: verum
end;
end;
hence T is order_consistent by Def2; ::_thesis: verum
end;
theorem Th3: :: WAYBEL32:3
for R being non empty reflexive transitive antisymmetric up-complete RelStr ex T being TopAugmentation of R st T is Scott
proof
let R be non empty reflexive transitive antisymmetric up-complete RelStr ; ::_thesis: ex T being TopAugmentation of R st T is Scott
set T = the Scott TopAugmentation of R;
take the Scott TopAugmentation of R ; ::_thesis: the Scott TopAugmentation of R is Scott
thus the Scott TopAugmentation of R is Scott ; ::_thesis: verum
end;
theorem :: WAYBEL32:4
for R being non empty up-complete Poset
for T being TopAugmentation of R st T is Scott holds
T is correct ;
registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster Scott -> correct for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R st b1 is Scott holds
b1 is correct ;
end;
registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster non empty correct reflexive transitive antisymmetric up-complete Scott for TopAugmentation of R;
existence
ex b1 being TopAugmentation of R st
( b1 is Scott & b1 is correct )
proof
consider T being TopAugmentation of R such that
A1: T is Scott by Th3;
take T ; ::_thesis: ( T is Scott & T is correct )
thus ( T is Scott & T is correct ) by A1; ::_thesis: verum
end;
end;
theorem Th5: :: WAYBEL32:5
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds Cl {x} = downarrow x
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for x being Element of T holds Cl {x} = downarrow x
let x be Element of T; ::_thesis: Cl {x} = downarrow x
reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44;
reconsider dx = downarrow x as Subset of T9 ;
reconsider A = {x} as Subset of T9 ;
A1: downarrow x is closed by WAYBEL11:11;
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_T9_st_A_c=_C_&_C_is_closed_holds_
dx_c=_C
let C be Subset of T9; ::_thesis: ( A c= C & C is closed implies dx c= C )
assume A3: A c= C ; ::_thesis: ( C is closed implies dx c= C )
reconsider D = C as Subset of T9 ;
assume C is closed ; ::_thesis: dx c= C
then A4: D is lower by WAYBEL11:7;
x in C by A3, ZFMISC_1:31;
hence dx c= C by A4, WAYBEL11:6; ::_thesis: verum
end;
hence Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum
end;
theorem Th6: :: WAYBEL32:6
for T being non empty up-complete Scott TopPoset holds T is order_consistent
proof
let T be non empty up-complete Scott TopPoset; ::_thesis: T is order_consistent
for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
proof
let x be Element of T; ::_thesis: ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V
proof
let N be eventually-directed net of T; ::_thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V )
assume x = sup N ; ::_thesis: for V being a_neighborhood of x holds N is_eventually_in V
then x = Sup by WAYBEL_2:def_1;
then A1: x = sup (rng the mapping of N) by YELLOW_2:def_5;
let V be a_neighborhood of x; ::_thesis: N is_eventually_in V
A2: x in Int V by CONNSP_2:def_1;
reconsider rngN = rng (netmap (N,T)) as Subset of T ;
rngN is directed by WAYBEL_2:18;
then Int V meets rngN by A1, A2, WAYBEL11:def_1;
then consider z being set such that
A3: z in Int V and
A4: z in rngN by XBOOLE_0:3;
reconsider z9 = z as Element of T by A3;
consider i being set such that
A5: i in dom the mapping of N and
A6: z9 = the mapping of N . i by A4, FUNCT_1:def_3;
reconsider i = i as Element of N by A5;
consider j being Element of N such that
A7: for k being Element of N st j <= k holds
N . i <= N . k by WAYBEL_0:11;
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 V )
let l be Element of N; ::_thesis: ( not j <= l or N . l in V )
assume j <= l ; ::_thesis: N . l in V
then N . i <= N . l by A7;
then A8: N . l in Int V by A3, A6, WAYBEL_0:def_20;
Int V c= V by TOPS_1:16;
hence N . l in V by A8; ::_thesis: verum
end;
hence ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) ) by Th5; ::_thesis: verum
end;
hence T is order_consistent by Def2; ::_thesis: verum
end;
theorem Th7: :: WAYBEL32:7
for R being /\-complete Semilattice
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 Semilattice; ::_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;
consider j9 being Element of Z such that
A6: j9 >= j and
j9 >= j by YELLOW_6:def_3;
deffunc H1( Element of Z) -> Element of the carrier of R = Z . $1;
defpred S1[ Element of Z] means $1 >= jx;
defpred S2[ Element of Z] means $1 >= jy;
defpred S3[ Element of Z] means $1 >= j;
set Ex = { H1(k) where k is Element of Z : S1[k] } ;
set Ey = { H1(k) where k is Element of Z : S2[k] } ;
set E = { H1(k) where k is Element of Z : S3[k] } ;
A7: Z . j in { H1(k) where k is Element of Z : S1[k] } by A4;
A8: Z . j in { H1(k) where k is Element of Z : S2[k] } by A5;
A9: Z . j9 in { H1(k) where k is Element of Z : S3[k] } by A6;
A10: { H1(k) where k is Element of Z : S1[k] } is Subset of R from DOMAIN_1:sch_8();
A11: { H1(k) where k is Element of Z : S2[k] } is Subset of R from DOMAIN_1:sch_8();
A12: { H1(k) where k is Element of Z : S3[k] } is Subset of R from DOMAIN_1:sch_8();
take z = "/\" ( { (Z . k) where k is Element of Z : k >= j } ,R); ::_thesis: ( z in D & x <= z & y <= z )
reconsider Ex9 = { H1(k) where k is Element of Z : S1[k] } as non empty Subset of R by A7, A10;
reconsider Ey9 = { H1(k) where k is Element of Z : S2[k] } as non empty Subset of R by A8, A11;
reconsider E9 = { H1(k) where k is Element of Z : S3[k] } as non empty Subset of R by A9, A12;
A13: ex_inf_of E9,R by WAYBEL_0:76;
A14: ex_inf_of Ex9,R by WAYBEL_0:76;
A15: ex_inf_of Ey9,R by WAYBEL_0:76;
thus z in D by A1; ::_thesis: ( x <= z & y <= z )
E9 c= Ex9
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in E9 or e in Ex9 )
assume e in E9 ; ::_thesis: e in Ex9
then consider k being Element of Z such that
A16: e = Z . k and
A17: k >= j ;
reconsider k = k as Element of Z ;
k >= jx by A4, A17, YELLOW_0:def_2;
hence e in Ex9 by A16; ::_thesis: verum
end;
hence x <= z by A2, A13, A14, YELLOW_0:35; ::_thesis: y <= z
E9 c= Ey9
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in E9 or e in Ey9 )
assume e in E9 ; ::_thesis: e in Ey9
then consider k being Element of Z such that
A18: e = Z . k and
A19: k >= j ;
reconsider k = k as Element of Z ;
k >= jy by A5, A19, YELLOW_0:def_2;
hence e in Ey9 by A18; ::_thesis: verum
end;
hence y <= z by A3, A13, A15, YELLOW_0:35; ::_thesis: verum
end;
theorem Th8: :: WAYBEL32:8
for R being /\-complete Semilattice
for S being Subset of R
for a being Element of R st a in S holds
"/\" (S,R) <= a
proof
let R be /\-complete Semilattice; ::_thesis: for S being Subset of R
for a being Element of R st a in S holds
"/\" (S,R) <= a
let S be Subset of R; ::_thesis: for a being Element of R st a in S holds
"/\" (S,R) <= a
let a be Element of R; ::_thesis: ( a in S implies "/\" (S,R) <= a )
assume A1: a in S ; ::_thesis: "/\" (S,R) <= a
then ex_inf_of S,R by WAYBEL_0:76;
then S is_>=_than "/\" (S,R) by YELLOW_0:31;
hence "/\" (S,R) <= a by A1, LATTICE3:def_8; ::_thesis: verum
end;
theorem Th9: :: WAYBEL32:9
for R being /\-complete Semilattice
for N being reflexive monotone net of R holds lim_inf N = sup N
proof
let R be /\-complete Semilattice; ::_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
deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,R);
deffunc H2( Element of N) -> Element of the carrier of R = N . $1;
defpred S1[ set ] means verum;
set X = { H1(j) where j is Element of N : S1[j] } ;
A1: for j being Element of N holds H2(j) = H1(j)
proof
let j be Element of N; ::_thesis: H2(j) = H1(j)
defpred S2[ Element of N] means $1 >= j;
set Y = { H2(i) where i is Element of N : S2[i] } ;
j <= j ;
then A2: N . j in { H2(i) where i is Element of N : S2[i] } ;
{ H2(i) where i is Element of N : S2[i] } is Subset of R from DOMAIN_1:sch_8();
then A3: ex_inf_of { H2(i) where i is Element of N : S2[i] } ,R by A2, WAYBEL_0:76;
A4: N . j is_<=_than { H2(i) where i is Element of N : S2[i] }
proof
let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in { H2(i) where i is Element of N : S2[i] } or N . j <= y )
assume y in { H2(i) where i is Element of N : S2[i] } ; ::_thesis: N . j <= y
then ex i being Element of N st
( y = N . i & j <= i ) ;
hence N . j <= y by WAYBEL11:def_9; ::_thesis: verum
end;
for b being Element of R st b is_<=_than { H2(i) where i is Element of N : S2[i] } holds
N . j >= b
proof
let b be Element of R; ::_thesis: ( b is_<=_than { H2(i) where i is Element of N : S2[i] } implies N . j >= b )
assume A5: b is_<=_than { H2(i) where i is Element of N : S2[i] } ; ::_thesis: N . j >= b
reconsider j9 = j as Element of N ;
j9 <= j9 ;
then N . j9 in { H2(i) where i is Element of N : S2[i] } ;
hence N . j >= b by A5, LATTICE3:def_8; ::_thesis: verum
end;
hence H2(j) = H1(j) by A3, A4, YELLOW_0:def_10; ::_thesis: verum
end;
rng the mapping of N = { H2(j) where j is Element of N : S1[j] } by WAYBEL11:19
.= { 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 Th10: :: WAYBEL32:10
for R being /\-complete Semilattice
for S being Subset of R holds
( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
proof
let R be /\-complete Semilattice; ::_thesis: for S being Subset of R holds
( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
set SC = Scott-Convergence R;
set T = ConvergenceSpace (Scott-Convergence R);
A1: the topology of (ConvergenceSpace (Scott-Convergence R)) = { V where V is Subset of R : for p being Element of R st p in V holds
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in V } by YELLOW_6:def_24;
let S be Subset of R; ::_thesis: ( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
hereby ::_thesis: ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence R)) )
assume S in the topology of (ConvergenceSpace (Scott-Convergence R)) ; ::_thesis: ( S is inaccessible & S is upper )
then A2: ex V being Subset of R st
( S = V & ( for p being Element of R st p in V holds
for N being net of R st [N,p] in Scott-Convergence R 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 R; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,R) in S or not D misses S )
assume A3: sup D in S ; ::_thesis: not D misses 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 R by A4, FUNCT_2:def_1, RELSET_1:4;
reconsider N = Net-Str (D,f) as reflexive strict monotone net of R by A5, WAYBEL11:20;
A6: N in NetUniv R by WAYBEL11:21;
lim_inf N = sup N by Th9
.= Sup by WAYBEL_2:def_1
.= "\/" ((rng the mapping of N),R) by YELLOW_2:def_5
.= "\/" ((rng f),R) by WAYBEL11:def_10
.= sup D by RELAT_1:45 ;
then sup D is_S-limit_of N by WAYBEL11:def_7;
then [N,(sup D)] in Scott-Convergence R by A6, WAYBEL11:def_8;
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 WAYBEL11:def_10;
N . j0 = (id D) . j0 by WAYBEL11:def_10
.= j0 by A10, FUNCT_1:18 ;
hence not D misses S by A9, A10, XBOOLE_0:3; ::_thesis: verum
end;
thus S is upper ::_thesis: verum
proof
let x, y be Element of R; :: 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 R by WAYBEL11:29;
y = lim_inf (Net-Str y) by WAYBEL11:28;
then x is_S-limit_of Net-Str y by A12, WAYBEL11:def_7;
then [(Net-Str y),x] in Scott-Convergence R by A13, WAYBEL11:def_8;
then Net-Str y is_eventually_in S by A2, A11;
hence y in S by WAYBEL11:27; ::_thesis: verum
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper ; ::_thesis: S in the topology of (ConvergenceSpace (Scott-Convergence R))
for p being Element of R st p in S holds
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S
proof
let p be Element of R; ::_thesis: ( p in S implies for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S )
assume A16: p in S ; ::_thesis: for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S
reconsider p9 = p as Element of R ;
let N be net of R; ::_thesis: ( [N,p] in Scott-Convergence R implies N is_eventually_in S )
assume A17: [N,p] in Scott-Convergence R ; ::_thesis: N is_eventually_in S
Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
then A18: N in NetUniv R by A17, ZFMISC_1:87;
then ex N9 being strict net of R st
( N9 = N & the carrier of N9 in the_universe_of the carrier of R ) by YELLOW_6:def_11;
then p is_S-limit_of N by A17, A18, WAYBEL11:def_8;
then A19: p9 <= lim_inf N by WAYBEL11:def_7;
deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,R);
defpred S1[ set ] means verum;
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 R from DOMAIN_1:sch_8();
then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th7;
sup D in S by A15, A16, A19, WAYBEL_0:def_20;
then D meets S by A14, WAYBEL11:def_1;
then D /\ S <> {} by XBOOLE_0:def_7;
then consider d being Element of R such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d = d as Element of R ;
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 } ,R) ;
defpred S2[ Element of N] means $1 >= j;
deffunc H2( Element of N) -> Element of the carrier of R = N . $1;
{ H2(i) where i is Element of N : S2[i] } is Subset of R from DOMAIN_1:sch_8();
then reconsider Y = { (N . i) where i is Element of N : i >= j } as Subset of R ;
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 Y ;
then d <= N . i0 by A21, Th8;
hence N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum
end;
hence S in the topology of (ConvergenceSpace (Scott-Convergence R)) by A1; ::_thesis: verum
end;
theorem Th11: :: WAYBEL32:11
for R being up-complete /\-complete Semilattice
for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott
proof
let R be up-complete /\-complete Semilattice; ::_thesis: for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott
let T be TopAugmentation of R; ::_thesis: ( the topology of T = sigma R implies T is Scott )
assume A1: the topology of T = sigma R ; ::_thesis: T is Scott
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
T is Scott
proof
let S be Subset of T; :: according to WAYBEL11:def_4 ::_thesis: ( ( not S is open or ( S is inaccessible_by_directed_joins & S is upper ) ) & ( not S is inaccessible_by_directed_joins or not S is upper or S is open ) )
reconsider A = S as Subset of R by A2;
thus ( S is open implies ( S is inaccessible & S is upper ) ) ::_thesis: ( not S is inaccessible_by_directed_joins or not S is upper or S is open )
proof
assume S is open ; ::_thesis: ( S is inaccessible & S is upper )
then S in the topology of T by PRE_TOPC:def_2;
then ( A is inaccessible & A is upper ) by A1, Th10;
hence ( S is inaccessible & S is upper ) by A2, WAYBEL_0:25, YELLOW_9:47; ::_thesis: verum
end;
assume A3: ( S is inaccessible & S is upper ) ; ::_thesis: S is open
A is inaccessible
proof
let D be non empty directed Subset of R; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,R) in A or not D misses A )
assume A4: sup D in A ; ::_thesis: not D misses A
reconsider E = D as Subset of T by A2;
ex a being Element of R st
( a is_>=_than D & ( for b being Element of R st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def_39;
then A5: ex_sup_of D,R by YELLOW_0:15;
A6: E is directed by A2, WAYBEL_0:3;
sup D = sup E by A2, A5, YELLOW_0:26;
hence not D misses A by A3, A4, A6, WAYBEL11:def_1; ::_thesis: verum
end;
then ( A is inaccessible & A is upper ) by A2, A3, WAYBEL_0:25;
then A in the topology of T by A1, Th10;
hence S is open by PRE_TOPC:def_2; ::_thesis: verum
end;
hence T is Scott ; ::_thesis: verum
end;
registration
let R be up-complete /\-complete Semilattice;
cluster non empty correct reflexive transitive antisymmetric up-complete strict Scott for TopAugmentation of R;
existence
ex b1 being TopAugmentation of R st
( b1 is strict & b1 is Scott & b1 is correct )
proof
set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #);
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 #) ;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopAugmentation of R by YELLOW_9:def_4;
take T ; ::_thesis: ( T is strict & T is Scott & T is correct )
thus ( T is strict & T is Scott & T is correct ) by Th11, YELLOW_9:48; ::_thesis: verum
end;
end;
theorem :: WAYBEL32:12
for S being up-complete /\-complete Semilattice
for T being Scott TopAugmentation of S holds sigma S = the topology of T
proof
let S be up-complete /\-complete Semilattice; ::_thesis: for T being Scott TopAugmentation of S holds sigma S = the topology of T
let T be Scott TopAugmentation of S; ::_thesis: sigma S = the topology of T
thus sigma S c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= sigma S
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in sigma S or e in the topology of T )
assume A1: e in sigma S ; ::_thesis: e in the topology of T
then reconsider A = e as Subset of S ;
A2: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider A9 = A as Subset of T ;
( A is inaccessible & A is upper ) by A1, Th10;
then ( A9 is inaccessible & A9 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;
hence e in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of T or e in sigma S )
assume A3: e in the topology of T ; ::_thesis: e in sigma S
then reconsider A = e as Subset of T ;
A4: A is open by A3, PRE_TOPC:def_2;
A5: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider A9 = A as Subset of S ;
A9 is inaccessible
proof
let D be non empty directed Subset of S; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,S) in A9 or not D misses A9 )
assume A6: sup D in A9 ; ::_thesis: not D misses A9
reconsider E = D as Subset of T by A5;
ex a being Element of S st
( a is_>=_than D & ( for b being Element of S st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def_39;
then A7: ex_sup_of D,S by YELLOW_0:15;
A8: E is directed by A5, WAYBEL_0:3;
sup D = sup E by A5, A7, YELLOW_0:26;
hence not D misses A9 by A4, A6, A8, WAYBEL11:def_1; ::_thesis: verum
end;
then ( A9 is inaccessible & A9 is upper ) by A4, A5, WAYBEL_0:25;
hence e in sigma S by Th10; ::_thesis: verum
end;
theorem :: WAYBEL32:13
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr holds T is T_0-TopSpace
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: T is T_0-TopSpace
reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44;
now__::_thesis:_for_x,_y_being_Point_of_T9_st_x_<>_y_holds_
Cl_{x}_<>_Cl_{y}
let x, y be Point of T9; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} )
reconsider x9 = x, y9 = y as Element of T9 ;
A1: Cl {x9} = downarrow x9 by Th5;
A2: Cl {y9} = downarrow y9 by Th5;
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;
registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster -> up-complete for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is up-complete ;
end;
theorem Th14: :: WAYBEL32:14
for R being non empty reflexive transitive antisymmetric up-complete RelStr
for T being Scott TopAugmentation of R
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 R be non empty reflexive transitive antisymmetric up-complete RelStr ; ::_thesis: for T being Scott TopAugmentation of R
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 T be Scott TopAugmentation of R; ::_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 closed by WAYBEL11:11;
then (downarrow x) ` is open ;
then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23;
A misses downarrow x by A1, WAYBEL11:5;
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 :: WAYBEL32:15
for R being non empty reflexive transitive antisymmetric up-complete TopRelStr
for T being Scott TopAugmentation of R
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 R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for T being Scott TopAugmentation of R
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 T be Scott TopAugmentation of R; ::_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, Th14;
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 :: WAYBEL32:16
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_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 S is upper ; ::_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: ( not "\/" (D,T) in S or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in S ) ) ) )
assume sup D in S ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in S ) ) )
then S meets D by A1, WAYBEL11:def_1;
then consider y being set such that
A2: y in S and
A3: y in D by XBOOLE_0:3;
reconsider y = y as Element of T by A2;
take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S ) ) )
thus ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S ) ) ) by A1, A2, A3, WAYBEL_0:def_20; ::_thesis: verum
end;
end;
assume that
A4: S is upper and
A5: 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: ( not "\/" (D,T) in S or not D misses S )
assume sup D in S ; ::_thesis: not D misses S
then consider y being Element of T such that
A6: y in D and
A7: for x being Element of T st x in D & x >= y holds
x in S by A5, WAYBEL11:def_3;
y >= y by YELLOW_0:def_1;
then y in S by A6, A7;
hence not D misses S by A6, XBOOLE_0:3; ::_thesis: verum
end;
hence S is open by A4; ::_thesis: verum
end;
theorem Th17: :: WAYBEL32:17
for R being non empty reflexive transitive antisymmetric up-complete TopRelStr
for S being non empty directed Subset of R
for a being Element of R st a in S holds
a <= "\/" (S,R)
proof
let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for S being non empty directed Subset of R
for a being Element of R st a in S holds
a <= "\/" (S,R)
let S be non empty directed Subset of R; ::_thesis: for a being Element of R st a in S holds
a <= "\/" (S,R)
let a be Element of R; ::_thesis: ( a in S implies a <= "\/" (S,R) )
assume A1: a in S ; ::_thesis: a <= "\/" (S,R)
ex_sup_of S,R by WAYBEL_0:75;
then S is_<=_than "\/" (S,R) by YELLOW_0:30;
hence a <= "\/" (S,R) by A1, LATTICE3:def_9; ::_thesis: verum
end;
registration
let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ;
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: ( not "\/" (D,T) in S or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in S ) ) ) )
assume A2: sup D in S ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 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 b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S ) ) )
thus y in D by A3; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S )
let x be Element of T; ::_thesis: ( not x in D or not y <= x or x in S )
assume that
A4: x in D and
x >= y ; ::_thesis: x in S
x <= sup D by A4, Th17;
hence x in S by A1, A2, WAYBEL_0:def_19; ::_thesis: verum
end;
end;
theorem :: WAYBEL32:18
for T being non empty finite up-complete Poset
for S being Subset of T holds S is inaccessible
proof
let T be non empty finite up-complete Poset; ::_thesis: for S being Subset of T holds S is inaccessible
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: ( not "\/" (D,T) in S or not D misses S )
assume A1: sup D in S ; ::_thesis: not D misses S
sup D in D
proof
reconsider D9 = D as finite Subset of T ;
D9 c= D9 ;
then reconsider E = D9 as finite Subset of D ;
consider x being Element of T such that
A2: x in D and
A3: x is_>=_than E by WAYBEL_0:1;
A4: for b being Element of T st D is_<=_than b holds
b >= x by A2, 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
A5: D is_<=_than c and
A6: for b being Element of T st D is_<=_than b holds
b >= c ; ::_thesis: c = x
A7: x >= c by A3, A6;
c >= x by A2, A5, LATTICE3:def_9;
hence c = x by A7, ORDERS_2:2; ::_thesis: verum
end;
then ex_sup_of D,T by A3, A4, YELLOW_0:def_7;
hence sup D in D by A2, A3, A4, YELLOW_0:def_9; ::_thesis: verum
end;
hence not D misses S by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th19: :: WAYBEL32:19
for R being complete connected LATTICE
for T being Scott TopAugmentation of R
for x being Element of T holds (downarrow x) ` is open
proof
let R be complete connected LATTICE; ::_thesis: for T being Scott TopAugmentation of R
for x being Element of T holds (downarrow x) ` is open
let T be Scott TopAugmentation of R; ::_thesis: for x being Element of T holds (downarrow x) ` is open
let x be Element of T; ::_thesis: (downarrow x) ` is open
reconsider S = downarrow x as lower directly_closed Subset of T by WAYBEL11:8;
S ` is open ;
hence (downarrow x) ` is open ; ::_thesis: verum
end;
theorem :: WAYBEL32:20
for R being complete connected LATTICE
for T being Scott TopAugmentation of R
for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) )
proof
let R be complete connected LATTICE; ::_thesis: for T being Scott TopAugmentation of R
for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) )
let T be Scott TopAugmentation of R; ::_thesis: for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) )
let S be Subset of T; ::_thesis: ( S is open iff ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) )
set DD = { ((downarrow x) `) where x is Element of T : verum } ;
thus ( not S is open or S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ::_thesis: ( ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) implies S is open )
proof
assume A1: S is open ; ::_thesis: ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } )
assume that
A2: S <> the carrier of T and
A3: not S in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: contradiction
A4: ([#] T) \ S <> {} by A2, PRE_TOPC:4;
A5: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then reconsider K = S ` as Subset of R ;
reconsider D = K as non empty directed Subset of T by A4, A5, WAYBEL_0:3;
A6: D misses S by SUBSET_1:23;
reconsider x = sup D as Element of T ;
S ` = downarrow x
proof
thus S ` c= downarrow x :: according to XBOOLE_0:def_10 ::_thesis: downarrow x c= S `
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S ` or a in downarrow x )
assume A7: a in S ` ; ::_thesis: a in downarrow x
then reconsider A = a as Element of T ;
x is_>=_than S ` by YELLOW_0:32;
then A <= x by A7, LATTICE3:def_9;
hence a in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in S ` )
assume A8: a in downarrow x ; ::_thesis: a in S `
then reconsider A = a as Element of T ;
A9: A <= x by A8, WAYBEL_0:17;
not x in S by A1, A6, WAYBEL11:def_1;
then not A in S by A1, A9, WAYBEL_0:def_20;
hence a in S ` by XBOOLE_0:def_5; ::_thesis: verum
end;
then (downarrow x) ` = S ;
hence contradiction by A3; ::_thesis: verum
end;
assume A10: ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) ; ::_thesis: S is open
percases ( S = the carrier of T or S in { ((downarrow x) `) where x is Element of T : verum } ) by A10;
supposeA11: S = the carrier of T ; ::_thesis: S is open
A12: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then S = [#] R by A11;
then A13: S is inaccessible by A12, YELLOW_9:47;
S is upper
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
x in S and
x <= y ; ::_thesis: y in S
thus y in S by A11; ::_thesis: verum
end;
hence S is open by A13; ::_thesis: verum
end;
suppose S in { ((downarrow x) `) where x is Element of T : verum } ; ::_thesis: S is open
then ex x being Element of T st S = (downarrow x) ` ;
hence S is open by Th19; ::_thesis: verum
end;
end;
end;
registration
let R be non empty up-complete Poset;
cluster non empty correct reflexive transitive antisymmetric up-complete order_consistent for TopAugmentation of R;
correctness
existence
ex b1 being correct TopAugmentation of R st b1 is order_consistent ;
proof
set T = the correct Scott TopAugmentation of R;
take the correct Scott TopAugmentation of R ; ::_thesis: the correct Scott TopAugmentation of R is order_consistent
thus the correct Scott TopAugmentation of R is order_consistent by Th6; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete order_consistent for TopRelStr ;
correctness
existence
ex b1 being TopLattice st
( b1 is order_consistent & b1 is complete );
proof
set T = the complete Scott TopLattice;
take the complete Scott TopLattice ; ::_thesis: ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete )
thus ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete ) by Th6; ::_thesis: verum
end;
end;
theorem Th21: :: WAYBEL32:21
for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds
A is upper
proof
let R be non empty TopRelStr ; ::_thesis: for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds
A is upper
let A be Subset of R; ::_thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) & A is open implies A is upper )
assume A1: for x being Element of R holds downarrow x = Cl {x} ; ::_thesis: ( not A is open or A is upper )
assume A2: A is open ; ::_thesis: A is upper
let x, y be Element of R; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A )
assume that
A3: x in A and
A4: x <= y ; ::_thesis: y in A
x in downarrow y by A4, WAYBEL_0:17;
then x in Cl {y} by A1;
then A meets {y} by A2, A3, PRE_TOPC:24;
then consider z being set such that
A5: z in A /\ {y} by XBOOLE_0:4;
A6: z in A by A5, XBOOLE_0:def_4;
z in {y} by A5, XBOOLE_0:def_4;
hence y in A by A6, TARSKI:def_1; ::_thesis: verum
end;
theorem :: WAYBEL32:22
for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds
for A being Subset of R st A is closed holds
A is lower
proof
let R be non empty TopRelStr ; ::_thesis: for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds
for A being Subset of R st A is closed holds
A is lower
let A be Subset of R; ::_thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) implies for A being Subset of R st A is closed holds
A is lower )
assume A1: for x being Element of R holds downarrow x = Cl {x} ; ::_thesis: for A being Subset of R st A is closed holds
A is lower
let A be Subset of R; ::_thesis: ( A is closed implies A is lower )
assume A2: A is closed ; ::_thesis: A is lower
let x, y be Element of R; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in A or not y <= x or y in A )
assume that
A3: x in A and
A4: y <= x ; ::_thesis: y in A
y in downarrow x by A4, WAYBEL_0:17;
then A5: y in Cl {x} by A1;
{x} c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in A )
assume a in {x} ; ::_thesis: a in A
hence a in A by A3, TARSKI:def_1; ::_thesis: verum
end;
hence y in A by A2, A5, PRE_TOPC:15; ::_thesis: verum
end;
definition
let S be non empty 1-sorted ;
let R be non empty RelStr ;
let f be Function of the carrier of R, the carrier of S;
funcR *' f -> non empty strict NetStr over S means :Def3: :: WAYBEL32:def 3
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of it = f );
existence
ex b1 being non empty strict NetStr over S st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f )
proof
reconsider M = NetStr(# the carrier of R, the InternalRel of R,f #) as non empty strict NetStr over S ;
take M ; ::_thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f )
thus ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict NetStr over S st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b2 = f holds
b1 = b2 ;
end;
:: deftheorem Def3 defines *' WAYBEL32:def_3_:_
for S being non empty 1-sorted
for R being non empty RelStr
for f being Function of the carrier of R, the carrier of S
for b4 being non empty strict NetStr over S holds
( b4 = R *' f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b4 = f ) );
registration
let S be non empty 1-sorted ;
let R be non empty transitive RelStr ;
let f be Function of the carrier of R, the carrier of S;
clusterR *' f -> non empty transitive strict ;
coherence
R *' f is transitive
proof
RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def3;
hence R *' f is transitive by WAYBEL_8:13; ::_thesis: verum
end;
end;
registration
let S be non empty 1-sorted ;
let R be non empty directed RelStr ;
let f be Function of the carrier of R, the carrier of S;
clusterR *' f -> non empty strict directed ;
coherence
R *' f is directed
proof
A1: RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def3;
[#] R is directed by WAYBEL_0:def_6;
hence [#] (R *' f) is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;
definition
let R be non empty RelStr ;
let N be prenet of R;
func inf_net N -> strict prenet of R means :Def4: :: WAYBEL32:def 4
ex f being Function of N,R st
( it = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) );
existence
ex b1 being strict prenet of R ex f being Function of N,R st
( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) )
proof
deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . k) where k is Element of N : k >= $1 } ,R);
consider g being Function of the carrier of N, the carrier of R such that
A1: for i being Element of N holds g . i = H1(i) from FUNCT_2:sch_4();
reconsider f = g as Function of N,R ;
reconsider M = N *' f as strict prenet of R ;
take M ; ::_thesis: ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) )
thus ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict prenet of R st ex f being Function of N,R st
( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) & ex f being Function of N,R st
( b2 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) holds
b1 = b2
proof
let M, P be strict prenet of R; ::_thesis: ( ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) & ex f being Function of N,R st
( P = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) implies M = P )
assume that
A2: ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) and
A3: ex f being Function of N,R st
( P = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) ; ::_thesis: M = P
consider f1 being Function of N,R such that
A4: M = N *' f1 and
A5: for i being Element of N holds f1 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A2;
consider f2 being Function of N,R such that
A6: P = N *' f2 and
A7: for i being Element of N holds f2 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A3;
for i being set st i in the carrier of N holds
f1 . i = f2 . i
proof
let i be set ; ::_thesis: ( i in the carrier of N implies f1 . i = f2 . i )
assume i in the carrier of N ; ::_thesis: f1 . i = f2 . i
then reconsider i = i as Element of N ;
f1 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A5
.= f2 . i by A7 ;
hence f1 . i = f2 . i ; ::_thesis: verum
end;
hence M = P by A4, A6, FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines inf_net WAYBEL32:def_4_:_
for R being non empty RelStr
for N being prenet of R
for b3 being strict prenet of R holds
( b3 = inf_net N iff ex f being Function of N,R st
( b3 = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) );
registration
let R be non empty RelStr ;
let N be net of R;
cluster inf_net N -> transitive strict ;
coherence
inf_net N is transitive
proof
ex f being Function of N,R st
( inf_net N = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) by Def4;
hence inf_net N is transitive ; ::_thesis: verum
end;
end;
registration
let R be non empty RelStr ;
let N be net of R;
cluster inf_net N -> strict ;
coherence
inf_net N is directed ;
end;
registration
let R be non empty reflexive antisymmetric /\-complete RelStr ;
let N be net of R;
cluster inf_net N -> strict monotone ;
coherence
inf_net N is monotone
proof
let i, j be Element of (inf_net N); :: according to WAYBEL11:def_9 ::_thesis: ( not i <= j or (inf_net N) . i <= (inf_net N) . j )
assume A1: i <= j ; ::_thesis: (inf_net N) . i <= (inf_net N) . j
consider f being Function of N,R such that
A2: inf_net N = N *' f and
A3: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4;
A4: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A2, Def3;
then reconsider i9 = i, j9 = j as Element of N ;
deffunc H1( Element of N) -> Element of the carrier of R = N . R;
defpred S1[ Element of N] means R >= j9;
defpred S2[ Element of N] means R >= i9;
set J = { H1(k) where k is Element of N : S1[k] } ;
set I = { H1(k) where k is Element of N : S2[k] } ;
A5: { H1(k) where k is Element of N : S1[k] } is Subset of R from DOMAIN_1:sch_8();
consider j0 being Element of N such that
A6: j0 >= j9 and
j0 >= j9 by YELLOW_6:def_3;
N . j0 in { H1(k) where k is Element of N : S1[k] } by A6;
then reconsider J9 = { H1(k) where k is Element of N : S1[k] } as non empty Subset of R by A5;
A7: { H1(k) where k is Element of N : S2[k] } is Subset of R from DOMAIN_1:sch_8();
consider j1 being Element of N such that
A8: j1 >= i9 and
j1 >= i9 by YELLOW_6:def_3;
N . j1 in { H1(k) where k is Element of N : S2[k] } by A8;
then reconsider I9 = { H1(k) where k is Element of N : S2[k] } as non empty Subset of R by A7;
A9: ex_inf_of J9,R by WAYBEL_0:76;
A10: ex_inf_of I9,R by WAYBEL_0:76;
A11: J9 c= I9
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in J9 or a in I9 )
assume A12: a in J9 ; ::_thesis: a in I9
then reconsider x = a as Element of R ;
consider k being Element of N such that
A13: x = N . k and
A14: k >= j9 by A12;
reconsider k9 = k as Element of N ;
i9 <= j9 by A1, A4, YELLOW_0:1;
then i9 <= k9 by A14, YELLOW_0:def_2;
hence a in I9 by A13; ::_thesis: verum
end;
A15: f . i9 = "/\" ( { H1(k) where k is Element of N : S2[k] } ,R) by A3;
A16: f . j9 = "/\" ( { H1(k) where k is Element of N : S1[k] } ,R) by A3;
the mapping of (inf_net N) = f by A2, Def3;
hence (inf_net N) . i <= (inf_net N) . j by A9, A10, A11, A15, A16, YELLOW_0:35; ::_thesis: verum
end;
end;
registration
let R be non empty reflexive antisymmetric /\-complete RelStr ;
let N be net of R;
cluster inf_net N -> strict eventually-directed ;
coherence
inf_net N is eventually-directed ;
end;
theorem Th23: :: WAYBEL32:23
for R being non empty RelStr
for N being net of R holds rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }
proof
let R be non empty RelStr ; ::_thesis: for N being net of R holds rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }
let N be net of R; ::_thesis: rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }
consider f being Function of N,R such that
A1: inf_net N = N *' f and
A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4;
A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3;
A4: the mapping of (inf_net N) = f by A1, Def3;
then A5: the carrier of (inf_net N) = dom f by FUNCT_2:def_1;
thus rng the mapping of (inf_net N) c= { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } :: according to XBOOLE_0:def_10 ::_thesis: { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } c= rng the mapping of (inf_net N)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng the mapping of (inf_net N) or e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } )
assume e in rng the mapping of (inf_net N) ; ::_thesis: e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }
then consider u being set such that
A6: u in dom f and
A7: e = f . u by A4, FUNCT_1:def_3;
reconsider u = u as Element of N by A6;
f . u = "/\" ( { (N . k) where k is Element of N : k >= u } ,R) by A2;
hence e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } by A7; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } or e in rng the mapping of (inf_net N) )
assume e in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; ::_thesis: e in rng the mapping of (inf_net N)
then consider j being Element of N such that
A8: e = "/\" ( { (N . i) where i is Element of N : i >= j } ,R) ;
e = the mapping of (inf_net N) . j by A2, A4, A8;
hence e in rng the mapping of (inf_net N) by A3, A4, A5, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th24: :: WAYBEL32:24
for R being up-complete /\-complete LATTICE
for N being net of R holds sup (inf_net N) = lim_inf N
proof
let R be up-complete /\-complete LATTICE; ::_thesis: for N being net of R holds sup (inf_net N) = lim_inf N
let N be net of R; ::_thesis: sup (inf_net N) = lim_inf N
defpred S1[ set ] means verum;
deffunc H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . l) where l is Element of N : l >= $1 } ,R);
sup (inf_net N) = Sup by WAYBEL_2:def_1
.= sup (rng the mapping of (inf_net N)) by YELLOW_2:def_5
.= lim_inf N by Th23 ;
hence sup (inf_net N) = lim_inf N ; ::_thesis: verum
end;
theorem :: WAYBEL32:25
for R being up-complete /\-complete LATTICE
for N being net of R
for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
proof
let R be up-complete /\-complete LATTICE; ::_thesis: for N being net of R
for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
let N be net of R; ::_thesis: for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
let i be Element of N; ::_thesis: sup (inf_net N) = lim_inf (N | i)
sup (inf_net N) = lim_inf N by Th24;
hence sup (inf_net N) = lim_inf (N | i) by WAYBEL21:41; ::_thesis: verum
end;
theorem Th26: :: WAYBEL32:26
for R being /\-complete Semilattice
for N being net of R
for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
proof
let R be /\-complete Semilattice; ::_thesis: for N being net of R
for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
let N be net of R; ::_thesis: for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
let V be upper Subset of R; ::_thesis: ( inf_net N is_eventually_in V implies N is_eventually_in V )
consider f being Function of N,R such that
A1: inf_net N = N *' f and
A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4;
A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3;
assume inf_net N is_eventually_in V ; ::_thesis: N is_eventually_in V
then consider i being Element of (inf_net N) such that
A4: for j being Element of (inf_net N) st i <= j holds
(inf_net N) . j in V by WAYBEL_0:def_11;
consider j0 being Element of (inf_net N) such that
A5: i <= j0 and
i <= j0 by YELLOW_6:def_3;
A6: (inf_net N) . j0 in V by A4, A5;
reconsider j9 = j0 as Element of N by A3;
take j9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j9 <= b1 or N . b1 in V )
let j be Element of N; ::_thesis: ( not j9 <= j or N . j in V )
assume A7: j9 <= j ; ::_thesis: N . j in V
defpred S1[ Element of N] means $1 >= j9;
deffunc H1( Element of N) -> Element of the carrier of R = N . $1;
set E = { H1(k) where k is Element of N : S1[k] } ;
{ H1(k) where k is Element of N : S1[k] } is Subset of R from DOMAIN_1:sch_8();
then reconsider E = { H1(k) where k is Element of N : S1[k] } as Subset of R ;
the mapping of (inf_net N) = f by A1, Def3;
then A8: (inf_net N) . j0 = "/\" (E,R) by A2;
N . j in E by A7;
then "/\" (E,R) <= N . j by Th8;
hence N . j in V by A6, A8, WAYBEL_0:def_20; ::_thesis: verum
end;
theorem :: WAYBEL32:27
for R being /\-complete Semilattice
for N being net of R
for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
proof
let R be /\-complete Semilattice; ::_thesis: for N being net of R
for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
let N be net of R; ::_thesis: for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
let V be lower Subset of R; ::_thesis: ( N is_eventually_in V implies inf_net N is_eventually_in V )
consider f being Function of N,R such that
A1: inf_net N = N *' f and
A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4;
A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3;
assume N is_eventually_in V ; ::_thesis: inf_net N is_eventually_in V
then consider i being Element of N such that
A4: for j being Element of N st i <= j holds
N . j in V by WAYBEL_0:def_11;
reconsider i9 = i as Element of (inf_net N) by A3;
take i9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (inf_net N) holds
( not i9 <= b1 or (inf_net N) . b1 in V )
let j be Element of (inf_net N); ::_thesis: ( not i9 <= j or (inf_net N) . j in V )
assume A5: i9 <= j ; ::_thesis: (inf_net N) . j in V
reconsider j0 = j as Element of N by A3;
defpred S1[ Element of N] means $1 >= j0;
deffunc H1( Element of N) -> Element of the carrier of R = N . $1;
set E = { H1(k) where k is Element of N : S1[k] } ;
consider j1 being Element of N such that
A6: j1 >= j0 and
j1 >= j0 by YELLOW_6:def_3;
{ H1(k) where k is Element of N : S1[k] } is Subset of R from DOMAIN_1:sch_8();
then reconsider E = { H1(k) where k is Element of N : S1[k] } as Subset of R ;
i <= j0 by A3, A5, YELLOW_0:1;
then i <= j1 by A6, YELLOW_0:def_2;
then A7: N . j1 in V by A4;
N . j1 in E by A6;
then A8: "/\" (E,R) <= N . j1 by Th8;
the mapping of (inf_net N) = f by A1, Def3;
then (inf_net N) . j = "/\" (E,R) by A2;
hence (inf_net N) . j in V by A7, A8, WAYBEL_0:def_19; ::_thesis: verum
end;
theorem Th28: :: WAYBEL32:28
for R being non empty up-complete /\-complete order_consistent TopLattice
for N being net of R
for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
proof
let R be non empty up-complete /\-complete order_consistent TopLattice; ::_thesis: for N being net of R
for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
let N be net of R; ::_thesis: for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
let x be Element of R; ::_thesis: ( x <= lim_inf N implies x is_a_cluster_point_of N )
assume A1: x <= lim_inf N ; ::_thesis: x is_a_cluster_point_of N
defpred S1[ Element of N] 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] } ;
{ H1(j) where j is Element of N : S1[j] } is Subset of R from DOMAIN_1:sch_8();
then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th7;
sup D = lim_inf N ;
then A2: sup D = sup (inf_net N) by Th24;
let V be a_neighborhood of x; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in V
for a being Element of R holds downarrow a = Cl {a} by Def2;
then A3: Int V is upper by Th21;
x in Int V by CONNSP_2:def_1;
then sup D in Int V by A1, A3, WAYBEL_0:def_20;
then reconsider W = Int V as a_neighborhood of sup D by CONNSP_2:3;
A4: Int V c= V by TOPS_1:16;
inf_net N is_eventually_in W by A2, Def2;
then N is_eventually_in W by A3, Th26;
then N is_eventually_in V by A4, WAYBEL_0:8;
hence N is_often_in V by YELLOW_6:19; ::_thesis: verum
end;
theorem :: WAYBEL32:29
for R being non empty up-complete /\-complete order_consistent TopLattice
for N being eventually-directed net of R
for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
proof
let R be non empty up-complete /\-complete order_consistent TopLattice; ::_thesis: for N being eventually-directed net of R
for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let N be eventually-directed net of R; ::_thesis: for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let x be Element of R; ::_thesis: ( x <= lim_inf N iff x is_a_cluster_point_of N )
thus ( x <= lim_inf N implies x is_a_cluster_point_of N ) by Th28; ::_thesis: ( x is_a_cluster_point_of N implies x <= lim_inf N )
thus ( x is_a_cluster_point_of N implies x <= lim_inf N ) ::_thesis: verum
proof
assume A1: x is_a_cluster_point_of N ; ::_thesis: x <= lim_inf N
defpred S1[ Element of N] 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] } ;
{ H1(j) where j is Element of N : S1[j] } is Subset of R from DOMAIN_1:sch_8();
then reconsider D = { H1(j) where j is Element of N : S1[j] } as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th7;
for G being Subset of R st G is open & x in G holds
{(sup D)} meets G
proof
let G be Subset of R; ::_thesis: ( G is open & x in G implies {(sup D)} meets G )
assume A2: G is open ; ::_thesis: ( not x in G or {(sup D)} meets G )
assume x in G ; ::_thesis: {(sup D)} meets G
then reconsider G = G as a_neighborhood of x by A2, CONNSP_2:3;
A3: N is_often_in G by A1, WAYBEL_9:def_9;
now__::_thesis:_for_i_being_Element_of_N_holds_sup_D_in_G
let i be Element of N; ::_thesis: sup D in G
consider j1 being Element of N such that
i <= j1 and
A4: N . j1 in G by A3, WAYBEL_0:def_12;
consider j2 being Element of N such that
A5: for k being Element of N st j2 <= k holds
N . j1 <= N . k by WAYBEL_0:11;
defpred S2[ Element of N] means $1 >= j2;
deffunc H2( Element of N) -> Element of the carrier of R = N . $1;
set E = { H2(k) where k is Element of N : S2[k] } ;
A6: { H2(k) where k is Element of N : S2[k] } is Subset of R from DOMAIN_1:sch_8();
consider j9 being Element of N such that
A7: j9 >= j2 and
j9 >= j2 by YELLOW_6:def_3;
N . j9 in { H2(k) where k is Element of N : S2[k] } by A7;
then reconsider E9 = { H2(k) where k is Element of N : S2[k] } as non empty Subset of R by A6;
A8: ex_inf_of E9,R by WAYBEL_0:76;
N . j1 is_<=_than E9
proof
let b be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not b in E9 or N . j1 <= b )
assume b in E9 ; ::_thesis: N . j1 <= b
then ex k being Element of N st
( b = N . k & k >= j2 ) ;
hence N . j1 <= b by A5; ::_thesis: verum
end;
then A9: N . j1 <= "/\" (E9,R) by A8, YELLOW_0:31;
for a being Element of R holds downarrow a = Cl {a} by Def2;
then A10: G is upper by A2, Th21;
then A11: "/\" (E9,R) in G by A4, A9, WAYBEL_0:def_20;
"/\" (E9,R) in D ;
then "/\" (E9,R) <= sup D by Th17;
hence sup D in G by A10, A11, WAYBEL_0:def_20; ::_thesis: verum
end;
then A12: sup D in G ;
sup D in {(sup D)} by TARSKI:def_1;
hence {(sup D)} meets G by A12, XBOOLE_0:3; ::_thesis: verum
end;
then x in Cl {(sup D)} by PRE_TOPC:24;
then x in downarrow (sup D) by Def2;
hence x <= lim_inf N by WAYBEL_0:17; ::_thesis: verum
end;
end;