:: WAYBEL14 semantic presentation
begin
theorem Th1: :: WAYBEL14:1
for X being set
for F being finite Subset-Family of X ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
proof
let X be set ; ::_thesis: for F being finite Subset-Family of X ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
defpred S1[ Nat] means for F being finite Subset-Family of X st card F = $1 holds
ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) );
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let F be finite Subset-Family of X; ::_thesis: ( card F = n + 1 implies ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) ) )
assume A3: card F = n + 1 ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
percases ( ex g being Subset of X st
( g in F & g c= union (F \ {g}) ) or for g being Subset of X holds
( not g in F or not g c= union (F \ {g}) ) ) ;
suppose ex g being Subset of X st
( g in F & g c= union (F \ {g}) ) ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
then consider g being Subset of X such that
A4: g in F and
A5: g c= union (F \ {g}) ;
reconsider FF = F \ {g} as finite Subset-Family of X ;
{g} c= F by A4, ZFMISC_1:31;
then A6: F = FF \/ {g} by XBOOLE_1:45;
A7: union F c= union FF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in union FF )
assume x in union F ; ::_thesis: x in union FF
then consider X being set such that
A8: x in X and
A9: X in F by TARSKI:def_4;
percases ( X in FF or X in {g} ) by A6, A9, XBOOLE_0:def_3;
suppose X in FF ; ::_thesis: x in union FF
then X c= union FF by ZFMISC_1:74;
hence x in union FF by A8; ::_thesis: verum
end;
suppose X in {g} ; ::_thesis: x in union FF
then X = g by TARSKI:def_1;
hence x in union FF by A5, A8; ::_thesis: verum
end;
end;
end;
g in {g} by TARSKI:def_1;
then not g in FF by XBOOLE_0:def_5;
then card (FF \/ {g}) = (card FF) + 1 by CARD_2:41;
then consider G being finite Subset-Family of X such that
A10: G c= FF and
A11: union G = union FF and
A12: for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A2, A3, A6, XCMPLX_1:2;
take G ; ::_thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
FF c= F by A6, XBOOLE_1:7;
hence G c= F by A10, XBOOLE_1:1; ::_thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
union FF c= union F by A6, XBOOLE_1:7, ZFMISC_1:77;
hence union G = union F by A11, A7, XBOOLE_0:def_10; ::_thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A12; ::_thesis: verum
end;
supposeA13: for g being Subset of X holds
( not g in F or not g c= union (F \ {g}) ) ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
take G = F; ::_thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus G c= F ; ::_thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus union G = union F ; ::_thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A13; ::_thesis: verum
end;
end;
end;
end;
let F be finite Subset-Family of X; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
A14: card F = card F ;
A15: S1[ 0 ]
proof
let F be finite Subset-Family of X; ::_thesis: ( card F = 0 implies ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) ) )
assume A16: card F = 0 ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
take G = F; ::_thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus G c= F ; ::_thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus union G = union F ; ::_thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A16; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_2(A15, A1);
hence ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) ) by A14; ::_thesis: verum
end;
Lm1: for S being 1-sorted
for X, Y being Subset of S holds
( X c= Y ` iff Y c= X ` )
proof
let S be 1-sorted ; ::_thesis: for X, Y being Subset of S holds
( X c= Y ` iff Y c= X ` )
let X, Y be Subset of S; ::_thesis: ( X c= Y ` iff Y c= X ` )
Y = (Y `) ` ;
hence ( X c= Y ` iff Y c= X ` ) by SUBSET_1:12; ::_thesis: verum
end;
theorem Th2: :: WAYBEL14:2
for S being 1-sorted
for X being Subset of S holds
( X ` = the carrier of S iff X is empty )
proof
let S be 1-sorted ; ::_thesis: for X being Subset of S holds
( X ` = the carrier of S iff X is empty )
let X be Subset of S; ::_thesis: ( X ` = the carrier of S iff X is empty )
hereby ::_thesis: ( X is empty implies X ` = the carrier of S )
assume X ` = the carrier of S ; ::_thesis: X is empty
then X = ([#] the carrier of S) ` ;
hence X is empty by XBOOLE_1:37; ::_thesis: verum
end;
assume X is empty ; ::_thesis: X ` = the carrier of S
hence X ` = the carrier of S ; ::_thesis: verum
end;
theorem Th3: :: WAYBEL14:3
for R being non empty transitive antisymmetric with_infima RelStr
for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)
proof
let R be non empty transitive antisymmetric with_infima RelStr ; ::_thesis: for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)
let x, y be Element of R; ::_thesis: downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_downarrow_(x_"/\"_y)_implies_z_in_(downarrow_x)_/\_(downarrow_y)_)_&_(_z_in_(downarrow_x)_/\_(downarrow_y)_implies_z_in_downarrow_(x_"/\"_y)_)_)
let z be set ; ::_thesis: ( ( z in downarrow (x "/\" y) implies z in (downarrow x) /\ (downarrow y) ) & ( z in (downarrow x) /\ (downarrow y) implies z in downarrow (x "/\" y) ) )
hereby ::_thesis: ( z in (downarrow x) /\ (downarrow y) implies z in downarrow (x "/\" y) )
assume A1: z in downarrow (x "/\" y) ; ::_thesis: z in (downarrow x) /\ (downarrow y)
then reconsider z9 = z as Element of R ;
A2: z9 <= x "/\" y by A1, WAYBEL_0:17;
x "/\" y <= y by YELLOW_0:23;
then z9 <= y by A2, YELLOW_0:def_2;
then A3: z9 in downarrow y by WAYBEL_0:17;
x "/\" y <= x by YELLOW_0:23;
then z9 <= x by A2, YELLOW_0:def_2;
then z9 in downarrow x by WAYBEL_0:17;
hence z in (downarrow x) /\ (downarrow y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A4: z in (downarrow x) /\ (downarrow y) ; ::_thesis: z in downarrow (x "/\" y)
then reconsider z9 = z as Element of R ;
z in downarrow y by A4, XBOOLE_0:def_4;
then A5: z9 <= y by WAYBEL_0:17;
z in downarrow x by A4, XBOOLE_0:def_4;
then z9 <= x by WAYBEL_0:17;
then x "/\" y >= z9 by A5, YELLOW_0:23;
hence z in downarrow (x "/\" y) by WAYBEL_0:17; ::_thesis: verum
end;
hence downarrow (x "/\" y) = (downarrow x) /\ (downarrow y) by TARSKI:1; ::_thesis: verum
end;
theorem :: WAYBEL14:4
for R being non empty transitive antisymmetric with_suprema RelStr
for x, y being Element of R holds uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)
proof
let R be non empty transitive antisymmetric with_suprema RelStr ; ::_thesis: for x, y being Element of R holds uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)
let x, y be Element of R; ::_thesis: uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_uparrow_(x_"\/"_y)_implies_z_in_(uparrow_x)_/\_(uparrow_y)_)_&_(_z_in_(uparrow_x)_/\_(uparrow_y)_implies_z_in_uparrow_(x_"\/"_y)_)_)
let z be set ; ::_thesis: ( ( z in uparrow (x "\/" y) implies z in (uparrow x) /\ (uparrow y) ) & ( z in (uparrow x) /\ (uparrow y) implies z in uparrow (x "\/" y) ) )
hereby ::_thesis: ( z in (uparrow x) /\ (uparrow y) implies z in uparrow (x "\/" y) )
assume A1: z in uparrow (x "\/" y) ; ::_thesis: z in (uparrow x) /\ (uparrow y)
then reconsider z9 = z as Element of R ;
A2: z9 >= x "\/" y by A1, WAYBEL_0:18;
x "\/" y >= y by YELLOW_0:22;
then z9 >= y by A2, YELLOW_0:def_2;
then A3: z9 in uparrow y by WAYBEL_0:18;
x "\/" y >= x by YELLOW_0:22;
then z9 >= x by A2, YELLOW_0:def_2;
then z9 in uparrow x by WAYBEL_0:18;
hence z in (uparrow x) /\ (uparrow y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A4: z in (uparrow x) /\ (uparrow y) ; ::_thesis: z in uparrow (x "\/" y)
then reconsider z9 = z as Element of R ;
z in uparrow y by A4, XBOOLE_0:def_4;
then A5: z9 >= y by WAYBEL_0:18;
z in uparrow x by A4, XBOOLE_0:def_4;
then z9 >= x by WAYBEL_0:18;
then x "\/" y <= z9 by A5, YELLOW_0:22;
hence z in uparrow (x "\/" y) by WAYBEL_0:18; ::_thesis: verum
end;
hence uparrow (x "\/" y) = (uparrow x) /\ (uparrow y) by TARSKI:1; ::_thesis: verum
end;
theorem Th5: :: WAYBEL14:5
for L being non empty antisymmetric complete RelStr
for X being lower Subset of L st sup X in X holds
X = downarrow (sup X)
proof
let L be non empty antisymmetric complete RelStr ; ::_thesis: for X being lower Subset of L st sup X in X holds
X = downarrow (sup X)
let X be lower Subset of L; ::_thesis: ( sup X in X implies X = downarrow (sup X) )
assume A1: sup X in X ; ::_thesis: X = downarrow (sup X)
X is_<=_than sup X by YELLOW_0:32;
hence X c= downarrow (sup X) by YELLOW_2:1; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (sup X) c= X
thus downarrow (sup X) c= X by A1, WAYBEL11:6; ::_thesis: verum
end;
theorem :: WAYBEL14:6
for L being non empty antisymmetric complete RelStr
for X being upper Subset of L st inf X in X holds
X = uparrow (inf X)
proof
let L be non empty antisymmetric complete RelStr ; ::_thesis: for X being upper Subset of L st inf X in X holds
X = uparrow (inf X)
let X be upper Subset of L; ::_thesis: ( inf X in X implies X = uparrow (inf X) )
assume A1: inf X in X ; ::_thesis: X = uparrow (inf X)
X is_>=_than inf X by YELLOW_0:33;
hence X c= uparrow (inf X) by YELLOW_2:2; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (inf X) c= X
thus uparrow (inf X) c= X by A1, WAYBEL11:42; ::_thesis: verum
end;
theorem Th7: :: WAYBEL14:7
for R being non empty reflexive transitive RelStr
for x, y being Element of R holds
( x << y iff uparrow y c= wayabove x )
proof
let R be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of R holds
( x << y iff uparrow y c= wayabove x )
let x, y be Element of R; ::_thesis: ( x << y iff uparrow y c= wayabove x )
hereby ::_thesis: ( uparrow y c= wayabove x implies x << y )
assume A1: x << y ; ::_thesis: uparrow y c= wayabove x
thus uparrow y c= wayabove x ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow y or z in wayabove x )
assume A2: z in uparrow y ; ::_thesis: z in wayabove x
then reconsider z9 = z as Element of R ;
y <= z9 by A2, WAYBEL_0:18;
then x << z9 by A1, WAYBEL_3:2;
hence z in wayabove x ; ::_thesis: verum
end;
end;
y <= y ;
then A3: y in uparrow y by WAYBEL_0:18;
assume uparrow y c= wayabove x ; ::_thesis: x << y
hence x << y by A3, WAYBEL_3:8; ::_thesis: verum
end;
theorem :: WAYBEL14:8
for R being non empty reflexive transitive RelStr
for x, y being Element of R holds
( x << y iff downarrow x c= waybelow y )
proof
let R be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of R holds
( x << y iff downarrow x c= waybelow y )
let x, y be Element of R; ::_thesis: ( x << y iff downarrow x c= waybelow y )
hereby ::_thesis: ( downarrow x c= waybelow y implies x << y )
assume A1: x << y ; ::_thesis: downarrow x c= waybelow y
thus downarrow x c= waybelow y ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow x or z in waybelow y )
assume A2: z in downarrow x ; ::_thesis: z in waybelow y
then reconsider z9 = z as Element of R ;
z9 <= x by A2, WAYBEL_0:17;
then z9 << y by A1, WAYBEL_3:2;
hence z in waybelow y ; ::_thesis: verum
end;
end;
x <= x ;
then A3: x in downarrow x by WAYBEL_0:17;
assume downarrow x c= waybelow y ; ::_thesis: x << y
hence x << y by A3, WAYBEL_3:7; ::_thesis: verum
end;
theorem Th9: :: WAYBEL14:9
for R being non empty reflexive antisymmetric complete RelStr
for x being Element of R holds
( sup (waybelow x) <= x & x <= inf (wayabove x) )
proof
let R be non empty reflexive antisymmetric complete RelStr ; ::_thesis: for x being Element of R holds
( sup (waybelow x) <= x & x <= inf (wayabove x) )
let x be Element of R; ::_thesis: ( sup (waybelow x) <= x & x <= inf (wayabove x) )
x is_>=_than waybelow x by WAYBEL_3:9;
hence sup (waybelow x) <= x by YELLOW_0:32; ::_thesis: x <= inf (wayabove x)
x is_<=_than wayabove x by WAYBEL_3:10;
hence x <= inf (wayabove x) by YELLOW_0:33; ::_thesis: verum
end;
theorem Th10: :: WAYBEL14:10
for L being non empty antisymmetric lower-bounded RelStr holds uparrow (Bottom L) = the carrier of L
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: uparrow (Bottom L) = the carrier of L
set uL = uparrow (Bottom L);
set cL = the carrier of L;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_uparrow_(Bottom_L)_implies_x_in_the_carrier_of_L_)_&_(_x_in_the_carrier_of_L_implies_x_in_uparrow_(Bottom_L)_)_)
let x be set ; ::_thesis: ( ( x in uparrow (Bottom L) implies x in the carrier of L ) & ( x in the carrier of L implies x in uparrow (Bottom L) ) )
thus ( x in uparrow (Bottom L) implies x in the carrier of L ) ; ::_thesis: ( x in the carrier of L implies x in uparrow (Bottom L) )
assume x in the carrier of L ; ::_thesis: x in uparrow (Bottom L)
then reconsider x9 = x as Element of L ;
Bottom L <= x9 by YELLOW_0:44;
hence x in uparrow (Bottom L) by WAYBEL_0:18; ::_thesis: verum
end;
hence uparrow (Bottom L) = the carrier of L by TARSKI:1; ::_thesis: verum
end;
theorem :: WAYBEL14:11
for L being non empty antisymmetric upper-bounded RelStr holds downarrow (Top L) = the carrier of L
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: downarrow (Top L) = the carrier of L
set uL = downarrow (Top L);
set cL = the carrier of L;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_downarrow_(Top_L)_implies_x_in_the_carrier_of_L_)_&_(_x_in_the_carrier_of_L_implies_x_in_downarrow_(Top_L)_)_)
let x be set ; ::_thesis: ( ( x in downarrow (Top L) implies x in the carrier of L ) & ( x in the carrier of L implies x in downarrow (Top L) ) )
thus ( x in downarrow (Top L) implies x in the carrier of L ) ; ::_thesis: ( x in the carrier of L implies x in downarrow (Top L) )
assume x in the carrier of L ; ::_thesis: x in downarrow (Top L)
then reconsider x9 = x as Element of L ;
Top L >= x9 by YELLOW_0:45;
hence x in downarrow (Top L) by WAYBEL_0:17; ::_thesis: verum
end;
hence downarrow (Top L) = the carrier of L by TARSKI:1; ::_thesis: verum
end;
theorem Th12: :: WAYBEL14:12
for P being with_suprema Poset
for x, y being Element of P holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
proof
let R be with_suprema Poset; ::_thesis: for x, y being Element of R holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
let x, y be Element of R; ::_thesis: (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
( {x} "\/" {y} = {(x "\/" y)} & (uparrow x) "\/" (uparrow y) c= uparrow ((uparrow x) "\/" (uparrow y)) ) by WAYBEL_0:16, YELLOW_4:19;
then A1: (uparrow x) "\/" (uparrow y) c= uparrow (x "\/" y) by YELLOW_4:35;
( wayabove x c= uparrow x & wayabove y c= uparrow y ) by WAYBEL_3:11;
then (wayabove x) "\/" (wayabove y) c= (uparrow x) "\/" (uparrow y) by YELLOW_4:21;
hence (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: WAYBEL14:13
for P being with_infima Poset
for x, y being Element of P holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
proof
let R be with_infima Poset; ::_thesis: for x, y being Element of R holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
let x, y be Element of R; ::_thesis: (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
( {x} "/\" {y} = {(x "/\" y)} & (downarrow x) "/\" (downarrow y) c= downarrow ((downarrow x) "/\" (downarrow y)) ) by WAYBEL_0:16, YELLOW_4:46;
then A1: (downarrow x) "/\" (downarrow y) c= downarrow (x "/\" y) by YELLOW_4:62;
( waybelow x c= downarrow x & waybelow y c= downarrow y ) by WAYBEL_3:11;
then (waybelow x) "/\" (waybelow y) c= (downarrow x) "/\" (downarrow y) by YELLOW_4:48;
hence (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th14: :: WAYBEL14:14
for R being non empty with_suprema Poset
for l being Element of R holds
( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
proof
let R be non empty with_suprema Poset; ::_thesis: for l being Element of R holds
( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
let l be Element of R; ::_thesis: ( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
hereby ::_thesis: ( ( for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) ) implies l is co-prime )
assume l is co-prime ; ::_thesis: for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y )
then A1: l ~ is prime by WAYBEL_6:def_8;
let x, y be Element of R; ::_thesis: ( not l <= x "\/" y or l <= x or l <= y )
assume l <= x "\/" y ; ::_thesis: ( l <= x or l <= y )
then A2: (x "\/" y) ~ <= l ~ by LATTICE3:9;
(x "\/" y) ~ = x "\/" y by LATTICE3:def_6
.= (x ~) "/\" (y ~) by YELLOW_7:23 ;
then ( x ~ <= l ~ or y ~ <= l ~ ) by A1, A2, WAYBEL_6:def_6;
hence ( l <= x or l <= y ) by LATTICE3:9; ::_thesis: verum
end;
assume A3: for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) ; ::_thesis: l is co-prime
let x, y be Element of (R ~); :: according to WAYBEL_6:def_6,WAYBEL_6:def_8 ::_thesis: ( not x "/\" y <= l ~ or x <= l ~ or y <= l ~ )
A4: ~ (x "/\" y) = x "/\" y by LATTICE3:def_7
.= (~ x) "\/" (~ y) by YELLOW_7:24 ;
assume x "/\" y <= l ~ ; ::_thesis: ( x <= l ~ or y <= l ~ )
then l <= (~ x) "\/" (~ y) by A4, YELLOW_7:2;
then ( l <= ~ x or l <= ~ y ) by A3;
hence ( x <= l ~ or y <= l ~ ) by YELLOW_7:2; ::_thesis: verum
end;
theorem Th15: :: WAYBEL14:15
for P being non empty complete Poset
for V being non empty Subset of P holds downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }
proof
let P be non empty complete Poset; ::_thesis: for V being non empty Subset of P holds downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }
let V be non empty Subset of P; ::_thesis: downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }
set F = { (downarrow u) where u is Element of P : u in V } ;
consider u being set such that
A1: u in V by XBOOLE_0:def_1;
A2: { (downarrow u) where u is Element of P : u in V } c= bool the carrier of P
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (downarrow u) where u is Element of P : u in V } or X in bool the carrier of P )
assume X in { (downarrow u) where u is Element of P : u in V } ; ::_thesis: X in bool the carrier of P
then ex u being Element of P st
( X = downarrow u & u in V ) ;
hence X in bool the carrier of P ; ::_thesis: verum
end;
reconsider u = u as Element of P by A1;
A3: downarrow u in { (downarrow u) where u is Element of P : u in V } by A1;
reconsider F = { (downarrow u) where u is Element of P : u in V } as Subset-Family of P by A2;
reconsider F = F as Subset-Family of P ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_downarrow_(inf_V)_implies_x_in_meet_F_)_&_(_x_in_meet_F_implies_x_in_downarrow_(inf_V)_)_)
let x be set ; ::_thesis: ( ( x in downarrow (inf V) implies x in meet F ) & ( x in meet F implies x in downarrow (inf V) ) )
hereby ::_thesis: ( x in meet F implies x in downarrow (inf V) )
assume A4: x in downarrow (inf V) ; ::_thesis: x in meet F
then reconsider d = x as Element of P ;
A5: d <= inf V by A4, WAYBEL_0:17;
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in F implies x in Y )
assume Y in F ; ::_thesis: x in Y
then consider u being Element of P such that
A6: Y = downarrow u and
A7: u in V ;
inf V is_<=_than V by YELLOW_0:33;
then inf V <= u by A7, LATTICE3:def_8;
then d <= u by A5, ORDERS_2:3;
hence x in Y by A6, WAYBEL_0:17; ::_thesis: verum
end;
hence x in meet F by A3, SETFAM_1:def_1; ::_thesis: verum
end;
assume A8: x in meet F ; ::_thesis: x in downarrow (inf V)
then reconsider d = x as Element of P ;
now__::_thesis:_for_b_being_Element_of_P_st_b_in_V_holds_
d_<=_b
let b be Element of P; ::_thesis: ( b in V implies d <= b )
assume b in V ; ::_thesis: d <= b
then downarrow b in F ;
then d in downarrow b by A8, SETFAM_1:def_1;
hence d <= b by WAYBEL_0:17; ::_thesis: verum
end;
then d is_<=_than V by LATTICE3:def_8;
then d <= inf V by YELLOW_0:33;
hence x in downarrow (inf V) by WAYBEL_0:17; ::_thesis: verum
end;
hence downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V } by TARSKI:1; ::_thesis: verum
end;
theorem :: WAYBEL14:16
for P being non empty complete Poset
for V being non empty Subset of P holds uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }
proof
let P be non empty complete Poset; ::_thesis: for V being non empty Subset of P holds uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }
let V be non empty Subset of P; ::_thesis: uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }
set F = { (uparrow u) where u is Element of P : u in V } ;
consider u being set such that
A1: u in V by XBOOLE_0:def_1;
A2: { (uparrow u) where u is Element of P : u in V } c= bool the carrier of P
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (uparrow u) where u is Element of P : u in V } or X in bool the carrier of P )
assume X in { (uparrow u) where u is Element of P : u in V } ; ::_thesis: X in bool the carrier of P
then ex u being Element of P st
( X = uparrow u & u in V ) ;
hence X in bool the carrier of P ; ::_thesis: verum
end;
reconsider u = u as Element of P by A1;
A3: uparrow u in { (uparrow u) where u is Element of P : u in V } by A1;
reconsider F = { (uparrow u) where u is Element of P : u in V } as Subset-Family of P by A2;
reconsider F = F as Subset-Family of P ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_uparrow_(sup_V)_implies_x_in_meet_F_)_&_(_x_in_meet_F_implies_x_in_uparrow_(sup_V)_)_)
let x be set ; ::_thesis: ( ( x in uparrow (sup V) implies x in meet F ) & ( x in meet F implies x in uparrow (sup V) ) )
hereby ::_thesis: ( x in meet F implies x in uparrow (sup V) )
assume A4: x in uparrow (sup V) ; ::_thesis: x in meet F
then reconsider d = x as Element of P ;
A5: d >= sup V by A4, WAYBEL_0:18;
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in F implies x in Y )
assume Y in F ; ::_thesis: x in Y
then consider u being Element of P such that
A6: Y = uparrow u and
A7: u in V ;
sup V is_>=_than V by YELLOW_0:32;
then sup V >= u by A7, LATTICE3:def_9;
then d >= u by A5, ORDERS_2:3;
hence x in Y by A6, WAYBEL_0:18; ::_thesis: verum
end;
hence x in meet F by A3, SETFAM_1:def_1; ::_thesis: verum
end;
assume A8: x in meet F ; ::_thesis: x in uparrow (sup V)
then reconsider d = x as Element of P ;
now__::_thesis:_for_b_being_Element_of_P_st_b_in_V_holds_
d_>=_b
let b be Element of P; ::_thesis: ( b in V implies d >= b )
assume b in V ; ::_thesis: d >= b
then uparrow b in F ;
then d in uparrow b by A8, SETFAM_1:def_1;
hence d >= b by WAYBEL_0:18; ::_thesis: verum
end;
then d is_>=_than V by LATTICE3:def_9;
then d >= sup V by YELLOW_0:32;
hence x in uparrow (sup V) by WAYBEL_0:18; ::_thesis: verum
end;
hence uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V } by TARSKI:1; ::_thesis: verum
end;
registration
let L be sup-Semilattice;
let x be Element of L;
cluster compactbelow x -> directed ;
coherence
compactbelow x is directed
proof
set cX = compactbelow x;
let xx, yy be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not xx in compactbelow x or not yy in compactbelow x or ex b1 being Element of the carrier of L st
( b1 in compactbelow x & xx <= b1 & yy <= b1 ) )
assume that
A1: xx in compactbelow x and
A2: yy in compactbelow x ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in compactbelow x & xx <= b1 & yy <= b1 )
set z = xx "\/" yy;
yy is compact by A2, WAYBEL_8:4;
then ( yy <= xx "\/" yy & yy << yy ) by WAYBEL_3:def_2, YELLOW_0:22;
then A3: yy << xx "\/" yy by WAYBEL_3:2;
xx is compact by A1, WAYBEL_8:4;
then ( xx <= xx "\/" yy & xx << xx ) by WAYBEL_3:def_2, YELLOW_0:22;
then xx << xx "\/" yy by WAYBEL_3:2;
then xx "\/" yy << xx "\/" yy by A3, WAYBEL_3:3;
then A4: xx "\/" yy is compact by WAYBEL_3:def_2;
take xx "\/" yy ; ::_thesis: ( xx "\/" yy in compactbelow x & xx <= xx "\/" yy & yy <= xx "\/" yy )
( xx <= x & yy <= x ) by A1, A2, WAYBEL_8:4;
then xx "\/" yy <= x by YELLOW_0:22;
hence xx "\/" yy in compactbelow x by A4; ::_thesis: ( xx <= xx "\/" yy & yy <= xx "\/" yy )
thus ( xx <= xx "\/" yy & yy <= xx "\/" yy ) by YELLOW_0:22; ::_thesis: verum
end;
end;
theorem Th17: :: WAYBEL14:17
for T being non empty TopSpace
for S being irreducible Subset of T
for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
proof
let T be non empty TopSpace; ::_thesis: for S being irreducible Subset of T
for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
let S be irreducible Subset of T; ::_thesis: for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
let V be Element of (InclPoset the topology of T); ::_thesis: ( V = S ` implies V is prime )
assume A1: V = S ` ; ::_thesis: V is prime
set sL = the topology of T;
let X, Y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def_6 ::_thesis: ( not X "/\" Y <= V or X <= V or Y <= V )
A2: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then ( X in the topology of T & Y in the topology of T ) ;
then reconsider X9 = X, Y9 = Y as Subset of T ;
X9 /\ Y9 in the topology of T by A2, PRE_TOPC:def_1;
then A3: X /\ Y = X "/\" Y by YELLOW_1:9;
assume X "/\" Y <= V ; ::_thesis: ( X <= V or Y <= V )
then X /\ Y c= V by A3, YELLOW_1:3;
then S c= (X9 /\ Y9) ` by A1, Lm1;
then S c= (X9 `) \/ (Y9 `) by XBOOLE_1:54;
then S = ((X9 `) \/ (Y9 `)) /\ S by XBOOLE_1:28;
then A4: S = ((X9 `) /\ S) \/ ((Y9 `) /\ S) by XBOOLE_1:23;
A5: S is closed by YELLOW_8:def_3;
Y9 is open by A2, PRE_TOPC:def_2;
then Y9 ` is closed ;
then A6: (Y9 `) /\ S is closed by A5;
X9 is open by A2, PRE_TOPC:def_2;
then X9 ` is closed ;
then (X9 `) /\ S is closed by A5;
then ( S = (X9 `) /\ S or S = (Y9 `) /\ S ) by A6, A4, YELLOW_8:def_3;
then ( S c= X9 ` or S c= Y9 ` ) by XBOOLE_1:17;
then ( X c= V or Y c= V ) by A1, Lm1;
hence ( X <= V or Y <= V ) by YELLOW_1:3; ::_thesis: verum
end;
theorem Th18: :: WAYBEL14:18
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
proof
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x "\/" y = x \/ y & x "/\" y = x /\ y )
A1: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then ( x in the topology of T & y in the topology of T ) ;
then reconsider x9 = x, y9 = y as Subset of T ;
( x9 is open & y9 is open ) by A1, PRE_TOPC:def_2;
then x9 \/ y9 is open ;
then x9 \/ y9 in the topology of T by PRE_TOPC:def_2;
hence x "\/" y = x \/ y by YELLOW_1:8; ::_thesis: x "/\" y = x /\ y
x9 /\ y9 in the topology of T by A1, PRE_TOPC:def_1;
hence x "/\" y = x /\ y by YELLOW_1:9; ::_thesis: verum
end;
theorem Th19: :: WAYBEL14:19
for T being non empty TopSpace
for V being Element of (InclPoset the topology of T) holds
( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) )
proof
let T be non empty TopSpace; ::_thesis: for V being Element of (InclPoset the topology of T) holds
( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) )
let V be Element of (InclPoset the topology of T); ::_thesis: ( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) )
hereby ::_thesis: ( ( for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) ) implies V is prime )
assume A1: V is prime ; ::_thesis: for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V )
let X, Y be Element of (InclPoset the topology of T); ::_thesis: ( not X /\ Y c= V or X c= V or Y c= V )
assume A2: X /\ Y c= V ; ::_thesis: ( X c= V or Y c= V )
X /\ Y = X "/\" Y by Th18;
then X "/\" Y <= V by A2, YELLOW_1:3;
then ( X <= V or Y <= V ) by A1, WAYBEL_6:def_6;
hence ( X c= V or Y c= V ) by YELLOW_1:3; ::_thesis: verum
end;
assume A3: for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) ; ::_thesis: V is prime
let X, Y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def_6 ::_thesis: ( not X "/\" Y <= V or X <= V or Y <= V )
assume A4: X "/\" Y <= V ; ::_thesis: ( X <= V or Y <= V )
X /\ Y = X "/\" Y by Th18;
then X /\ Y c= V by A4, YELLOW_1:3;
then ( X c= V or Y c= V ) by A3;
hence ( X <= V or Y <= V ) by YELLOW_1:3; ::_thesis: verum
end;
theorem :: WAYBEL14:20
for T being non empty TopSpace
for V being Element of (InclPoset the topology of T) holds
( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )
proof
let T be non empty TopSpace; ::_thesis: for V being Element of (InclPoset the topology of T) holds
( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )
let V be Element of (InclPoset the topology of T); ::_thesis: ( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )
hereby ::_thesis: ( ( for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) ) implies V is co-prime )
assume A1: V is co-prime ; ::_thesis: for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y )
let X, Y be Element of (InclPoset the topology of T); ::_thesis: ( not V c= X \/ Y or V c= X or V c= Y )
assume A2: V c= X \/ Y ; ::_thesis: ( V c= X or V c= Y )
X \/ Y = X "\/" Y by Th18;
then V <= X "\/" Y by A2, YELLOW_1:3;
then ( V <= X or V <= Y ) by A1, Th14;
hence ( V c= X or V c= Y ) by YELLOW_1:3; ::_thesis: verum
end;
assume A3: for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) ; ::_thesis: V is co-prime
now__::_thesis:_for_X,_Y_being_Element_of_(InclPoset_the_topology_of_T)_holds_
(_not_V_<=_X_"\/"_Y_or_V_<=_X_or_V_<=_Y_)
let X, Y be Element of (InclPoset the topology of T); ::_thesis: ( not V <= X "\/" Y or V <= X or V <= Y )
assume A4: V <= X "\/" Y ; ::_thesis: ( V <= X or V <= Y )
X \/ Y = X "\/" Y by Th18;
then V c= X \/ Y by A4, YELLOW_1:3;
then ( V c= X or V c= Y ) by A3;
hence ( V <= X or V <= Y ) by YELLOW_1:3; ::_thesis: verum
end;
hence V is co-prime by Th14; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster InclPoset the topology of T -> distributive ;
coherence
InclPoset the topology of T is distributive
proof
let x, y, z be Element of (InclPoset the topology of T); :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = x /\ (y "\/" z) by Th18
.= x /\ (y \/ z) by Th18
.= (x /\ y) \/ (x /\ z) by XBOOLE_1:23
.= (x "/\" y) \/ (x /\ z) by Th18
.= (x "/\" y) \/ (x "/\" z) by Th18
.= (x "/\" y) "\/" (x "/\" z) by Th18 ; ::_thesis: verum
end;
end;
theorem Th21: :: WAYBEL14:21
for T being non empty TopSpace
for L being TopLattice
for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
proof
let T be non empty TopSpace; ::_thesis: for L being TopLattice
for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let L be TopLattice; ::_thesis: for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let t be Point of T; ::_thesis: for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let l be Point of L; ::_thesis: for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let X be Subset-Family of L; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l implies X is Basis of t )
assume A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) ; ::_thesis: ( not t = l or not X is Basis of l or X is Basis of t )
then reconsider X9 = X as Subset-Family of T ;
assume A2: t = l ; ::_thesis: ( not X is Basis of l or X is Basis of t )
assume A3: X is Basis of l ; ::_thesis: X is Basis of t
then A4: X c= the topology of L by TOPS_2:64;
A5: l in Intersect X by A3, YELLOW_8:def_1;
A6: for S being Subset of L st S is open & l in S holds
ex V being Subset of L st
( V in X & V c= S ) by A3, YELLOW_8:def_1;
now__::_thesis:_for_S_being_Subset_of_T_st_S_is_open_&_t_in_S_holds_
ex_V_being_Subset_of_T_st_
(_V_in_X9_&_V_c=_S_)
let S be Subset of T; ::_thesis: ( S is open & t in S implies ex V being Subset of T st
( V in X9 & V c= S ) )
assume that
A7: S is open and
A8: t in S ; ::_thesis: ex V being Subset of T st
( V in X9 & V c= S )
reconsider S9 = S as Subset of L by A1;
S in the topology of T by A7, PRE_TOPC:def_2;
then S9 is open by A1, PRE_TOPC:def_2;
then consider V being Subset of L such that
A9: ( V in X & V c= S9 ) by A2, A6, A8;
reconsider V = V as Subset of T by A1;
take V = V; ::_thesis: ( V in X9 & V c= S )
thus ( V in X9 & V c= S ) by A9; ::_thesis: verum
end;
hence X is Basis of t by A1, A2, A4, A5, TOPS_2:64, YELLOW_8:def_1; ::_thesis: verum
end;
theorem Th22: :: WAYBEL14:22
for L being TopLattice
for x being Element of L st ( for X being Subset of L st X is open holds
X is upper ) holds
uparrow x is compact
proof
let L be TopLattice; ::_thesis: for x being Element of L st ( for X being Subset of L st X is open holds
X is upper ) holds
uparrow x is compact
let x be Element of L; ::_thesis: ( ( for X being Subset of L st X is open holds
X is upper ) implies uparrow x is compact )
assume A1: for X being Subset of L st X is open holds
X is upper ; ::_thesis: uparrow x is compact
set P = uparrow x;
let F be Subset-Family of L; :: according to COMPTS_1:def_4 ::_thesis: ( not F is Cover of uparrow x or not F is open or ex b1 being Element of bool (bool the carrier of L) st
( b1 c= F & b1 is Cover of uparrow x & b1 is finite ) )
assume that
A2: F is Cover of uparrow x and
A3: F is open ; ::_thesis: ex b1 being Element of bool (bool the carrier of L) st
( b1 c= F & b1 is Cover of uparrow x & b1 is finite )
x <= x ;
then A4: x in uparrow x by WAYBEL_0:18;
uparrow x c= union F by A2, SETFAM_1:def_11;
then consider Y being set such that
A5: x in Y and
A6: Y in F by A4, TARSKI:def_4;
reconsider Y = Y as Subset of L by A6;
reconsider G = {Y} as Subset-Family of L ;
reconsider G = G as Subset-Family of L ;
take G ; ::_thesis: ( G c= F & G is Cover of uparrow x & G is finite )
thus G c= F by A6, ZFMISC_1:31; ::_thesis: ( G is Cover of uparrow x & G is finite )
Y is open by A3, A6, TOPS_2:def_1;
then Y is upper by A1;
then uparrow x c= Y by A5, WAYBEL11:42;
hence uparrow x c= union G by ZFMISC_1:25; :: according to SETFAM_1:def_11 ::_thesis: G is finite
thus G is finite ; ::_thesis: verum
end;
begin
registration
let L be complete LATTICE;
cluster sigma L -> non empty ;
coherence
not sigma L is empty
proof
sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def_12;
hence not sigma L is empty ; ::_thesis: verum
end;
end;
theorem Th23: :: WAYBEL14:23
for L being complete Scott TopLattice holds sigma L = the topology of L
proof
let L be complete Scott TopLattice; ::_thesis: sigma L = the topology of L
TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
hence sigma L = the topology of L by WAYBEL11:def_12; ::_thesis: verum
end;
theorem Th24: :: WAYBEL14:24
for L being complete Scott TopLattice
for X being Subset of L holds
( X in sigma L iff X is open )
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L holds
( X in sigma L iff X is open )
let X be Subset of L; ::_thesis: ( X in sigma L iff X is open )
sigma L = the topology of L by Th23;
hence ( X in sigma L iff X is open ) by PRE_TOPC:def_2; ::_thesis: verum
end;
Lm2: for L being complete Scott TopLattice
for V being filtered Subset of L
for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
proof
let L be complete Scott TopLattice; ::_thesis: for V being filtered Subset of L
for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
let V be filtered Subset of L; ::_thesis: for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
let F be Subset-Family of L; ::_thesis: for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
let CF be Subset of (InclPoset (sigma L)); ::_thesis: ( F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F implies CF is directed )
assume that
A1: F = { (downarrow u) where u is Element of L : u in V } and
A2: CF = COMPLEMENT F ; ::_thesis: CF is directed
set IPs = InclPoset (sigma L);
let x, y be Element of (InclPoset (sigma L)); :: according to WAYBEL_0:def_1 ::_thesis: ( not x in CF or not y in CF or ex b1 being Element of the carrier of (InclPoset (sigma L)) st
( b1 in CF & x <= b1 & y <= b1 ) )
assume that
A3: x in CF and
A4: y in CF ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (sigma L)) st
( b1 in CF & x <= b1 & y <= b1 )
A5: sigma L = the topology of L by Th23;
then A6: the carrier of (InclPoset (sigma L)) = the topology of L by YELLOW_1:1;
then ( x in sigma L & y in sigma L ) by A5;
then reconsider x9 = x, y9 = y as Subset of L ;
x9 ` in F by A2, A3, SETFAM_1:def_7;
then consider ux being Element of L such that
A7: x9 ` = downarrow ux and
A8: ux in V by A1;
y9 ` in F by A2, A4, SETFAM_1:def_7;
then consider uy being Element of L such that
A9: y9 ` = downarrow uy and
A10: uy in V by A1;
consider uz being Element of L such that
A11: uz in V and
A12: uz <= ux and
A13: uz <= uy by A8, A10, WAYBEL_0:def_2;
(downarrow uz) ` is open by WAYBEL11:12;
then reconsider z = (downarrow uz) ` as Element of (InclPoset (sigma L)) by A6, PRE_TOPC:def_2;
take z ; ::_thesis: ( z in CF & x <= z & y <= z )
downarrow uz in F by A1, A11;
hence z in CF by A2, YELLOW_8:5; ::_thesis: ( x <= z & y <= z )
downarrow uz c= downarrow uy by A13, WAYBEL_0:21;
then A14: (downarrow uy) ` c= (downarrow uz) ` by SUBSET_1:12;
downarrow uz c= downarrow ux by A12, WAYBEL_0:21;
then (downarrow ux) ` c= (downarrow uz) ` by SUBSET_1:12;
hence ( x <= z & y <= z ) by A7, A9, A14, YELLOW_1:3; ::_thesis: verum
end;
theorem Th25: :: WAYBEL14:25
for L being complete Scott TopLattice
for VV being Subset of (InclPoset (sigma L))
for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds
VV is directed
proof
let L be complete Scott TopLattice; ::_thesis: for VV being Subset of (InclPoset (sigma L))
for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds
VV is directed
let VV be Subset of (InclPoset (sigma L)); ::_thesis: for X being filtered Subset of L st VV = { ((downarrow x) `) where x is Element of L : x in X } holds
VV is directed
let V be filtered Subset of L; ::_thesis: ( VV = { ((downarrow x) `) where x is Element of L : x in V } implies VV is directed )
set F = { (downarrow u) where u is Element of L : u in V } ;
{ (downarrow u) where u is Element of L : u in V } c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (downarrow u) where u is Element of L : u in V } or x in bool the carrier of L )
assume x in { (downarrow u) where u is Element of L : u in V } ; ::_thesis: x in bool the carrier of L
then ex u being Element of L st
( x = downarrow u & u in V ) ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider F = { (downarrow u) where u is Element of L : u in V } as Subset-Family of L ;
reconsider F = F as Subset-Family of L ;
assume A1: VV = { ((downarrow x) `) where x is Element of L : x in V } ; ::_thesis: VV is directed
VV c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VV or x in bool the carrier of L )
assume x in VV ; ::_thesis: x in bool the carrier of L
then ex u being Element of L st
( x = (downarrow u) ` & u in V ) by A1;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider VV = VV as Subset-Family of L ;
reconsider VV = VV as Subset-Family of L ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_VV_implies_x_in_COMPLEMENT_F_)_&_(_x_in_COMPLEMENT_F_implies_x_in_VV_)_)
let x be set ; ::_thesis: ( ( x in VV implies x in COMPLEMENT F ) & ( x in COMPLEMENT F implies x in VV ) )
hereby ::_thesis: ( x in COMPLEMENT F implies x in VV )
assume x in VV ; ::_thesis: x in COMPLEMENT F
then consider u being Element of L such that
A2: x = (downarrow u) ` and
A3: u in V by A1;
downarrow u in F by A3;
hence x in COMPLEMENT F by A2, YELLOW_8:5; ::_thesis: verum
end;
assume A4: x in COMPLEMENT F ; ::_thesis: x in VV
then reconsider X = x as Subset of L ;
X ` in F by A4, SETFAM_1:def_7;
then consider u being Element of L such that
A5: X ` = downarrow u and
A6: u in V ;
X = (downarrow u) ` by A5;
hence x in VV by A1, A6; ::_thesis: verum
end;
then VV = COMPLEMENT F by TARSKI:1;
hence VV is directed by Lm2; ::_thesis: verum
end;
theorem Th26: :: WAYBEL14:26
for L being complete Scott TopLattice
for x being Element of L
for X being Subset of L st X is open & x in X holds
inf X << x
proof
let L be complete Scott TopLattice; ::_thesis: for x being Element of L
for X being Subset of L st X is open & x in X holds
inf X << x
let x be Element of L; ::_thesis: for X being Subset of L st X is open & x in X holds
inf X << x
let X be Subset of L; ::_thesis: ( X is open & x in X implies inf X << x )
assume that
A1: X is open and
A2: x in X ; ::_thesis: inf X << x
A3: ( X is upper & X is property(S) ) by A1, WAYBEL11:15;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_L_st_x_<=_sup_D_holds_
ex_y_being_Element_of_L_st_
(_y_in_D_&_inf_X_<=_y_)
let D be non empty directed Subset of L; ::_thesis: ( x <= sup D implies ex y being Element of L st
( y in D & inf X <= y ) )
assume x <= sup D ; ::_thesis: ex y being Element of L st
( y in D & inf X <= y )
then sup D in X by A2, A3, WAYBEL_0:def_20;
then consider y being Element of L such that
A4: y in D and
A5: for x being Element of L st x in D & x >= y holds
x in X by A3, WAYBEL11:def_3;
take y = y; ::_thesis: ( y in D & inf X <= y )
thus y in D by A4; ::_thesis: inf X <= y
y <= y ;
then ( inf X is_<=_than X & y in X ) by A4, A5, YELLOW_0:33;
hence inf X <= y by LATTICE3:def_8; ::_thesis: verum
end;
hence inf X << x by WAYBEL_3:def_1; ::_thesis: verum
end;
definition
let R be non empty reflexive RelStr ;
let f be Function of [:R,R:],R;
attrf is jointly_Scott-continuous means :Def1: :: WAYBEL14:def 1
for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds
ex ft being Function of [:T,T:],T st
( ft = f & ft is continuous );
end;
:: deftheorem Def1 defines jointly_Scott-continuous WAYBEL14:def_1_:_
for R being non empty reflexive RelStr
for f being Function of [:R,R:],R holds
( f is jointly_Scott-continuous iff for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds
ex ft being Function of [:T,T:],T st
( ft = f & ft is continuous ) );
theorem Th27: :: WAYBEL14:27
for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
let X be Subset of L; ::_thesis: for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
let V be Element of (InclPoset (sigma L)); ::_thesis: ( V = X implies ( V is co-prime iff ( X is filtered & X is upper ) ) )
assume A1: V = X ; ::_thesis: ( V is co-prime iff ( X is filtered & X is upper ) )
A2: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
A3: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def_12;
A4: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
then A5: X is upper by A1, A3, WAYBEL11:31;
hereby ::_thesis: ( X is filtered & X is upper implies V is co-prime )
assume A6: V is co-prime ; ::_thesis: ( X is filtered & X is upper )
thus X is filtered ::_thesis: X is upper
proof
let v, w be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not v in X or not w in X or ex b1 being Element of the carrier of L st
( b1 in X & b1 <= v & b1 <= w ) )
assume that
A7: v in X and
A8: w in X ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in X & b1 <= v & b1 <= w )
( (downarrow w) ` is open & (downarrow v) ` is open ) by WAYBEL11:12;
then reconsider mdw = (downarrow w) ` , mdv = (downarrow v) ` as Element of (InclPoset (sigma L)) by A3, A4, A2, PRE_TOPC:def_2;
w <= w ;
then w in downarrow w by WAYBEL_0:17;
then not V c= (downarrow w) ` by A1, A8, XBOOLE_0:def_5;
then A9: not V <= mdw by YELLOW_1:3;
v <= v ;
then v in downarrow v by WAYBEL_0:17;
then not V c= (downarrow v) ` by A1, A7, XBOOLE_0:def_5;
then not V <= mdv by YELLOW_1:3;
then not V <= mdv "\/" mdw by A3, A6, A9, Th14;
then A10: not V c= mdv "\/" mdw by YELLOW_1:3;
take z = v "/\" w; ::_thesis: ( z in X & z <= v & z <= w )
A11: mdv \/ mdw = ((downarrow v) /\ (downarrow w)) ` by XBOOLE_1:54
.= (downarrow (v "/\" w)) ` by Th3 ;
mdv \/ mdw c= mdv "\/" mdw by A3, YELLOW_1:6;
then not V c= mdv \/ mdw by A10, XBOOLE_1:1;
then X meets ((downarrow (v "/\" w)) `) ` by A1, A11, SUBSET_1:24;
then X /\ (((downarrow (v "/\" w)) `) `) <> {} by XBOOLE_0:def_7;
then consider zz being set such that
A12: zz in X /\ (downarrow (v "/\" w)) by XBOOLE_0:def_1;
A13: zz in downarrow (v "/\" w) by A12, XBOOLE_0:def_4;
A14: zz in X by A12, XBOOLE_0:def_4;
reconsider zz = zz as Element of L by A12;
zz <= v "/\" w by A13, WAYBEL_0:17;
hence z in X by A5, A14, WAYBEL_0:def_20; ::_thesis: ( z <= v & z <= w )
thus ( z <= v & z <= w ) by YELLOW_0:23; ::_thesis: verum
end;
thus X is upper by A1, A3, A4, WAYBEL11:31; ::_thesis: verum
end;
assume A15: ( X is filtered & X is upper ) ; ::_thesis: V is co-prime
assume not V is co-prime ; ::_thesis: contradiction
then consider Xx, Y being Element of (InclPoset (sigma L)) such that
A16: V <= Xx "\/" Y and
A17: not V <= Xx and
A18: not V <= Y by A3, Th14;
( Xx in sigma L & Y in sigma L ) by A4;
then reconsider Xx9 = Xx, Y9 = Y as Subset of L ;
A19: Y9 is open by A3, A4, A2, PRE_TOPC:def_2;
then A20: Y9 is upper by WAYBEL11:def_4;
A21: Xx9 is open by A3, A4, A2, PRE_TOPC:def_2;
then Xx9 \/ Y9 is open by A19;
then Xx \/ Y in sigma L by A3, A2, PRE_TOPC:def_2;
then Xx \/ Y = Xx "\/" Y by YELLOW_1:8;
then A22: V c= Xx \/ Y by A16, YELLOW_1:3;
not V c= Y by A18, YELLOW_1:3;
then consider w being set such that
A23: w in V and
A24: not w in Y by TARSKI:def_3;
not V c= Xx by A17, YELLOW_1:3;
then consider v being set such that
A25: v in V and
A26: not v in Xx by TARSKI:def_3;
reconsider v = v, w = w as Element of L by A1, A25, A23;
A27: Xx9 is upper by A21, WAYBEL11:def_4;
A28: now__::_thesis:_not_v_"/\"_w_in_Xx9_\/_Y9
assume A29: v "/\" w in Xx9 \/ Y9 ; ::_thesis: contradiction
percases ( v "/\" w in Xx9 or v "/\" w in Y9 ) by A29, XBOOLE_0:def_3;
supposeA30: v "/\" w in Xx9 ; ::_thesis: contradiction
v "/\" w <= v by YELLOW_0:23;
hence contradiction by A26, A27, A30, WAYBEL_0:def_20; ::_thesis: verum
end;
supposeA31: v "/\" w in Y9 ; ::_thesis: contradiction
v "/\" w <= w by YELLOW_0:23;
hence contradiction by A24, A20, A31, WAYBEL_0:def_20; ::_thesis: verum
end;
end;
end;
v "/\" w in X by A1, A15, A25, A23, WAYBEL_0:41;
hence contradiction by A1, A22, A28; ::_thesis: verum
end;
theorem :: WAYBEL14:28
for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds
( V is prime & V <> the carrier of L )
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds
( V is prime & V <> the carrier of L )
let X be Subset of L; ::_thesis: for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds
( V is prime & V <> the carrier of L )
let V be Element of (InclPoset (sigma L)); ::_thesis: ( V = X & ex x being Element of L st X = (downarrow x) ` implies ( V is prime & V <> the carrier of L ) )
assume A1: V = X ; ::_thesis: ( for x being Element of L holds not X = (downarrow x) ` or ( V is prime & V <> the carrier of L ) )
A2: ( sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) & TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) ) by WAYBEL11:32, WAYBEL11:def_12;
given u being Element of L such that A3: X = (downarrow u) ` ; ::_thesis: ( V is prime & V <> the carrier of L )
( Cl {u} = downarrow u & Cl {u} is irreducible ) by WAYBEL11:9, YELLOW_8:17;
hence V is prime by A1, A2, A3, Th17; ::_thesis: V <> the carrier of L
assume V = the carrier of L ; ::_thesis: contradiction
hence contradiction by A1, A3, Th2; ::_thesis: verum
end;
theorem Th29: :: WAYBEL14:29
for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
let X be Subset of L; ::_thesis: for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
let V be Element of (InclPoset (sigma L)); ::_thesis: ( V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L implies ex x being Element of L st X = (downarrow x) ` )
assume that
A1: V = X and
A2: sup_op L is jointly_Scott-continuous and
A3: V is prime and
A4: V <> the carrier of L ; ::_thesis: ex x being Element of L st X = (downarrow x) `
A5: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
set A = X ` ;
A6: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def_12;
A7: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
then A8: X is open by A1, A6, A5, PRE_TOPC:def_2;
then X ` is closed ;
then A9: ( X ` is directly_closed & X ` is lower ) by WAYBEL11:7;
A10: X ` is directed
proof
set LxL = [:L,L:];
given a, b being Element of L such that A11: ( a in X ` & b in X ` ) and
A12: for z being Element of L holds
( not z in X ` or not a <= z or not b <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: contradiction
( a <= a "\/" b & b <= a "\/" b ) by YELLOW_0:22;
then not a "\/" b in X ` by A12;
then A13: a "\/" b in X by XBOOLE_0:def_5;
consider Tsup being Function of [:L,L:],L such that
A14: Tsup = sup_op L and
A15: Tsup is continuous by A2, A5, Def1;
A16: Tsup . (a,b) = a "\/" b by A14, WAYBEL_2:def_5;
[#] L <> {} ;
then Tsup " X is open by A8, A15, TOPS_2:43;
then consider AA being Subset-Family of [:L,L:] such that
A17: Tsup " X = union AA and
A18: for e being set st e in AA holds
ex X1, Y1 being Subset of L st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
A19: the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by BORSUK_1:def_2;
then [a,b] in the carrier of [:L,L:] by ZFMISC_1:def_2;
then [a,b] in Tsup " X by A13, A16, FUNCT_2:38;
then consider AAe being set such that
A20: [a,b] in AAe and
A21: AAe in AA by A17, TARSKI:def_4;
consider Va, Vb being Subset of L such that
A22: AAe = [:Va,Vb:] and
A23: Va is open and
A24: Vb is open by A18, A21;
A25: ( a in Va & b in Vb ) by A20, A22, ZFMISC_1:87;
reconsider Va9 = Va, Vb9 = Vb as Subset of L ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Tsup_.:_AAe_implies_x_in_Va_/\_Vb_)_&_(_x_in_Va_/\_Vb_implies_x_in_Tsup_.:_AAe_)_)
let x be set ; ::_thesis: ( ( x in Tsup .: AAe implies x in Va /\ Vb ) & ( x in Va /\ Vb implies x in Tsup .: AAe ) )
hereby ::_thesis: ( x in Va /\ Vb implies x in Tsup .: AAe )
assume x in Tsup .: AAe ; ::_thesis: x in Va /\ Vb
then consider cd being set such that
A26: cd in the carrier of [:L,L:] and
A27: cd in AAe and
A28: Tsup . cd = x by FUNCT_2:64;
consider c, d being Element of L such that
A29: cd = [c,d] by A19, A26, DOMAIN_1:1;
reconsider c = c, d = d as Element of L ;
A30: x = Tsup . (c,d) by A28, A29
.= c "\/" d by A14, WAYBEL_2:def_5 ;
A31: ( d <= c "\/" d & Vb9 is upper ) by A24, WAYBEL11:def_4, YELLOW_0:22;
d in Vb by A22, A27, A29, ZFMISC_1:87;
then A32: x in Vb by A30, A31, WAYBEL_0:def_20;
A33: ( c <= c "\/" d & Va9 is upper ) by A23, WAYBEL11:def_4, YELLOW_0:22;
c in Va by A22, A27, A29, ZFMISC_1:87;
then x in Va by A30, A33, WAYBEL_0:def_20;
hence x in Va /\ Vb by A32, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A34: x in Va /\ Vb ; ::_thesis: x in Tsup .: AAe
then reconsider c = x as Element of L ;
( x in Va & x in Vb ) by A34, XBOOLE_0:def_4;
then A35: [c,c] in AAe by A22, ZFMISC_1:87;
c <= c ;
then c = c "\/" c by YELLOW_0:24;
then A36: c = Tsup . (c,c) by A14, WAYBEL_2:def_5;
[c,c] in the carrier of [:L,L:] by A19, ZFMISC_1:87;
hence x in Tsup .: AAe by A35, A36, FUNCT_2:35; ::_thesis: verum
end;
then A37: Tsup .: AAe = Va /\ Vb by TARSKI:1;
A38: Tsup .: (Tsup " X) c= X by FUNCT_1:75;
Tsup .: AAe c= Tsup .: (Tsup " X) by A17, A21, RELAT_1:123, ZFMISC_1:74;
then A39: Tsup .: AAe c= X by A38, XBOOLE_1:1;
( Va in sigma L & Vb in sigma L ) by A6, A5, A23, A24, PRE_TOPC:def_2;
then ( Va c= X or Vb c= X ) by A1, A3, A6, A7, A37, A39, Th19;
hence contradiction by A11, A25, XBOOLE_0:def_5; ::_thesis: verum
end;
take u = sup (X `); ::_thesis: X = (downarrow u) `
now__::_thesis:_not_X_`_=_{}
assume X ` = {} ; ::_thesis: contradiction
then (X `) ` = the carrier of L ;
hence contradiction by A1, A4; ::_thesis: verum
end;
then u in X ` by A9, A10, WAYBEL11:def_2;
then X ` = downarrow u by A9, Th5;
hence X = (downarrow u) ` ; ::_thesis: verum
end;
theorem Th30: :: WAYBEL14:30
for L being complete Scott TopLattice st L is continuous holds
sup_op L is jointly_Scott-continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( L is continuous implies sup_op L is jointly_Scott-continuous )
assume A1: L is continuous ; ::_thesis: sup_op L is jointly_Scott-continuous
set Tsup = sup_op L;
let T be non empty TopSpace; :: according to WAYBEL14:def_1 ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence L) implies ex ft being Function of [:T,T:],T st
( ft = sup_op L & ft is continuous ) )
assume A2: TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence L) ; ::_thesis: ex ft being Function of [:T,T:],T st
( ft = sup_op L & ft is continuous )
A3: the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
A4: the carrier of T = the carrier of L by A2, YELLOW_6:def_24;
then the carrier of [:T,T:] = the carrier of [:L,L:] by A3, YELLOW_3:def_2;
then reconsider Tsup = sup_op L as Function of [:T,T:],T by A4;
take Tsup ; ::_thesis: ( Tsup = sup_op L & Tsup is continuous )
thus Tsup = sup_op L ; ::_thesis: Tsup is continuous
A5: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
for x being Point of [:T,T:] holds Tsup is_continuous_at x
proof
reconsider Lc = L as complete continuous Scott TopLattice by A1;
let ab be Point of [:T,T:]; ::_thesis: Tsup is_continuous_at ab
reconsider Tsab = Tsup . ab as Point of T ;
consider a, b being Point of T such that
A6: ab = [a,b] by A3, DOMAIN_1:1;
reconsider a9 = a, b9 = b as Element of L by A2, YELLOW_6:def_24;
set D1 = waybelow a9;
set D2 = waybelow b9;
set D = (waybelow a9) "\/" (waybelow b9);
reconsider Tsab9 = Tsab as Element of L by A2, YELLOW_6:def_24;
let G be a_neighborhood of Tsup . ab; :: according to TMAP_1:def_2 ::_thesis: ex b1 being a_neighborhood of ab st Tsup .: b1 c= G
A7: Tsab in Int G by CONNSP_2:def_1;
reconsider basab = { (wayabove q) where q is Element of L : q << Tsab9 } as Basis of Tsab9 by A1, WAYBEL11:44;
basab is Basis of Tsab by A2, A5, Th21;
then consider V being Subset of T such that
A8: V in basab and
A9: V c= Int G by A7, YELLOW_8:def_1;
consider u being Element of L such that
A10: V = wayabove u and
A11: u << Tsab9 by A8;
A12: (waybelow a9) "\/" (waybelow b9) = { (x "\/" y) where x, y is Element of L : ( x in waybelow a9 & y in waybelow b9 ) } by YELLOW_4:def_3;
Lc = L ;
then A13: ( a9 = sup (waybelow a9) & b9 = sup (waybelow b9) ) by WAYBEL_3:def_5;
Tsab9 = Tsup . (a,b) by A6
.= a9 "\/" b9 by WAYBEL_2:def_5
.= sup ((waybelow a9) "\/" (waybelow b9)) by A13, WAYBEL_2:4 ;
then consider xy being Element of L such that
A14: xy in (waybelow a9) "\/" (waybelow b9) and
A15: u << xy by A1, A11, WAYBEL_4:53;
consider x, y being Element of L such that
A16: xy = x "\/" y and
A17: x in waybelow a9 and
A18: y in waybelow b9 by A14, A12;
reconsider H = [:(wayabove x),(wayabove y):] as Subset of [:T,T:] by A4, A3, YELLOW_3:def_2;
y << b9 by A18, WAYBEL_3:7;
then A19: b9 in wayabove y ;
Int G c= G by TOPS_1:16;
then A20: V c= G by A9, XBOOLE_1:1;
reconsider wx = wayabove x, wy = wayabove y as Subset of T by A2, YELLOW_6:def_24;
wayabove y is open by A1, WAYBEL11:36;
then wayabove y in the topology of L by PRE_TOPC:def_2;
then A21: wy is open by A2, A5, PRE_TOPC:def_2;
wayabove x is open by A1, WAYBEL11:36;
then wayabove x in the topology of L by PRE_TOPC:def_2;
then wx is open by A2, A5, PRE_TOPC:def_2;
then H is open by A21, BORSUK_1:6;
then A22: H = Int H by TOPS_1:23;
x << a9 by A17, WAYBEL_3:7;
then a9 in wayabove x ;
then [a9,b9] in H by A19, ZFMISC_1:87;
then reconsider H = H as a_neighborhood of ab by A6, A22, CONNSP_2:def_1;
take H ; ::_thesis: Tsup .: H c= G
A23: ( Tsup .: H = (wayabove x) "\/" (wayabove y) & (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) ) by Th12, WAYBEL_2:35;
uparrow (x "\/" y) c= wayabove u by A15, A16, Th7;
then Tsup .: H c= V by A10, A23, XBOOLE_1:1;
hence Tsup .: H c= G by A20, XBOOLE_1:1; ::_thesis: verum
end;
hence Tsup is continuous by TMAP_1:44; ::_thesis: verum
end;
theorem Th31: :: WAYBEL14:31
for L being complete Scott TopLattice st sup_op L is jointly_Scott-continuous holds
L is sober
proof
let L be complete Scott TopLattice; ::_thesis: ( sup_op L is jointly_Scott-continuous implies L is sober )
assume A1: sup_op L is jointly_Scott-continuous ; ::_thesis: L is sober
let S be irreducible Subset of L; :: according to YELLOW_8:def_5 ::_thesis: ex b1 being Element of the carrier of L st
( b1 is_dense_point_of S & ( for b2 being Element of the carrier of L holds
( not b2 is_dense_point_of S or b1 = b2 ) ) )
A2: ( sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) & TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) ) by WAYBEL11:32, WAYBEL11:def_12;
A3: ( not S is empty & S is closed ) by YELLOW_8:def_3;
then ( the carrier of (InclPoset (sigma L)) = sigma L & S ` is open ) by YELLOW_1:1;
then reconsider V = S ` as Element of (InclPoset (sigma L)) by A2, PRE_TOPC:def_2;
S ` <> the carrier of L by Th2;
then consider p being Element of L such that
A4: V = (downarrow p) ` by A1, A2, Th17, Th29;
A5: L is T_0 by WAYBEL11:10;
take p ; ::_thesis: ( p is_dense_point_of S & ( for b1 being Element of the carrier of L holds
( not b1 is_dense_point_of S or p = b1 ) ) )
A6: Cl {p} = downarrow p by WAYBEL11:9;
A7: S = downarrow p by A4, TOPS_1:1;
hence p is_dense_point_of S by A6, YELLOW_8:18; ::_thesis: for b1 being Element of the carrier of L holds
( not b1 is_dense_point_of S or p = b1 )
let q be Point of L; ::_thesis: ( not q is_dense_point_of S or p = q )
assume q is_dense_point_of S ; ::_thesis: p = q
then Cl {q} = S by A3, YELLOW_8:16;
hence p = q by A7, A6, A5, YELLOW_8:23; ::_thesis: verum
end;
theorem :: WAYBEL14:32
for L being complete Scott TopLattice st L is continuous holds
( L is compact & L is locally-compact & L is sober & L is Baire )
proof
let L be complete Scott TopLattice; ::_thesis: ( L is continuous implies ( L is compact & L is locally-compact & L is sober & L is Baire ) )
assume A1: L is continuous ; ::_thesis: ( L is compact & L is locally-compact & L is sober & L is Baire )
A2: ( uparrow (Bottom L) = the carrier of L & [#] L = the carrier of L ) by Th10;
A3: for X being Subset of L st X is open holds
X is upper by WAYBEL11:def_4;
then uparrow (Bottom L) is compact by Th22;
hence L is compact by A2, COMPTS_1:1; ::_thesis: ( L is locally-compact & L is sober & L is Baire )
thus A4: L is locally-compact ::_thesis: ( L is sober & L is Baire )
proof
let x be Point of L; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of bool the carrier of L holds
( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of L st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let X be Subset of L; ::_thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume that
A5: x in X and
A6: X is open ; ::_thesis: ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact )
reconsider x9 = x as Element of L ;
consider y being Element of L such that
A7: y << x9 and
A8: y in X by A1, A5, A6, WAYBEL11:43;
set Y = uparrow y;
set bas = { (wayabove q) where q is Element of L : q << x9 } ;
A9: { (wayabove q) where q is Element of L : q << x9 } is Basis of x by A1, WAYBEL11:44;
wayabove y in { (wayabove q) where q is Element of L : q << x9 } by A7;
then wayabove y is open by A9, YELLOW_8:12;
then A10: wayabove y c= Int (uparrow y) by TOPS_1:24, WAYBEL_3:11;
take uparrow y ; ::_thesis: ( x in Int (uparrow y) & uparrow y c= X & uparrow y is compact )
x in wayabove y by A7;
hence x in Int (uparrow y) by A10; ::_thesis: ( uparrow y c= X & uparrow y is compact )
X is upper by A6, WAYBEL11:def_4;
hence uparrow y c= X by A8, WAYBEL11:42; ::_thesis: uparrow y is compact
thus uparrow y is compact by A3, Th22; ::_thesis: verum
end;
sup_op L is jointly_Scott-continuous by A1, Th30;
hence L is sober by Th31; ::_thesis: L is Baire
hence L is Baire by A4, WAYBEL12:44; ::_thesis: verum
end;
theorem Th33: :: WAYBEL14:33
for L being complete Scott TopLattice
for X being Subset of L st L is continuous & X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X }
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L st L is continuous & X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X }
let X be Subset of L; ::_thesis: ( L is continuous & X in sigma L implies X = union { (wayabove x) where x is Element of L : x in X } )
assume that
A1: L is continuous and
A2: X in sigma L ; ::_thesis: X = union { (wayabove x) where x is Element of L : x in X }
set WAV = { (wayabove x) where x is Element of L : x in X } ;
A3: X is open by A2, Th24;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_X_implies_x_in_union__{__(wayabove_x)_where_x_is_Element_of_L_:_x_in_X__}__)_&_(_x_in_union__{__(wayabove_x)_where_x_is_Element_of_L_:_x_in_X__}__implies_x_in_X_)_)
let x be set ; ::_thesis: ( ( x in X implies x in union { (wayabove x) where x is Element of L : x in X } ) & ( x in union { (wayabove x) where x is Element of L : x in X } implies x in X ) )
hereby ::_thesis: ( x in union { (wayabove x) where x is Element of L : x in X } implies x in X )
assume A4: x in X ; ::_thesis: x in union { (wayabove x) where x is Element of L : x in X }
then reconsider x9 = x as Element of L ;
consider q being Element of L such that
A5: ( q << x9 & q in X ) by A1, A3, A4, WAYBEL11:43;
( x9 in wayabove q & wayabove q in { (wayabove x) where x is Element of L : x in X } ) by A5;
hence x in union { (wayabove x) where x is Element of L : x in X } by TARSKI:def_4; ::_thesis: verum
end;
assume x in union { (wayabove x) where x is Element of L : x in X } ; ::_thesis: x in X
then consider Y being set such that
A6: x in Y and
A7: Y in { (wayabove x) where x is Element of L : x in X } by TARSKI:def_4;
consider q being Element of L such that
A8: Y = wayabove q and
A9: q in X by A7;
A10: wayabove q c= uparrow q by WAYBEL_3:11;
X is upper by A3, WAYBEL11:def_4;
then uparrow q c= X by A9, WAYBEL11:42;
then Y c= X by A8, A10, XBOOLE_1:1;
hence x in X by A6; ::_thesis: verum
end;
hence X = union { (wayabove x) where x is Element of L : x in X } by TARSKI:1; ::_thesis: verum
end;
theorem :: WAYBEL14:34
for L being complete Scott TopLattice st ( for X being Subset of L st X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X } ) holds
L is continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( ( for X being Subset of L st X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X } ) implies L is continuous )
assume A1: for X being Subset of L st X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X } ; ::_thesis: L is continuous
thus for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( L is up-complete & L is satisfying_axiom_of_approximation )
thus L is up-complete ; ::_thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),L)
set y = sup (waybelow x);
set X = (downarrow (sup (waybelow x))) ` ;
assume A2: x <> sup (waybelow x) ; ::_thesis: contradiction
A3: sup (waybelow x) <= x by Th9;
now__::_thesis:_not_x_in_downarrow_(sup_(waybelow_x))
assume x in downarrow (sup (waybelow x)) ; ::_thesis: contradiction
then x <= sup (waybelow x) by WAYBEL_0:17;
hence contradiction by A3, A2, ORDERS_2:2; ::_thesis: verum
end;
then A4: x in (downarrow (sup (waybelow x))) ` by XBOOLE_0:def_5;
set Z = { (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) ` } ;
A5: sup (waybelow x) is_>=_than waybelow x by YELLOW_0:32;
(downarrow (sup (waybelow x))) ` is open by WAYBEL11:12;
then (downarrow (sup (waybelow x))) ` in sigma L by Th24;
then (downarrow (sup (waybelow x))) ` = union { (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) ` } by A1;
then consider Y being set such that
A6: x in Y and
A7: Y in { (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) ` } by A4, TARSKI:def_4;
consider z being Element of L such that
A8: Y = wayabove z and
A9: z in (downarrow (sup (waybelow x))) ` by A7;
z << x by A6, A8, WAYBEL_3:8;
then z in waybelow x ;
then z <= sup (waybelow x) by A5, LATTICE3:def_9;
then z in downarrow (sup (waybelow x)) by WAYBEL_0:17;
hence contradiction by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: WAYBEL14:35
for L being complete Scott TopLattice
for x being Element of L st L is continuous holds
ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
proof
let L be complete Scott TopLattice; ::_thesis: for x being Element of L st L is continuous holds
ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
let x be Element of L; ::_thesis: ( L is continuous implies ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) )
set B = { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } ;
{ V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } c= bool the carrier of L
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } or X in bool the carrier of L )
assume X in { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } ; ::_thesis: X in bool the carrier of L
then ex V being Subset of L st
( X = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence X in bool the carrier of L ; ::_thesis: verum
end;
then reconsider B = { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
assume A1: L is continuous ; ::_thesis: ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
then reconsider A = { (wayabove q) where q is Element of L : q << x } as Basis of x by WAYBEL11:44;
A2: B is Basis of x
proof
A3: B is open
proof
let Y be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not Y in B or Y is open )
assume Y in B ; ::_thesis: Y is open
then ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence Y is open ; ::_thesis: verum
end;
B is x -quasi_basis
proof
thus x in Intersect B :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in B & b2 c= b1 ) )
proof
percases ( B is empty or not B is empty ) ;
suppose B is empty ; ::_thesis: x in Intersect B
then Intersect B = the carrier of L by SETFAM_1:def_9;
hence x in Intersect B ; ::_thesis: verum
end;
supposeA4: not B is empty ; ::_thesis: x in Intersect B
A5: now__::_thesis:_for_Y_being_set_st_Y_in_B_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in B implies x in Y )
assume Y in B ; ::_thesis: x in Y
then ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence x in Y ; ::_thesis: verum
end;
Intersect B = meet B by A4, SETFAM_1:def_9;
hence x in Intersect B by A4, A5, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S ) )
assume ( S is open & x in S ) ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S )
then consider V being Subset of L such that
A6: V in A and
A7: V c= S by YELLOW_8:def_1;
consider q being Element of L such that
A8: V = wayabove q and
A9: q << x by A6;
consider F being Open Filter of L such that
A10: x in F and
A11: F c= wayabove q by A1, A9, WAYBEL_6:8;
take F ; ::_thesis: ( F in B & F c= S )
F is open by WAYBEL11:41;
hence F in B by A9, A10, A11; ::_thesis: F c= S
thus F c= S by A7, A8, A11, XBOOLE_1:1; ::_thesis: verum
end;
hence B is Basis of x by A3; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_Subset_of_L_st_Y_in_B_holds_
(_Y_is_open_&_Y_is_filtered_)
let Y be Subset of L; ::_thesis: ( Y in B implies ( Y is open & Y is filtered ) )
assume Y in B ; ::_thesis: ( Y is open & Y is filtered )
then ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence ( Y is open & Y is filtered ) ; ::_thesis: verum
end;
hence ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) by A2; ::_thesis: verum
end;
theorem :: WAYBEL14:36
for L being complete Scott TopLattice st L is continuous holds
InclPoset (sigma L) is continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( L is continuous implies InclPoset (sigma L) is continuous )
assume A1: L is continuous ; ::_thesis: InclPoset (sigma L) is continuous
set IPs = InclPoset the topology of L;
A2: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
InclPoset the topology of L is satisfying_axiom_of_approximation
proof
let V be Element of (InclPoset the topology of L); :: according to WAYBEL_3:def_5 ::_thesis: V = "\/" ((waybelow V),(InclPoset the topology of L))
set VV = { (wayabove x) where x is Element of L : x in V } ;
set wV = waybelow V;
V in sigma L by A3, A2;
then A4: V = union { (wayabove x) where x is Element of L : x in V } by A1, Th33;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_V_implies_x_in_union_(waybelow_V)_)_&_(_x_in_union_(waybelow_V)_implies_x_in_V_)_)
let x be set ; ::_thesis: ( ( x in V implies x in union (waybelow V) ) & ( x in union (waybelow V) implies x in V ) )
hereby ::_thesis: ( x in union (waybelow V) implies x in V )
assume x in V ; ::_thesis: x in union (waybelow V)
then consider xU being set such that
A5: x in xU and
A6: xU in { (wayabove x) where x is Element of L : x in V } by A4, TARSKI:def_4;
consider y being Element of L such that
A7: xU = wayabove y and
A8: y in V by A6;
wayabove y is open by A1, WAYBEL11:36;
then reconsider xU = xU as Element of (InclPoset the topology of L) by A2, A7, PRE_TOPC:def_2;
xU << V
proof
let D be non empty directed Subset of (InclPoset the topology of L); :: according to WAYBEL_3:def_1 ::_thesis: ( not V <= "\/" (D,(InclPoset the topology of L)) or ex b1 being Element of the carrier of (InclPoset the topology of L) st
( b1 in D & xU <= b1 ) )
assume V <= sup D ; ::_thesis: ex b1 being Element of the carrier of (InclPoset the topology of L) st
( b1 in D & xU <= b1 )
then V c= sup D by YELLOW_1:3;
then V c= union D by YELLOW_1:22;
then consider DD being set such that
A9: y in DD and
A10: DD in D by A8, TARSKI:def_4;
DD in sigma L by A3, A2, A10;
then reconsider DD = DD as Subset of L ;
DD is open by A2, A10, PRE_TOPC:def_2;
then DD is upper by WAYBEL11:def_4;
then A11: uparrow y c= DD by A9, WAYBEL11:42;
reconsider d = DD as Element of (InclPoset the topology of L) by A10;
take d ; ::_thesis: ( d in D & xU <= d )
thus d in D by A10; ::_thesis: xU <= d
wayabove y c= uparrow y by WAYBEL_3:11;
then wayabove y c= DD by A11, XBOOLE_1:1;
hence xU <= d by A7, YELLOW_1:3; ::_thesis: verum
end;
then xU in waybelow V ;
hence x in union (waybelow V) by A5, TARSKI:def_4; ::_thesis: verum
end;
assume x in union (waybelow V) ; ::_thesis: x in V
then consider X being set such that
A12: x in X and
A13: X in waybelow V by TARSKI:def_4;
reconsider X = X as Element of (InclPoset the topology of L) by A13;
X << V by A13, WAYBEL_3:7;
then X <= V by WAYBEL_3:1;
then X c= V by YELLOW_1:3;
hence x in V by A12; ::_thesis: verum
end;
then V = union (waybelow V) by TARSKI:1;
hence V = "\/" ((waybelow V),(InclPoset the topology of L)) by YELLOW_1:22; ::_thesis: verum
end;
hence InclPoset (sigma L) is continuous by Th23; ::_thesis: verum
end;
theorem Th37: :: WAYBEL14:37
for L being complete Scott TopLattice
for x being Element of L st ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds
x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)
proof
let L be complete Scott TopLattice; ::_thesis: for x being Element of L st ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds
x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)
let x be Element of L; ::_thesis: ( ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous implies x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L) )
assume that
A1: for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) and
A2: InclPoset (sigma L) is continuous ; ::_thesis: x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)
A3: sigma L = the topology of L by Th23;
set IU = { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ;
set IPs = InclPoset the topology of L;
A4: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
set y = "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L);
set VVl = (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` ;
now__::_thesis:_for_b_being_Element_of_L_st_b_in__{__(inf_V)_where_V_is_Subset_of_L_:_(_x_in_V_&_V_in_sigma_L_)__}__holds_
b_<=_x
let b be Element of L; ::_thesis: ( b in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } implies b <= x )
assume b in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ; ::_thesis: b <= x
then consider V being Subset of L such that
A5: b = inf V and
A6: x in V and
V in sigma L ;
b is_<=_than V by A5, YELLOW_0:33;
hence b <= x by A6, LATTICE3:def_8; ::_thesis: verum
end;
then x is_>=_than { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } by LATTICE3:def_9;
then A7: "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) <= x by YELLOW_0:32;
assume A8: x <> "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) ; ::_thesis: contradiction
now__::_thesis:_not_x_in_downarrow_("\/"_(_{__(inf_V)_where_V_is_Subset_of_L_:_(_x_in_V_&_V_in_sigma_L_)__}__,L))
assume x in downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L)) ; ::_thesis: contradiction
then x <= "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by WAYBEL_0:17;
hence contradiction by A7, A8, ORDERS_2:2; ::_thesis: verum
end;
then A9: x in (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` by XBOOLE_0:def_5;
(downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` is open by WAYBEL11:12;
then reconsider VVp = (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` as Element of (InclPoset the topology of L) by A3, A4, Th24;
VVp = sup (waybelow VVp) by A2, A3, WAYBEL_3:def_5;
then VVp = union (waybelow VVp) by YELLOW_1:22;
then consider Vp being set such that
A10: x in Vp and
A11: Vp in waybelow VVp by A9, TARSKI:def_4;
reconsider Vp = Vp as Element of (InclPoset the topology of L) by A11;
Vp in sigma L by A3, A4;
then reconsider Vl = Vp as Subset of L ;
A12: Vp << VVp by A11, WAYBEL_3:7;
consider bas being Basis of x such that
A13: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered ) by A1;
A14: "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) is_>=_than { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } by YELLOW_0:32;
Vl is open by A4, PRE_TOPC:def_2;
then consider Ul being Subset of L such that
A15: Ul in bas and
A16: Ul c= Vl by A10, YELLOW_8:def_1;
set F = { (downarrow u) where u is Element of L : u in Ul } ;
A17: x in Ul by A15, YELLOW_8:12;
then A18: downarrow x in { (downarrow u) where u is Element of L : u in Ul } ;
{ (downarrow u) where u is Element of L : u in Ul } c= bool the carrier of L
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in { (downarrow u) where u is Element of L : u in Ul } or X in bool the carrier of L )
assume X in { (downarrow u) where u is Element of L : u in Ul } ; ::_thesis: X in bool the carrier of L
then ex u being Element of L st
( X = downarrow u & u in Ul ) ;
hence X in bool the carrier of L ; ::_thesis: verum
end;
then reconsider F = { (downarrow u) where u is Element of L : u in Ul } as non empty Subset-Family of L by A18;
COMPLEMENT F c= the topology of L
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in COMPLEMENT F or X in the topology of L )
assume A19: X in COMPLEMENT F ; ::_thesis: X in the topology of L
then reconsider X9 = X as Subset of L ;
X9 ` in F by A19, SETFAM_1:def_7;
then consider u being Element of L such that
A20: X9 ` = downarrow u and
u in Ul ;
X9 = (downarrow u) ` by A20;
then X9 is open by WAYBEL11:12;
hence X in the topology of L by PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider CF = COMPLEMENT F as Subset of (InclPoset the topology of L) by YELLOW_1:1;
Ul is filtered by A13, A15;
then A21: CF is directed by A3, Lm2;
Ul is open by A15, YELLOW_8:12;
then Ul in sigma L by A3, PRE_TOPC:def_2;
then inf Ul in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } by A17;
then inf Ul <= "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by A14, LATTICE3:def_9;
then downarrow (inf Ul) c= downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L)) by WAYBEL_0:21;
then A22: (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` c= (downarrow (inf Ul)) ` by SUBSET_1:12;
downarrow (inf Ul) = meet F by A17, Th15;
then (downarrow (inf Ul)) ` = union (COMPLEMENT F) by TOPS_2:7;
then VVp c= sup CF by A22, YELLOW_1:22;
then A23: VVp <= sup CF by YELLOW_1:3;
(downarrow x) ` in COMPLEMENT F by A18, YELLOW_8:5;
then consider d being Element of (InclPoset the topology of L) such that
A24: d in CF and
A25: Vp << d by A2, A3, A12, A21, A23, WAYBEL_4:53;
Vp <= d by A25, WAYBEL_3:1;
then A26: Vp c= d by YELLOW_1:3;
d in sigma L by A3, A4;
then reconsider d9 = d as Subset of L ;
d9 ` in F by A24, SETFAM_1:def_7;
then consider u being Element of L such that
A27: d9 ` = downarrow u and
A28: u in Ul ;
u <= u ;
then u in downarrow u by WAYBEL_0:17;
then not u in Vp by A27, A26, XBOOLE_0:def_5;
hence contradiction by A16, A28; ::_thesis: verum
end;
theorem Th38: :: WAYBEL14:38
for L being complete Scott TopLattice st ( for x being Element of L holds x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L) ) holds
L is continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( ( for x being Element of L holds x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L) ) implies L is continuous )
assume A1: for x being Element of L holds x = "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) ; ::_thesis: L is continuous
thus for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( L is up-complete & L is satisfying_axiom_of_approximation )
thus L is up-complete ; ::_thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),L)
set VV = { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ;
A2: sup (waybelow x) <= x by Th9;
A3: { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } c= waybelow x
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } or d in waybelow x )
assume d in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ; ::_thesis: d in waybelow x
then consider V being Subset of L such that
A4: inf V = d and
A5: x in V and
A6: V in sigma L ;
V is open by A6, Th24;
then inf V << x by A5, Th26;
hence d in waybelow x by A4; ::_thesis: verum
end;
( ex_sup_of { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L & ex_sup_of waybelow x,L ) by YELLOW_0:17;
then A7: "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) <= sup (waybelow x) by A3, YELLOW_0:34;
x = "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by A1;
hence x = "\/" ((waybelow x),L) by A7, A2, ORDERS_2:2; ::_thesis: verum
end;
theorem Th39: :: WAYBEL14:39
for L being complete Scott TopLattice holds
( ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) iff for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) )
proof
let L be complete Scott TopLattice; ::_thesis: ( ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) iff for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) )
set IPs = InclPoset the topology of L;
A1: sigma L = the topology of L by Th23;
then A2: the carrier of (InclPoset the topology of L) = sigma L by YELLOW_1:1;
hereby ::_thesis: ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) implies for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) )
assume A3: for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds
( Y is open & Y is filtered ) ; ::_thesis: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime ) )
let V be Element of (InclPoset (sigma L)); ::_thesis: ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime ) )
set X = { Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } ;
now__::_thesis:_for_YY_being_set_st_YY_in__{__Y_where_Y_is_Subset_of_L_:_(_Y_c=_V_&_ex_x_being_Element_of_L_ex_bas_being_Basis_of_x_st_
(_x_in_V_&_Y_in_bas_&_(_for_Yx_being_Subset_of_L_st_Yx_in_bas_holds_
(_Yx_is_open_&_Yx_is_filtered_)_)_)_)__}__holds_
YY_in_the_carrier_of_(InclPoset_(sigma_L))
let YY be set ; ::_thesis: ( YY in { Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } implies YY in the carrier of (InclPoset (sigma L)) )
assume YY in { Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } ; ::_thesis: YY in the carrier of (InclPoset (sigma L))
then consider Y being Subset of L such that
A4: Y = YY and
Y c= V and
A5: ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ;
Y is open by A5;
then Y in sigma L by Th24;
hence YY in the carrier of (InclPoset (sigma L)) by A4, YELLOW_1:1; ::_thesis: verum
end;
then reconsider X = { Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) } as Subset of (InclPoset (sigma L)) by TARSKI:def_3;
take X = X; ::_thesis: ( V = sup X & ( for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime ) )
V in sigma L by A1, A2;
then reconsider Vl = V as Subset of L ;
A6: Vl is open by A1, A2, Th24;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_V_implies_x_in_union_X_)_&_(_x_in_union_X_implies_x_in_V_)_)
let x be set ; ::_thesis: ( ( x in V implies x in union X ) & ( x in union X implies x in V ) )
hereby ::_thesis: ( x in union X implies x in V )
assume A7: x in V ; ::_thesis: x in union X
Vl = V ;
then reconsider d = x as Element of L by A7;
consider bas being Basis of d such that
A8: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered ) by A3;
consider Y being Subset of L such that
A9: Y in bas and
A10: Y c= V by A6, A7, YELLOW_8:13;
A11: x in Y by A9, YELLOW_8:12;
Y in X by A7, A8, A9, A10;
hence x in union X by A11, TARSKI:def_4; ::_thesis: verum
end;
assume x in union X ; ::_thesis: x in V
then consider YY being set such that
A12: x in YY and
A13: YY in X by TARSKI:def_4;
ex Y being Subset of L st
( Y = YY & Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) by A13;
hence x in V by A12; ::_thesis: verum
end;
then V = union X by TARSKI:1;
hence V = sup X by A1, YELLOW_1:22; ::_thesis: for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime
let Yp be Element of (InclPoset (sigma L)); ::_thesis: ( Yp in X implies Yp is co-prime )
assume Yp in X ; ::_thesis: Yp is co-prime
then consider Y being Subset of L such that
A14: Y = Yp and
Y c= V and
A15: ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ;
A16: ( Y is open & Y is filtered ) by A15;
then Y is upper by WAYBEL11:def_4;
hence Yp is co-prime by A14, A16, Th27; ::_thesis: verum
end;
assume A17: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for x being Element of (InclPoset (sigma L)) st x in X holds
x is co-prime ) ) ; ::_thesis: for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered )
let x be Element of L; ::_thesis: ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered )
set bas = { V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } ;
{ V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } c= bool the carrier of L
proof
let VV be set ; :: according to TARSKI:def_3 ::_thesis: ( not VV in { V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } or VV in bool the carrier of L )
assume VV in { V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } ; ::_thesis: VV in bool the carrier of L
then ex V being Element of (InclPoset (sigma L)) st
( VV = V & x in V & V is co-prime ) ;
then VV in sigma L by A1, A2;
hence VV in bool the carrier of L ; ::_thesis: verum
end;
then reconsider bas = { V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime ) } as Subset-Family of L ;
reconsider bas = bas as Subset-Family of L ;
bas is Basis of x
proof
A18: bas is open
proof
let VV be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not VV in bas or VV is open )
assume VV in bas ; ::_thesis: VV is open
then ex V being Element of (InclPoset (sigma L)) st
( VV = V & x in V & V is co-prime ) ;
hence VV is open by A1, A2, PRE_TOPC:def_2; ::_thesis: verum
end;
bas is x -quasi_basis
proof
now__::_thesis:_x_in_Intersect_bas
percases ( bas is empty or not bas is empty ) ;
suppose bas is empty ; ::_thesis: x in Intersect bas
then Intersect bas = the carrier of L by SETFAM_1:def_9;
hence x in Intersect bas ; ::_thesis: verum
end;
supposeA19: not bas is empty ; ::_thesis: x in Intersect bas
A20: now__::_thesis:_for_Y_being_set_st_Y_in_bas_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in bas implies x in Y )
assume Y in bas ; ::_thesis: x in Y
then ex V being Element of (InclPoset (sigma L)) st
( Y = V & x in V & V is co-prime ) ;
hence x in Y ; ::_thesis: verum
end;
Intersect bas = meet bas by A19, SETFAM_1:def_9;
hence x in Intersect bas by A19, A20, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
hence x in Intersect bas ; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in bas & b2 c= b1 ) )
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in bas & b1 c= S ) )
assume that
A21: S is open and
A22: x in S ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in bas & b1 c= S )
reconsider S9 = S as Element of (InclPoset the topology of L) by A2, A21, Th24;
consider X being Subset of (InclPoset the topology of L) such that
A23: S9 = sup X and
A24: for x being Element of (InclPoset the topology of L) st x in X holds
x is co-prime by A1, A17;
S9 = union X by A23, YELLOW_1:22;
then consider V being set such that
A25: x in V and
A26: V in X by A22, TARSKI:def_4;
V in sigma L by A2, A26;
then reconsider V = V as Subset of L ;
reconsider Vp = V as Element of (InclPoset the topology of L) by A26;
take V ; ::_thesis: ( V in bas & V c= S )
Vp is co-prime by A24, A26;
hence V in bas by A1, A25; ::_thesis: V c= S
sup X is_>=_than X by YELLOW_0:32;
then Vp <= sup X by A26, LATTICE3:def_9;
hence V c= S by A23, YELLOW_1:3; ::_thesis: verum
end;
hence bas is Basis of x by A18; ::_thesis: verum
end;
then reconsider bas = bas as Basis of x ;
take bas ; ::_thesis: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered )
let V be Subset of L; ::_thesis: ( V in bas implies ( V is open & V is filtered ) )
assume V in bas ; ::_thesis: ( V is open & V is filtered )
then ex Vp being Element of (InclPoset (sigma L)) st
( V = Vp & x in Vp & Vp is co-prime ) ;
hence ( V is open & V is filtered ) by A1, A2, Th24, Th27; ::_thesis: verum
end;
theorem :: WAYBEL14:40
for L being complete Scott TopLattice holds
( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive )
proof
let L be complete Scott TopLattice; ::_thesis: ( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive )
InclPoset (sigma L) = InclPoset the topology of L by Th23;
hence ( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive ) by WAYBEL_6:38; ::_thesis: verum
end;
theorem :: WAYBEL14:41
for L being complete Scott TopLattice holds
( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )
proof
let L be complete Scott TopLattice; ::_thesis: ( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )
InclPoset (sigma L) = InclPoset the topology of L by Th23;
hence ( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) ) by WAYBEL_6:39; ::_thesis: verum
end;
theorem :: WAYBEL14:42
for L being complete Scott TopLattice st L is algebraic holds
ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
proof
let L be complete Scott TopLattice; ::_thesis: ( L is algebraic implies ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } )
set P = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ;
{ (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } or x in bool the carrier of L )
assume x in { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; ::_thesis: x in bool the carrier of L
then ex k being Element of L st
( x = uparrow k & k in the carrier of (CompactSublatt L) ) ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider P = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } as Subset-Family of L ;
reconsider P = P as Subset-Family of L ;
A1: P c= the topology of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in the topology of L )
assume x in P ; ::_thesis: x in the topology of L
then consider k being Element of L such that
A2: x = uparrow k and
A3: k in the carrier of (CompactSublatt L) ;
k is compact by A3, WAYBEL_8:def_1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
hence x in the topology of L by A2, PRE_TOPC:def_2; ::_thesis: verum
end;
assume A4: L is algebraic ; ::_thesis: ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
now__::_thesis:_for_x_being_Point_of_L_ex_B_being_Basis_of_x_st_B_c=_P
let x be Point of L; ::_thesis: ex B being Basis of x st B c= P
set B = { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } ;
{ (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } c= bool the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } or y in bool the carrier of L )
assume y in { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } ; ::_thesis: y in bool the carrier of L
then ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence y in bool the carrier of L ; ::_thesis: verum
end;
then reconsider B = { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
B is Basis of x
proof
A5: B is open
proof
let y be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not y in B or y is open )
assume y in B ; ::_thesis: y is open
then ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence y is open by A1, PRE_TOPC:def_2; ::_thesis: verum
end;
B is x -quasi_basis
proof
now__::_thesis:_x_in_Intersect_B
percases ( B is empty or not B is empty ) ;
suppose B is empty ; ::_thesis: x in Intersect B
then Intersect B = the carrier of L by SETFAM_1:def_9;
hence x in Intersect B ; ::_thesis: verum
end;
supposeA6: not B is empty ; ::_thesis: x in Intersect B
A7: now__::_thesis:_for_Y_being_set_st_Y_in_B_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in B implies x in Y )
assume Y in B ; ::_thesis: x in Y
then ex k being Element of L st
( Y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence x in Y ; ::_thesis: verum
end;
Intersect B = meet B by A6, SETFAM_1:def_9;
hence x in Intersect B by A6, A7, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
hence x in Intersect B ; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in B & b2 c= b1 ) )
reconsider x9 = x as Element of L ;
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S ) )
assume that
A8: S is open and
A9: x in S ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S )
A10: x = sup (compactbelow x9) by A4, WAYBEL_8:def_3;
S is inaccessible by A8, WAYBEL11:def_4;
then compactbelow x9 meets S by A9, A10, WAYBEL11:def_1;
then consider k being set such that
A11: k in compactbelow x9 and
A12: k in S by XBOOLE_0:3;
reconsider k = k as Element of L by A11;
A13: compactbelow x9 = (downarrow x9) /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
then k in downarrow x9 by A11, XBOOLE_0:def_4;
then k <= x9 by WAYBEL_0:17;
then A14: x in uparrow k by WAYBEL_0:18;
take V = uparrow k; ::_thesis: ( V in B & V c= S )
k in the carrier of (CompactSublatt L) by A11, A13, XBOOLE_0:def_4;
then uparrow k in P ;
hence V in B by A14; ::_thesis: V c= S
S is upper by A8, WAYBEL11:def_4;
hence V c= S by A12, WAYBEL11:42; ::_thesis: verum
end;
hence B is Basis of x by A5; ::_thesis: verum
end;
then reconsider B = B as Basis of x ;
take B = B; ::_thesis: B c= P
thus B c= P ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in P )
assume y in B ; ::_thesis: y in P
then ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence y in P ; ::_thesis: verum
end;
end;
then P is Basis of L by A1, YELLOW_8:14;
hence ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } ; ::_thesis: verum
end;
theorem :: WAYBEL14:43
for L being complete Scott TopLattice st ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } holds
( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) )
proof
let L be complete Scott TopLattice; ::_thesis: ( ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } implies ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) ) )
given B being Basis of L such that A1: B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; ::_thesis: ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) )
set IPs = InclPoset (sigma L);
set IPt = InclPoset the topology of L;
A2: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
A4: InclPoset (sigma L) = InclPoset the topology of L by Th23;
thus InclPoset (sigma L) is algebraic ::_thesis: for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) )
proof
thus for X being Element of (InclPoset (sigma L)) holds
( not compactbelow X is empty & compactbelow X is directed ) by A3; :: according to WAYBEL_8:def_4 ::_thesis: ( InclPoset (sigma L) is up-complete & InclPoset (sigma L) is satisfying_axiom_K )
thus InclPoset (sigma L) is up-complete by A4; ::_thesis: InclPoset (sigma L) is satisfying_axiom_K
let X be Element of (InclPoset (sigma L)); :: according to WAYBEL_8:def_3 ::_thesis: X = "\/" ((compactbelow X),(InclPoset (sigma L)))
set cX = compactbelow X;
set GB = { G where G is Subset of L : ( G in B & G c= X ) } ;
X in sigma L by A2;
then reconsider X9 = X as Subset of L ;
X9 is open by A2, Th24;
then A5: X = union { G where G is Subset of L : ( G in B & G c= X ) } by YELLOW_8:9;
A6: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_X_implies_x_in_union_(compactbelow_X)_)_&_(_x_in_union_(compactbelow_X)_implies_x_in_X_)_)
let x be set ; ::_thesis: ( ( x in X implies x in union (compactbelow X) ) & ( x in union (compactbelow X) implies x in X ) )
hereby ::_thesis: ( x in union (compactbelow X) implies x in X )
assume x in X ; ::_thesis: x in union (compactbelow X)
then consider GG being set such that
A7: x in GG and
A8: GG in { G where G is Subset of L : ( G in B & G c= X ) } by A5, TARSKI:def_4;
consider G being Subset of L such that
A9: G = GG and
A10: G in B and
A11: G c= X by A8;
consider k being Element of L such that
A12: G = uparrow k and
A13: k in the carrier of (CompactSublatt L) by A1, A10;
k is compact by A13, WAYBEL_8:def_1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
then reconsider G = G as Element of (InclPoset (sigma L)) by A3, A2, A12, PRE_TOPC:def_2;
for X being Subset of L st X is open holds
X is upper by WAYBEL11:def_4;
then uparrow k is compact by Th22;
then A14: G is compact by A3, A12, WAYBEL_3:36;
G <= X by A11, YELLOW_1:3;
then G in compactbelow X by A14;
hence x in union (compactbelow X) by A7, A9, TARSKI:def_4; ::_thesis: verum
end;
assume x in union (compactbelow X) ; ::_thesis: x in X
then consider G being set such that
A15: x in G and
A16: G in compactbelow X by TARSKI:def_4;
reconsider G = G as Element of (InclPoset (sigma L)) by A16;
G <= X by A16, WAYBEL_8:4;
then G c= X by YELLOW_1:3;
hence x in X by A15; ::_thesis: verum
end;
sup (compactbelow X) = union (compactbelow X) by A3, YELLOW_1:22;
hence X = "\/" ((compactbelow X),(InclPoset (sigma L))) by A6, TARSKI:1; ::_thesis: verum
end;
let V be Element of (InclPoset (sigma L)); ::_thesis: ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) )
V in sigma L by A2;
then reconsider V9 = V as Subset of L ;
set GB = { G where G is Subset of L : ( G in B & G c= V ) } ;
{ G where G is Subset of L : ( G in B & G c= V ) } c= the carrier of (InclPoset (sigma L))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { G where G is Subset of L : ( G in B & G c= V ) } or x in the carrier of (InclPoset (sigma L)) )
assume x in { G where G is Subset of L : ( G in B & G c= V ) } ; ::_thesis: x in the carrier of (InclPoset (sigma L))
then consider G being Subset of L such that
A17: G = x and
A18: G in B and
G c= V ;
G is open by A18, YELLOW_8:10;
hence x in the carrier of (InclPoset (sigma L)) by A2, A17, Th24; ::_thesis: verum
end;
then reconsider GB = { G where G is Subset of L : ( G in B & G c= V ) } as Subset of (InclPoset (sigma L)) ;
take GB ; ::_thesis: ( V = sup GB & ( for W being Element of (InclPoset (sigma L)) st W in GB holds
W is co-prime ) )
V9 is open by A2, Th24;
then V = union GB by YELLOW_8:9;
hence V = sup GB by A3, YELLOW_1:22; ::_thesis: for W being Element of (InclPoset (sigma L)) st W in GB holds
W is co-prime
let x be Element of (InclPoset (sigma L)); ::_thesis: ( x in GB implies x is co-prime )
assume x in GB ; ::_thesis: x is co-prime
then consider G being Subset of L such that
A19: G = x and
A20: G in B and
G c= V ;
ex k being Element of L st
( G = uparrow k & k in the carrier of (CompactSublatt L) ) by A1, A20;
hence x is co-prime by A19, Th27; ::_thesis: verum
end;
theorem :: WAYBEL14:44
for L being complete Scott TopLattice st InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) holds
ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
proof
let L be complete Scott TopLattice; ::_thesis: ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) implies ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } )
set IPt = InclPoset the topology of L;
set IPs = InclPoset (sigma L);
A1: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
set B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ;
{ (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } or x in bool the carrier of L )
assume x in { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; ::_thesis: x in bool the carrier of L
then ex k being Element of L st
( x = uparrow k & k in the carrier of (CompactSublatt L) ) ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } as Subset-Family of L ;
assume that
A2: InclPoset (sigma L) is algebraic and
A3: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for x being Element of (InclPoset (sigma L)) st x in X holds
x is co-prime ) ) ; ::_thesis: ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
InclPoset (sigma L) = InclPoset the topology of L by Th23;
then reconsider ips = InclPoset (sigma L) as algebraic LATTICE by A2;
reconsider B = B as Subset-Family of L ;
A4: B c= the topology of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in the topology of L )
assume x in B ; ::_thesis: x in the topology of L
then consider k being Element of L such that
A5: x = uparrow k and
A6: k in the carrier of (CompactSublatt L) ;
k is compact by A6, WAYBEL_8:def_1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
hence x in the topology of L by A5, PRE_TOPC:def_2; ::_thesis: verum
end;
A7: sigma L = the topology of L by Th23;
( ips is continuous & ( for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds
( Y is open & Y is filtered ) ) ) by A3, Th39;
then for x being Element of L holds x = "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by Th37;
then A8: L is continuous by Th38;
now__::_thesis:_for_x_being_Point_of_L_ex_Bx_being_Basis_of_x_st_Bx_c=_B
let x be Point of L; ::_thesis: ex Bx being Basis of x st Bx c= B
set Bx = { (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } ;
{ (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } c= bool the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } or y in bool the carrier of L )
assume y in { (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } ; ::_thesis: y in bool the carrier of L
then ex k being Element of L st
( y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence y in bool the carrier of L ; ::_thesis: verum
end;
then reconsider Bx = { (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } as Subset-Family of L ;
reconsider Bx = Bx as Subset-Family of L ;
Bx is Basis of x
proof
A9: Bx is open
proof
let y be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not y in Bx or y is open )
assume y in Bx ; ::_thesis: y is open
then ex k being Element of L st
( y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence y is open by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
Bx is x -quasi_basis
proof
now__::_thesis:_x_in_Intersect_Bx
percases ( Bx is empty or not Bx is empty ) ;
suppose Bx is empty ; ::_thesis: x in Intersect Bx
then Intersect Bx = the carrier of L by SETFAM_1:def_9;
hence x in Intersect Bx ; ::_thesis: verum
end;
supposeA10: not Bx is empty ; ::_thesis: x in Intersect Bx
A11: now__::_thesis:_for_Y_being_set_st_Y_in_Bx_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in Bx implies x in Y )
assume Y in Bx ; ::_thesis: x in Y
then ex k being Element of L st
( Y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence x in Y ; ::_thesis: verum
end;
Intersect Bx = meet Bx by A10, SETFAM_1:def_9;
hence x in Intersect Bx by A10, A11, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
hence x in Intersect Bx ; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in Bx & b2 c= b1 ) )
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in Bx & b1 c= S ) )
assume that
A12: S is open and
A13: x in S ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in Bx & b1 c= S )
reconsider S9 = S as Element of (InclPoset the topology of L) by A7, A1, A12, PRE_TOPC:def_2;
S9 = sup (compactbelow S9) by A2, A7, WAYBEL_8:def_3;
then S9 = union (compactbelow S9) by YELLOW_1:22;
then consider UA being set such that
A14: x in UA and
A15: UA in compactbelow S9 by A13, TARSKI:def_4;
reconsider UA = UA as Element of (InclPoset the topology of L) by A15;
UA is compact by A15, WAYBEL_8:4;
then A16: UA << UA by WAYBEL_3:def_2;
UA in the topology of L by A7, A1;
then reconsider UA9 = UA as Subset of L ;
UA <= S9 by A15, WAYBEL_8:4;
then A17: UA c= S by YELLOW_1:3;
consider F being Subset of (InclPoset (sigma L)) such that
A18: UA = sup F and
A19: for x being Element of (InclPoset (sigma L)) st x in F holds
x is co-prime by A3, A7;
reconsider F9 = F as Subset-Family of L by A1, XBOOLE_1:1;
A20: UA = union F by A7, A18, YELLOW_1:22;
F9 is open
proof
let P be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not P in F9 or P is open )
assume P in F9 ; ::_thesis: P is open
hence P is open by A7, A1, PRE_TOPC:def_2; ::_thesis: verum
end;
then consider G being finite Subset of F9 such that
A21: UA c= union G by A20, A16, WAYBEL_3:34;
union G c= union F by ZFMISC_1:77;
then A22: UA = union G by A20, A21, XBOOLE_0:def_10;
reconsider G = G as finite Subset-Family of L by XBOOLE_1:1;
consider Gg being finite Subset-Family of L such that
A23: Gg c= G and
A24: union Gg = union G and
A25: for g being Subset of L st g in Gg holds
not g c= union (Gg \ {g}) by Th1;
consider U1 being set such that
A26: x in U1 and
A27: U1 in Gg by A14, A21, A24, TARSKI:def_4;
A28: Gg c= F by A23, XBOOLE_1:1;
then U1 in F by A27;
then reconsider U1 = U1 as Element of (InclPoset (sigma L)) ;
U1 in the topology of L by A7, A1;
then reconsider U19 = U1 as Subset of L ;
set k = inf U19;
A29: U19 c= uparrow (inf U19)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in U19 or x in uparrow (inf U19) )
assume A30: x in U19 ; ::_thesis: x in uparrow (inf U19)
then reconsider x9 = x as Element of L ;
inf U19 is_<=_than U19 by YELLOW_0:33;
then inf U19 <= x9 by A30, LATTICE3:def_8;
hence x in uparrow (inf U19) by WAYBEL_0:18; ::_thesis: verum
end;
U1 is co-prime by A19, A27, A28;
then A31: ( U19 is filtered & U19 is upper ) by Th27;
now__::_thesis:_inf_U19_in_U19
set D = { ((downarrow u) `) where u is Element of L : u in U19 } ;
A32: { ((downarrow u) `) where u is Element of L : u in U19 } c= the topology of L
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in { ((downarrow u) `) where u is Element of L : u in U19 } or d in the topology of L )
assume d in { ((downarrow u) `) where u is Element of L : u in U19 } ; ::_thesis: d in the topology of L
then consider u being Element of L such that
A33: d = (downarrow u) ` and
u in U19 ;
(downarrow u) ` is open by WAYBEL11:12;
hence d in the topology of L by A33, PRE_TOPC:def_2; ::_thesis: verum
end;
consider u being set such that
A34: u in U19 by A26;
reconsider u = u as Element of L by A34;
(downarrow u) ` in { ((downarrow u) `) where u is Element of L : u in U19 } by A34;
then reconsider D = { ((downarrow u) `) where u is Element of L : u in U19 } as non empty Subset of (InclPoset the topology of L) by A32, YELLOW_1:1;
assume A35: not inf U19 in U19 ; ::_thesis: contradiction
now__::_thesis:_UA_c=_union_D
assume not UA c= union D ; ::_thesis: contradiction
then consider l being set such that
A36: l in UA9 and
A37: not l in union D by TARSKI:def_3;
reconsider l = l as Element of L by A36;
consider Uk being set such that
A38: l in Uk and
A39: Uk in Gg by A21, A24, A36, TARSKI:def_4;
A40: Gg c= F by A23, XBOOLE_1:1;
then Uk in F by A39;
then reconsider Uk = Uk as Element of (InclPoset (sigma L)) ;
Uk in the topology of L by A7, A1;
then reconsider Uk9 = Uk as Subset of L ;
Uk is co-prime by A19, A39, A40;
then A41: ( Uk9 is filtered & Uk9 is upper ) by Th27;
now__::_thesis:_l_is_<=_than_U19
assume not l is_<=_than U19 ; ::_thesis: contradiction
then consider m being Element of L such that
A42: m in U19 and
A43: not l <= m by LATTICE3:def_8;
(downarrow m) ` in D by A42;
then not l in (downarrow m) ` by A37, TARSKI:def_4;
then l in downarrow m by XBOOLE_0:def_5;
hence contradiction by A43, WAYBEL_0:17; ::_thesis: verum
end;
then l <= inf U19 by YELLOW_0:33;
then A44: inf U19 in Uk9 by A38, A41, WAYBEL_0:def_20;
A45: inf U19 is_<=_than U19 by YELLOW_0:33;
A46: U19 c= Uk
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in U19 or u in Uk )
assume A47: u in U19 ; ::_thesis: u in Uk
then reconsider d = u as Element of L ;
inf U19 <= d by A45, A47, LATTICE3:def_8;
hence u in Uk by A41, A44, WAYBEL_0:def_20; ::_thesis: verum
end;
U19 c= union (Gg \ {U19})
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in U19 or u in union (Gg \ {U19}) )
assume A48: u in U19 ; ::_thesis: u in union (Gg \ {U19})
Uk in Gg \ {U19} by A35, A39, A44, ZFMISC_1:56;
hence u in union (Gg \ {U19}) by A46, A48, TARSKI:def_4; ::_thesis: verum
end;
hence contradiction by A25, A27; ::_thesis: verum
end;
then UA c= sup D by YELLOW_1:22;
then A49: UA <= sup D by YELLOW_1:3;
D is directed by A7, A31, Th25;
then consider d being Element of (InclPoset the topology of L) such that
A50: d in D and
A51: UA <= d by A16, A49, WAYBEL_3:def_1;
consider u being Element of L such that
A52: d = (downarrow u) ` and
A53: u in U19 by A50;
U1 c= UA by A20, A27, A28, ZFMISC_1:74;
then A54: u in UA by A53;
A55: u <= u ;
UA c= d by A51, YELLOW_1:3;
then not u in downarrow u by A52, A54, XBOOLE_0:def_5;
hence contradiction by A55, WAYBEL_0:17; ::_thesis: verum
end;
then uparrow (inf U19) c= U19 by A31, WAYBEL11:42;
then A56: U19 = uparrow (inf U19) by A29, XBOOLE_0:def_10;
take V = uparrow (inf U19); ::_thesis: ( V in Bx & V c= S )
U19 is open by A7, A1, PRE_TOPC:def_2;
then U19 is Open by A8, A31, WAYBEL11:46;
then inf U19 is compact by A56, WAYBEL_8:2;
then inf U19 in the carrier of (CompactSublatt L) by WAYBEL_8:def_1;
then uparrow (inf U19) in B ;
hence V in Bx by A26, A29; ::_thesis: V c= S
U1 c= UA by A22, A24, A27, ZFMISC_1:74;
hence V c= S by A56, A17, XBOOLE_1:1; ::_thesis: verum
end;
hence Bx is Basis of x by A9; ::_thesis: verum
end;
then reconsider Bx = Bx as Basis of x ;
take Bx = Bx; ::_thesis: Bx c= B
thus Bx c= B ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Bx or y in B )
assume y in Bx ; ::_thesis: y in B
then ex k being Element of L st
( y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence y in B ; ::_thesis: verum
end;
end;
then reconsider B = B as Basis of L by A4, YELLOW_8:14;
take B ; ::_thesis: B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
thus B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } ; ::_thesis: verum
end;
theorem :: WAYBEL14:45
for L being complete Scott TopLattice st ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } holds
L is algebraic
proof
let L be complete Scott TopLattice; ::_thesis: ( ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } implies L is algebraic )
given B being Basis of L such that A1: B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; ::_thesis: L is algebraic
thus for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def_4 ::_thesis: ( L is up-complete & L is satisfying_axiom_K )
thus L is up-complete ; ::_thesis: L is satisfying_axiom_K
let x be Element of L; :: according to WAYBEL_8:def_3 ::_thesis: x = "\/" ((compactbelow x),L)
set y = sup (compactbelow x);
set cx = compactbelow x;
set dx = downarrow x;
set dy = downarrow (sup (compactbelow x));
now__::_thesis:_not_sup_(compactbelow_x)_<>_x
for z being Element of L st z in downarrow x holds
z <= x by WAYBEL_0:17;
then x is_>=_than downarrow x by LATTICE3:def_9;
then A2: sup (downarrow x) <= x by YELLOW_0:32;
set GB = { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } ;
A3: compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
A4: sup (compactbelow x) is_>=_than compactbelow x by YELLOW_0:32;
( ex_sup_of compactbelow x,L & ex_sup_of downarrow x,L ) by YELLOW_0:17;
then sup (compactbelow x) <= sup (downarrow x) by A3, XBOOLE_1:17, YELLOW_0:34;
then A5: sup (compactbelow x) <= x by A2, ORDERS_2:3;
assume A6: sup (compactbelow x) <> x ; ::_thesis: contradiction
now__::_thesis:_not_x_in_downarrow_(sup_(compactbelow_x))
assume x in downarrow (sup (compactbelow x)) ; ::_thesis: contradiction
then x <= sup (compactbelow x) by WAYBEL_0:17;
hence contradiction by A6, A5, ORDERS_2:2; ::_thesis: verum
end;
then A7: x in (downarrow (sup (compactbelow x))) ` by XBOOLE_0:def_5;
(downarrow (sup (compactbelow x))) ` = union { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } by WAYBEL11:12, YELLOW_8:9;
then consider X being set such that
A8: x in X and
A9: X in { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } by A7, TARSKI:def_4;
consider G being Subset of L such that
A10: G = X and
A11: G in B and
A12: G c= (downarrow (sup (compactbelow x))) ` by A9;
consider k being Element of L such that
A13: G = uparrow k and
A14: k in the carrier of (CompactSublatt L) by A1, A11;
A15: k is compact by A14, WAYBEL_8:def_1;
k <= x by A8, A10, A13, WAYBEL_0:18;
then k in compactbelow x by A15;
then k <= sup (compactbelow x) by A4, LATTICE3:def_9;
then sup (compactbelow x) in uparrow k by WAYBEL_0:18;
then ( sup (compactbelow x) <= sup (compactbelow x) & not sup (compactbelow x) in downarrow (sup (compactbelow x)) ) by A12, A13, XBOOLE_0:def_5;
hence contradiction by WAYBEL_0:17; ::_thesis: verum
end;
hence x = "\/" ((compactbelow x),L) ; ::_thesis: verum
end;