:: WAYBEL30 semantic presentation
begin
theorem Th1: :: WAYBEL30:1
for x being set
for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum }
proof
let x be set ; ::_thesis: for D being non empty set holds x /\ (union D) = union { (x /\ d) where d is Element of D : verum }
let D be non empty set ; ::_thesis: x /\ (union D) = union { (x /\ d) where d is Element of D : verum }
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (x /\ d) where d is Element of D : verum } c= x /\ (union D)
let a be set ; ::_thesis: ( a in x /\ (union D) implies a in union { (x /\ d) where d is Element of D : verum } )
assume A1: a in x /\ (union D) ; ::_thesis: a in union { (x /\ d) where d is Element of D : verum }
then a in union D by XBOOLE_0:def_4;
then consider Z being set such that
A2: a in Z and
A3: Z in D by TARSKI:def_4;
A4: x /\ Z in { (x /\ d) where d is Element of D : verum } by A3;
a in x by A1, XBOOLE_0:def_4;
then a in x /\ Z by A2, XBOOLE_0:def_4;
hence a in union { (x /\ d) where d is Element of D : verum } by A4, TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (x /\ d) where d is Element of D : verum } or a in x /\ (union D) )
assume a in union { (x /\ d) where d is Element of D : verum } ; ::_thesis: a in x /\ (union D)
then consider Z being set such that
A5: a in Z and
A6: Z in { (x /\ d) where d is Element of D : verum } by TARSKI:def_4;
consider d being Element of D such that
A7: Z = x /\ d and
verum by A6;
a in d by A5, A7, XBOOLE_0:def_4;
then A8: a in union D by TARSKI:def_4;
a in x by A5, A7, XBOOLE_0:def_4;
hence a in x /\ (union D) by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th2: :: WAYBEL30:2
for R being non empty reflexive transitive RelStr
for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R
proof
let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R)) holds union D is Ideal of R
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: union D is Ideal of R
set d = the Element of D;
D c= the carrier of (InclPoset (Ids R)) ;
then A1: D c= Ids R by YELLOW_1:1;
A2: D c= bool the carrier of R
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in D or d in bool the carrier of R )
assume d in D ; ::_thesis: d in bool the carrier of R
then d in Ids R by A1;
then ex I being Ideal of R st d = I ;
hence d in bool the carrier of R ; ::_thesis: verum
end;
the Element of D in D ;
then the Element of D in Ids R by A1;
then consider I being Ideal of R such that
A3: the Element of D = I and
verum ;
A4: for X being Subset of R st X in D holds
X is directed
proof
let X be Subset of R; ::_thesis: ( X in D implies X is directed )
assume X in D ; ::_thesis: X is directed
then X in Ids R by A1;
then ex I being Ideal of R st X = I ;
hence X is directed ; ::_thesis: verum
end;
A5: for X, Y being Subset of R st X in D & Y in D holds
ex Z being Subset of R st
( Z in D & X \/ Y c= Z )
proof
let X, Y be Subset of R; ::_thesis: ( X in D & Y in D implies ex Z being Subset of R st
( Z in D & X \/ Y c= Z ) )
assume that
A6: X in D and
A7: Y in D ; ::_thesis: ex Z being Subset of R st
( Z in D & X \/ Y c= Z )
reconsider X1 = X, Y1 = Y as Element of (InclPoset (Ids R)) by A6, A7;
consider Z1 being Element of (InclPoset (Ids R)) such that
A8: Z1 in D and
A9: X1 <= Z1 and
A10: Y1 <= Z1 by A6, A7, WAYBEL_0:def_1;
Z1 in Ids R by A1, A8;
then ex I being Ideal of R st Z1 = I ;
then reconsider Z = Z1 as Subset of R ;
take Z ; ::_thesis: ( Z in D & X \/ Y c= Z )
thus Z in D by A8; ::_thesis: X \/ Y c= Z
A11: Y1 c= Z1 by A10, YELLOW_1:3;
X1 c= Z1 by A9, YELLOW_1:3;
hence X \/ Y c= Z by A11, XBOOLE_1:8; ::_thesis: verum
end;
A12: for X being Subset of R st X in D holds
X is lower
proof
let X be Subset of R; ::_thesis: ( X in D implies X is lower )
assume X in D ; ::_thesis: X is lower
then X in Ids R by A1;
then ex I being Ideal of R st X = I ;
hence X is lower ; ::_thesis: verum
end;
set i = the Element of I;
the Element of I in the Element of D by A3;
hence union D is Ideal of R by A12, A2, A4, A5, TARSKI:def_4, WAYBEL_0:26, WAYBEL_0:46; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_R_being_non_empty_reflexive_transitive_RelStr_
for_D_being_non_empty_directed_Subset_of_(InclPoset_(Ids_R))
for_UD_being_Element_of_(InclPoset_(Ids_R))_st_UD_=_union_D_holds_
D_is_<=_than_UD
let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for UD being Element of (InclPoset (Ids R)) st UD = union D holds
D is_<=_than UD
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds
D is_<=_than UD
let UD be Element of (InclPoset (Ids R)); ::_thesis: ( UD = union D implies D is_<=_than UD )
assume A1: UD = union D ; ::_thesis: D is_<=_than UD
thus D is_<=_than UD ::_thesis: verum
proof
let d be Element of (InclPoset (Ids R)); :: according to LATTICE3:def_9 ::_thesis: ( not d in D or d <= UD )
assume A2: d in D ; ::_thesis: d <= UD
d c= UD
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in d or a in UD )
assume a in d ; ::_thesis: a in UD
hence a in UD by A1, A2, TARSKI:def_4; ::_thesis: verum
end;
hence d <= UD by YELLOW_1:3; ::_thesis: verum
end;
end;
Lm2: now__::_thesis:_for_R_being_non_empty_reflexive_transitive_RelStr_
for_D_being_non_empty_directed_Subset_of_(InclPoset_(Ids_R))
for_UD_being_Element_of_(InclPoset_(Ids_R))_st_UD_=_union_D_holds_
for_b_being_Element_of_(InclPoset_(Ids_R))_st_b_is_>=_than_D_holds_
UD_<=_b
let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for UD being Element of (InclPoset (Ids R)) st UD = union D holds
for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for UD being Element of (InclPoset (Ids R)) st UD = union D holds
for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b
let UD be Element of (InclPoset (Ids R)); ::_thesis: ( UD = union D implies for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b )
assume A1: UD = union D ; ::_thesis: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b
thus for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b ::_thesis: verum
proof
let b be Element of (InclPoset (Ids R)); ::_thesis: ( b is_>=_than D implies UD <= b )
assume A2: for a being Element of (InclPoset (Ids R)) st a in D holds
b >= a ; :: according to LATTICE3:def_9 ::_thesis: UD <= b
UD c= b
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UD or x in b )
assume x in UD ; ::_thesis: x in b
then consider Z being set such that
A3: x in Z and
A4: Z in D by A1, TARSKI:def_4;
reconsider Z = Z as Element of (InclPoset (Ids R)) by A4;
b >= Z by A2, A4;
then Z c= b by YELLOW_1:3;
hence x in b by A3; ::_thesis: verum
end;
hence UD <= b by YELLOW_1:3; ::_thesis: verum
end;
end;
registration
let R be non empty reflexive transitive RelStr ;
cluster InclPoset (Ids R) -> up-complete ;
coherence
InclPoset (Ids R) is up-complete
proof
set I = InclPoset (Ids R);
let D be non empty directed Subset of (InclPoset (Ids R)); :: according to WAYBEL_0:def_39 ::_thesis: ex b1 being Element of the carrier of (InclPoset (Ids R)) st
( D is_<=_than b1 & ( for b2 being Element of the carrier of (InclPoset (Ids R)) holds
( not D is_<=_than b2 or b1 <= b2 ) ) )
reconsider UD = union D as Ideal of R by Th2;
UD in Ids R ;
then reconsider UD = UD as Element of (InclPoset (Ids R)) by YELLOW_1:1;
take UD ; ::_thesis: ( D is_<=_than UD & ( for b1 being Element of the carrier of (InclPoset (Ids R)) holds
( not D is_<=_than b1 or UD <= b1 ) ) )
thus ( D is_<=_than UD & ( for b1 being Element of the carrier of (InclPoset (Ids R)) holds
( not D is_<=_than b1 or UD <= b1 ) ) ) by Lm1, Lm2; ::_thesis: verum
end;
end;
theorem Th3: :: WAYBEL30:3
for R being non empty reflexive transitive RelStr
for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D
proof
let R be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R)) holds sup D = union D
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: sup D = union D
reconsider UD = union D as Ideal of R by Th2;
A1: ex_sup_of D, InclPoset (Ids R) by WAYBEL_0:75;
UD in Ids R ;
then reconsider UD = UD as Element of (InclPoset (Ids R)) by YELLOW_1:1;
A2: for b being Element of (InclPoset (Ids R)) st b is_>=_than D holds
UD <= b by Lm2;
D is_<=_than UD by Lm1;
hence sup D = union D by A2, A1, YELLOW_0:def_9; ::_thesis: verum
end;
theorem Th4: :: WAYBEL30:4
for R being Semilattice
for D being non empty directed Subset of (InclPoset (Ids R))
for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
proof
let R be Semilattice; ::_thesis: for D being non empty directed Subset of (InclPoset (Ids R))
for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: for x being Element of (InclPoset (Ids R)) holds sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
let x be Element of (InclPoset (Ids R)); ::_thesis: sup ({x} "/\" D) = union { (x /\ d) where d is Element of D : verum }
set I = InclPoset (Ids R);
set A = { (x /\ d) where d is Element of D : verum } ;
set xD = { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } ;
{ (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } c= the carrier of (InclPoset (Ids R))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } or a in the carrier of (InclPoset (Ids R)) )
assume a in { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } ; ::_thesis: a in the carrier of (InclPoset (Ids R))
then ex d being Element of (InclPoset (Ids R)) st
( a = x "/\" d & d in D ) ;
hence a in the carrier of (InclPoset (Ids R)) ; ::_thesis: verum
end;
then reconsider xD = { (x "/\" d) where d is Element of (InclPoset (Ids R)) : d in D } as Subset of (InclPoset (Ids R)) ;
A1: ex_sup_of {x} "/\" D, InclPoset (Ids R) by WAYBEL_2:1;
then ex_sup_of xD, InclPoset (Ids R) by YELLOW_4:42;
then A2: sup xD is_>=_than xD by YELLOW_0:def_9;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: union { (x /\ d) where d is Element of D : verum } c= sup ({x} "/\" D)
set A = { (x /\ w) where w is Element of D : verum } ;
let a be set ; ::_thesis: ( a in sup ({x} "/\" D) implies a in union { (x /\ w) where w is Element of D : verum } )
ex_sup_of D, InclPoset (Ids R) by WAYBEL_0:75;
then sup ({x} "/\" D) <= x "/\" (sup D) by A1, YELLOW_4:53;
then A3: sup ({x} "/\" D) c= x "/\" (sup D) by YELLOW_1:3;
assume a in sup ({x} "/\" D) ; ::_thesis: a in union { (x /\ w) where w is Element of D : verum }
then a in x "/\" (sup D) by A3;
then A4: a in x /\ (sup D) by YELLOW_2:43;
then a in sup D by XBOOLE_0:def_4;
then a in union D by Th3;
then consider d being set such that
A5: a in d and
A6: d in D by TARSKI:def_4;
reconsider d = d as Element of (InclPoset (Ids R)) by A6;
A7: x /\ d in { (x /\ w) where w is Element of D : verum } by A6;
a in x by A4, XBOOLE_0:def_4;
then a in x /\ d by A5, XBOOLE_0:def_4;
hence a in union { (x /\ w) where w is Element of D : verum } by A7, TARSKI:def_4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { (x /\ d) where d is Element of D : verum } or a in sup ({x} "/\" D) )
assume a in union { (x /\ d) where d is Element of D : verum } ; ::_thesis: a in sup ({x} "/\" D)
then consider Z being set such that
A8: a in Z and
A9: Z in { (x /\ d) where d is Element of D : verum } by TARSKI:def_4;
consider d being Element of D such that
A10: Z = x /\ d and
verum by A9;
reconsider d = d as Element of (InclPoset (Ids R)) ;
A11: xD = {x} "/\" D by YELLOW_4:42;
then x "/\" d in {x} "/\" D ;
then sup xD >= x "/\" d by A2, A11, LATTICE3:def_9;
then A12: x "/\" d c= sup xD by YELLOW_1:3;
x /\ d = x "/\" d by YELLOW_2:43;
then a in sup xD by A12, A8, A10;
hence a in sup ({x} "/\" D) by YELLOW_4:42; ::_thesis: verum
end;
registration
let R be Semilattice;
cluster InclPoset (Ids R) -> satisfying_MC ;
coherence
InclPoset (Ids R) is satisfying_MC
proof
set I = InclPoset (Ids R);
let x be Element of (InclPoset (Ids R)); :: according to WAYBEL_2:def_6 ::_thesis: for b1 being Element of bool the carrier of (InclPoset (Ids R)) holds x "/\" ("\/" (b1,(InclPoset (Ids R)))) = "\/" (({x} "/\" b1),(InclPoset (Ids R)))
let D be non empty directed Subset of (InclPoset (Ids R)); ::_thesis: x "/\" ("\/" (D,(InclPoset (Ids R)))) = "\/" (({x} "/\" D),(InclPoset (Ids R)))
thus x "/\" (sup D) = x /\ (sup D) by YELLOW_2:43
.= x /\ (union D) by Th3
.= union { (x /\ d) where d is Element of D : verum } by Th1
.= sup ({x} "/\" D) by Th4 ; ::_thesis: verum
end;
end;
registration
let R be 1 -element RelStr ;
cluster -> trivial for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is trivial
proof
let T be TopAugmentation of R; ::_thesis: T is trivial
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
hence T is trivial ; ::_thesis: verum
end;
end;
theorem :: WAYBEL30:5
for S being complete Scott TopLattice
for T being complete LATTICE
for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
proof
let S be complete Scott TopLattice; ::_thesis: for T being complete LATTICE
for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
let T be complete LATTICE; ::_thesis: for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
let A be Scott TopAugmentation of T; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) )
assume A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)
A2: the topology of S = sigma S by WAYBEL14:23
.= sigma T by A1, YELLOW_9:52
.= the topology of A by YELLOW_9:51 ;
RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of S, the InternalRel of S #) by A1, YELLOW_9:def_4;
hence TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by A2; ::_thesis: verum
end;
theorem :: WAYBEL30:6
for N being complete Lawson TopLattice
for T being complete LATTICE
for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
proof
let N be complete Lawson TopLattice; ::_thesis: for T being complete LATTICE
for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
let T be complete LATTICE; ::_thesis: for A being correct Lawson TopAugmentation of T st RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
let A be correct Lawson TopAugmentation of T; ::_thesis: ( RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) implies TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) )
assume A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #)
A2: omega T = omega N by A1, WAYBEL19:3;
set S = the correct Scott TopAugmentation of T;
set l = the correct lower TopAugmentation of T;
A3: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A4: RelStr(# the carrier of the correct Scott TopAugmentation of T, the InternalRel of the correct Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T c= bool the carrier of N
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T or a in bool the carrier of N )
assume a in the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T ; ::_thesis: a in bool the carrier of N
then ( a in the topology of the correct Scott TopAugmentation of T or a in the topology of the correct lower TopAugmentation of T ) by XBOOLE_0:def_3;
hence a in bool the carrier of N by A1, A4, A3; ::_thesis: verum
end;
then reconsider X = the topology of the correct Scott TopAugmentation of T \/ the topology of the correct lower TopAugmentation of T as Subset-Family of N ;
reconsider X = X as Subset-Family of N ;
A5: the topology of the correct lower TopAugmentation of T = omega T by WAYBEL19:def_2;
(sigma N) \/ (omega N) is prebasis of N by WAYBEL19:def_3;
then A6: (sigma T) \/ (omega N) is prebasis of N by A1, YELLOW_9:52;
A7: the topology of the correct Scott TopAugmentation of T = sigma T by YELLOW_9:51;
the carrier of N = the carrier of the correct Scott TopAugmentation of T \/ the carrier of the correct lower TopAugmentation of T by A1, A4, A3;
then N is Refinement of the correct Scott TopAugmentation of T, the correct lower TopAugmentation of T by A2, A6, A5, A7, YELLOW_9:def_6;
then A8: the topology of N = UniCl (FinMeetCl X) by YELLOW_9:56
.= lambda T by A1, A5, A7, WAYBEL19:33
.= the topology of A by WAYBEL19:def_4 ;
RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, YELLOW_9:def_4;
hence TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of N, the InternalRel of N, the topology of N #) by A8; ::_thesis: verum
end;
theorem :: WAYBEL30:7
for N being complete Lawson TopLattice
for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & J is closed holds
A is closed
proof
let N be complete Lawson TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & J is closed holds
A is closed
let S be Scott TopAugmentation of N; ::_thesis: for A being Subset of N
for J being Subset of S st A = J & J is closed holds
A is closed
let A be Subset of N; ::_thesis: for J being Subset of S st A = J & J is closed holds
A is closed
let J be Subset of S; ::_thesis: ( A = J & J is closed implies A is closed )
assume A1: A = J ; ::_thesis: ( not J is closed or A is closed )
assume J is closed ; ::_thesis: A is closed
then A2: ([#] S) \ J is open by PRE_TOPC:def_3;
A3: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then N is correct Lawson TopAugmentation of S by YELLOW_9:def_4;
hence ([#] N) \ A is open by A1, A3, A2, WAYBEL19:37; :: according to PRE_TOPC:def_3 ::_thesis: verum
end;
registration
let A be complete LATTICE;
cluster lambda A -> non empty ;
coherence
not lambda A is empty
proof
set S = the correct Lawson TopAugmentation of A;
not InclPoset the topology of the correct Lawson TopAugmentation of A is trivial ;
hence not lambda A is empty by WAYBEL19:def_4; ::_thesis: verum
end;
end;
registration
let S be complete Scott TopLattice;
cluster InclPoset (sigma S) -> non trivial complete ;
coherence
( InclPoset (sigma S) is complete & not InclPoset (sigma S) is trivial ) ;
end;
registration
let N be complete Lawson TopLattice;
cluster InclPoset (sigma N) -> non trivial complete ;
coherence
( InclPoset (sigma N) is complete & not InclPoset (sigma N) is trivial ) ;
cluster InclPoset (lambda N) -> non trivial complete ;
coherence
( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial )
proof
set S = the correct Lawson TopAugmentation of N;
( InclPoset the topology of the correct Lawson TopAugmentation of N is complete & not InclPoset the topology of the correct Lawson TopAugmentation of N is trivial ) ;
hence ( InclPoset (lambda N) is complete & not InclPoset (lambda N) is trivial ) by WAYBEL19:def_4; ::_thesis: verum
end;
end;
theorem Th8: :: WAYBEL30:8
for T being non empty reflexive RelStr holds sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
proof
let T be non empty reflexive RelStr ; ::_thesis: sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in sigma T or s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
A1: s \ (uparrow ({} T)) = s ;
assume s in sigma T ; ::_thesis: s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
hence s in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A1; ::_thesis: verum
end;
theorem Th9: :: WAYBEL30:9
for N being complete Lawson TopLattice holds lambda N = the topology of N
proof
let N be complete Lawson TopLattice; ::_thesis: lambda N = the topology of N
N is correct Lawson TopAugmentation of N by YELLOW_9:44;
hence lambda N = the topology of N by WAYBEL19:def_4; ::_thesis: verum
end;
theorem Th10: :: WAYBEL30:10
for N being complete Lawson TopLattice holds sigma N c= lambda N
proof
let N be complete Lawson TopLattice; ::_thesis: sigma N c= lambda N
set Z = { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } ;
{ (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } is Basis of N by WAYBEL19:32;
then { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } c= the topology of N by TOPS_2:64;
then A1: { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } c= lambda N by Th9;
sigma N c= { (W \ (uparrow F)) where W, F is Subset of N : ( W in sigma N & F is finite ) } by Th8;
hence sigma N c= lambda N by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: WAYBEL30:11
for M, N being complete LATTICE st RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) holds
lambda M = lambda N
proof
let M, N be complete LATTICE; ::_thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) implies lambda M = lambda N )
assume A1: RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of N, the InternalRel of N #) ; ::_thesis: lambda M = lambda N
A2: lambda N = UniCl (FinMeetCl ((sigma N) \/ (omega N))) by WAYBEL19:33;
A3: lambda M = UniCl (FinMeetCl ((sigma M) \/ (omega M))) by WAYBEL19:33;
sigma M = sigma N by A1, YELLOW_9:52;
hence lambda M = lambda N by A1, A3, A2, WAYBEL19:3; ::_thesis: verum
end;
theorem Th12: :: WAYBEL30:12
for N being complete Lawson TopLattice
for X being Subset of N holds
( X in lambda N iff X is open )
proof
let N be complete Lawson TopLattice; ::_thesis: for X being Subset of N holds
( X in lambda N iff X is open )
let X be Subset of N; ::_thesis: ( X in lambda N iff X is open )
lambda N = the topology of N by Th9;
hence ( X in lambda N iff X is open ) by PRE_TOPC:def_2; ::_thesis: verum
end;
registration
cluster1 -element TopSpace-like reflexive -> 1 -element reflexive Scott for TopRelStr ;
coherence
for b1 being 1 -element reflexive TopRelStr st b1 is TopSpace-like holds
b1 is Scott
proof
let T be 1 -element reflexive TopRelStr ; ::_thesis: ( T is TopSpace-like implies T is Scott )
assume T is TopSpace-like ; ::_thesis: T is Scott
then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ;
W is Scott
proof
let S be Subset of W; :: according to WAYBEL11:def_5 ::_thesis: ( ( not S is open or S is upper ) & ( not S is upper or S is open ) )
thus ( S is open implies S is upper ) ; ::_thesis: ( not S is upper or S is open )
thus ( not S is upper or S is open ) by TDLAT_3:15; ::_thesis: verum
end;
hence T is Scott ; ::_thesis: verum
end;
end;
registration
cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete -> complete Lawson for TopRelStr ;
coherence
for b1 being complete TopLattice st b1 is trivial holds
b1 is Lawson
proof
let T be complete TopLattice; ::_thesis: ( T is trivial implies T is Lawson )
assume T is trivial ; ::_thesis: T is Lawson
then the carrier of T is 1 -element ;
then reconsider W = T as 1 -element complete TopLattice by STRUCT_0:def_19;
set N = the correct Lawson TopAugmentation of W;
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of the correct Lawson TopAugmentation of W, the InternalRel of the correct Lawson TopAugmentation of W #) by YELLOW_9:def_4;
the topology of W = {{}, the carrier of W} by TDLAT_3:def_2;
then the topology of T = the topology of the correct Lawson TopAugmentation of W by A1, TDLAT_3:def_2
.= lambda T by WAYBEL19:def_4
.= UniCl (FinMeetCl ((sigma T) \/ (omega T))) by WAYBEL19:33 ;
then FinMeetCl ((omega T) \/ (sigma T)) is Basis of T by YELLOW_9:22;
hence (omega T) \/ (sigma T) is prebasis of T by YELLOW_9:23; :: according to WAYBEL19:def_3 ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Scott continuous non void meet-continuous for TopRelStr ;
existence
ex b1 being complete TopLattice st
( b1 is strict & b1 is continuous & b1 is lower-bounded & b1 is meet-continuous & b1 is Scott )
proof
set A = the 1 -element strict TopLattice;
take the 1 -element strict TopLattice ; ::_thesis: ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is continuous & the 1 -element strict TopLattice is lower-bounded & the 1 -element strict TopLattice is meet-continuous & the 1 -element strict TopLattice is Scott )
thus ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is continuous & the 1 -element strict TopLattice is lower-bounded & the 1 -element strict TopLattice is meet-continuous & the 1 -element strict TopLattice is Scott ) ; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like Hausdorff reflexive transitive antisymmetric lower-bounded upper-bounded V155() up-complete /\-complete with_suprema with_infima complete strict Lawson continuous non void compact for TopRelStr ;
existence
ex b1 being complete TopLattice st
( b1 is strict & b1 is continuous & b1 is compact & b1 is Hausdorff & b1 is Lawson )
proof
set R = the trivial complete strict TopLattice;
take the trivial complete strict TopLattice ; ::_thesis: ( the trivial complete strict TopLattice is strict & the trivial complete strict TopLattice is continuous & the trivial complete strict TopLattice is compact & the trivial complete strict TopLattice is Hausdorff & the trivial complete strict TopLattice is Lawson )
thus ( the trivial complete strict TopLattice is strict & the trivial complete strict TopLattice is continuous & the trivial complete strict TopLattice is compact & the trivial complete strict TopLattice is Hausdorff & the trivial complete strict TopLattice is Lawson ) ; ::_thesis: verum
end;
end;
scheme :: WAYBEL30:sch 1
EmptySch{ F1() -> Scott TopLattice, F2() -> set , F3( set ) -> set } :
{ F3(w) where w is Element of F1() : w in {} } = {}
proof
thus { F3(w) where w is Element of F1() : w in {} } c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= { F3(w) where w is Element of F1() : w in {} }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F3(w) where w is Element of F1() : w in {} } or a in {} )
assume a in { F3(w) where w is Element of F1() : w in {} } ; ::_thesis: a in {}
then A1: ex w being Element of F1() st
( a = F3(w) & w in {} ) ;
assume not a in {} ; ::_thesis: contradiction
thus contradiction by A1; ::_thesis: verum
end;
thus {} c= { F3(w) where w is Element of F1() : w in {} } by XBOOLE_1:2; ::_thesis: verum
end;
theorem Th13: :: WAYBEL30:13
for N being meet-continuous LATTICE
for A being Subset of N st A is property(S) holds
uparrow A is property(S)
proof
let N be meet-continuous LATTICE; ::_thesis: for A being Subset of N st A is property(S) holds
uparrow A is property(S)
let A be Subset of N; ::_thesis: ( A is property(S) implies uparrow A is property(S) )
assume A1: for D being non empty directed Subset of N st sup D in A holds
ex y being Element of N st
( y in D & ( for x being Element of N st x in D & x >= y holds
x in A ) ) ; :: according to WAYBEL11:def_3 ::_thesis: uparrow A is property(S)
let D be non empty directed Subset of N; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,N) in uparrow A or ex b1 being Element of the carrier of N st
( b1 in D & ( for b2 being Element of the carrier of N holds
( not b2 in D or not b1 <= b2 or b2 in uparrow A ) ) ) )
assume sup D in uparrow A ; ::_thesis: ex b1 being Element of the carrier of N st
( b1 in D & ( for b2 being Element of the carrier of N holds
( not b2 in D or not b1 <= b2 or b2 in uparrow A ) ) )
then consider a being Element of N such that
A2: a <= sup D and
A3: a in A by WAYBEL_0:def_16;
reconsider aa = {a} as non empty directed Subset of N by WAYBEL_0:5;
a = sup ({a} "/\" D) by A2, WAYBEL_2:52;
then consider y being Element of N such that
A4: y in aa "/\" D and
A5: for x being Element of N st x in aa "/\" D & x >= y holds
x in A by A1, A3;
aa "/\" D = { (a "/\" d) where d is Element of N : d in D } by YELLOW_4:42;
then consider d being Element of N such that
A6: y = a "/\" d and
A7: d in D by A4;
take d ; ::_thesis: ( d in D & ( for b1 being Element of the carrier of N holds
( not b1 in D or not d <= b1 or b1 in uparrow A ) ) )
thus d in D by A7; ::_thesis: for b1 being Element of the carrier of N holds
( not b1 in D or not d <= b1 or b1 in uparrow A )
let x be Element of N; ::_thesis: ( not x in D or not d <= x or x in uparrow A )
assume that
x in D and
A8: x >= d ; ::_thesis: x in uparrow A
d >= y by A6, YELLOW_0:23;
then A9: x >= y by A8, ORDERS_2:3;
y in A by A4, A5, ORDERS_2:1;
hence x in uparrow A by A9, WAYBEL_0:def_16; ::_thesis: verum
end;
registration
let N be meet-continuous LATTICE;
let A be property(S) Subset of N;
cluster uparrow A -> property(S) ;
coherence
uparrow A is property(S) by Th13;
end;
theorem Th14: :: WAYBEL30:14
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for A being Subset of N st A in lambda N holds
uparrow A in sigma S
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for A being Subset of N st A in lambda N holds
uparrow A in sigma S
let S be Scott TopAugmentation of N; ::_thesis: for A being Subset of N st A in lambda N holds
uparrow A in sigma S
let A be Subset of N; ::_thesis: ( A in lambda N implies uparrow A in sigma S )
assume A in lambda N ; ::_thesis: uparrow A in sigma S
then A1: A is open by Th12;
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider Y = A as Subset of S ;
A3: S is meet-continuous by A2, YELLOW12:14;
reconsider UA = uparrow A as Subset of S by A2;
A4: uparrow A = uparrow Y by A2, WAYBEL_0:13;
Y is property(S) by A1, A2, WAYBEL19:36, YELLOW12:19;
then UA is open by A3, A4, WAYBEL11:15;
then uparrow A in the topology of S by PRE_TOPC:def_2;
hence uparrow A in sigma S by WAYBEL14:23; ::_thesis: verum
end;
theorem Th15: :: WAYBEL30:15
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & A is open holds
uparrow J is open
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for A being Subset of N
for J being Subset of S st A = J & A is open holds
uparrow J is open
let S be Scott TopAugmentation of N; ::_thesis: for A being Subset of N
for J being Subset of S st A = J & A is open holds
uparrow J is open
let A be Subset of N; ::_thesis: for J being Subset of S st A = J & A is open holds
uparrow J is open
let J be Subset of S; ::_thesis: ( A = J & A is open implies uparrow J is open )
assume A1: A = J ; ::_thesis: ( not A is open or uparrow J is open )
assume A is open ; ::_thesis: uparrow J is open
then A in lambda N by Th12;
then A2: uparrow A in sigma S by Th14;
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then uparrow J in sigma S by A2, A1, WAYBEL_0:13;
hence uparrow J is open by WAYBEL14:24; ::_thesis: verum
end;
theorem Th16: :: WAYBEL30:16
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for x being Point of S
for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for x being Point of S
for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let S be Scott TopAugmentation of N; ::_thesis: for x being Point of S
for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let x be Point of S; ::_thesis: for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let y be Point of N; ::_thesis: for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let J be Basis of y; ::_thesis: ( x = y implies { (uparrow A) where A is Subset of N : A in J } is Basis of x )
assume A1: x = y ; ::_thesis: { (uparrow A) where A is Subset of N : A in J } is Basis of x
set Z = { (uparrow A) where A is Subset of N : A in J } ;
set K = { (uparrow A) where A is Subset of N : A in J } ;
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
{ (uparrow A) where A is Subset of N : A in J } c= bool the carrier of S
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (uparrow A) where A is Subset of N : A in J } or k in bool the carrier of S )
assume k in { (uparrow A) where A is Subset of N : A in J } ; ::_thesis: k in bool the carrier of S
then ex A being Subset of N st
( k = uparrow A & A in J ) ;
hence k in bool the carrier of S by A2; ::_thesis: verum
end;
then reconsider K = { (uparrow A) where A is Subset of N : A in J } as Subset-Family of S ;
K is Basis of x
proof
A3: K is open
proof
let k be Subset of S; :: according to TOPS_2:def_1 ::_thesis: ( not k in K or k is open )
assume k in K ; ::_thesis: k is open
then consider A being Subset of N such that
A4: k = uparrow A and
A5: A in J ;
reconsider A9 = A as Subset of S by A2;
uparrow A9 is open by A5, Th15, YELLOW_8:12;
then uparrow A9 in the topology of S by PRE_TOPC:def_2;
then uparrow A in the topology of S by A2, WAYBEL_0:13;
hence k is open by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
K is x -quasi_basis
proof
for k being set st k in K holds
x in k
proof
let k be set ; ::_thesis: ( k in K implies x in k )
assume k in K ; ::_thesis: x in k
then consider A being Subset of N such that
A6: k = uparrow A and
A7: A in J ;
A8: A c= uparrow A by WAYBEL_0:16;
y in Intersect J by YELLOW_8:def_1;
then y in A by A7, SETFAM_1:43;
hence x in k by A8, A1, A6; ::_thesis: verum
end;
hence x in Intersect K by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of S holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of S st
( b2 in K & b2 c= b1 ) )
let sA be Subset of S; ::_thesis: ( not sA is open or not x in sA or ex b1 being Element of bool the carrier of S st
( b1 in K & b1 c= sA ) )
assume that
A9: sA is open and
A10: x in sA ; ::_thesis: ex b1 being Element of bool the carrier of S st
( b1 in K & b1 c= sA )
sA is upper by A9, WAYBEL11:def_4;
then A11: uparrow sA c= sA by WAYBEL_0:24;
reconsider lA = sA as Subset of N by A2;
N is correct Lawson TopAugmentation of S by A2, YELLOW_9:def_4;
then lA is open by A9, WAYBEL19:37;
then lA in lambda N by Th12;
then A12: uparrow lA in sigma S by Th14;
A13: lA c= uparrow lA by WAYBEL_0:16;
sigma N c= lambda N by Th10;
then sigma S c= lambda N by A2, YELLOW_9:52;
then uparrow lA is open by A12, Th12;
then consider lV1 being Subset of N such that
A14: lV1 in J and
A15: lV1 c= uparrow lA by A13, A1, A10, YELLOW_8:def_1;
reconsider sUV = uparrow lV1 as Subset of S by A2;
take sUV ; ::_thesis: ( sUV in K & sUV c= sA )
thus sUV in K by A14; ::_thesis: sUV c= sA
A16: lV1 is_coarser_than uparrow lA by A15, WAYBEL12:16;
sA c= uparrow sA by WAYBEL_0:16;
then A17: sA = uparrow sA by A11, XBOOLE_0:def_10;
uparrow sA = uparrow lA by A2, WAYBEL_0:13;
hence sUV c= sA by A16, A17, YELLOW12:28; ::_thesis: verum
end;
hence K is Basis of x by A3; ::_thesis: verum
end;
hence { (uparrow A) where A is Subset of N : A in J } is Basis of x ; ::_thesis: verum
end;
theorem Th17: :: WAYBEL30:17
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for X being upper Subset of N
for Y being Subset of S st X = Y holds
Int X = Int Y
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for X being upper Subset of N
for Y being Subset of S st X = Y holds
Int X = Int Y
let S be Scott TopAugmentation of N; ::_thesis: for X being upper Subset of N
for Y being Subset of S st X = Y holds
Int X = Int Y
let X be upper Subset of N; ::_thesis: for Y being Subset of S st X = Y holds
Int X = Int Y
let Y be Subset of S; ::_thesis: ( X = Y implies Int X = Int Y )
assume A1: X = Y ; ::_thesis: Int X = Int Y
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider K = uparrow (Int X) as Subset of S ;
reconsider sX = Int X as Subset of S by A2;
A3: K c= Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in K or a in Y )
A4: Int X c= X by TOPS_1:16;
assume A5: a in K ; ::_thesis: a in Y
then reconsider x = a as Element of N ;
A6: X c= uparrow X by WAYBEL_0:16;
uparrow X c= X by WAYBEL_0:24;
then A7: uparrow X = X by A6, XBOOLE_0:def_10;
ex y being Element of N st
( y <= x & y in Int X ) by A5, WAYBEL_0:def_16;
hence a in Y by A7, A1, A4, WAYBEL_0:def_16; ::_thesis: verum
end;
A8: Int X c= uparrow (Int X) by WAYBEL_0:16;
uparrow sX is open by Th15;
then K is open by A2, WAYBEL_0:13;
then uparrow (Int X) c= Int Y by A3, TOPS_1:24;
hence Int X c= Int Y by A8, XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: Int Y c= Int X
reconsider A = Int Y as Subset of N by A2;
N is correct Lawson TopAugmentation of S by A2, YELLOW_9:def_4;
then A is open by WAYBEL19:37;
hence Int Y c= Int X by A1, TOPS_1:16, TOPS_1:24; ::_thesis: verum
end;
theorem :: WAYBEL30:18
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for X being lower Subset of N
for Y being Subset of S st X = Y holds
Cl X = Cl Y
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for X being lower Subset of N
for Y being Subset of S st X = Y holds
Cl X = Cl Y
let S be Scott TopAugmentation of N; ::_thesis: for X being lower Subset of N
for Y being Subset of S st X = Y holds
Cl X = Cl Y
let X be lower Subset of N; ::_thesis: for Y being Subset of S st X = Y holds
Cl X = Cl Y
let Y be Subset of S; ::_thesis: ( X = Y implies Cl X = Cl Y )
assume A1: X = Y ; ::_thesis: Cl X = Cl Y
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider A = Cl Y as Subset of N ;
(Cl X) ` = (Cl ((X `) `)) `
.= Int (X `) by TOPS_1:def_1
.= Int (Y `) by A1, A2, Th17
.= (Cl ((Y `) `)) ` by TOPS_1:def_1
.= A ` by A2 ;
hence Cl X = Cl Y by TOPS_1:1; ::_thesis: verum
end;
theorem Th19: :: WAYBEL30:19
for M, N being complete LATTICE
for LM being correct Lawson TopAugmentation of M
for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
the topology of [:LM,LN:] = lambda [:M,N:]
proof
let M, N be complete LATTICE; ::_thesis: for LM being correct Lawson TopAugmentation of M
for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
the topology of [:LM,LN:] = lambda [:M,N:]
let LM be correct Lawson TopAugmentation of M; ::_thesis: for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
the topology of [:LM,LN:] = lambda [:M,N:]
let LN be correct Lawson TopAugmentation of N; ::_thesis: ( InclPoset (sigma N) is continuous implies the topology of [:LM,LN:] = lambda [:M,N:] )
assume A1: InclPoset (sigma N) is continuous ; ::_thesis: the topology of [:LM,LN:] = lambda [:M,N:]
set SMN = the non empty correct Scott TopAugmentation of [:M,N:];
set lMN = the non empty correct lower TopAugmentation of [:M,N:];
set LMN = the non empty correct Lawson TopAugmentation of [:M,N:];
A2: [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #)
proof
set lN = the non empty correct lower TopAugmentation of N;
set lM = the non empty correct lower TopAugmentation of M;
set SN = the non empty correct Scott TopAugmentation of N;
set SM = the non empty correct Scott TopAugmentation of M;
A3: LN is Refinement of the non empty correct Scott TopAugmentation of N, the non empty correct lower TopAugmentation of N by WAYBEL19:29;
A4: RelStr(# the carrier of the non empty correct lower TopAugmentation of N, the InternalRel of the non empty correct lower TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
(omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of the non empty correct Lawson TopAugmentation of [:M,N:] by WAYBEL19:def_3;
then A5: (omega the non empty correct Lawson TopAugmentation of [:M,N:]) \/ (sigma the non empty correct Lawson TopAugmentation of [:M,N:]) is prebasis of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by YELLOW12:33;
A6: RelStr(# the carrier of LM, the InternalRel of LM #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4;
A7: RelStr(# the carrier of LN, the InternalRel of LN #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
A8: RelStr(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the InternalRel of the non empty correct Lawson TopAugmentation of [:M,N:] #) = RelStr(# the carrier of [:M,N:], the InternalRel of [:M,N:] #) by YELLOW_9:def_4;
A9: the carrier of [:LM,LN:] = [: the carrier of LM, the carrier of LN:] by BORSUK_1:def_2
.= the carrier of the non empty correct Lawson TopAugmentation of [:M,N:] by A6, A7, A8, YELLOW_3:def_2 ;
A10: the topology of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] = omega [:M,N:] by WAYBEL19:15
.= omega the non empty correct Lawson TopAugmentation of [:M,N:] by A8, WAYBEL19:3 ;
A11: RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4
.= RelStr(# the carrier of (Sigma M), the InternalRel of (Sigma M) #) by YELLOW_9:def_4 ;
then A12: TopStruct(# the carrier of the non empty correct Scott TopAugmentation of M, the topology of the non empty correct Scott TopAugmentation of M #) = TopStruct(# the carrier of (Sigma M), the topology of (Sigma M) #) by WAYBEL29:13;
A13: RelStr(# the carrier of the non empty correct lower TopAugmentation of M, the InternalRel of the non empty correct lower TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4;
RelStr(# the carrier of the non empty correct Scott TopAugmentation of N, the InternalRel of the non empty correct Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4
.= RelStr(# the carrier of (Sigma N), the InternalRel of (Sigma N) #) by YELLOW_9:def_4 ;
then TopStruct(# the carrier of the non empty correct Scott TopAugmentation of N, the topology of the non empty correct Scott TopAugmentation of N #) = TopStruct(# the carrier of (Sigma N), the topology of (Sigma N) #) by WAYBEL29:13;
then A14: the topology of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] = the topology of [:(Sigma M),(Sigma N):] by A12, WAYBEL29:7
.= sigma [:M,N:] by A1, WAYBEL29:30
.= sigma the non empty correct Lawson TopAugmentation of [:M,N:] by A8, YELLOW_9:52 ;
A15: RelStr(# the carrier of the non empty correct Scott TopAugmentation of M, the InternalRel of the non empty correct Scott TopAugmentation of M #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4;
A16: LM is Refinement of the non empty correct Scott TopAugmentation of M, the non empty correct lower TopAugmentation of M by WAYBEL19:29;
then [:LM,LN:] is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A3, A15, A11, A13, A4, YELLOW12:50;
then the carrier of TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) = the carrier of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:] \/ the carrier of [: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A9, YELLOW_9:def_6;
then TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) is Refinement of [: the non empty correct Scott TopAugmentation of M, the non empty correct Scott TopAugmentation of N:],[: the non empty correct lower TopAugmentation of M, the non empty correct lower TopAugmentation of N:] by A5, A14, A10, YELLOW_9:def_6;
hence [:LM,LN:] = TopStruct(# the carrier of the non empty correct Lawson TopAugmentation of [:M,N:], the topology of the non empty correct Lawson TopAugmentation of [:M,N:] #) by A16, A3, A15, A11, A13, A4, A9, YELLOW12:49; ::_thesis: verum
end;
the non empty correct Lawson TopAugmentation of [:M,N:] is Refinement of the non empty correct Scott TopAugmentation of [:M,N:], the non empty correct lower TopAugmentation of [:M,N:] by WAYBEL19:29;
then reconsider R = [:LM,LN:] as Refinement of the non empty correct Scott TopAugmentation of [:M,N:], the non empty correct lower TopAugmentation of [:M,N:] by A2, YELLOW12:47;
the topology of [:LM,LN:] = the topology of R ;
hence the topology of [:LM,LN:] = lambda [:M,N:] by WAYBEL19:34; ::_thesis: verum
end;
theorem Th20: :: WAYBEL30:20
for M, N being complete LATTICE
for P being correct Lawson TopAugmentation of [:M,N:]
for Q being correct Lawson TopAugmentation of M
for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]
proof
let M, N be complete LATTICE; ::_thesis: for P being correct Lawson TopAugmentation of [:M,N:]
for Q being correct Lawson TopAugmentation of M
for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]
let P be correct Lawson TopAugmentation of [:M,N:]; ::_thesis: for Q being correct Lawson TopAugmentation of M
for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]
let Q be correct Lawson TopAugmentation of M; ::_thesis: for R being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]
let R be correct Lawson TopAugmentation of N; ::_thesis: ( InclPoset (sigma N) is continuous implies TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] )
assume A1: InclPoset (sigma N) is continuous ; ::_thesis: TopStruct(# the carrier of P, the topology of P #) = [:Q,R:]
A2: the topology of P = lambda [:M,N:] by WAYBEL19:def_4
.= the topology of [:Q,R:] by A1, Th19 ;
A3: RelStr(# the carrier of Q, the InternalRel of Q #) = RelStr(# the carrier of M, the InternalRel of M #) by YELLOW_9:def_4;
A4: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
RelStr(# the carrier of P, the InternalRel of P #) = RelStr(# the carrier of [:M,N:], the InternalRel of [:M,N:] #) by YELLOW_9:def_4;
then the carrier of P = [: the carrier of Q, the carrier of N:] by A3, YELLOW_3:def_2
.= the carrier of [:Q,R:] by A4, BORSUK_1:def_2 ;
hence TopStruct(# the carrier of P, the topology of P #) = [:Q,R:] by A2; ::_thesis: verum
end;
theorem Th21: :: WAYBEL30:21
for N being complete Lawson meet-continuous TopLattice
for x being Element of N holds x "/\" is continuous
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for x being Element of N holds x "/\" is continuous
let x be Element of N; ::_thesis: x "/\" is continuous
for X being non empty Subset of N holds x "/\" preserves_inf_of X by YELLOW13:11;
hence x "/\" is continuous by WAYBEL21:45; ::_thesis: verum
end;
registration
let N be complete Lawson meet-continuous TopLattice;
let x be Element of N;
clusterx "/\" -> continuous ;
coherence
x "/\" is continuous by Th21;
end;
theorem Th22: :: WAYBEL30:22
for N being complete Lawson meet-continuous TopLattice st InclPoset (sigma N) is continuous holds
N is topological_semilattice
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( InclPoset (sigma N) is continuous implies N is topological_semilattice )
assume A1: InclPoset (sigma N) is continuous ; ::_thesis: N is topological_semilattice
set NN = the correct Lawson TopAugmentation of [:N,N:];
N is TopAugmentation of N by YELLOW_9:44;
then A2: TopStruct(# the carrier of the correct Lawson TopAugmentation of [:N,N:], the topology of the correct Lawson TopAugmentation of [:N,N:] #) = [:N,N:] by A1, Th20;
A3: RelStr(# the carrier of the correct Lawson TopAugmentation of [:N,N:], the InternalRel of the correct Lawson TopAugmentation of [:N,N:] #) = RelStr(# the carrier of [:N,N:], the InternalRel of [:N,N:] #) by YELLOW_9:def_4;
then reconsider h = inf_op N as Function of the correct Lawson TopAugmentation of [:N,N:],N ;
A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N, the InternalRel of N #) ;
A5: h is directed-sups-preserving
proof
let X be Subset of the correct Lawson TopAugmentation of [:N,N:]; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or h preserves_sup_of X )
assume ( not X is empty & X is directed ) ; ::_thesis: h preserves_sup_of X
then reconsider X1 = X as non empty directed Subset of [:N,N:] by A3, WAYBEL_0:3;
inf_op N preserves_sup_of X1 by WAYBEL_0:def_37;
hence h preserves_sup_of X by A3, A4, WAYBEL_0:65; ::_thesis: verum
end;
A6: h is infs-preserving
proof
let X be Subset of the correct Lawson TopAugmentation of [:N,N:]; :: according to WAYBEL_0:def_32 ::_thesis: h preserves_inf_of X
reconsider X1 = X as Subset of [:N,N:] by A3;
inf_op N preserves_inf_of X1 by WAYBEL_0:def_32;
hence h preserves_inf_of X by A3, A4, WAYBEL_0:65; ::_thesis: verum
end;
then h is SemilatticeHomomorphism of the correct Lawson TopAugmentation of [:N,N:],N by WAYBEL21:5;
then A7: h is continuous by A5, A6, WAYBEL21:46;
A8: TopStruct(# the carrier of N, the topology of N #) = TopStruct(# the carrier of N, the topology of N #) ;
let g be Function of [:N,N:],N; :: according to YELLOW13:def_5 ::_thesis: ( not R16( the carrier of [:N,N:], the carrier of N, the carrier of [:N,N:], the carrier of N,g, inf_op N) or g is continuous )
assume g = inf_op N ; ::_thesis: g is continuous
hence g is continuous by A2, A7, A8, YELLOW12:36; ::_thesis: verum
end;
Lm3: now__::_thesis:_for_S,_T,_x1,_x2_being_set_st_x1_in_S_&_x2_in_T_holds_
<:(pr2_(S,T)),(pr1_(S,T)):>_._[x1,x2]_=_[x2,x1]
let S, T, x1, x2 be set ; ::_thesis: ( x1 in S & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1] )
assume that
A1: x1 in S and
A2: x2 in T ; ::_thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [x2,x1]
A3: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def_7
.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def_4
.= [:S,T:] /\ [:S,T:] by FUNCT_3:def_5
.= [:S,T:] ;
[x1,x2] in [:S,T:] by A1, A2, ZFMISC_1:87;
hence <:(pr2 (S,T)),(pr1 (S,T)):> . [x1,x2] = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A3, FUNCT_3:def_7
.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, A2, FUNCT_3:def_5
.= [x2,x1] by A1, A2, FUNCT_3:def_4 ;
::_thesis: verum
end;
theorem :: WAYBEL30:23
for N being complete Lawson meet-continuous TopLattice st InclPoset (sigma N) is continuous holds
( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed )
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( InclPoset (sigma N) is continuous implies ( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed ) )
assume A1: InclPoset (sigma N) is continuous ; ::_thesis: ( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed )
A2: [: the carrier of N, the carrier of N:] = the carrier of [:N,N:] by BORSUK_1:def_2;
hereby ::_thesis: ( ( for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed ) implies N is Hausdorff )
reconsider D = id the carrier of N as Subset of [:N,N:] by BORSUK_1:def_2;
set INF = inf_op N;
set f = <:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):>;
assume N is Hausdorff ; ::_thesis: for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed
then A3: D is closed by YELLOW12:46;
A4: the carrier of [:N,N:] = [: the carrier of N, the carrier of N:] by YELLOW_3:def_2;
then reconsider f = <:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):> as Function of [:N,N:],[:N,N:] by A2, FUNCT_3:58;
let X be Subset of [:N,N:]; ::_thesis: ( X = the InternalRel of N implies X is closed )
assume A5: X = the InternalRel of N ; ::_thesis: X is closed
A6: for x, y being Element of N holds f . [x,y] = [x,(x "/\" y)]
proof
let x, y be Element of N; ::_thesis: f . [x,y] = [x,(x "/\" y)]
A7: dom (pr1 ( the carrier of N, the carrier of N)) = [: the carrier of N, the carrier of N:] by FUNCT_2:def_1;
A8: [x,y] in [: the carrier of N, the carrier of N:] by ZFMISC_1:87;
dom (inf_op N) = [: the carrier of N, the carrier of N:] by A4, FUNCT_2:def_1;
hence f . [x,y] = [((pr1 ( the carrier of N, the carrier of N)) . (x,y)),((inf_op N) . (x,y))] by A8, A7, FUNCT_3:49
.= [x,((inf_op N) . (x,y))] by FUNCT_3:def_4
.= [x,(x "/\" y)] by WAYBEL_2:def_4 ;
::_thesis: verum
end;
A9: X = f " D
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: f " D c= X
let a be set ; ::_thesis: ( a in X implies a in f " D )
assume A10: a in X ; ::_thesis: a in f " D
then consider s, t being set such that
A11: s in the carrier of N and
A12: t in the carrier of N and
A13: a = [s,t] by A5, ZFMISC_1:def_2;
reconsider s = s, t = t as Element of N by A11, A12;
s <= t by A5, A10, A13, ORDERS_2:def_5;
then s "/\" t = s by YELLOW_0:25;
then f . [s,t] = [s,s] by A6;
then A14: f . a in D by A13, RELAT_1:def_10;
dom f = the carrier of [:N,N:] by FUNCT_2:def_1;
then a in dom f by A2, A11, A12, A13, ZFMISC_1:87;
hence a in f " D by A14, FUNCT_1:def_7; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f " D or a in X )
assume A15: a in f " D ; ::_thesis: a in X
then A16: f . a in D by FUNCT_1:def_7;
consider s, t being set such that
A17: s in the carrier of N and
A18: t in the carrier of N and
A19: a = [s,t] by A2, A15, ZFMISC_1:def_2;
reconsider s = s, t = t as Element of N by A17, A18;
f . a = [s,(s "/\" t)] by A6, A19;
then s = s "/\" t by A16, RELAT_1:def_10;
then s <= t by YELLOW_0:25;
hence a in X by A5, A19, ORDERS_2:def_5; ::_thesis: verum
end;
reconsider INF = inf_op N as Function of [:N,N:],N by A2, A4;
N is topological_semilattice by A1, Th22;
then A20: INF is continuous by YELLOW13:def_5;
pr1 ( the carrier of N, the carrier of N) is continuous Function of [:N,N:],N by YELLOW12:39;
then f is continuous by A20, YELLOW12:41;
hence X is closed by A9, A3, PRE_TOPC:def_6; ::_thesis: verum
end;
assume A21: for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed ; ::_thesis: N is Hausdorff
A22: the InternalRel of N /\ the InternalRel of (N ~) c= id the carrier of N by YELLOW12:23;
id the carrier of N c= the InternalRel of N /\ the InternalRel of (N ~) by YELLOW12:22;
then A23: id the carrier of N = the InternalRel of N /\ the InternalRel of (N ~) by A22, XBOOLE_0:def_10;
for A being Subset of [:N,N:] st A = id the carrier of N holds
A is closed
proof
reconsider f = <:(pr2 ( the carrier of N, the carrier of N)),(pr1 ( the carrier of N, the carrier of N)):> as continuous Function of [:N,N:],[:N,N:] by YELLOW12:42;
reconsider X = the InternalRel of N, Y = the InternalRel of (N ~) as Subset of [:N,N:] by BORSUK_1:def_2;
let A be Subset of [:N,N:]; ::_thesis: ( A = id the carrier of N implies A is closed )
assume A24: A = id the carrier of N ; ::_thesis: A is closed
reconsider X = X, Y = Y as Subset of [:N,N:] ;
A25: X is closed by A21;
A26: dom f = [: the carrier of N, the carrier of N:] by YELLOW12:4;
A27: f .: X = Y
proof
thus f .: X c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= f .: X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in Y )
assume y in f .: X ; ::_thesis: y in Y
then consider x being set such that
x in dom f and
A28: x in X and
A29: y = f . x by FUNCT_1:def_6;
consider x1, x2 being set such that
A30: x1 in the carrier of N and
A31: x2 in the carrier of N and
A32: x = [x1,x2] by A28, ZFMISC_1:def_2;
f . x = [x2,x1] by A30, A31, A32, Lm3;
hence y in Y by A28, A29, A32, RELAT_1:def_7; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in f .: X )
assume A33: y in Y ; ::_thesis: y in f .: X
then consider y1, y2 being set such that
A34: y1 in the carrier of N and
A35: y2 in the carrier of N and
A36: y = [y1,y2] by ZFMISC_1:def_2;
A37: [y2,y1] in X by A33, A36, RELAT_1:def_7;
f . [y2,y1] = y by A34, A35, A36, Lm3;
hence y in f .: X by A26, A37, FUNCT_1:def_6; ::_thesis: verum
end;
f is being_homeomorphism by YELLOW12:43;
then Y is closed by A25, A27, TOPS_2:58;
hence A is closed by A23, A24, A25; ::_thesis: verum
end;
hence N is Hausdorff by YELLOW12:46; ::_thesis: verum
end;
definition
let N be non empty reflexive RelStr ;
let X be Subset of N;
funcX ^0 -> Subset of N equals :: WAYBEL30:def 1
{ u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D } ;
coherence
{ u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D } is Subset of N
proof
defpred S1[ Element of N] means for D being non empty directed Subset of N st $1 <= sup D holds
X meets D;
thus { u where u is Element of N : S1[u] } is Subset of N from DOMAIN_1:sch_7(); ::_thesis: verum
end;
end;
:: deftheorem defines ^0 WAYBEL30:def_1_:_
for N being non empty reflexive RelStr
for X being Subset of N holds X ^0 = { u where u is Element of N : for D being non empty directed Subset of N st u <= sup D holds
X meets D } ;
registration
let N be non empty reflexive antisymmetric RelStr ;
let X be empty Subset of N;
clusterX ^0 -> empty ;
coherence
X ^0 is empty
proof
X ^0 c= {}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X ^0 or a in {} )
assume that
A1: a in X ^0 and
not a in {} ; ::_thesis: contradiction
consider u being Element of N such that
a = u and
A2: for D being non empty directed Subset of N st u <= sup D holds
X meets D by A1;
reconsider D = {u} as non empty directed Subset of N by WAYBEL_0:5;
A3: X misses D by XBOOLE_1:65;
u <= sup D by YELLOW_0:39;
hence contradiction by A3, A2; ::_thesis: verum
end;
hence X ^0 is empty ; ::_thesis: verum
end;
end;
theorem :: WAYBEL30:24
for N being non empty reflexive RelStr
for A, J being Subset of N st A c= J holds
A ^0 c= J ^0
proof
let N be non empty reflexive RelStr ; ::_thesis: for A, J being Subset of N st A c= J holds
A ^0 c= J ^0
let A, J be Subset of N; ::_thesis: ( A c= J implies A ^0 c= J ^0 )
assume A1: A c= J ; ::_thesis: A ^0 c= J ^0
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A ^0 or a in J ^0 )
assume a in A ^0 ; ::_thesis: a in J ^0
then consider u being Element of N such that
A2: a = u and
A3: for D being non empty directed Subset of N st u <= sup D holds
A meets D ;
for D being non empty directed Subset of N st u <= sup D holds
J meets D by A1, A3, XBOOLE_1:63;
hence a in J ^0 by A2; ::_thesis: verum
end;
theorem Th25: :: WAYBEL30:25
for N being non empty reflexive RelStr
for x being Element of N holds (uparrow x) ^0 = wayabove x
proof
let N be non empty reflexive RelStr ; ::_thesis: for x being Element of N holds (uparrow x) ^0 = wayabove x
let x be Element of N; ::_thesis: (uparrow x) ^0 = wayabove x
thus (uparrow x) ^0 c= wayabove x :: according to XBOOLE_0:def_10 ::_thesis: wayabove x c= (uparrow x) ^0
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (uparrow x) ^0 or a in wayabove x )
assume a in (uparrow x) ^0 ; ::_thesis: a in wayabove x
then consider u being Element of N such that
A1: a = u and
A2: for D being non empty directed Subset of N st u <= sup D holds
uparrow x meets D ;
u >> x
proof
let D be non empty directed Subset of N; :: according to WAYBEL_3:def_1 ::_thesis: ( not u <= "\/" (D,N) or ex b1 being Element of the carrier of N st
( b1 in D & x <= b1 ) )
assume u <= sup D ; ::_thesis: ex b1 being Element of the carrier of N st
( b1 in D & x <= b1 )
then uparrow x meets D by A2;
then consider d being set such that
A3: d in (uparrow x) /\ D by XBOOLE_0:4;
reconsider d = d as Element of N by A3;
take d ; ::_thesis: ( d in D & x <= d )
thus d in D by A3, XBOOLE_0:def_4; ::_thesis: x <= d
d in uparrow x by A3, XBOOLE_0:def_4;
hence x <= d by WAYBEL_0:18; ::_thesis: verum
end;
hence a in wayabove x by A1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in wayabove x or a in (uparrow x) ^0 )
assume A4: a in wayabove x ; ::_thesis: a in (uparrow x) ^0
then reconsider b = a as Element of N ;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_N_st_b_<=_sup_D_holds_
uparrow_x_meets_D
A5: b >> x by A4, WAYBEL_3:8;
let D be non empty directed Subset of N; ::_thesis: ( b <= sup D implies uparrow x meets D )
assume b <= sup D ; ::_thesis: uparrow x meets D
then consider d being Element of N such that
A6: d in D and
A7: x <= d by A5, WAYBEL_3:def_1;
d in uparrow x by A7, WAYBEL_0:18;
hence uparrow x meets D by A6, XBOOLE_0:3; ::_thesis: verum
end;
hence a in (uparrow x) ^0 ; ::_thesis: verum
end;
theorem Th26: :: WAYBEL30:26
for N being Scott TopLattice
for X being upper Subset of N holds Int X c= X ^0
proof
let N be Scott TopLattice; ::_thesis: for X being upper Subset of N holds Int X c= X ^0
let X be upper Subset of N; ::_thesis: Int X c= X ^0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int X or x in X ^0 )
assume A1: x in Int X ; ::_thesis: x in X ^0
then reconsider y = x as Element of N ;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_N_st_y_<=_sup_D_holds_
X_meets_D
A2: ( Int X is upper & Int X is inaccessible ) by WAYBEL11:def_4;
let D be non empty directed Subset of N; ::_thesis: ( y <= sup D implies X meets D )
assume y <= sup D ; ::_thesis: X meets D
then sup D in Int X by A2, A1, WAYBEL_0:def_20;
then D meets Int X by A2, WAYBEL11:def_1;
hence X meets D by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum
end;
hence x in X ^0 ; ::_thesis: verum
end;
theorem Th27: :: WAYBEL30:27
for N being non empty reflexive RelStr
for X, Y being Subset of N holds (X ^0) \/ (Y ^0) c= (X \/ Y) ^0
proof
let N be non empty reflexive RelStr ; ::_thesis: for X, Y being Subset of N holds (X ^0) \/ (Y ^0) c= (X \/ Y) ^0
let X, Y be Subset of N; ::_thesis: (X ^0) \/ (Y ^0) c= (X \/ Y) ^0
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (X ^0) \/ (Y ^0) or a in (X \/ Y) ^0 )
assume A1: a in (X ^0) \/ (Y ^0) ; ::_thesis: a in (X \/ Y) ^0
then reconsider b = a as Element of N ;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_N_st_b_<=_sup_D_holds_
X_\/_Y_meets_D
let D be non empty directed Subset of N; ::_thesis: ( b <= sup D implies X \/ Y meets D )
assume A2: b <= sup D ; ::_thesis: X \/ Y meets D
now__::_thesis:_(X_\/_Y)_/\_D_<>_{}
percases ( a in X ^0 or a in Y ^0 ) by A1, XBOOLE_0:def_3;
suppose a in X ^0 ; ::_thesis: (X \/ Y) /\ D <> {}
then ex x being Element of N st
( a = x & ( for D being non empty directed Subset of N st x <= sup D holds
X meets D ) ) ;
then X meets D by A2;
then X /\ D <> {} by XBOOLE_0:def_7;
then (X /\ D) \/ (Y /\ D) <> {} ;
hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; ::_thesis: verum
end;
suppose a in Y ^0 ; ::_thesis: (X \/ Y) /\ D <> {}
then ex y being Element of N st
( a = y & ( for D being non empty directed Subset of N st y <= sup D holds
Y meets D ) ) ;
then Y meets D by A2;
then Y /\ D <> {} by XBOOLE_0:def_7;
then (X /\ D) \/ (Y /\ D) <> {} ;
hence (X \/ Y) /\ D <> {} by XBOOLE_1:23; ::_thesis: verum
end;
end;
end;
hence X \/ Y meets D by XBOOLE_0:def_7; ::_thesis: verum
end;
hence a in (X \/ Y) ^0 ; ::_thesis: verum
end;
theorem Th28: :: WAYBEL30:28
for N being meet-continuous LATTICE
for X, Y being upper Subset of N holds (X ^0) \/ (Y ^0) = (X \/ Y) ^0
proof
let N be meet-continuous LATTICE; ::_thesis: for X, Y being upper Subset of N holds (X ^0) \/ (Y ^0) = (X \/ Y) ^0
let X, Y be upper Subset of N; ::_thesis: (X ^0) \/ (Y ^0) = (X \/ Y) ^0
thus (X ^0) \/ (Y ^0) c= (X \/ Y) ^0 by Th27; :: according to XBOOLE_0:def_10 ::_thesis: (X \/ Y) ^0 c= (X ^0) \/ (Y ^0)
assume not (X \/ Y) ^0 c= (X ^0) \/ (Y ^0) ; ::_thesis: contradiction
then consider s being set such that
A1: s in (X \/ Y) ^0 and
A2: not s in (X ^0) \/ (Y ^0) by TARSKI:def_3;
A3: not s in X ^0 by A2, XBOOLE_0:def_3;
A4: not s in Y ^0 by A2, XBOOLE_0:def_3;
reconsider s = s as Element of N by A1;
consider D being non empty directed Subset of N such that
A5: s <= sup D and
A6: X misses D by A3;
consider E being non empty directed Subset of N such that
A7: s <= sup E and
A8: Y misses E by A4;
s "/\" s = s by YELLOW_0:25;
then s <= (sup D) "/\" (sup E) by A5, A7, YELLOW_3:2;
then A9: s <= sup (D "/\" E) by WAYBEL_2:51;
ex xy being Element of N st
( s = xy & ( for D being non empty directed Subset of N st xy <= sup D holds
X \/ Y meets D ) ) by A1;
then X \/ Y meets D "/\" E by A9;
then A10: (X \/ Y) /\ (D "/\" E) <> {} by XBOOLE_0:def_7;
X misses D "/\" E by A6, YELLOW12:21;
then A11: X /\ (D "/\" E) = {} by XBOOLE_0:def_7;
Y misses D "/\" E by A8, YELLOW12:21;
then (X /\ (D "/\" E)) \/ (Y /\ (D "/\" E)) = {} by A11, XBOOLE_0:def_7;
hence contradiction by A10, XBOOLE_1:23; ::_thesis: verum
end;
theorem Th29: :: WAYBEL30:29
for S being Scott meet-continuous TopLattice
for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }
proof
let S be Scott meet-continuous TopLattice; ::_thesis: for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }
let F be finite Subset of S; ::_thesis: Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }
defpred S1[ set ] means ex UU being Subset-Family of S st
( UU = { (uparrow x) where x is Element of S : x in $1 } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in $1 } );
A1: for b, J being set st b in F & J c= F & S1[J] holds
S1[J \/ {b}]
proof
let b, J be set ; ::_thesis: ( b in F & J c= F & S1[J] implies S1[J \/ {b}] )
assume that
A2: b in F and
J c= F ; ::_thesis: ( not S1[J] or S1[J \/ {b}] )
reconsider bb = b as Element of S by A2;
A3: (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }
proof
{ ((uparrow x) ^0) where x is Element of S : x in J } c= { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) ^0) where x is Element of S : x in J } or a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } )
assume a in { ((uparrow x) ^0) where x is Element of S : x in J } ; ::_thesis: a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }
then A4: ex y being Element of S st
( a = (uparrow y) ^0 & y in J ) ;
J c= J \/ {b} by XBOOLE_1:7;
hence a in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A4; ::_thesis: verum
end;
then A5: union { ((uparrow x) ^0) where x is Element of S : x in J } c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:77;
A6: {b} c= J \/ {b} by XBOOLE_1:7;
b in {b} by TARSKI:def_1;
then (uparrow bb) ^0 in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A6;
then (uparrow bb) ^0 c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by ZFMISC_1:74;
hence (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) c= union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A5, XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } or a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) )
assume a in union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } ; ::_thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
then consider A being set such that
A7: a in A and
A8: A in { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by TARSKI:def_4;
consider y being Element of S such that
A9: A = (uparrow y) ^0 and
A10: y in J \/ {b} by A8;
percases ( y in J or y in {b} ) by A10, XBOOLE_0:def_3;
suppose y in J ; ::_thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
then (uparrow y) ^0 in { ((uparrow x) ^0) where x is Element of S : x in J } ;
then A11: a in union { ((uparrow x) ^0) where x is Element of S : x in J } by A7, A9, TARSKI:def_4;
union { ((uparrow x) ^0) where x is Element of S : x in J } c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7;
hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A11; ::_thesis: verum
end;
supposeA12: y in {b} ; ::_thesis: a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0)
A13: (uparrow bb) ^0 c= (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by XBOOLE_1:7;
y = b by A12, TARSKI:def_1;
hence a in (union { ((uparrow x) ^0) where x is Element of S : x in J } ) \/ ((uparrow bb) ^0) by A13, A7, A9; ::_thesis: verum
end;
end;
end;
assume S1[J] ; ::_thesis: S1[J \/ {b}]
then consider UU being Subset-Family of S such that
A14: UU = { (uparrow x) where x is Element of S : x in J } and
A15: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J } ;
reconsider I = UU \/ {(uparrow bb)} as Subset-Family of S ;
take I ; ::_thesis: ( I = { (uparrow x) where x is Element of S : x in J \/ {b} } & (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } )
thus I = { (uparrow x) where x is Element of S : x in J \/ {b} } ::_thesis: (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} }
proof
thus I c= { (uparrow x) where x is Element of S : x in J \/ {b} } :: according to XBOOLE_0:def_10 ::_thesis: { (uparrow x) where x is Element of S : x in J \/ {b} } c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in I or a in { (uparrow x) where x is Element of S : x in J \/ {b} } )
assume A16: a in I ; ::_thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} }
percases ( a in UU or a in {(uparrow bb)} ) by A16, XBOOLE_0:def_3;
supposeA17: a in UU ; ::_thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} }
A18: J c= J \/ {b} by XBOOLE_1:7;
ex x being Element of S st
( a = uparrow x & x in J ) by A17, A14;
hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A18; ::_thesis: verum
end;
supposeA19: a in {(uparrow bb)} ; ::_thesis: a in { (uparrow x) where x is Element of S : x in J \/ {b} }
A20: b in {b} by TARSKI:def_1;
A21: {b} c= J \/ {b} by XBOOLE_1:7;
a = uparrow bb by A19, TARSKI:def_1;
hence a in { (uparrow x) where x is Element of S : x in J \/ {b} } by A20, A21; ::_thesis: verum
end;
end;
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (uparrow x) where x is Element of S : x in J \/ {b} } or a in I )
assume a in { (uparrow x) where x is Element of S : x in J \/ {b} } ; ::_thesis: a in I
then consider x being Element of S such that
A22: a = uparrow x and
A23: x in J \/ {b} ;
percases ( x in J or x in {b} ) by A23, XBOOLE_0:def_3;
supposeA24: x in J ; ::_thesis: a in I
A25: UU c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
uparrow x in UU by A24, A14;
hence a in I by A25, A22; ::_thesis: verum
end;
supposeA26: x in {b} ; ::_thesis: a in I
A27: {(uparrow bb)} c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
A28: a in {(uparrow x)} by A22, TARSKI:def_1;
x = b by A26, TARSKI:def_1;
hence a in I by A27, A28; ::_thesis: verum
end;
end;
end;
A29: (union UU) \/ (uparrow bb) = union I
proof
thus (union UU) \/ (uparrow bb) c= union I :: according to XBOOLE_0:def_10 ::_thesis: union I c= (union UU) \/ (uparrow bb)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (union UU) \/ (uparrow bb) or a in union I )
assume A30: a in (union UU) \/ (uparrow bb) ; ::_thesis: a in union I
percases ( a in union UU or a in uparrow bb ) by A30, XBOOLE_0:def_3;
supposeA31: a in union UU ; ::_thesis: a in union I
A32: UU c= I by XBOOLE_1:7;
ex A being set st
( a in A & A in UU ) by A31, TARSKI:def_4;
hence a in union I by A32, TARSKI:def_4; ::_thesis: verum
end;
supposeA33: a in uparrow bb ; ::_thesis: a in union I
A34: uparrow bb in {(uparrow bb)} by TARSKI:def_1;
{(uparrow bb)} c= UU \/ {(uparrow bb)} by XBOOLE_1:7;
hence a in union I by A34, A33, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union I or a in (union UU) \/ (uparrow bb) )
assume a in union I ; ::_thesis: a in (union UU) \/ (uparrow bb)
then consider A being set such that
A35: a in A and
A36: A in I by TARSKI:def_4;
percases ( A in UU or A in {(uparrow bb)} ) by A36, XBOOLE_0:def_3;
suppose A in UU ; ::_thesis: a in (union UU) \/ (uparrow bb)
then A c= union UU by ZFMISC_1:74;
then A37: a in union UU by A35;
union UU c= (union UU) \/ (uparrow bb) by XBOOLE_1:7;
hence a in (union UU) \/ (uparrow bb) by A37; ::_thesis: verum
end;
supposeA38: A in {(uparrow bb)} ; ::_thesis: a in (union UU) \/ (uparrow bb)
A39: uparrow bb c= (union UU) \/ (uparrow bb) by XBOOLE_1:7;
A = uparrow bb by A38, TARSKI:def_1;
hence a in (union UU) \/ (uparrow bb) by A39, A35; ::_thesis: verum
end;
end;
end;
for X being Subset of S st X in UU holds
X is upper
proof
let X be Subset of S; ::_thesis: ( X in UU implies X is upper )
assume X in UU ; ::_thesis: X is upper
then ex x being Element of S st
( X = uparrow x & x in J ) by A14;
hence X is upper ; ::_thesis: verum
end;
then union UU is upper by WAYBEL_0:28;
hence (union I) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in J \/ {b} } by A3, A15, A29, Th28; ::_thesis: verum
end;
A40: S1[ {} ]
proof
deffunc H1( Element of S) -> Subset of S = (uparrow $1) ^0 ;
reconsider UU = {} as Subset-Family of S by XBOOLE_1:2;
take UU ; ::_thesis: ( UU = { (uparrow x) where x is Element of S : x in {} } & (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } )
reconsider K = union UU as empty Subset of S ;
A41: K ^0 is empty ;
thus UU = { (uparrow x) where x is Element of S : x in {} } ::_thesis: (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} }
proof
deffunc H2( Element of S) -> Element of bool the carrier of S = uparrow $1;
{ H2(x) where x is Element of S : x in {} } = {} from WAYBEL30:sch_1();
hence UU = { (uparrow x) where x is Element of S : x in {} } ; ::_thesis: verum
end;
{ H1(x) where x is Element of S : x in {} } = {} from WAYBEL30:sch_1();
hence (union UU) ^0 = union { ((uparrow x) ^0) where x is Element of S : x in {} } by A41; ::_thesis: verum
end;
A42: { ((uparrow x) ^0) where x is Element of S : x in F } = { (wayabove x) where x is Element of S : x in F }
proof
thus { ((uparrow x) ^0) where x is Element of S : x in F } c= { (wayabove x) where x is Element of S : x in F } :: according to XBOOLE_0:def_10 ::_thesis: { (wayabove x) where x is Element of S : x in F } c= { ((uparrow x) ^0) where x is Element of S : x in F }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) ^0) where x is Element of S : x in F } or a in { (wayabove x) where x is Element of S : x in F } )
assume a in { ((uparrow x) ^0) where x is Element of S : x in F } ; ::_thesis: a in { (wayabove x) where x is Element of S : x in F }
then consider x being Element of S such that
A43: a = (uparrow x) ^0 and
A44: x in F ;
(uparrow x) ^0 = wayabove x by Th25;
hence a in { (wayabove x) where x is Element of S : x in F } by A43, A44; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (wayabove x) where x is Element of S : x in F } or a in { ((uparrow x) ^0) where x is Element of S : x in F } )
assume a in { (wayabove x) where x is Element of S : x in F } ; ::_thesis: a in { ((uparrow x) ^0) where x is Element of S : x in F }
then consider x being Element of S such that
A45: a = wayabove x and
A46: x in F ;
(uparrow x) ^0 = wayabove x by Th25;
hence a in { ((uparrow x) ^0) where x is Element of S : x in F } by A45, A46; ::_thesis: verum
end;
A47: F is finite ;
S1[F] from FINSET_1:sch_2(A47, A40, A1);
then (uparrow F) ^0 = union { (wayabove x) where x is Element of S : x in F } by A42, YELLOW_9:4;
hence Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F } by Th26; ::_thesis: verum
end;
theorem Th30: :: WAYBEL30:30
for N being complete Lawson TopLattice holds
( N is continuous iff ( N is meet-continuous & N is Hausdorff ) )
proof
let N be complete Lawson TopLattice; ::_thesis: ( N is continuous iff ( N is meet-continuous & N is Hausdorff ) )
thus ( N is continuous implies ( N is meet-continuous & N is Hausdorff ) ) ; ::_thesis: ( N is meet-continuous & N is Hausdorff implies N is continuous )
assume A1: ( N is meet-continuous & N is Hausdorff ) ; ::_thesis: N is continuous
thus A2: for x being Element of N holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( N is up-complete & N is satisfying_axiom_of_approximation )
thus N is up-complete ; ::_thesis: N is satisfying_axiom_of_approximation
for x, y being Element of N st not x <= y holds
ex u being Element of N st
( u << x & not u <= y )
proof
reconsider J = { (O \ (uparrow F)) where O, F is Subset of N : ( O in sigma N & F is finite ) } as Basis of N by WAYBEL19:32;
set S = the Scott TopAugmentation of N;
A3: for N being Semilattice
for x, y being Element of N st ex u being Element of N st
( u << x & not u <= x "/\" y ) holds
ex u being Element of N st
( u << x & not u <= y )
proof
let N be Semilattice; ::_thesis: for x, y being Element of N st ex u being Element of N st
( u << x & not u <= x "/\" y ) holds
ex u being Element of N st
( u << x & not u <= y )
let x, y be Element of N; ::_thesis: ( ex u being Element of N st
( u << x & not u <= x "/\" y ) implies ex u being Element of N st
( u << x & not u <= y ) )
given u being Element of N such that A4: u << x and
A5: not u <= x "/\" y ; ::_thesis: ex u being Element of N st
( u << x & not u <= y )
take u ; ::_thesis: ( u << x & not u <= y )
thus u << x by A4; ::_thesis: not u <= y
assume A6: u <= y ; ::_thesis: contradiction
u <= x by A4, WAYBEL_3:1;
then u "/\" u <= x "/\" y by A6, YELLOW_3:2;
hence contradiction by A5, YELLOW_0:25; ::_thesis: verum
end;
let x, y be Element of N; ::_thesis: ( not x <= y implies ex u being Element of N st
( u << x & not u <= y ) )
assume not x <= y ; ::_thesis: ex u being Element of N st
( u << x & not u <= y )
then x "/\" y <> x by YELLOW_0:23;
then consider W, V being Subset of N such that
A7: W is open and
A8: V is open and
A9: x in W and
A10: x "/\" y in V and
A11: W misses V by A1, PRE_TOPC:def_10;
V = union { G where G is Subset of N : ( G in J & G c= V ) } by A8, YELLOW_8:9;
then consider K being set such that
A12: x "/\" y in K and
A13: K in { G where G is Subset of N : ( G in J & G c= V ) } by A10, TARSKI:def_4;
consider V1 being Subset of N such that
A14: K = V1 and
A15: V1 in J and
A16: V1 c= V by A13;
consider U2, F being Subset of N such that
A17: V1 = U2 \ (uparrow F) and
A18: U2 in sigma N and
A19: F is finite by A15;
A20: RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
then reconsider x1 = x, y1 = y as Element of the Scott TopAugmentation of N ;
A21: ex_inf_of {x1,y1}, the Scott TopAugmentation of N by YELLOW_0:21;
reconsider U1 = U2 as Subset of the Scott TopAugmentation of N by A20;
reconsider WU1 = W /\ U2 as Subset of N ;
reconsider W1 = WU1 as Subset of the Scott TopAugmentation of N by A20;
A22: uparrow W1 = uparrow WU1 by A20, WAYBEL_0:13;
U2 in sigma the Scott TopAugmentation of N by A20, A18, YELLOW_9:52;
then A23: U1 is open by WAYBEL14:24;
then A24: U1 is upper by WAYBEL11:def_4;
WU1 c= uparrow F
proof
A25: W misses V1 by A11, A16, XBOOLE_1:63;
A26: WU1 \ (uparrow F) c= U1 \ (uparrow F) by XBOOLE_1:17, XBOOLE_1:33;
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in WU1 or w in uparrow F )
assume that
A27: w in WU1 and
A28: not w in uparrow F ; ::_thesis: contradiction
A29: w in W by A27, XBOOLE_0:def_4;
w in WU1 \ (uparrow F) by A27, A28, XBOOLE_0:def_5;
hence contradiction by A26, A17, A29, A25, XBOOLE_0:3; ::_thesis: verum
end;
then WU1 is_coarser_than uparrow F by WAYBEL12:16;
then A30: uparrow WU1 c= uparrow F by YELLOW12:28;
A31: x1 "/\" y1 <= x1 by YELLOW_0:23;
x "/\" y = inf {x,y} by YELLOW_0:40
.= "/\" ({x1,y1}, the Scott TopAugmentation of N) by A20, A21, YELLOW_0:27
.= x1 "/\" y1 by YELLOW_0:40 ;
then x1 "/\" y1 in U1 by A12, A14, A17, XBOOLE_0:def_5;
then x1 in U1 by A24, A31, WAYBEL_0:def_20;
then A32: x in W1 by A9, XBOOLE_0:def_4;
W1 c= uparrow W1 by WAYBEL_0:16;
then A33: x in uparrow W1 by A32;
reconsider F1 = F as finite Subset of the Scott TopAugmentation of N by A20, A19;
A34: uparrow F1 = uparrow F by A20, WAYBEL_0:13;
N is correct Lawson TopAugmentation of the Scott TopAugmentation of N by A20, YELLOW_9:def_4;
then U2 is open by A23, WAYBEL19:37;
then uparrow W1 c= Int (uparrow F1) by A7, A1, A30, A22, A34, Th15, TOPS_1:24;
then A35: x in Int (uparrow F1) by A33;
the Scott TopAugmentation of N is meet-continuous by A1, A20, YELLOW12:14;
then Int (uparrow F1) c= union { (wayabove u) where u is Element of the Scott TopAugmentation of N : u in F1 } by Th29;
then consider A being set such that
A36: x in A and
A37: A in { (wayabove u) where u is Element of the Scott TopAugmentation of N : u in F1 } by A35, TARSKI:def_4;
consider u being Element of the Scott TopAugmentation of N such that
A38: A = wayabove u and
A39: u in F1 by A37;
reconsider u1 = u as Element of N by A20;
A40: wayabove u1 = wayabove u by A20, YELLOW12:13;
now__::_thesis:_ex_u1_being_Element_of_N_st_
(_u1_<<_x_&_not_u1_<=_x_"/\"_y_)
take u1 = u1; ::_thesis: ( u1 << x & not u1 <= x "/\" y )
thus u1 << x by A36, A38, A40, WAYBEL_3:8; ::_thesis: not u1 <= x "/\" y
uparrow u1 c= uparrow F by A39, YELLOW12:30;
then not x "/\" y in uparrow u1 by A12, A14, A17, XBOOLE_0:def_5;
hence not u1 <= x "/\" y by WAYBEL_0:18; ::_thesis: verum
end;
then consider u2 being Element of N such that
A41: u2 << x and
A42: not u2 <= y by A3;
take u2 ; ::_thesis: ( u2 << x & not u2 <= y )
thus ( u2 << x & not u2 <= y ) by A41, A42; ::_thesis: verum
end;
hence N is satisfying_axiom_of_approximation by A2, WAYBEL_3:24; ::_thesis: verum
end;
registration
cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous -> Hausdorff complete for TopRelStr ;
coherence
for b1 being complete TopLattice st b1 is continuous & b1 is Lawson holds
b1 is Hausdorff ;
cluster TopSpace-like Hausdorff reflexive transitive antisymmetric with_suprema with_infima complete Lawson meet-continuous -> complete continuous for TopRelStr ;
coherence
for b1 being complete TopLattice st b1 is meet-continuous & b1 is Lawson & b1 is Hausdorff holds
b1 is continuous by Th30;
end;
definition
let N be non empty TopRelStr ;
attrN is with_small_semilattices means :: WAYBEL30:def 2
for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting ;
attrN is with_compact_semilattices means :: WAYBEL30:def 3
for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact );
attrN is with_open_semilattices means :Def4: :: WAYBEL30:def 4
for x being Point of N ex J being Basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting ;
end;
:: deftheorem defines with_small_semilattices WAYBEL30:def_2_:_
for N being non empty TopRelStr holds
( N is with_small_semilattices iff for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting );
:: deftheorem defines with_compact_semilattices WAYBEL30:def_3_:_
for N being non empty TopRelStr holds
( N is with_compact_semilattices iff for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact ) );
:: deftheorem Def4 defines with_open_semilattices WAYBEL30:def_4_:_
for N being non empty TopRelStr holds
( N is with_open_semilattices iff for x being Point of N ex J being Basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting );
registration
cluster non empty TopSpace-like with_open_semilattices -> non empty TopSpace-like with_small_semilattices for TopRelStr ;
coherence
for b1 being non empty TopSpace-like TopRelStr st b1 is with_open_semilattices holds
b1 is with_small_semilattices
proof
let N be non empty TopSpace-like TopRelStr ; ::_thesis: ( N is with_open_semilattices implies N is with_small_semilattices )
assume A1: for x being Point of N ex J being Basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting ; :: according to WAYBEL30:def_4 ::_thesis: N is with_small_semilattices
let x be Point of N; :: according to WAYBEL30:def_2 ::_thesis: ex J being basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting
consider J being Basis of x such that
A2: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A1;
reconsider J = J as basis of x by YELLOW13:23;
take J ; ::_thesis: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting
thus for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A2; ::_thesis: verum
end;
cluster non empty TopSpace-like with_compact_semilattices -> non empty TopSpace-like with_small_semilattices for TopRelStr ;
coherence
for b1 being non empty TopSpace-like TopRelStr st b1 is with_compact_semilattices holds
b1 is with_small_semilattices
proof
let N be non empty TopSpace-like TopRelStr ; ::_thesis: ( N is with_compact_semilattices implies N is with_small_semilattices )
assume A3: for x being Point of N ex J being basis of x st
for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact ) ; :: according to WAYBEL30:def_3 ::_thesis: N is with_small_semilattices
let x be Point of N; :: according to WAYBEL30:def_2 ::_thesis: ex J being basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting
consider J being basis of x such that
A4: for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact ) by A3;
take J ; ::_thesis: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting
thus for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A4; ::_thesis: verum
end;
cluster non empty anti-discrete -> non empty with_small_semilattices with_open_semilattices for TopRelStr ;
coherence
for b1 being non empty TopRelStr st b1 is anti-discrete holds
( b1 is with_small_semilattices & b1 is with_open_semilattices )
proof
let T be non empty TopRelStr ; ::_thesis: ( T is anti-discrete implies ( T is with_small_semilattices & T is with_open_semilattices ) )
assume T is anti-discrete ; ::_thesis: ( T is with_small_semilattices & T is with_open_semilattices )
then reconsider W = T as non empty anti-discrete TopRelStr ;
set J = { the carrier of W};
A5: now__::_thesis:_for_A_being_Subset_of_W_st_A_in_{_the_carrier_of_W}_holds_
subrelstr_A_is_meet-inheriting
let A be Subset of W; ::_thesis: ( A in { the carrier of W} implies subrelstr A is meet-inheriting )
A6: subrelstr ([#] W) is infs-inheriting ;
assume A in { the carrier of W} ; ::_thesis: subrelstr A is meet-inheriting
then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A6, TARSKI:def_1;
K is meet-inheriting ;
hence subrelstr A is meet-inheriting ; ::_thesis: verum
end;
A7: W is with_open_semilattices
proof
let x be Point of W; :: according to WAYBEL30:def_4 ::_thesis: ex J being Basis of x st
for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
reconsider J = { the carrier of W} as Basis of x by YELLOW13:13;
take J ; ::_thesis: for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
let A be Subset of W; ::_thesis: ( A in J implies subrelstr A is meet-inheriting )
assume A in J ; ::_thesis: subrelstr A is meet-inheriting
hence subrelstr A is meet-inheriting by A5; ::_thesis: verum
end;
W is with_small_semilattices
proof
let x be Point of W; :: according to WAYBEL30:def_2 ::_thesis: ex J being basis of x st
for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
reconsider J = { the carrier of W} as basis of x by YELLOW13:21;
take J ; ::_thesis: for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
let A be Subset of W; ::_thesis: ( A in J implies subrelstr A is meet-inheriting )
assume A in J ; ::_thesis: subrelstr A is meet-inheriting
hence subrelstr A is meet-inheriting by A5; ::_thesis: verum
end;
hence ( T is with_small_semilattices & T is with_open_semilattices ) by A7; ::_thesis: verum
end;
cluster1 -element TopSpace-like reflexive -> 1 -element with_compact_semilattices for TopRelStr ;
coherence
for b1 being 1 -element TopRelStr st b1 is reflexive & b1 is TopSpace-like holds
b1 is with_compact_semilattices
proof
let T be 1 -element TopRelStr ; ::_thesis: ( T is reflexive & T is TopSpace-like implies T is with_compact_semilattices )
assume ( T is reflexive & T is TopSpace-like ) ; ::_thesis: T is with_compact_semilattices
then reconsider W = T as 1 -element TopSpace-like reflexive TopRelStr ;
W is with_compact_semilattices
proof
let x be Point of W; :: according to WAYBEL30:def_3 ::_thesis: ex J being basis of x st
for A being Subset of W st A in J holds
( subrelstr A is meet-inheriting & A is compact )
reconsider J = { the carrier of W} as basis of x by YELLOW13:21;
take J ; ::_thesis: for A being Subset of W st A in J holds
( subrelstr A is meet-inheriting & A is compact )
let A be Subset of W; ::_thesis: ( A in J implies ( subrelstr A is meet-inheriting & A is compact ) )
assume A8: A in J ; ::_thesis: ( subrelstr A is meet-inheriting & A is compact )
subrelstr ([#] W) is infs-inheriting ;
then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A8, TARSKI:def_1;
K is meet-inheriting ;
hence subrelstr A is meet-inheriting ; ::_thesis: A is compact
A = [#] W by A8, TARSKI:def_1;
hence A is compact ; ::_thesis: verum
end;
hence T is with_compact_semilattices ; ::_thesis: verum
end;
end;
registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima strict lower non void for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is strict & b1 is trivial & b1 is lower )
proof
set T = the 1 -element strict TopLattice;
take the 1 -element strict TopLattice ; ::_thesis: ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is trivial & the 1 -element strict TopLattice is lower )
thus ( the 1 -element strict TopLattice is strict & the 1 -element strict TopLattice is trivial & the 1 -element strict TopLattice is lower ) ; ::_thesis: verum
end;
end;
theorem Th31: :: WAYBEL30:31
for N being with_infima topological_semilattice TopPoset
for C being Subset of N st subrelstr C is meet-inheriting holds
subrelstr (Cl C) is meet-inheriting
proof
let N be with_infima topological_semilattice TopPoset; ::_thesis: for C being Subset of N st subrelstr C is meet-inheriting holds
subrelstr (Cl C) is meet-inheriting
let C be Subset of N; ::_thesis: ( subrelstr C is meet-inheriting implies subrelstr (Cl C) is meet-inheriting )
assume A1: subrelstr C is meet-inheriting ; ::_thesis: subrelstr (Cl C) is meet-inheriting
set A = Cl C;
set S = subrelstr (Cl C);
let x, y be Element of N; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (subrelstr (Cl C)) or not y in the carrier of (subrelstr (Cl C)) or not ex_inf_of {x,y},N or "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) )
assume that
A2: x in the carrier of (subrelstr (Cl C)) and
A3: y in the carrier of (subrelstr (Cl C)) and
ex_inf_of {x,y},N ; ::_thesis: "/\" ({x,y},N) in the carrier of (subrelstr (Cl C))
A4: the carrier of (subrelstr (Cl C)) = Cl C by YELLOW_0:def_15;
for V being a_neighborhood of x "/\" y holds V meets C
proof
set NN = [:N,N:];
let V be a_neighborhood of x "/\" y; ::_thesis: V meets C
A5: the carrier of [:N,N:] = [: the carrier of N, the carrier of N:] by BORSUK_1:def_2;
then reconsider xy = [x,y] as Point of [:N,N:] by YELLOW_3:def_2;
the carrier of [:N,N:] = [: the carrier of N, the carrier of N:] by YELLOW_3:def_2;
then reconsider f = inf_op N as Function of [:N,N:],N by A5;
A6: f . xy = f . (x,y)
.= x "/\" y by WAYBEL_2:def_4 ;
f is continuous by YELLOW13:def_5;
then consider H being a_neighborhood of xy such that
A7: f .: H c= V by A6, BORSUK_1:def_1;
consider A being Subset-Family of [:N,N:] such that
A8: Int H = union A and
A9: for e being set st e in A holds
ex X1, Y1 being Subset of N st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
xy in union A by A8, CONNSP_2:def_1;
then consider K being set such that
A10: xy in K and
A11: K in A by TARSKI:def_4;
consider Ix, Iy being Subset of N such that
A12: K = [:Ix,Iy:] and
A13: Ix is open and
A14: Iy is open by A9, A11;
A15: x in Ix by A10, A12, ZFMISC_1:87;
A16: y in Iy by A10, A12, ZFMISC_1:87;
A17: Ix = Int Ix by A13, TOPS_1:23;
Iy = Int Iy by A14, TOPS_1:23;
then reconsider Iy = Iy as a_neighborhood of y by A16, CONNSP_2:def_1;
Iy meets C by A3, A4, CONNSP_2:27;
then consider iy being set such that
A18: iy in Iy and
A19: iy in C by XBOOLE_0:3;
reconsider Ix = Ix as a_neighborhood of x by A15, A17, CONNSP_2:def_1;
Ix meets C by A2, A4, CONNSP_2:27;
then consider ix being set such that
A20: ix in Ix and
A21: ix in C by XBOOLE_0:3;
reconsider ix = ix, iy = iy as Element of N by A20, A18;
now__::_thesis:_ex_a_being_Element_of_the_carrier_of_N_st_
(_a_in_V_&_a_in_C_)
[ix,iy] in K by A12, A20, A18, ZFMISC_1:87;
then A22: [ix,iy] in Int H by A8, A11, TARSKI:def_4;
take a = ix "/\" iy; ::_thesis: ( a in V & a in C )
A23: dom f = the carrier of [:N,N:] by FUNCT_2:def_1;
A24: Int H c= H by TOPS_1:16;
f . (ix,iy) = ix "/\" iy by WAYBEL_2:def_4;
then ix "/\" iy in f .: H by A24, A23, A22, FUNCT_1:def_6;
hence a in V by A7; ::_thesis: a in C
A25: ex_inf_of {ix,iy},N by YELLOW_0:21;
the carrier of (subrelstr C) = C by YELLOW_0:def_15;
then inf {ix,iy} in C by A25, A1, A21, A19, YELLOW_0:def_16;
hence a in C by YELLOW_0:40; ::_thesis: verum
end;
hence V meets C by XBOOLE_0:3; ::_thesis: verum
end;
then x "/\" y in Cl C by CONNSP_2:27;
hence "/\" ({x,y},N) in the carrier of (subrelstr (Cl C)) by A4, YELLOW_0:40; ::_thesis: verum
end;
theorem Th32: :: WAYBEL30:32
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N holds
( ( for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S ) iff N is with_open_semilattices )
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N holds
( ( for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S ) iff N is with_open_semilattices )
let S be Scott TopAugmentation of N; ::_thesis: ( ( for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S ) iff N is with_open_semilattices )
A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
hereby ::_thesis: ( N is with_open_semilattices implies for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S )
assume A2: for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S ; ::_thesis: N is with_open_semilattices
thus N is with_open_semilattices ::_thesis: verum
proof
let x be Point of N; :: according to WAYBEL30:def_4 ::_thesis: ex J being Basis of x st
for A being Subset of N st A in J holds
subrelstr A is meet-inheriting
defpred S1[ set ] means ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st
( $1 = W1 & U1 \ (uparrow F) = $1 & x in $1 & W1 is open );
consider SF being Subset-Family of N such that
A3: for W being Subset of N holds
( W in SF iff S1[W] ) from SUBSET_1:sch_3();
reconsider SF = SF as Subset-Family of N ;
A4: now__::_thesis:_for_W_being_Subset_of_N_st_W_is_open_&_x_in_W_holds_
ex_U2_being_Filter_of_N_ex_F_being_finite_Subset_of_N_ex_IT_being_Subset_of_N_st_
(_IT_=_U2_\_(uparrow_F)_&_x_in_IT_&_IT_is_open_&_IT_c=_W_)
reconsider BL = { (O \ (uparrow F)) where O, F is Subset of N : ( O in sigma N & F is finite ) } as Basis of N by WAYBEL19:32;
A5: BL c= the topology of N by TOPS_2:64;
reconsider y = x as Point of S by A1;
let W be Subset of N; ::_thesis: ( W is open & x in W implies ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st
( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) )
assume that
A6: W is open and
A7: x in W ; ::_thesis: ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st
( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )
consider By being Basis of y such that
A8: for A being Subset of S st A in By holds
A is Filter of S by A2;
W = union { G where G is Subset of N : ( G in BL & G c= W ) } by A6, YELLOW_8:9;
then consider K being set such that
A9: x in K and
A10: K in { G where G is Subset of N : ( G in BL & G c= W ) } by A7, TARSKI:def_4;
consider G being Subset of N such that
A11: K = G and
A12: G in BL and
A13: G c= W by A10;
consider V, F being Subset of N such that
A14: G = V \ (uparrow F) and
A15: V in sigma N and
A16: F is finite by A12;
reconsider F = F as finite Subset of N by A16;
A17: not x in uparrow F by A9, A11, A14, XBOOLE_0:def_5;
reconsider V = V as Subset of S by A1;
A18: y in V by A9, A11, A14, XBOOLE_0:def_5;
A19: sigma N = sigma S by A1, YELLOW_9:52;
then V is open by A15, WAYBEL14:24;
then consider U1 being Subset of S such that
A20: U1 in By and
A21: U1 c= V by A18, YELLOW_8:13;
reconsider U2 = U1 as Subset of N by A1;
U1 is Filter of S by A8, A20;
then reconsider U2 = U2 as Filter of N by A1, WAYBEL_0:4, WAYBEL_0:25;
U2 \ (uparrow F) is Subset of N ;
then reconsider IT = U1 \ (uparrow F) as Subset of N ;
take U2 = U2; ::_thesis: ex F being finite Subset of N ex IT being Subset of N st
( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )
take F = F; ::_thesis: ex IT being Subset of N st
( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )
take IT = IT; ::_thesis: ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )
thus IT = U2 \ (uparrow F) ; ::_thesis: ( x in IT & IT is open & IT c= W )
y in U1 by A20, YELLOW_8:12;
hence x in IT by A17, XBOOLE_0:def_5; ::_thesis: ( IT is open & IT c= W )
U1 is open by A20, YELLOW_8:12;
then U1 in sigma S by WAYBEL14:24;
then IT in BL by A19;
hence IT is open by A5, PRE_TOPC:def_2; ::_thesis: IT c= W
IT c= G by A14, A21, XBOOLE_1:33;
hence IT c= W by A13, XBOOLE_1:1; ::_thesis: verum
end;
SF is Basis of x
proof
A22: SF is open
proof
let a be Subset of N; :: according to TOPS_2:def_1 ::_thesis: ( not a in SF or a is open )
assume A23: a in SF ; ::_thesis: a is open
reconsider W = a as Subset of N ;
ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st
( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A23;
hence a is open ; ::_thesis: verum
end;
SF is x -quasi_basis
proof
for a being set st a in SF holds
x in a
proof
let a be set ; ::_thesis: ( a in SF implies x in a )
assume A24: a in SF ; ::_thesis: x in a
then reconsider W = a as Subset of N ;
ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st
( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A24;
hence x in a ; ::_thesis: verum
end;
hence x in Intersect SF by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of N holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of N st
( b2 in SF & b2 c= b1 ) )
let W be Subset of N; ::_thesis: ( not W is open or not x in W or ex b1 being Element of bool the carrier of N st
( b1 in SF & b1 c= W ) )
assume that
A25: W is open and
A26: x in W ; ::_thesis: ex b1 being Element of bool the carrier of N st
( b1 in SF & b1 c= W )
consider U2 being Filter of N, F being finite Subset of N, IT being Subset of N such that
A27: IT = U2 \ (uparrow F) and
A28: x in IT and
A29: IT is open and
A30: IT c= W by A25, A26, A4;
take IT ; ::_thesis: ( IT in SF & IT c= W )
thus ( IT in SF & IT c= W ) by A3, A27, A28, A29, A30; ::_thesis: verum
end;
hence SF is Basis of x by A22; ::_thesis: verum
end;
then reconsider SF = SF as Basis of x ;
take SF ; ::_thesis: for A being Subset of N st A in SF holds
subrelstr A is meet-inheriting
let W be Subset of N; ::_thesis: ( W in SF implies subrelstr W is meet-inheriting )
assume W in SF ; ::_thesis: subrelstr W is meet-inheriting
then consider U1 being Filter of N, F being finite Subset of N, W1 being Subset of N such that
W1 = W and
A31: U1 \ (uparrow F) = W and
x in W and
W1 is open by A3;
set SW = subrelstr W;
thus subrelstr W is meet-inheriting ::_thesis: verum
proof
let a, b be Element of N; :: according to YELLOW_0:def_16 ::_thesis: ( not a in the carrier of (subrelstr W) or not b in the carrier of (subrelstr W) or not ex_inf_of {a,b},N or "/\" ({a,b},N) in the carrier of (subrelstr W) )
assume that
A32: a in the carrier of (subrelstr W) and
A33: b in the carrier of (subrelstr W) and
ex_inf_of {a,b},N ; ::_thesis: "/\" ({a,b},N) in the carrier of (subrelstr W)
A34: the carrier of (subrelstr W) = W by YELLOW_0:def_15;
then A35: b in U1 by A31, A33, XBOOLE_0:def_5;
A36: not a in uparrow F by A34, A31, A32, XBOOLE_0:def_5;
for y being Element of N st y <= a "/\" b holds
not y in F
proof
A37: a "/\" b <= a by YELLOW_0:23;
let y be Element of N; ::_thesis: ( y <= a "/\" b implies not y in F )
assume y <= a "/\" b ; ::_thesis: not y in F
then y <= a by A37, ORDERS_2:3;
hence not y in F by A36, WAYBEL_0:def_16; ::_thesis: verum
end;
then A38: not a "/\" b in uparrow F by WAYBEL_0:def_16;
a in U1 by A34, A31, A32, XBOOLE_0:def_5;
then consider z being Element of N such that
A39: z in U1 and
A40: z <= a and
A41: z <= b by A35, WAYBEL_0:def_2;
z "/\" z <= a "/\" b by A40, A41, YELLOW_3:2;
then z <= a "/\" b by YELLOW_0:25;
then a "/\" b in U1 by A39, WAYBEL_0:def_20;
then a "/\" b in W by A38, A31, XBOOLE_0:def_5;
hence "/\" ({a,b},N) in the carrier of (subrelstr W) by A34, YELLOW_0:40; ::_thesis: verum
end;
end;
end;
assume A42: N is with_open_semilattices ; ::_thesis: for x being Point of S ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S
let x be Point of S; ::_thesis: ex J being Basis of x st
for W being Subset of S st W in J holds
W is Filter of S
reconsider y = x as Point of N by A1;
consider J being Basis of y such that
A43: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A42, Def4;
reconsider J9 = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16;
take J9 ; ::_thesis: for W being Subset of S st W in J9 holds
W is Filter of S
let W be Subset of S; ::_thesis: ( W in J9 implies W is Filter of S )
assume W in J9 ; ::_thesis: W is Filter of S
then consider V being Subset of N such that
A44: W = uparrow V and
A45: V in J ;
subrelstr V is meet-inheriting by A43, A45;
then A46: V is filtered by YELLOW12:26;
x in V by A45, YELLOW_8:12;
hence W is Filter of S by A46, A1, A44, WAYBEL_0:4, WAYBEL_0:25; ::_thesis: verum
end;
theorem Th33: :: WAYBEL30:33
for N being complete Lawson TopLattice
for S being Scott TopAugmentation of N
for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
proof
let N be complete Lawson TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
let S be Scott TopAugmentation of N; ::_thesis: for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
let x be Element of N; ::_thesis: { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } c= { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
set s = { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } ;
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } or k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } )
assume k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } ; ::_thesis: k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
then consider J being Subset of S such that
A1: k = inf J and
A2: x in J and
A3: J in sigma S ;
A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider A = J as Subset of N ;
sigma N c= lambda N by Th10;
then A5: sigma S c= lambda N by A4, YELLOW_9:52;
inf A = inf J by A4, YELLOW_0:17, YELLOW_0:27;
hence k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } by A5, A1, A2, A3; ::_thesis: verum
end;
theorem Th34: :: WAYBEL30:34
for N being complete Lawson meet-continuous TopLattice
for S being Scott TopAugmentation of N
for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: for S being Scott TopAugmentation of N
for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
let S be Scott TopAugmentation of N; ::_thesis: for x being Element of N holds { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
let x be Element of N; ::_thesis: { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } = { (inf J) where J is Subset of N : ( x in J & J in lambda N ) }
set l = { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ;
set s = { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } ;
thus { (inf J) where J is Subset of S : ( x in J & J in sigma S ) } c= { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } by Th33; :: according to XBOOLE_0:def_10 ::_thesis: { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } c= { (inf A) where A is Subset of S : ( x in A & A in sigma S ) }
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (inf J) where J is Subset of N : ( x in J & J in lambda N ) } or k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } )
assume k in { (inf A) where A is Subset of N : ( x in A & A in lambda N ) } ; ::_thesis: k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) }
then consider A being Subset of N such that
A1: k = inf A and
A2: x in A and
A3: A in lambda N ;
A4: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then reconsider J = A as Subset of S ;
A is open by A3, Th12;
then uparrow J is open by Th15;
then A5: uparrow J in sigma S by WAYBEL14:24;
A6: J c= uparrow J by WAYBEL_0:16;
inf A = inf J by A4, YELLOW_0:17, YELLOW_0:27
.= inf (uparrow J) by WAYBEL_0:38, YELLOW_0:17 ;
hence k in { (inf A) where A is Subset of S : ( x in A & A in sigma S ) } by A5, A1, A2, A6; ::_thesis: verum
end;
theorem Th35: :: WAYBEL30:35
for N being complete Lawson meet-continuous TopLattice holds
( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) )
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( N is continuous iff ( N is with_open_semilattices & InclPoset (sigma N) is continuous ) )
set S = the Scott TopAugmentation of N;
A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) by YELLOW_9:def_4;
hereby ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is continuous implies N is continuous )
assume A2: N is continuous ; ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is continuous )
for x being Point of the Scott TopAugmentation of N ex J being Basis of x st
for W being Subset of the Scott TopAugmentation of N st W in J holds
W is Filter of the Scott TopAugmentation of N
proof
let x be Point of the Scott TopAugmentation of N; ::_thesis: ex J being Basis of x st
for W being Subset of the Scott TopAugmentation of N st W in J holds
W is Filter of the Scott TopAugmentation of N
consider J being Basis of x such that
A3: for W being Subset of the Scott TopAugmentation of N st W in J holds
( W is open & W is filtered ) by A2, WAYBEL14:35;
take J ; ::_thesis: for W being Subset of the Scott TopAugmentation of N st W in J holds
W is Filter of the Scott TopAugmentation of N
let W be Subset of the Scott TopAugmentation of N; ::_thesis: ( W in J implies W is Filter of the Scott TopAugmentation of N )
assume A4: W in J ; ::_thesis: W is Filter of the Scott TopAugmentation of N
then W is open by A3;
hence W is Filter of the Scott TopAugmentation of N by A3, A4, WAYBEL11:def_4, YELLOW_8:12; ::_thesis: verum
end;
hence N is with_open_semilattices by Th32; ::_thesis: InclPoset (sigma N) is continuous
InclPoset (sigma the Scott TopAugmentation of N) is continuous by A2, WAYBEL14:36;
hence InclPoset (sigma N) is continuous by A1, YELLOW_9:52; ::_thesis: verum
end;
assume that
A5: N is with_open_semilattices and
A6: InclPoset (sigma N) is continuous ; ::_thesis: N is continuous
A7: for x being Element of the Scott TopAugmentation of N ex J being Basis of x st
for Y being Subset of the Scott TopAugmentation of N st Y in J holds
( Y is open & Y is filtered )
proof
let x be Element of the Scott TopAugmentation of N; ::_thesis: ex J being Basis of x st
for Y being Subset of the Scott TopAugmentation of N st Y in J holds
( Y is open & Y is filtered )
reconsider y = x as Element of N by A1;
consider J being Basis of y such that
A8: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A5, Def4;
reconsider J9 = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16;
take J9 ; ::_thesis: for Y being Subset of the Scott TopAugmentation of N st Y in J9 holds
( Y is open & Y is filtered )
let Y be Subset of the Scott TopAugmentation of N; ::_thesis: ( Y in J9 implies ( Y is open & Y is filtered ) )
assume A9: Y in J9 ; ::_thesis: ( Y is open & Y is filtered )
then consider A being Subset of N such that
A10: Y = uparrow A and
A11: A in J ;
subrelstr A is meet-inheriting by A8, A11;
then A is filtered by YELLOW12:26;
hence ( Y is open & Y is filtered ) by A1, A9, A10, WAYBEL_0:4, YELLOW_8:12; ::_thesis: verum
end;
sigma the Scott TopAugmentation of N = sigma N by A1, YELLOW_9:52;
then for x being Element of the Scott TopAugmentation of N holds x = "\/" ( { (inf X) where X is Subset of the Scott TopAugmentation of N : ( x in X & X in sigma the Scott TopAugmentation of N ) } , the Scott TopAugmentation of N) by A7, A6, WAYBEL14:37;
then the Scott TopAugmentation of N is continuous by WAYBEL14:38;
hence N is continuous by A1, YELLOW12:15; ::_thesis: verum
end;
registration
cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson continuous -> complete Lawson with_open_semilattices for TopRelStr ;
coherence
for b1 being complete Lawson TopLattice st b1 is continuous holds
b1 is with_open_semilattices by Th35;
end;
registration
let N be complete Lawson continuous TopLattice;
cluster InclPoset (sigma N) -> continuous ;
coherence
InclPoset (sigma N) is continuous by Th35;
end;
theorem :: WAYBEL30:36
for N being complete Lawson continuous TopLattice holds
( N is compact & N is Hausdorff & N is topological_semilattice & N is with_open_semilattices )
proof
let N be complete Lawson continuous TopLattice; ::_thesis: ( N is compact & N is Hausdorff & N is topological_semilattice & N is with_open_semilattices )
thus ( N is compact & N is Hausdorff ) ; ::_thesis: ( N is topological_semilattice & N is with_open_semilattices )
InclPoset (sigma N) is continuous ;
hence N is topological_semilattice by Th22; ::_thesis: N is with_open_semilattices
thus N is with_open_semilattices ; ::_thesis: verum
end;
theorem :: WAYBEL30:37
for N being Hausdorff complete Lawson topological_semilattice with_open_semilattices TopLattice holds N is with_compact_semilattices
proof
let N be Hausdorff complete Lawson topological_semilattice with_open_semilattices TopLattice; ::_thesis: N is with_compact_semilattices
let x be Point of N; :: according to WAYBEL30:def_3 ::_thesis: ex J being basis of x st
for A being Subset of N st A in J holds
( subrelstr A is meet-inheriting & A is compact )
consider BO being Basis of x such that
A1: for A being Subset of N st A in BO holds
subrelstr A is meet-inheriting by Def4;
set BC = { (Cl A) where A is Subset of N : A in BO } ;
{ (Cl A) where A is Subset of N : A in BO } c= bool the carrier of N
proof
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in { (Cl A) where A is Subset of N : A in BO } or k in bool the carrier of N )
assume k in { (Cl A) where A is Subset of N : A in BO } ; ::_thesis: k in bool the carrier of N
then ex A being Subset of N st
( k = Cl A & A in BO ) ;
hence k in bool the carrier of N ; ::_thesis: verum
end;
then reconsider BC = { (Cl A) where A is Subset of N : A in BO } as Subset-Family of N ;
BC is basis of x
proof
let S be a_neighborhood of x; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of x st
( b1 in BC & b1 c= S )
A2: Int S c= S by TOPS_1:16;
x in Int S by CONNSP_2:def_1;
then consider W being Subset of N such that
A3: W in BO and
A4: W c= Int S by YELLOW_8:13;
A5: W is open by A3, YELLOW_8:12;
x in W by A3, YELLOW_8:12;
then x in Int W by A5, TOPS_1:23;
then reconsider T = W as a_neighborhood of x by CONNSP_2:def_1;
percases ( W <> [#] N or W = [#] N ) ;
supposeA6: W <> [#] N ; ::_thesis: ex b1 being a_neighborhood of x st
( b1 in BC & b1 c= S )
x in W by A3, YELLOW_8:12;
then {x} c= W by ZFMISC_1:31;
then consider G being Subset of N such that
A7: G is open and
A8: {x} c= G and
A9: Cl G c= W by A5, A6, CONNSP_2:20;
x in G by A8, ZFMISC_1:31;
then consider K being Subset of N such that
A10: K in BO and
A11: K c= G by A7, YELLOW_8:13;
A12: K is open by A10, YELLOW_8:12;
A13: Int K c= Int (Cl K) by PRE_TOPC:18, TOPS_1:19;
x in K by A10, YELLOW_8:12;
then x in Int K by A12, TOPS_1:23;
then reconsider KK = Cl K as a_neighborhood of x by A13, CONNSP_2:def_1;
take KK ; ::_thesis: ( KK in BC & KK c= S )
thus KK in BC by A10; ::_thesis: KK c= S
Cl K c= Cl G by A11, PRE_TOPC:19;
then Cl K c= W by A9, XBOOLE_1:1;
then KK c= Int S by A4, XBOOLE_1:1;
hence KK c= S by A2, XBOOLE_1:1; ::_thesis: verum
end;
supposeA14: W = [#] N ; ::_thesis: ex b1 being a_neighborhood of x st
( b1 in BC & b1 c= S )
take T ; ::_thesis: ( T in BC & T c= S )
Cl ([#] N) = [#] N by TOPS_1:2;
hence T in BC by A3, A14; ::_thesis: T c= S
thus T c= S by A4, A2, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
then reconsider BC = BC as basis of x ;
take BC ; ::_thesis: for A being Subset of N st A in BC holds
( subrelstr A is meet-inheriting & A is compact )
let A be Subset of N; ::_thesis: ( A in BC implies ( subrelstr A is meet-inheriting & A is compact ) )
assume A in BC ; ::_thesis: ( subrelstr A is meet-inheriting & A is compact )
then consider C being Subset of N such that
A15: A = Cl C and
A16: C in BO ;
subrelstr C is meet-inheriting by A1, A16;
hence subrelstr A is meet-inheriting by A15, Th31; ::_thesis: A is compact
thus A is compact by A15, COMPTS_1:8; ::_thesis: verum
end;
theorem :: WAYBEL30:38
for N being Hausdorff complete Lawson meet-continuous TopLattice
for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)
proof
let N be Hausdorff complete Lawson meet-continuous TopLattice; ::_thesis: for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)
let x be Element of N; ::_thesis: x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)
set S = the complete Scott TopAugmentation of N;
A1: InclPoset (sigma the complete Scott TopAugmentation of N) is continuous by WAYBEL14:36;
A2: RelStr(# the carrier of the complete Scott TopAugmentation of N, the InternalRel of the complete Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
then reconsider y = x as Element of the complete Scott TopAugmentation of N ;
for y being Element of the complete Scott TopAugmentation of N ex J being Basis of y st
for X being Subset of the complete Scott TopAugmentation of N st X in J holds
( X is open & X is filtered ) by WAYBEL14:35;
hence x = "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( y in X & X in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A1, WAYBEL14:37
.= "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } ,N) by A2, YELLOW_0:17, YELLOW_0:26
.= "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by Th34 ;
::_thesis: verum
end;
theorem :: WAYBEL30:39
for N being complete Lawson meet-continuous TopLattice holds
( N is continuous iff for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) )
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( N is continuous iff for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) )
set S = the complete Scott TopAugmentation of N;
A1: RelStr(# the carrier of the complete Scott TopAugmentation of N, the InternalRel of the complete Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
hereby ::_thesis: ( ( for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) ) implies N is continuous )
assume A2: N is continuous ; ::_thesis: for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)
then A3: for x being Element of the complete Scott TopAugmentation of N ex J being Basis of x st
for Y being Subset of the complete Scott TopAugmentation of N st Y in J holds
( Y is open & Y is filtered ) by WAYBEL14:35;
let x be Element of N; ::_thesis: x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N)
InclPoset (sigma the complete Scott TopAugmentation of N) is continuous by A2, WAYBEL14:36;
hence x = "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A3, A1, WAYBEL14:37
.= "\/" ( { (inf X) where X is Subset of the complete Scott TopAugmentation of N : ( x in X & X in sigma the complete Scott TopAugmentation of N ) } ,N) by A1, YELLOW_0:17, YELLOW_0:26
.= "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by Th34 ;
::_thesis: verum
end;
assume A4: for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) ; ::_thesis: N is continuous
now__::_thesis:_for_x_being_Element_of_the_complete_Scott_TopAugmentation_of_N_holds_x_=_"\/"_(_{__(inf_V)_where_V_is_Subset_of_the_complete_Scott_TopAugmentation_of_N_:_(_x_in_V_&_V_in_sigma_the_complete_Scott_TopAugmentation_of_N_)__}__,_the_complete_Scott_TopAugmentation_of_N)
let x be Element of the complete Scott TopAugmentation of N; ::_thesis: x = "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N)
thus x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) by A1, A4
.= "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } ,N) by A1, Th34
.= "\/" ( { (inf V) where V is Subset of the complete Scott TopAugmentation of N : ( x in V & V in sigma the complete Scott TopAugmentation of N ) } , the complete Scott TopAugmentation of N) by A1, YELLOW_0:17, YELLOW_0:26 ; ::_thesis: verum
end;
then the complete Scott TopAugmentation of N is continuous by WAYBEL14:38;
hence N is continuous by A1, YELLOW12:15; ::_thesis: verum
end;
theorem Th40: :: WAYBEL30:40
for N being complete Lawson meet-continuous TopLattice holds
( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) )
proof
let N be complete Lawson meet-continuous TopLattice; ::_thesis: ( N is algebraic iff ( N is with_open_semilattices & InclPoset (sigma N) is algebraic ) )
set S = the Scott TopAugmentation of N;
A1: RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def_4;
hereby ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic implies N is algebraic )
assume A2: N is algebraic ; ::_thesis: ( N is with_open_semilattices & InclPoset (sigma N) is algebraic )
then reconsider M = N as algebraic LATTICE ;
M is continuous ;
hence N is with_open_semilattices ; ::_thesis: InclPoset (sigma N) is algebraic
the Scott TopAugmentation of N is algebraic by A1, A2, WAYBEL_8:17;
then ex K being Basis of the Scott TopAugmentation of N st K = { (uparrow x) where x is Element of the Scott TopAugmentation of N : x in the carrier of (CompactSublatt the Scott TopAugmentation of N) } by WAYBEL14:42;
then InclPoset (sigma the Scott TopAugmentation of N) is algebraic by WAYBEL14:43;
hence InclPoset (sigma N) is algebraic by A1, YELLOW_9:52; ::_thesis: verum
end;
assume that
A3: N is with_open_semilattices and
A4: InclPoset (sigma N) is algebraic ; ::_thesis: N is algebraic
reconsider T = InclPoset (sigma N) as algebraic LATTICE by A4;
T is continuous ;
then N is continuous by A3, Th35;
then for x being Element of the Scott TopAugmentation of N ex K being Basis of x st
for Y being Subset of the Scott TopAugmentation of N st Y in K holds
( Y is open & Y is filtered ) by WAYBEL14:35;
then A5: for V being Element of (InclPoset (sigma the Scott TopAugmentation of N)) ex VV being Subset of (InclPoset (sigma the Scott TopAugmentation of N)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma the Scott TopAugmentation of N)) st W in VV holds
W is co-prime ) ) by WAYBEL14:39;
InclPoset (sigma the Scott TopAugmentation of N) is algebraic by A1, A4, YELLOW_9:52;
then ex K being Basis of the Scott TopAugmentation of N st K = { (uparrow x) where x is Element of the Scott TopAugmentation of N : x in the carrier of (CompactSublatt the Scott TopAugmentation of N) } by A5, WAYBEL14:44;
then the Scott TopAugmentation of N is algebraic by WAYBEL14:45;
hence N is algebraic by A1, WAYBEL_8:17; ::_thesis: verum
end;
registration
let N be complete algebraic Lawson meet-continuous TopLattice;
cluster InclPoset (sigma N) -> algebraic ;
coherence
InclPoset (sigma N) is algebraic by Th40;
end;