let L be 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) `
let X be 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 V be Element of (InclPoset (sigma L)); ( 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
; 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 )
;
WAYBEL_0:def 1 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;
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 for x being object holds
( ( x in Tsup .: AAe implies x in Va /\ Vb ) & ( x in Va /\ Vb implies x in Tsup .: AAe ) )let x be
object ;
( ( x in Tsup .: AAe implies x in Va /\ Vb ) & ( x in Va /\ Vb implies x in Tsup .: AAe ) )hereby ( x in Va /\ Vb implies x in Tsup .: AAe )
assume
x in Tsup .: AAe
;
x in Va /\ Vbthen consider cd being
object 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;
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;
hence
x in Va /\ Vb
by A32, XBOOLE_0:def 4;
verum
end; assume A34:
x in Va /\ Vb
;
x in Tsup .: AAethen 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;
verum end;
then A37:
Tsup .: AAe = Va /\ Vb
by TARSKI:2;
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;
(
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;
verum
end;
take u = sup (X `); X = (downarrow u) `
then
u in X `
by A9, A10, WAYBEL11:def 2;
then
X ` = downarrow u
by A9, Th5;
hence
X = (downarrow u) `
; verum