let L be 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 ) )
let X be 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 V be Element of (InclPoset (sigma L)); ( V = X implies ( V is co-prime iff ( X is filtered & X is upper ) ) )
assume A1:
V = X
; ( 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 ( X is filtered & X is upper implies V is co-prime )
assume A6:
V is
co-prime
;
( X is filtered & X is upper )thus
X is
filtered
X is upper proof
let v,
w be
Element of
L;
WAYBEL_0:def 2 ( 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
;
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;
( 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;
then
X meets ((downarrow (v "/\" w)) `) `
by A1, A11, SUBSET_1:24;
then
X /\ (((downarrow (v "/\" w)) `) `) <> {}
;
then consider zz being
object 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;
( z <= v & z <= w )
thus
(
z <= v &
z <= w )
by YELLOW_0:23;
verum
end; thus
X is
upper
by A1, A3, A4, WAYBEL11:31;
verum
end;
assume A15:
( X is filtered & X is upper )
; V is co-prime
assume
not V is co-prime
; 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 object such that
A23:
w in V
and
A24:
not w in Y
;
not V c= Xx
by A17, YELLOW_1:3;
then consider v being object such that
A25:
v in V
and
A26:
not v in Xx
;
reconsider v = v, w = w as Element of L by A1, A25, A23;
A27:
Xx9 is upper
by A21, WAYBEL11:def 4;
v "/\" w in X
by A1, A15, A25, A23, WAYBEL_0:41;
hence
contradiction
by A1, A22, A28; verum