:: WAYBEL19 semantic presentation
begin
definition
let T be non empty TopRelStr ;
attrT is lower means :Def1: :: WAYBEL19:def 1
{ ((uparrow x) `) where x is Element of T : verum } is prebasis of T;
end;
:: deftheorem Def1 defines lower WAYBEL19:def_1_:_
for T being non empty TopRelStr holds
( T is lower iff { ((uparrow x) `) where x is Element of T : verum } is prebasis of T );
Lm1: now__::_thesis:_for_LL,_T_being_non_empty_RelStr_st_RelStr(#_the_carrier_of_LL,_the_InternalRel_of_LL_#)_=_RelStr(#_the_carrier_of_T,_the_InternalRel_of_T_#)_holds_
{__((uparrow_x)_`)_where_x_is_Element_of_LL_:_verum__}__=__{__((uparrow_x)_`)_where_x_is_Element_of_T_:_verum__}_
let LL, T be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) implies { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } )
assume A1: RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of T, the InternalRel of T #) ; ::_thesis: { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum }
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
set A = { ((uparrow x) `) where x is Element of LL : verum } ;
thus { ((uparrow x) `) where x is Element of LL : verum } = { ((uparrow x) `) where x is Element of T : verum } ::_thesis: verum
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { ((uparrow x) `) where x is Element of T : verum } c= { ((uparrow x) `) where x is Element of LL : verum }
let a be set ; ::_thesis: ( a in { ((uparrow x) `) where x is Element of LL : verum } implies a in { ((uparrow x) `) where x is Element of T : verum } )
assume a in { ((uparrow x) `) where x is Element of LL : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of T : verum }
then consider x being Element of LL such that
A2: a = (uparrow x) ` ;
reconsider y = x as Element of T by A1;
a = (uparrow y) ` by A1, A2, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in { ((uparrow x) `) where x is Element of LL : verum } )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of LL : verum }
then consider x being Element of T such that
A3: a = (uparrow x) ` ;
reconsider y = x as Element of LL by A1;
a = (uparrow y) ` by A1, A3, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of LL : verum } ; ::_thesis: verum
end;
end;
registration
cluster1 -element TopSpace-like reflexive -> 1 -element TopSpace-like reflexive lower for TopRelStr ;
coherence
for b1 being 1 -element TopSpace-like reflexive TopRelStr holds b1 is lower
proof
let T be 1 -element TopSpace-like reflexive TopRelStr ; ::_thesis: T is lower
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
reconsider F = { the carrier of T} as Basis of T by YELLOW_9:10;
{ ((uparrow x) `) where x is Element of T : verum } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in bool the carrier of T )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in bool the carrier of T
then ex x being Element of T st a = (uparrow x) ` ;
hence a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider C = { ((uparrow x) `) where x is Element of T : verum } as Subset-Family of T ;
reconsider C = C as Subset-Family of T ;
{ ((uparrow x) `) where x is Element of T : verum } = {{}}
proof
set x = the Element of T;
thus { ((uparrow x) `) where x is Element of T : verum } c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= { ((uparrow x) `) where x is Element of T : verum }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in {{}} )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in {{}}
then consider x being Element of T such that
A1: a = (uparrow x) ` ;
x <= x ;
then A2: x in uparrow x by WAYBEL_0:18;
the carrier of T = {x} by YELLOW_9:9;
then ( a = {} or ( a = the carrier of T & not x in a ) ) by A2, A1, XBOOLE_0:def_5, ZFMISC_1:33;
hence a in {{}} by TARSKI:def_1; ::_thesis: verum
end;
the Element of T <= the Element of T ;
then A3: the Element of T in uparrow the Element of T by WAYBEL_0:18;
the carrier of T = { the Element of T} by YELLOW_9:9;
then ( (uparrow the Element of T) ` = {} or ( (uparrow the Element of T) ` = the carrier of T & not the Element of T in (uparrow the Element of T) ` ) ) by A3, XBOOLE_0:def_5, ZFMISC_1:33;
then {} in { ((uparrow x) `) where x is Element of T : verum } ;
hence {{}} c= { ((uparrow x) `) where x is Element of T : verum } by ZFMISC_1:31; ::_thesis: verum
end;
then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11;
then A4: F c= FinMeetCl C by ZFMISC_1:7;
{ ((uparrow x) `) where x is Element of T : verum } c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in the topology of T )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in the topology of T
then consider x being Element of T such that
A5: a = (uparrow x) ` ;
a c= {}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in {} )
x <= x ;
then A6: x in uparrow x by WAYBEL_0:18;
A7: uparrow x misses a by A5, XBOOLE_1:79;
assume A8: y in a ; ::_thesis: y in {}
then y = x by A5, STRUCT_0:def_10;
then x in (uparrow x) /\ a by A6, A8, XBOOLE_0:def_4;
hence y in {} by A7, XBOOLE_0:def_7; ::_thesis: verum
end;
then a = {} ;
hence a in the topology of T by PRE_TOPC:1; ::_thesis: verum
end;
hence { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A4, CANTOR_1:def_4, TOPS_2:64; :: according to WAYBEL19:def_1 ::_thesis: verum
end;
end;
registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict non void lower for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is lower & b1 is trivial & b1 is complete & b1 is strict )
proof
set T = the 1 -element complete strict TopLattice;
take the 1 -element complete strict TopLattice ; ::_thesis: ( the 1 -element complete strict TopLattice is lower & the 1 -element complete strict TopLattice is trivial & the 1 -element complete strict TopLattice is complete & the 1 -element complete strict TopLattice is strict )
thus ( the 1 -element complete strict TopLattice is lower & the 1 -element complete strict TopLattice is trivial & the 1 -element complete strict TopLattice is complete & the 1 -element complete strict TopLattice is strict ) ; ::_thesis: verum
end;
end;
theorem Th1: :: WAYBEL19:1
for LL being non empty RelStr ex T being correct strict TopAugmentation of LL st T is lower
proof
let LL be non empty RelStr ; ::_thesis: ex T being correct strict TopAugmentation of LL st T is lower
set A = { ((uparrow x) `) where x is Element of LL : verum } ;
{ ((uparrow x) `) where x is Element of LL : verum } c= bool the carrier of LL
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of LL : verum } or a in bool the carrier of LL )
assume a in { ((uparrow x) `) where x is Element of LL : verum } ; ::_thesis: a in bool the carrier of LL
then ex x being Element of LL st a = (uparrow x) ` ;
hence a in bool the carrier of LL ; ::_thesis: verum
end;
then reconsider A = { ((uparrow x) `) where x is Element of LL : verum } as Subset-Family of LL ;
set T = TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #);
reconsider S = TopStruct(# the carrier of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace by CANTOR_1:15;
A1: TopStruct(# the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #), the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) #) = S ;
TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) is TopSpace-like
proof
thus the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) by A1, PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #)) holds
( not b1 c= the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of bool the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ) ) )
hereby ::_thesis: for b1, b2 being Element of bool the carrier of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) )
let a be Subset-Family of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #); ::_thesis: ( a c= the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) implies union a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) )
reconsider b = a as Subset-Family of S ;
assume a c= the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: union a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #)
then union b in the topology of S by PRE_TOPC:def_1;
hence union a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: verum
end;
let a, b be Subset of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #); ::_thesis: ( not a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or not b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) )
assume that
A2: a in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) and
A3: b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: a /\ b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #)
a /\ b in the topology of S by A2, A3, PRE_TOPC:def_1;
hence a /\ b in the topology of TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) ; ::_thesis: verum
end;
then reconsider T = TopRelStr(# the carrier of LL, the InternalRel of LL,(UniCl (FinMeetCl A)) #) as non empty TopSpace-like strict TopRelStr ;
take T ; ::_thesis: ( T is correct strict TopAugmentation of LL & T is lower )
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of LL, the InternalRel of LL #) ;
hence T is correct strict TopAugmentation of LL by YELLOW_9:def_4; ::_thesis: T is lower
A4: A is prebasis of S by CANTOR_1:18;
then consider F being Basis of S such that
A5: F c= FinMeetCl A by CANTOR_1:def_4;
A6: the topology of T c= UniCl F by CANTOR_1:def_2;
F c= the topology of T by TOPS_2:64;
then A7: F is Basis of T by A6, CANTOR_1:def_2, TOPS_2:64;
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of LL, the InternalRel of LL #) ;
then A8: A = { ((uparrow x) `) where x is Element of T : verum } by Lm1;
A c= the topology of S by A4, TOPS_2:64;
hence { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A7, A5, A8, CANTOR_1:def_4, TOPS_2:64; :: according to WAYBEL19:def_1 ::_thesis: verum
end;
registration
let R be non empty RelStr ;
cluster non empty correct strict lower for TopAugmentation of R;
existence
ex b1 being correct strict TopAugmentation of R st b1 is lower by Th1;
end;
theorem Th2: :: WAYBEL19:2
for L1, L2 being non empty TopSpace-like lower TopRelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
the topology of L1 = the topology of L2
proof
let L1, L2 be non empty TopSpace-like lower TopRelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies the topology of L1 = the topology of L2 )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: the topology of L1 = the topology of L2
set B2 = { ((uparrow x) `) where x is Element of L2 : verum } ;
set B1 = { ((uparrow x) `) where x is Element of L1 : verum } ;
A2: { ((uparrow x) `) where x is Element of L1 : verum } is prebasis of L1 by Def1;
A3: { ((uparrow x) `) where x is Element of L2 : verum } is prebasis of L2 by Def1;
{ ((uparrow x) `) where x is Element of L1 : verum } = { ((uparrow x) `) where x is Element of L2 : verum } by A1, Lm1;
hence the topology of L1 = the topology of L2 by A1, A2, A3, YELLOW_9:26; ::_thesis: verum
end;
definition
let R be non empty RelStr ;
func omega R -> Subset-Family of R means :Def2: :: WAYBEL19:def 2
for T being correct lower TopAugmentation of R holds it = the topology of T;
uniqueness
for b1, b2 being Subset-Family of R st ( for T being correct lower TopAugmentation of R holds b1 = the topology of T ) & ( for T being correct lower TopAugmentation of R holds b2 = the topology of T ) holds
b1 = b2
proof
set T = the correct lower TopAugmentation of R;
let X1, X2 be Subset-Family of R; ::_thesis: ( ( for T being correct lower TopAugmentation of R holds X1 = the topology of T ) & ( for T being correct lower TopAugmentation of R holds X2 = the topology of T ) implies X1 = X2 )
assume for T being correct lower TopAugmentation of R holds X1 = the topology of T ; ::_thesis: ( ex T being correct lower TopAugmentation of R st not X2 = the topology of T or X1 = X2 )
then X1 = the topology of the correct lower TopAugmentation of R ;
hence ( ex T being correct lower TopAugmentation of R st not X2 = the topology of T or X1 = X2 ) ; ::_thesis: verum
end;
existence
ex b1 being Subset-Family of R st
for T being correct lower TopAugmentation of R holds b1 = the topology of T
proof
set S = the correct lower TopAugmentation of R;
A1: RelStr(# the carrier of the correct lower TopAugmentation of R, the InternalRel of the correct lower TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then reconsider X = the topology of the correct lower TopAugmentation of R as Subset-Family of R ;
take X ; ::_thesis: for T being correct lower TopAugmentation of R holds X = the topology of T
let T be correct lower TopAugmentation of R; ::_thesis: X = the topology of T
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
hence X = the topology of T by A1, Th2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines omega WAYBEL19:def_2_:_
for R being non empty RelStr
for b2 being Subset-Family of R holds
( b2 = omega R iff for T being correct lower TopAugmentation of R holds b2 = the topology of T );
theorem Th3: :: WAYBEL19:3
for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
omega R1 = omega R2
proof
let R1, R2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies omega R1 = omega R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: omega R1 = omega R2
set S = the correct lower TopAugmentation of R1;
RelStr(# the carrier of the correct lower TopAugmentation of R1, the InternalRel of the correct lower TopAugmentation of R1 #) = RelStr(# the carrier of R1, the InternalRel of R1 #) by YELLOW_9:def_4;
then A2: the correct lower TopAugmentation of R1 is TopAugmentation of R2 by A1, YELLOW_9:def_4;
omega R1 = the topology of the correct lower TopAugmentation of R1 by Def2;
hence omega R1 = omega R2 by A2, Def2; ::_thesis: verum
end;
theorem Th4: :: WAYBEL19:4
for T being non empty lower TopRelStr
for x being Point of T holds
( (uparrow x) ` is open & uparrow x is closed )
proof
let T be non empty lower TopRelStr ; ::_thesis: for x being Point of T holds
( (uparrow x) ` is open & uparrow x is closed )
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
let x be Point of T; ::_thesis: ( (uparrow x) ` is open & uparrow x is closed )
reconsider a = x as Element of T ;
{ ((uparrow x) `) where x is Element of T : verum } is prebasis of T by Def1;
then A1: { ((uparrow x) `) where x is Element of T : verum } c= the topology of T by TOPS_2:64;
A2: (uparrow a) ` in { ((uparrow x) `) where x is Element of T : verum } ;
hence (uparrow x) ` in the topology of T by A1; :: according to PRE_TOPC:def_2 ::_thesis: uparrow x is closed
thus ([#] T) \ (uparrow x) in the topology of T by A2, A1; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: verum
end;
theorem Th5: :: WAYBEL19:5
for T being non empty transitive lower TopRelStr
for A being Subset of T st A is open holds
A is lower
proof
let T be non empty transitive lower TopRelStr ; ::_thesis: for A being Subset of T st A is open holds
A is lower
reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1;
let A be Subset of T; ::_thesis: ( A is open implies A is lower )
assume A1: A in the topology of T ; :: according to PRE_TOPC:def_2 ::_thesis: A is lower
let x, y be Element of T; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in A or not y <= x or y in A )
consider F being Basis of T such that
A2: F c= FinMeetCl BB by CANTOR_1:def_4;
the topology of T c= UniCl F by CANTOR_1:def_2;
then consider Y being Subset-Family of T such that
A3: Y c= F and
A4: A = union Y by A1, CANTOR_1:def_1;
assume x in A ; ::_thesis: ( not y <= x or y in A )
then consider Z being set such that
A5: x in Z and
A6: Z in Y by A4, TARSKI:def_4;
Z in F by A3, A6;
then consider X being Subset-Family of T such that
A7: X c= BB and
X is finite and
A8: Z = Intersect X by A2, CANTOR_1:def_3;
assume A9: x >= y ; ::_thesis: y in A
now__::_thesis:_for_Q_being_set_st_Q_in_X_holds_
y_in_Q
let Q be set ; ::_thesis: ( Q in X implies y in Q )
assume A10: Q in X ; ::_thesis: y in Q
then Q in BB by A7;
then consider z being Element of T such that
A11: Q = (uparrow z) ` ;
uparrow z misses Q by A11, XBOOLE_1:79;
then A12: (uparrow z) /\ Q = {} T by XBOOLE_0:def_7;
x in Q by A5, A8, A10, SETFAM_1:43;
then not x in uparrow z by A12, XBOOLE_0:def_4;
then not x >= z by WAYBEL_0:18;
then not y >= z by A9, ORDERS_2:3;
then not y in uparrow z by WAYBEL_0:18;
hence y in Q by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then y in Z by A8, SETFAM_1:43;
hence y in A by A4, A6, TARSKI:def_4; ::_thesis: verum
end;
theorem Th6: :: WAYBEL19:6
for T being non empty transitive lower TopRelStr
for A being Subset of T st A is closed holds
A is upper
proof
let T be non empty transitive lower TopRelStr ; ::_thesis: for A being Subset of T st A is closed holds
A is upper
let A be Subset of T; ::_thesis: ( A is closed implies A is upper )
assume ([#] T) \ A in the topology of T ; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: A is upper
then A ` is open by PRE_TOPC:def_2;
then A1: A ` is lower by Th5;
let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A )
assume that
A2: x in A and
A3: x <= y and
A4: not y in A ; ::_thesis: contradiction
A5: y in A ` by A4, XBOOLE_0:def_5;
not x in A ` by A2, XBOOLE_0:def_5;
hence contradiction by A5, A1, A3, WAYBEL_0:def_19; ::_thesis: verum
end;
theorem Th7: :: WAYBEL19:7
for T being non empty TopSpace-like TopRelStr holds
( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T )
proof
let T be non empty TopSpace-like TopRelStr ; ::_thesis: ( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T )
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
{ ((uparrow x) `) where x is Element of T : verum } c= bool the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((uparrow x) `) where x is Element of T : verum } or x in bool the carrier of T )
assume x in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: x in bool the carrier of T
then ex y being Element of T st x = (uparrow y) ` ;
hence x in bool the carrier of T ; ::_thesis: verum
end;
then reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as Subset-Family of T ;
reconsider T9 = T as non empty RelStr ;
set A = { ((uparrow F) `) where F is Subset of T : F is finite } ;
reconsider BB = BB as Subset-Family of T ;
A1: { ((uparrow F) `) where F is Subset of T : F is finite } = FinMeetCl BB
proof
deffunc H1( Element of T9) -> Element of bool the carrier of T9 = uparrow $1;
defpred S1[ set , set ] means ex x being Element of T st
( x = $2 & $1 = (uparrow x) ` );
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: FinMeetCl BB c= { ((uparrow F) `) where F is Subset of T : F is finite }
deffunc H2( Element of T9) -> Element of bool the carrier of T9 = uparrow $1;
let a be set ; ::_thesis: ( a in { ((uparrow F) `) where F is Subset of T : F is finite } implies a in FinMeetCl BB )
assume a in { ((uparrow F) `) where F is Subset of T : F is finite } ; ::_thesis: a in FinMeetCl BB
then consider F being Subset of T such that
A2: a = (uparrow F) ` and
A3: F is finite ;
set Y = { (uparrow x) where x is Element of T : x in F } ;
{ (uparrow x) where x is Element of T : x in F } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (uparrow x) where x is Element of T : x in F } or a in bool the carrier of T )
assume a in { (uparrow x) where x is Element of T : x in F } ; ::_thesis: a in bool the carrier of T
then ex x being Element of T st
( a = uparrow x & x in F ) ;
hence a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider Y = { (uparrow x) where x is Element of T : x in F } as Subset-Family of T ;
reconsider Y = Y as Subset-Family of T ;
uparrow F = union Y by YELLOW_9:4;
then A4: a = Intersect (COMPLEMENT Y) by A2, YELLOW_8:6;
reconsider Y9 = Y as Subset-Family of T9 ;
A5: Y9 = { H2(x) where x is Element of T9 : x in F } ;
A6: COMPLEMENT Y9 = { (H2(x) `) where x is Element of T9 : x in F } from YELLOW_9:sch_2(A5);
A7: COMPLEMENT Y c= BB
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in COMPLEMENT Y or b in BB )
assume b in COMPLEMENT Y ; ::_thesis: b in BB
then ex x being Element of T st
( b = (uparrow x) ` & x in F ) by A6;
hence b in BB ; ::_thesis: verum
end;
deffunc H3( Element of T) -> Element of bool the carrier of T = (uparrow $1) ` ;
{ H3(x) where x is Element of T : x in F } is finite from FRAENKEL:sch_21(A3);
hence a in FinMeetCl BB by A7, A6, A4, CANTOR_1:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in FinMeetCl BB or a in { ((uparrow F) `) where F is Subset of T : F is finite } )
assume a in FinMeetCl BB ; ::_thesis: a in { ((uparrow F) `) where F is Subset of T : F is finite }
then consider Y being Subset-Family of T such that
A8: Y c= BB and
A9: Y is finite and
A10: a = Intersect Y by CANTOR_1:def_3;
A11: now__::_thesis:_for_y_being_set_st_y_in_Y_holds_
ex_b_being_set_st_
(_b_in_the_carrier_of_T_&_S1[y,b]_)
let y be set ; ::_thesis: ( y in Y implies ex b being set st
( b in the carrier of T & S1[y,b] ) )
assume y in Y ; ::_thesis: ex b being set st
( b in the carrier of T & S1[y,b] )
then y in BB by A8;
then ex x being Element of T st y = (uparrow x) ` ;
hence ex b being set st
( b in the carrier of T & S1[y,b] ) ; ::_thesis: verum
end;
consider f being Function such that
A12: ( dom f = Y & rng f c= the carrier of T ) and
A13: for y being set st y in Y holds
S1[y,f . y] from FUNCT_1:sch_5(A11);
reconsider F = rng f as Subset of T by A12;
A14: F is finite by A9, A12, FINSET_1:8;
set X = { (uparrow x) where x is Element of T : x in F } ;
{ (uparrow x) where x is Element of T : x in F } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (uparrow x) where x is Element of T : x in F } or a in bool the carrier of T )
assume a in { (uparrow x) where x is Element of T : x in F } ; ::_thesis: a in bool the carrier of T
then ex x being Element of T st
( a = uparrow x & x in F ) ;
hence a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider X = { (uparrow x) where x is Element of T : x in F } as Subset-Family of T ;
reconsider X = X as Subset-Family of T ;
reconsider X9 = X as Subset-Family of T9 ;
A15: X9 = { H1(x) where x is Element of T9 : x in F } ;
A16: COMPLEMENT X9 = { (H1(x) `) where x is Element of T9 : x in F } from YELLOW_9:sch_2(A15);
A17: COMPLEMENT X = Y
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Y c= COMPLEMENT X
let a be set ; ::_thesis: ( a in COMPLEMENT X implies a in Y )
assume a in COMPLEMENT X ; ::_thesis: a in Y
then consider x being Element of T9 such that
A18: a = (uparrow x) ` and
A19: x in F by A16;
consider y being set such that
A20: y in Y and
A21: x = f . y by A12, A19, FUNCT_1:def_3;
ex z being Element of T st
( z = f . y & y = (uparrow z) ` ) by A13, A20;
hence a in Y by A18, A20, A21; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in COMPLEMENT X )
assume A22: a in Y ; ::_thesis: a in COMPLEMENT X
then consider z being Element of T such that
A23: z = f . a and
A24: a = (uparrow z) ` by A13;
z in F by A12, A22, A23, FUNCT_1:def_3;
hence a in COMPLEMENT X by A16, A24; ::_thesis: verum
end;
uparrow F = union X by YELLOW_9:4;
then a = (uparrow F) ` by A10, A17, YELLOW_8:6;
hence a in { ((uparrow F) `) where F is Subset of T : F is finite } by A14; ::_thesis: verum
end;
( T is lower iff BB is prebasis of T ) by Def1;
hence ( T is lower iff { ((uparrow F) `) where F is Subset of T : F is finite } is Basis of T ) by A1, YELLOW_9:23; ::_thesis: verum
end;
theorem Th8: :: WAYBEL19:8
for S, T being complete lower TopLattice
for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds
f is continuous
proof
let S, T be non empty complete lower TopLattice; ::_thesis: for f being Function of S,T st ( for X being non empty Subset of S holds f preserves_inf_of X ) holds
f is continuous
reconsider BB = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1;
let f be Function of S,T; ::_thesis: ( ( for X being non empty Subset of S holds f preserves_inf_of X ) implies f is continuous )
assume A1: for X being non empty Subset of S holds f preserves_inf_of X ; ::_thesis: f is continuous
now__::_thesis:_for_A_being_Subset_of_T_st_A_in_BB_holds_
f_"_(A_`)_is_closed
let A be Subset of T; ::_thesis: ( A in BB implies f " (b1 `) is closed )
A2: ex_inf_of f " (A `),S by YELLOW_0:17;
A3: ex_inf_of A ` ,T by YELLOW_0:17;
A4: ex_inf_of f .: (f " (A `)),T by YELLOW_0:17;
assume A in BB ; ::_thesis: f " (b1 `) is closed
then consider x being Element of T such that
A5: A = (uparrow x) ` ;
set s = inf (f " (uparrow x));
percases ( f " (A `) = {} S or f " (A `) <> {} ) ;
suppose f " (A `) = {} S ; ::_thesis: f " (b1 `) is closed
hence f " (A `) is closed ; ::_thesis: verum
end;
suppose f " (A `) <> {} ; ::_thesis: f " (b1 `) is closed
then f preserves_inf_of f " (A `) by A1;
then A6: f . (inf (f " (uparrow x))) = inf (f .: (f " (A `))) by A5, A2, WAYBEL_0:def_30;
inf (A `) = x by A5, WAYBEL_0:39;
then A7: x <= f . (inf (f " (uparrow x))) by A6, A3, A4, FUNCT_1:75, YELLOW_0:35;
f " (A `) = uparrow (inf (f " (uparrow x)))
proof
thus f " (A `) c= uparrow (inf (f " (uparrow x))) :: according to XBOOLE_0:def_10 ::_thesis: uparrow (inf (f " (uparrow x))) c= f " (A `)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f " (A `) or a in uparrow (inf (f " (uparrow x))) )
assume A8: a in f " (A `) ; ::_thesis: a in uparrow (inf (f " (uparrow x)))
then reconsider a = a as Element of S ;
inf (f " (uparrow x)) <= a by A5, A8, YELLOW_2:22;
hence a in uparrow (inf (f " (uparrow x))) by WAYBEL_0:18; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in uparrow (inf (f " (uparrow x))) or a in f " (A `) )
assume A9: a in uparrow (inf (f " (uparrow x))) ; ::_thesis: a in f " (A `)
then reconsider a = a as Element of S ;
f preserves_inf_of {(inf (f " (uparrow x))),a} by A1;
then A10: f . ((inf (f " (uparrow x))) "/\" a) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by YELLOW_3:8;
inf (f " (uparrow x)) <= a by A9, WAYBEL_0:18;
then f . (inf (f " (uparrow x))) = (f . (inf (f " (uparrow x)))) "/\" (f . a) by A10, YELLOW_5:10;
then f . (inf (f " (uparrow x))) <= f . a by YELLOW_0:23;
then x <= f . a by A7, ORDERS_2:3;
then f . a in uparrow x by WAYBEL_0:18;
hence a in f " (A `) by A5, FUNCT_2:38; ::_thesis: verum
end;
hence f " (A `) is closed by Th4; ::_thesis: verum
end;
end;
end;
hence f is continuous by YELLOW_9:35; ::_thesis: verum
end;
theorem Th9: :: WAYBEL19:9
for S, T being complete lower TopLattice
for f being Function of S,T st f is infs-preserving holds
f is continuous
proof
let S, T be non empty complete lower TopLattice; ::_thesis: for f being Function of S,T st f is infs-preserving holds
f is continuous
let f be Function of S,T; ::_thesis: ( f is infs-preserving implies f is continuous )
assume f is infs-preserving ; ::_thesis: f is continuous
then for X being non empty Subset of S holds f preserves_inf_of X by WAYBEL_0:def_32;
hence f is continuous by Th8; ::_thesis: verum
end;
theorem Th10: :: WAYBEL19:10
for T being complete lower TopLattice
for BB being prebasis of T
for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) holds
inf F in Cl F
proof
let T be complete lower TopLattice; ::_thesis: for BB being prebasis of T
for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) holds
inf F in Cl F
let BB be prebasis of T; ::_thesis: for F being non empty filtered Subset of T st ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) holds
inf F in Cl F
let F be non empty filtered Subset of T; ::_thesis: ( ( for A being Subset of T st A in BB & inf F in A holds
F meets A ) implies inf F in Cl F )
assume A1: for A being Subset of T st A in BB & inf F in A holds
F meets A ; ::_thesis: inf F in Cl F
set N = F opp+id ;
set x = inf F;
A2: for A being Subset of T st A in BB & inf F in A holds
F opp+id is_eventually_in A
proof
let A be Subset of T; ::_thesis: ( A in BB & inf F in A implies F opp+id is_eventually_in A )
assume that
A3: A in BB and
A4: inf F in A ; ::_thesis: F opp+id is_eventually_in A
A is open by A3, TOPS_2:def_1;
then A5: A is lower by Th5;
F meets A by A3, A4, A1;
then consider i being set such that
A6: i in F and
A7: i in A by XBOOLE_0:3;
reconsider i = i as Element of (F opp+id) by A6, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds
( not i <= b1 or (F opp+id) . b1 in A )
let j be Element of (F opp+id); ::_thesis: ( not i <= j or (F opp+id) . j in A )
A8: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
then reconsider a = i, b = j as Element of (T opp) by YELLOW_0:58;
assume i <= j ; ::_thesis: (F opp+id) . j in A
then a <= b by A8, YELLOW_0:59;
then A9: ~ b <= ~ a by YELLOW_7:1;
(F opp+id) . j = j by YELLOW_9:7;
hence (F opp+id) . j in A by A9, A7, A5, WAYBEL_0:def_19; ::_thesis: verum
end;
A10: the carrier of (F opp+id) = F by YELLOW_9:7;
rng (netmap ((F opp+id),T)) c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (netmap ((F opp+id),T)) or x in F )
assume x in rng (netmap ((F opp+id),T)) ; ::_thesis: x in F
then consider a being set such that
A11: a in dom (netmap ((F opp+id),T)) and
A12: x = (netmap ((F opp+id),T)) . a by FUNCT_1:def_3;
reconsider a = a as Element of (F opp+id) by A11;
x = (F opp+id) . a by A12
.= a by YELLOW_9:7 ;
hence x in F by A10; ::_thesis: verum
end;
hence inf F in Cl F by A2, YELLOW_9:39; ::_thesis: verum
end;
theorem Th11: :: WAYBEL19:11
for S, T being complete lower TopLattice
for f being Function of S,T st f is continuous holds
f is filtered-infs-preserving
proof
let S, T be complete lower TopLattice; ::_thesis: for f being Function of S,T st f is continuous holds
f is filtered-infs-preserving
reconsider BB = { ((uparrow x) `) where x is Element of S : verum } as prebasis of S by Def1;
let f be Function of S,T; ::_thesis: ( f is continuous implies f is filtered-infs-preserving )
assume A1: f is continuous ; ::_thesis: f is filtered-infs-preserving
let F be Subset of S; :: according to WAYBEL_0:def_36 ::_thesis: ( F is empty or not F is filtered or f preserves_inf_of F )
assume that
A2: ( not F is empty & F is filtered ) and
ex_inf_of F,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: F,T & "/\" ((f .: F),T) = K76( the carrier of S, the carrier of T,f,("/\" (F,S))) )
for A being Subset of S st A in BB & inf F in A holds
F meets A
proof
let A be Subset of S; ::_thesis: ( A in BB & inf F in A implies F meets A )
assume A in BB ; ::_thesis: ( not inf F in A or F meets A )
then consider x being Element of S such that
A3: A = (uparrow x) ` ;
assume inf F in A ; ::_thesis: F meets A
then not inf F >= x by A3, YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of S such that
A4: y in F and
A5: not y >= x by LATTICE3:def_8;
y in A by A3, A5, YELLOW_9:1;
hence F meets A by A4, XBOOLE_0:3; ::_thesis: verum
end;
then A6: inf F in Cl F by A2, Th10;
A7: f is monotone
proof
let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or K76( the carrier of S, the carrier of T,f,x) <= K76( the carrier of S, the carrier of T,f,y) )
assume A8: x <= y ; ::_thesis: K76( the carrier of S, the carrier of T,f,x) <= K76( the carrier of S, the carrier of T,f,y)
f . x <= f . x ;
then f . x in uparrow (f . x) by WAYBEL_0:18;
then A9: x in f " (uparrow (f . x)) by FUNCT_2:38;
uparrow (f . x) is closed by Th4;
then f " (uparrow (f . x)) is closed by A1, PRE_TOPC:def_6;
then f " (uparrow (f . x)) is upper by Th6;
then y in f " (uparrow (f . x)) by A9, A8, WAYBEL_0:def_20;
then f . y in uparrow (f . x) by FUNCT_2:38;
hence K76( the carrier of S, the carrier of T,f,x) <= K76( the carrier of S, the carrier of T,f,y) by WAYBEL_0:18; ::_thesis: verum
end;
f . (inf F) is_<=_than f .: F
proof
let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: F or f . (inf F) <= x )
assume x in f .: F ; ::_thesis: f . (inf F) <= x
then consider a being set such that
A10: a in the carrier of S and
A11: a in F and
A12: x = f . a by FUNCT_2:64;
reconsider a = a as Element of S by A10;
inf F is_<=_than F by YELLOW_0:33;
then inf F <= a by A11, LATTICE3:def_8;
hence f . (inf F) <= x by A7, A12, WAYBEL_1:def_2; ::_thesis: verum
end;
then A13: f . (inf F) <= inf (f .: F) by YELLOW_0:33;
thus ex_inf_of f .: F,T by YELLOW_0:17; ::_thesis: "/\" ((f .: F),T) = K76( the carrier of S, the carrier of T,f,("/\" (F,S)))
F c= f " (uparrow (inf (f .: F)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in f " (uparrow (inf (f .: F))) )
assume A14: x in F ; ::_thesis: x in f " (uparrow (inf (f .: F)))
then reconsider s = x as Element of S ;
f . s in f .: F by A14, FUNCT_2:35;
then inf (f .: F) <= f . s by YELLOW_2:22;
then f . s in uparrow (inf (f .: F)) by WAYBEL_0:18;
hence x in f " (uparrow (inf (f .: F))) by FUNCT_2:38; ::_thesis: verum
end;
then A15: Cl F c= Cl (f " (uparrow (inf (f .: F)))) by PRE_TOPC:19;
uparrow (inf (f .: F)) is closed by Th4;
then f " (uparrow (inf (f .: F))) is closed by A1, PRE_TOPC:def_6;
then Cl F c= f " (uparrow (inf (f .: F))) by A15, PRE_TOPC:22;
then f . (inf F) in uparrow (inf (f .: F)) by A6, FUNCT_2:38;
then f . (inf F) >= inf (f .: F) by WAYBEL_0:18;
hence inf (f .: F) = f . (inf F) by A13, ORDERS_2:2; ::_thesis: verum
end;
theorem :: WAYBEL19:12
for S, T being complete lower TopLattice
for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
proof
let S, T be complete lower TopLattice; ::_thesis: for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
let f be Function of S,T; ::_thesis: ( f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) implies f is infs-preserving )
assume f is continuous ; ::_thesis: ( ex X being finite Subset of S st not f preserves_inf_of X or f is infs-preserving )
then f is filtered-infs-preserving by Th11;
then for F being non empty filtered Subset of S holds f preserves_inf_of F by WAYBEL_0:def_36;
hence ( ex X being finite Subset of S st not f preserves_inf_of X or f is infs-preserving ) by WAYBEL_0:71; ::_thesis: verum
end;
theorem :: WAYBEL19:13
for T being non empty TopSpace-like reflexive transitive lower TopRelStr
for x being Point of T holds Cl {x} = uparrow x
proof
let T be non empty TopSpace-like reflexive transitive lower TopRelStr ; ::_thesis: for x being Point of T holds Cl {x} = uparrow x
let x be Point of T; ::_thesis: Cl {x} = uparrow x
reconsider y = x as Element of T ;
y <= y ;
then x in uparrow x by WAYBEL_0:18;
then {x} c= uparrow x by ZFMISC_1:31;
hence Cl {x} c= uparrow x by Th4, TOPS_1:5; :: according to XBOOLE_0:def_10 ::_thesis: uparrow x c= Cl {x}
Cl {x} is upper by Th6;
then A1: uparrow (Cl {x}) c= Cl {x} by WAYBEL_0:24;
uparrow {x} c= uparrow (Cl {x}) by PRE_TOPC:18, YELLOW_3:7;
hence uparrow x c= Cl {x} by A1, XBOOLE_1:1; ::_thesis: verum
end;
definition
mode TopPoset is TopSpace-like reflexive transitive antisymmetric TopRelStr ;
end;
registration
cluster non empty TopSpace-like reflexive transitive antisymmetric lower -> non empty T_0 for TopRelStr ;
coherence
for b1 being non empty TopPoset st b1 is lower holds
b1 is T_0
proof
let T be non empty TopPoset; ::_thesis: ( T is lower implies T is T_0 )
assume A1: T is lower ; ::_thesis: T is T_0
now__::_thesis:_(_not_T_is_empty_implies_for_x,_y_being_Point_of_T_holds_
(_not_x_<>_y_or_ex_V_being_Subset_of_T_st_
(_V_is_open_&_x_in_V_&_not_y_in_V_)_or_ex_V_being_Subset_of_T_st_
(_V_is_open_&_not_x_in_V_&_y_in_V_)_)_)
assume not T is empty ; ::_thesis: for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( b5 is open & V in b5 & not b4 in b5 ) or ex V being Subset of T st
( b5 is open & not V in b5 & b4 in b5 ) )
let x, y be Point of T; ::_thesis: ( not x <> y or ex V being Subset of T st
( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st
( b3 is open & not V in b3 & b2 in b3 ) )
assume A2: x <> y ; ::_thesis: ( ex V being Subset of T st
( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st
( b3 is open & not V in b3 & b2 in b3 ) )
reconsider a = x, b = y as Element of T ;
set Vy = (uparrow a) ` ;
set Vx = (uparrow b) ` ;
a <= a ;
then A3: not x in (uparrow a) ` by YELLOW_9:1;
b <= b ;
then A4: not y in (uparrow b) ` by YELLOW_9:1;
A5: (uparrow b) ` is open by A1, Th4;
A6: (uparrow a) ` is open by A1, Th4;
percases ( not b <= a or not a <= b ) by A2, YELLOW_0:def_3;
suppose not b <= a ; ::_thesis: ( ex V being Subset of T st
( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st
( b3 is open & not V in b3 & b2 in b3 ) )
then a in (uparrow b) ` by YELLOW_9:1;
hence ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex V being Subset of T st
( V is open & not x in V & y in V ) ) by A5, A4; ::_thesis: verum
end;
suppose not a <= b ; ::_thesis: ( ex V being Subset of T st
( b3 is open & V in b3 & not b2 in b3 ) or ex V being Subset of T st
( b3 is open & not V in b3 & b2 in b3 ) )
then b in (uparrow a) ` by YELLOW_9:1;
hence ( ex V being Subset of T st
( V is open & x in V & not y in V ) or ex V being Subset of T st
( V is open & not x in V & y in V ) ) by A6, A3; ::_thesis: verum
end;
end;
end;
hence T is T_0 by TSP_1:def_3; ::_thesis: verum
end;
end;
registration
let R be non empty lower-bounded RelStr ;
cluster -> lower-bounded for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is lower-bounded
proof
let T be TopAugmentation of R; ::_thesis: T is lower-bounded
RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
hence T is lower-bounded by YELLOW_0:13; ::_thesis: verum
end;
end;
theorem Th14: :: WAYBEL19:14
for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]
proof
let S, T be non empty RelStr ; ::_thesis: for s being Element of S
for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]
let s be Element of S; ::_thesis: for t being Element of T holds (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]
let t be Element of T; ::_thesis: (uparrow [s,t]) ` = [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):]
thus (uparrow [s,t]) ` = [: the carrier of S, the carrier of T:] \ (uparrow [s,t]) by YELLOW_3:def_2
.= [: the carrier of S, the carrier of T:] \ [:(uparrow s),(uparrow t):] by YELLOW10:40
.= [:((uparrow s) `), the carrier of T:] \/ [: the carrier of S,((uparrow t) `):] by ZFMISC_1:103 ; ::_thesis: verum
end;
theorem Th15: :: WAYBEL19:15
for S, T being non empty lower-bounded Poset
for S9 being correct lower TopAugmentation of S
for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]
proof
let S, T be non empty lower-bounded Poset; ::_thesis: for S9 being correct lower TopAugmentation of S
for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]
set ST = the correct lower TopAugmentation of [:S,T:];
reconsider BX = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of [:S,T:] : verum } as prebasis of the correct lower TopAugmentation of [:S,T:] by Def1;
let S9 be correct lower TopAugmentation of S; ::_thesis: for T9 being correct lower TopAugmentation of T holds omega [:S,T:] = the topology of [:S9,T9:]
reconsider BS = { ((uparrow x) `) where x is Element of S9 : verum } as prebasis of S9 by Def1;
let T9 be correct lower TopAugmentation of T; ::_thesis: omega [:S,T:] = the topology of [:S9,T9:]
set SxT = [:S9,T9:];
set B2 = { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } ;
A1: RelStr(# the carrier of T9, the InternalRel of T9 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
reconsider BT = { ((uparrow x) `) where x is Element of T9 : verum } as prebasis of T9 by Def1;
A2: RelStr(# the carrier of S9, the InternalRel of S9 #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
then A3: the carrier of [:S9,T9:] = [: the carrier of S, the carrier of T:] by A1, BORSUK_1:def_2;
A4: RelStr(# the carrier of the correct lower TopAugmentation of [:S,T:], the InternalRel of the correct lower TopAugmentation of [:S,T:] #) = [:S,T:] by YELLOW_9:def_4;
then A5: the carrier of the correct lower TopAugmentation of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
A6: BX c= the topology of [:S9,T9:]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in BX or z in the topology of [:S9,T9:] )
A7: [#] T9 is open ;
assume z in BX ; ::_thesis: z in the topology of [:S9,T9:]
then consider x being Element of the correct lower TopAugmentation of [:S,T:] such that
A8: z = (uparrow x) ` ;
consider s, t being set such that
A9: s in the carrier of S and
A10: t in the carrier of T and
A11: x = [s,t] by A5, ZFMISC_1:def_2;
reconsider t = t as Element of T by A10;
reconsider s = s as Element of S by A9;
uparrow x = uparrow [s,t] by A4, A11, WAYBEL_0:13;
then A12: z = [:((uparrow s) `),([#] T):] \/ [:([#] S),((uparrow t) `):] by A4, A8, Th14;
reconsider s9 = s as Element of S9 by A2;
reconsider t9 = t as Element of T9 by A1;
(uparrow t9) ` in BT ;
then A13: (uparrow t9) ` is open by TOPS_2:def_1;
reconsider A1 = [:((uparrow s) `),([#] T):], A2 = [:([#] S),((uparrow t) `):] as Subset of [:S9,T9:] by A3, YELLOW_3:def_2;
A14: [#] S9 is open ;
(uparrow s9) ` in BS ;
then A15: (uparrow s9) ` is open by TOPS_2:def_1;
uparrow t = uparrow t9 by A1, WAYBEL_0:13;
then A16: A2 is open by A13, A14, A2, A1, BORSUK_1:6;
uparrow s = uparrow s9 by A2, WAYBEL_0:13;
then A1 is open by A15, A7, A2, A1, BORSUK_1:6;
then A1 \/ A2 is open by A16;
hence z in the topology of [:S9,T9:] by A12, PRE_TOPC:def_2; ::_thesis: verum
end;
set B1 = { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } ;
reconsider BB = { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } \/ { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } as prebasis of [:S9,T9:] by YELLOW_9:41;
A17: UniCl the topology of [:S9,T9:] = the topology of [:S9,T9:] by CANTOR_1:6;
BB c= BX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in BB or z in BX )
assume A18: z in BB ; ::_thesis: z in BX
percases ( z in { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } or z in { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } ) by A18, XBOOLE_0:def_3;
suppose z in { [: the carrier of S9,b:] where b is Subset of T9 : b in BT } ; ::_thesis: z in BX
then consider b being Subset of T9 such that
A19: z = [: the carrier of S9,b:] and
A20: b in BT ;
consider t9 being Element of T9 such that
A21: b = (uparrow t9) ` by A20;
reconsider t = t9 as Element of T by A1;
reconsider x = [(Bottom S),t] as Element of the correct lower TopAugmentation of [:S,T:] by A4;
A22: uparrow x = uparrow [(Bottom S),t] by A4, WAYBEL_0:13;
uparrow (Bottom S) = the carrier of S by WAYBEL14:10;
then A23: (uparrow (Bottom S)) ` = {} by XBOOLE_1:37;
uparrow t = uparrow t9 by A1, WAYBEL_0:13;
then (uparrow [(Bottom S),t]) ` = [:{}, the carrier of T:] \/ [: the carrier of S,b:] by A23, A1, A21, Th14
.= {} \/ [: the carrier of S,b:] by ZFMISC_1:90
.= z by A2, A19 ;
hence z in BX by A4, A22; ::_thesis: verum
end;
suppose z in { [:a, the carrier of T9:] where a is Subset of S9 : a in BS } ; ::_thesis: z in BX
then consider a being Subset of S9 such that
A24: z = [:a, the carrier of T9:] and
A25: a in BS ;
consider s9 being Element of S9 such that
A26: a = (uparrow s9) ` by A25;
reconsider s = s9 as Element of S by A2;
reconsider x = [s,(Bottom T)] as Element of the correct lower TopAugmentation of [:S,T:] by A4;
A27: uparrow x = uparrow [s,(Bottom T)] by A4, WAYBEL_0:13;
uparrow (Bottom T) = the carrier of T by WAYBEL14:10;
then A28: (uparrow (Bottom T)) ` = {} by XBOOLE_1:37;
uparrow s = uparrow s9 by A2, WAYBEL_0:13;
then (uparrow [s,(Bottom T)]) ` = [:a, the carrier of T:] \/ [: the carrier of S,{}:] by A28, A2, A26, Th14
.= [:a, the carrier of T:] \/ {} by ZFMISC_1:90
.= z by A1, A24 ;
hence z in BX by A4, A27; ::_thesis: verum
end;
end;
end;
then FinMeetCl BB c= FinMeetCl BX by A5, A3, CANTOR_1:14;
then A29: UniCl (FinMeetCl BB) c= UniCl (FinMeetCl BX) by A5, A3, CANTOR_1:9;
FinMeetCl BB is Basis of [:S9,T9:] by YELLOW_9:23;
then A30: the topology of [:S9,T9:] = UniCl (FinMeetCl BB) by YELLOW_9:22;
FinMeetCl BX is Basis of the correct lower TopAugmentation of [:S,T:] by YELLOW_9:23;
then A31: the topology of the correct lower TopAugmentation of [:S,T:] = UniCl (FinMeetCl BX) by YELLOW_9:22;
FinMeetCl the topology of [:S9,T9:] = the topology of [:S9,T9:] by CANTOR_1:5;
then FinMeetCl BX c= the topology of [:S9,T9:] by A6, A5, A3, CANTOR_1:14;
then UniCl (FinMeetCl BX) c= the topology of [:S9,T9:] by A5, A3, A17, CANTOR_1:9;
then the topology of the correct lower TopAugmentation of [:S,T:] = the topology of [:S9,T9:] by A31, A30, A29, XBOOLE_0:def_10;
hence omega [:S,T:] = the topology of [:S9,T9:] by Def2; ::_thesis: verum
end;
theorem :: WAYBEL19:16
for S, T being non empty lower-bounded lower TopPoset holds omega [:S,T:] = the topology of [:S,T:]
proof
let S, T be non empty lower-bounded lower TopPoset; ::_thesis: omega [:S,T:] = the topology of [:S,T:]
A1: T is TopAugmentation of T by YELLOW_9:44;
S is TopAugmentation of S by YELLOW_9:44;
hence omega [:S,T:] = the topology of [:S,T:] by A1, Th15; ::_thesis: verum
end;
theorem :: WAYBEL19:17
for T, T2 being complete lower TopLattice st T2 is TopAugmentation of [:T,T:] holds
for f being Function of T2,T st f = inf_op T holds
f is continuous
proof
let T, T2 be complete lower TopLattice; ::_thesis: ( T2 is TopAugmentation of [:T,T:] implies for f being Function of T2,T st f = inf_op T holds
f is continuous )
assume A1: RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of [:T,T:], the InternalRel of [:T,T:] #) ; :: according to YELLOW_9:def_4 ::_thesis: for f being Function of T2,T st f = inf_op T holds
f is continuous
let f be Function of T2,T; ::_thesis: ( f = inf_op T implies f is continuous )
assume A2: f = inf_op T ; ::_thesis: f is continuous
f is infs-preserving
proof
let X be Subset of T2; :: according to WAYBEL_0:def_32 ::_thesis: f preserves_inf_of X
reconsider Y = X as Subset of [:T,T:] by A1;
assume A3: ex_inf_of X,T2 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = K76( the carrier of T2, the carrier of T,f,("/\" (X,T2))) )
thus ex_inf_of f .: X,T by YELLOW_0:17; ::_thesis: "/\" ((f .: X),T) = K76( the carrier of T2, the carrier of T,f,("/\" (X,T2)))
A4: inf_op T preserves_inf_of Y by WAYBEL_0:def_32;
ex_inf_of Y,[:T,T:] by A3, A1, YELLOW_0:14;
hence inf (f .: X) = (inf_op T) . (inf Y) by A2, A4, WAYBEL_0:def_30
.= f . (inf X) by A1, A2, A3, YELLOW_0:27 ;
::_thesis: verum
end;
hence f is continuous by Th9; ::_thesis: verum
end;
begin
scheme :: WAYBEL19:sch 1
TopInd{ F1() -> TopLattice, P1[ set ] } :
for A being Subset of F1() st A is open holds
P1[A]
provided
A1: ex K being prebasis of F1() st
for A being Subset of F1() st A in K holds
P1[A] and
A2: for F being Subset-Family of F1() st ( for A being Subset of F1() st A in F holds
P1[A] ) holds
P1[ union F] and
A3: for A1, A2 being Subset of F1() st P1[A1] & P1[A2] holds
P1[A1 /\ A2] and
A4: P1[ [#] F1()]
proof
consider K being prebasis of F1() such that
A5: for A being Subset of F1() st A in K holds
P1[A] by A1;
let A be Subset of F1(); ::_thesis: ( A is open implies P1[A] )
assume A6: A in the topology of F1() ; :: according to PRE_TOPC:def_2 ::_thesis: P1[A]
FinMeetCl K is Basis of F1() by YELLOW_9:23;
then UniCl (FinMeetCl K) = the topology of F1() by YELLOW_9:22;
then consider X being Subset-Family of F1() such that
A7: X c= FinMeetCl K and
A8: A = union X by A6, CANTOR_1:def_1;
reconsider X = X as Subset-Family of F1() ;
now__::_thesis:_for_A_being_Subset_of_F1()_st_A_in_X_holds_
P1[A]
defpred S1[ set ] means for a being Subset-Family of F1() st a = $1 holds
P1[ Intersect a];
let A be Subset of F1(); ::_thesis: ( A in X implies P1[A] )
assume A in X ; ::_thesis: P1[A]
then consider Y being Subset-Family of F1() such that
A9: Y c= K and
A10: Y is finite and
A11: A = Intersect Y by A7, CANTOR_1:def_3;
A12: for x, Z being set st x in Y & Z c= Y & S1[Z] holds
S1[Z \/ {x}]
proof
let x, Z be set ; ::_thesis: ( x in Y & Z c= Y & S1[Z] implies S1[Z \/ {x}] )
assume that
A13: x in Y and
A14: Z c= Y and
A15: S1[Z] ; ::_thesis: S1[Z \/ {x}]
reconsider xx = {x}, Z9 = Z as Subset-Family of F1() by A13, A14, XBOOLE_1:1, ZFMISC_1:31;
reconsider xx = xx, Z9 = Z9 as Subset-Family of F1() ;
reconsider xx = xx, Z9 = Z9 as Subset-Family of F1() ;
reconsider Ax = x, Ay = Intersect Z9 as Subset of F1() by A13;
A16: P1[Ay] by A15;
let a be Subset-Family of F1(); ::_thesis: ( a = Z \/ {x} implies P1[ Intersect a] )
assume A17: a = Z \/ {x} ; ::_thesis: P1[ Intersect a]
Intersect xx = Ax by MSSUBFAM:9;
then A18: Intersect a = Ax /\ Ay by A17, MSSUBFAM:8;
P1[Ax] by A5, A9, A13;
hence P1[ Intersect a] by A18, A3, A16; ::_thesis: verum
end;
A19: S1[ {} ] by A4, SETFAM_1:def_9;
S1[Y] from FINSET_1:sch_2(A10, A19, A12);
hence P1[A] by A11; ::_thesis: verum
end;
hence P1[A] by A2, A8; ::_thesis: verum
end;
theorem :: WAYBEL19:18
for L1, L2 being non empty reflexive antisymmetric up-complete RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & ( for x being Element of L1 holds
( waybelow x is directed & not waybelow x is empty ) ) & L1 is satisfying_axiom_of_approximation holds
L2 is satisfying_axiom_of_approximation
proof
let L1, L2 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & ( for x being Element of L1 holds
( waybelow x is directed & not waybelow x is empty ) ) & L1 is satisfying_axiom_of_approximation implies L2 is satisfying_axiom_of_approximation )
assume that
A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and
A2: for x being Element of L1 holds
( waybelow x is directed & not waybelow x is empty ) and
A3: for x being Element of L1 holds x = sup (waybelow x) ; :: according to WAYBEL_3:def_5 ::_thesis: L2 is satisfying_axiom_of_approximation
let x be Element of L2; :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),L2)
reconsider y = x as Element of L1 by A1;
A4: y = sup (waybelow y) by A3;
( waybelow y is directed & not waybelow y is empty ) by A2;
then A5: ex_sup_of waybelow y,L1 by WAYBEL_0:75;
waybelow y = waybelow x by A1, YELLOW12:13;
hence x = "\/" ((waybelow x),L2) by A4, A5, A1, YELLOW_0:26; ::_thesis: verum
end;
registration
let T be non empty continuous Poset;
cluster -> continuous for TopAugmentation of T;
coherence
for b1 being TopAugmentation of T holds b1 is continuous
proof
let S be TopAugmentation of T; ::_thesis: S is continuous
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
hence S is continuous by YELLOW12:15; ::_thesis: verum
end;
end;
theorem Th19: :: WAYBEL19:19
for T, S being TopSpace
for R being Refinement of T,S
for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds
W is open
proof
let T, S be TopSpace; ::_thesis: for R being Refinement of T,S
for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds
W is open
let R be Refinement of T,S; ::_thesis: for W being Subset of R st ( W in the topology of T or W in the topology of S ) holds
W is open
let W be Subset of R; ::_thesis: ( ( W in the topology of T or W in the topology of S ) implies W is open )
the topology of T \/ the topology of S is prebasis of R by YELLOW_9:def_6;
then A1: the topology of T \/ the topology of S c= the topology of R by TOPS_2:64;
assume ( W in the topology of T or W in the topology of S ) ; ::_thesis: W is open
then W in the topology of T \/ the topology of S by XBOOLE_0:def_3;
hence W in the topology of R by A1; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
theorem Th20: :: WAYBEL19:20
for T, S being TopSpace
for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is open holds
W is open
proof
let T, S be TopSpace; ::_thesis: for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is open holds
W is open
let R be Refinement of T,S; ::_thesis: for V being Subset of T
for W being Subset of R st W = V & V is open holds
W is open
let V be Subset of T; ::_thesis: for W being Subset of R st W = V & V is open holds
W is open
let W be Subset of R; ::_thesis: ( W = V & V is open implies W is open )
assume A1: W = V ; ::_thesis: ( not V is open or W is open )
assume V in the topology of T ; :: according to PRE_TOPC:def_2 ::_thesis: W is open
hence W is open by A1, Th19; ::_thesis: verum
end;
theorem Th21: :: WAYBEL19:21
for T, S being TopSpace st the carrier of T = the carrier of S holds
for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is closed holds
W is closed
proof
let T, S be TopSpace; ::_thesis: ( the carrier of T = the carrier of S implies for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is closed holds
W is closed )
assume A1: the carrier of T = the carrier of S ; ::_thesis: for R being Refinement of T,S
for V being Subset of T
for W being Subset of R st W = V & V is closed holds
W is closed
let R be Refinement of T,S; ::_thesis: for V being Subset of T
for W being Subset of R st W = V & V is closed holds
W is closed
let V be Subset of T; ::_thesis: for W being Subset of R st W = V & V is closed holds
W is closed
let W be Subset of R; ::_thesis: ( W = V & V is closed implies W is closed )
assume A2: W = V ; ::_thesis: ( not V is closed or W is closed )
assume V is closed ; ::_thesis: W is closed
then A3: V ` is open ;
the carrier of R = the carrier of T \/ the carrier of S by YELLOW_9:def_6
.= the carrier of T by A1 ;
then W ` in the topology of T by A3, A2, PRE_TOPC:def_2;
then W ` is open by Th19;
hence W is closed by TOPS_1:3; ::_thesis: verum
end;
theorem Th22: :: WAYBEL19:22
for T being non empty TopSpace
for K, O being set st K c= O & O c= the topology of T holds
( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )
proof
let T be non empty TopSpace; ::_thesis: for K, O being set st K c= O & O c= the topology of T holds
( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )
let K, O be set ; ::_thesis: ( K c= O & O c= the topology of T implies ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) ) )
assume that
A1: K c= O and
A2: O c= the topology of T ; ::_thesis: ( ( K is Basis of T implies O is Basis of T ) & ( K is prebasis of T implies O is prebasis of T ) )
K c= the topology of T by A1, A2, XBOOLE_1:1;
then reconsider K9 = K, O9 = O as Subset-Family of T by A2, XBOOLE_1:1;
reconsider K9 = K9, O9 = O9 as Subset-Family of T ;
reconsider K9 = K9, O9 = O9 as Subset-Family of T ;
A3: UniCl K9 c= UniCl O9 by A1, CANTOR_1:9;
A4: UniCl the topology of T = the topology of T by CANTOR_1:6;
then A5: UniCl O9 c= the topology of T by A2, CANTOR_1:9;
hereby ::_thesis: ( K is prebasis of T implies O is prebasis of T )
assume K is Basis of T ; ::_thesis: O is Basis of T
then UniCl K9 = the topology of T by YELLOW_9:22;
then UniCl O9 = the topology of T by A5, A3, XBOOLE_0:def_10;
hence O is Basis of T by YELLOW_9:22; ::_thesis: verum
end;
FinMeetCl the topology of T = the topology of T by CANTOR_1:5;
then FinMeetCl O9 c= the topology of T by A2, CANTOR_1:14;
then A6: UniCl (FinMeetCl O9) c= the topology of T by A4, CANTOR_1:9;
assume K is prebasis of T ; ::_thesis: O is prebasis of T
then FinMeetCl K9 is Basis of T by YELLOW_9:23;
then A7: UniCl (FinMeetCl K9) = the topology of T by YELLOW_9:22;
FinMeetCl K9 c= FinMeetCl O9 by A1, CANTOR_1:14;
then UniCl (FinMeetCl K9) c= UniCl (FinMeetCl O9) by CANTOR_1:9;
then UniCl (FinMeetCl O9) = the topology of T by A7, A6, XBOOLE_0:def_10;
then FinMeetCl O9 is Basis of T by YELLOW_9:22;
hence O is prebasis of T by YELLOW_9:23; ::_thesis: verum
end;
theorem Th23: :: WAYBEL19:23
for T1, T2 being non empty TopSpace st the carrier of T1 = the carrier of T2 holds
for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T
proof
let T1, T2 be non empty TopSpace; ::_thesis: ( the carrier of T1 = the carrier of T2 implies for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T )
assume A1: the carrier of T1 = the carrier of T2 ; ::_thesis: for T being Refinement of T1,T2
for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T
let T be Refinement of T1,T2; ::_thesis: for B1 being prebasis of T1
for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T
let B1 be prebasis of T1; ::_thesis: for B2 being prebasis of T2 holds B1 \/ B2 is prebasis of T
let B2 be prebasis of T2; ::_thesis: B1 \/ B2 is prebasis of T
the carrier of T = the carrier of T1 \/ the carrier of T2 by YELLOW_9:def_6
.= the carrier of T1 by A1 ;
then { the carrier of T1, the carrier of T2} = { the carrier of T} by A1, ENUMSET1:29;
then reconsider K = (B1 \/ B2) \/ { the carrier of T} as prebasis of T by YELLOW_9:58;
B1 \/ B2 c= K by XBOOLE_1:7;
then reconsider K9 = B1 \/ B2 as Subset-Family of T by XBOOLE_1:1;
K c= FinMeetCl K9
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in K or a in FinMeetCl K9 )
assume a in K ; ::_thesis: a in FinMeetCl K9
then ( ( a in K9 & K9 c= FinMeetCl K9 ) or ( a in { the carrier of T} & the carrier of T in FinMeetCl K9 ) ) by CANTOR_1:4, CANTOR_1:8, XBOOLE_0:def_3;
hence a in FinMeetCl K9 by TARSKI:def_1; ::_thesis: verum
end;
then FinMeetCl K c= FinMeetCl (FinMeetCl K9) by CANTOR_1:14;
then A2: FinMeetCl K c= FinMeetCl K9 by CANTOR_1:11;
FinMeetCl K9 c= FinMeetCl K by CANTOR_1:14, XBOOLE_1:7;
then FinMeetCl K9 = FinMeetCl K by A2, XBOOLE_0:def_10;
then FinMeetCl K9 is Basis of T by YELLOW_9:23;
hence B1 \/ B2 is prebasis of T by YELLOW_9:23; ::_thesis: verum
end;
theorem :: WAYBEL19:24
for T1, S1, T2, S2 being non empty TopSpace
for R1 being Refinement of T1,S1
for R2 being Refinement of T2,S2
for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
proof
let T1, S1, T2, S2 be non empty TopSpace; ::_thesis: for R1 being Refinement of T1,S1
for R2 being Refinement of T2,S2
for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let R1 be Refinement of T1,S1; ::_thesis: for R2 being Refinement of T2,S2
for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let R2 be Refinement of T2,S2; ::_thesis: for f being Function of T1,T2
for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let f be Function of T1,T2; ::_thesis: for g being Function of S1,S2
for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let g be Function of S1,S2; ::_thesis: for h being Function of R1,R2 st h = f & h = g & f is continuous & g is continuous holds
h is continuous
let h be Function of R1,R2; ::_thesis: ( h = f & h = g & f is continuous & g is continuous implies h is continuous )
assume that
A1: h = f and
A2: h = g ; ::_thesis: ( not f is continuous or not g is continuous or h is continuous )
A3: [#] S2 <> {} ;
reconsider K = the topology of T2 \/ the topology of S2 as prebasis of R2 by YELLOW_9:def_6;
A4: [#] T2 <> {} ;
assume A5: f is continuous ; ::_thesis: ( not g is continuous or h is continuous )
assume A6: g is continuous ; ::_thesis: h is continuous
now__::_thesis:_for_A_being_Subset_of_R2_st_A_in_K_holds_
h_"_A_is_open
let A be Subset of R2; ::_thesis: ( A in K implies h " b1 is open )
assume A7: A in K ; ::_thesis: h " b1 is open
percases ( A in the topology of T2 or A in the topology of S2 ) by A7, XBOOLE_0:def_3;
supposeA8: A in the topology of T2 ; ::_thesis: h " b1 is open
then reconsider A1 = A as Subset of T2 ;
A1 is open by A8, PRE_TOPC:def_2;
then f " A1 is open by A4, A5, TOPS_2:43;
hence h " A is open by A1, Th20; ::_thesis: verum
end;
supposeA9: A in the topology of S2 ; ::_thesis: h " b1 is open
then reconsider A1 = A as Subset of S2 ;
A1 is open by A9, PRE_TOPC:def_2;
then A10: g " A1 is open by A3, A6, TOPS_2:43;
R1 is Refinement of S1,T1 by YELLOW_9:55;
hence h " A is open by A10, A2, Th20; ::_thesis: verum
end;
end;
end;
hence h is continuous by YELLOW_9:36; ::_thesis: verum
end;
theorem Th25: :: WAYBEL19:25
for T being non empty TopSpace
for K being prebasis of T
for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
proof
let T be non empty TopSpace; ::_thesis: for K being prebasis of T
for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let K be prebasis of T; ::_thesis: for N being net of T
for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let N be net of T; ::_thesis: for p being Point of T st ( for A being Subset of T st p in A & A in K holds
N is_eventually_in A ) holds
p in Lim N
let x be Point of T; ::_thesis: ( ( for A being Subset of T st x in A & A in K holds
N is_eventually_in A ) implies x in Lim N )
assume A1: for A being Subset of T st x in A & A in K holds
N is_eventually_in A ; ::_thesis: x in Lim N
now__::_thesis:_for_A_being_a_neighborhood_of_x_holds_N_is_eventually_in_A
defpred S1[ set , set ] means for i, j being Element of N st i = $2 & j >= i holds
N . j in $1;
let A be a_neighborhood of x; ::_thesis: N is_eventually_in A
A2: Int A in the topology of T by PRE_TOPC:def_2;
FinMeetCl K is Basis of T by YELLOW_9:23;
then the topology of T = UniCl (FinMeetCl K) by YELLOW_9:22;
then consider Y being Subset-Family of T such that
A3: Y c= FinMeetCl K and
A4: Int A = union Y by A2, CANTOR_1:def_1;
x in Int A by CONNSP_2:def_1;
then consider y being set such that
A5: x in y and
A6: y in Y by A4, TARSKI:def_4;
consider Z being Subset-Family of T such that
A7: Z c= K and
A8: Z is finite and
A9: y = Intersect Z by A3, A6, CANTOR_1:def_3;
A10: for a being set st a in Z holds
ex b being set st
( b in the carrier of N & S1[a,b] )
proof
let a be set ; ::_thesis: ( a in Z implies ex b being set st
( b in the carrier of N & S1[a,b] ) )
assume A11: a in Z ; ::_thesis: ex b being set st
( b in the carrier of N & S1[a,b] )
then reconsider a = a as Subset of T ;
x in a by A5, A9, A11, SETFAM_1:43;
then N is_eventually_in a by A1, A7, A11;
then consider i being Element of N such that
A12: for j being Element of N st j >= i holds
N . j in a by WAYBEL_0:def_11;
take i ; ::_thesis: ( i in the carrier of N & S1[a,i] )
thus ( i in the carrier of N & S1[a,i] ) by A12; ::_thesis: verum
end;
consider f being Function such that
A13: ( dom f = Z & rng f c= the carrier of N ) and
A14: for a being set st a in Z holds
S1[a,f . a] from FUNCT_1:sch_5(A10);
reconsider z = rng f as finite Subset of ([#] N) by A8, A13, FINSET_1:8;
[#] N is directed by WAYBEL_0:def_6;
then consider k being Element of N such that
k in [#] N and
A15: k is_>=_than z by WAYBEL_0:1;
thus N is_eventually_in A ::_thesis: verum
proof
take k ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not k <= b1 or N . b1 in A )
let i be Element of N; ::_thesis: ( not k <= i or N . i in A )
A16: Int A c= A by TOPS_1:16;
assume A17: i >= k ; ::_thesis: N . i in A
now__::_thesis:_for_a_being_set_st_a_in_Z_holds_
N_._i_in_a
let a be set ; ::_thesis: ( a in Z implies N . i in a )
assume A18: a in Z ; ::_thesis: N . i in a
then A19: f . a in z by A13, FUNCT_1:def_3;
then reconsider j = f . a as Element of N ;
j <= k by A15, A19, LATTICE3:def_9;
hence N . i in a by A14, A17, A18, ORDERS_2:3; ::_thesis: verum
end;
then A20: N . i in y by A9, SETFAM_1:43;
y c= union Y by A6, ZFMISC_1:74;
then N . i in Int A by A20, A4;
hence N . i in A by A16; ::_thesis: verum
end;
end;
hence x in Lim N by YELLOW_6:def_15; ::_thesis: verum
end;
theorem Th26: :: WAYBEL19:26
for T being non empty TopSpace
for N being net of T
for S being Subset of T st N is_eventually_in S holds
Lim N c= Cl S
proof
let T be non empty TopSpace; ::_thesis: for N being net of T
for S being Subset of T st N is_eventually_in S holds
Lim N c= Cl S
let N be net of T; ::_thesis: for S being Subset of T st N is_eventually_in S holds
Lim N c= Cl S
let S be Subset of T; ::_thesis: ( N is_eventually_in S implies Lim N c= Cl S )
given i being Element of N such that A1: for j being Element of N st j >= i holds
N . j in S ; :: according to WAYBEL_0:def_11 ::_thesis: Lim N c= Cl S
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim N or x in Cl S )
assume A2: x in Lim N ; ::_thesis: x in Cl S
then reconsider x = x as Element of T ;
now__::_thesis:_for_G_being_a_neighborhood_of_x_holds_G_meets_S
let G be a_neighborhood of x; ::_thesis: G meets S
N is_eventually_in G by A2, YELLOW_6:def_15;
then consider k being Element of N such that
A3: for j being Element of N st j >= k holds
N . j in G by WAYBEL_0:def_11;
[#] N is directed by WAYBEL_0:def_6;
then consider j being Element of N such that
j in [#] N and
A4: j >= i and
A5: j >= k by WAYBEL_0:def_1;
A6: N . j in G by A3, A5;
N . j in S by A1, A4;
hence G meets S by A6, XBOOLE_0:3; ::_thesis: verum
end;
hence x in Cl S by CONNSP_2:27; ::_thesis: verum
end;
theorem Th27: :: WAYBEL19:27
for R being non empty RelStr
for X being non empty Subset of R holds
( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X )
proof
let R be non empty RelStr ; ::_thesis: for X being non empty Subset of R holds
( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X )
let X be non empty Subset of R; ::_thesis: ( the mapping of (X +id) = id X & the mapping of (X opp+id) = id X )
A1: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
the_mapping_of_(X_+id)_._x_=_x
let x be set ; ::_thesis: ( x in X implies the mapping of (X +id) . x = x )
assume x in X ; ::_thesis: the mapping of (X +id) . x = x
then reconsider i = x as Element of (X +id) by YELLOW_9:6;
thus the mapping of (X +id) . x = (X +id) . i
.= x by YELLOW_9:6 ; ::_thesis: verum
end;
the carrier of (X +id) = X by YELLOW_9:6;
then dom the mapping of (X +id) = X by FUNCT_2:def_1;
hence the mapping of (X +id) = id X by A1, FUNCT_1:17; ::_thesis: the mapping of (X opp+id) = id X
A2: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
the_mapping_of_(X_opp+id)_._x_=_x
let x be set ; ::_thesis: ( x in X implies the mapping of (X opp+id) . x = x )
assume x in X ; ::_thesis: the mapping of (X opp+id) . x = x
then reconsider i = x as Element of (X opp+id) by YELLOW_9:7;
thus the mapping of (X opp+id) . x = (X opp+id) . i
.= x by YELLOW_9:7 ; ::_thesis: verum
end;
the carrier of (X opp+id) = X by YELLOW_9:7;
then dom the mapping of (X opp+id) = X by FUNCT_2:def_1;
hence the mapping of (X opp+id) = id X by A2, FUNCT_1:17; ::_thesis: verum
end;
theorem Th28: :: WAYBEL19:28
for R being non empty reflexive antisymmetric RelStr
for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}
proof
let R be non empty reflexive antisymmetric RelStr ; ::_thesis: for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}
let x be Element of R; ::_thesis: (uparrow x) /\ (downarrow x) = {x}
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {x} c= (uparrow x) /\ (downarrow x)
let a be set ; ::_thesis: ( a in (uparrow x) /\ (downarrow x) implies a in {x} )
assume A1: a in (uparrow x) /\ (downarrow x) ; ::_thesis: a in {x}
then reconsider y = a as Element of R ;
y in downarrow x by A1, XBOOLE_0:def_4;
then A2: y <= x by WAYBEL_0:17;
y in uparrow x by A1, XBOOLE_0:def_4;
then x <= y by WAYBEL_0:18;
then x = a by A2, ORDERS_2:2;
hence a in {x} by TARSKI:def_1; ::_thesis: verum
end;
A3: x <= x ;
then A4: x in downarrow x by WAYBEL_0:17;
x in uparrow x by A3, WAYBEL_0:18;
then x in (uparrow x) /\ (downarrow x) by A4, XBOOLE_0:def_4;
hence {x} c= (uparrow x) /\ (downarrow x) by ZFMISC_1:31; ::_thesis: verum
end;
begin
definition
let T be non empty reflexive TopRelStr ;
attrT is Lawson means :Def3: :: WAYBEL19:def 3
(omega T) \/ (sigma T) is prebasis of T;
end;
:: deftheorem Def3 defines Lawson WAYBEL19:def_3_:_
for T being non empty reflexive TopRelStr holds
( T is Lawson iff (omega T) \/ (sigma T) is prebasis of T );
theorem Th29: :: WAYBEL19:29
for R being complete LATTICE
for LL being correct lower TopAugmentation of R
for S being Scott TopAugmentation of R
for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )
proof
let R be complete LATTICE; ::_thesis: for LL being correct lower TopAugmentation of R
for S being Scott TopAugmentation of R
for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )
let LL be correct lower TopAugmentation of R; ::_thesis: for S being Scott TopAugmentation of R
for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )
let S be Scott TopAugmentation of R; ::_thesis: for T being correct TopAugmentation of R holds
( T is Lawson iff T is Refinement of S,LL )
let T be correct TopAugmentation of R; ::_thesis: ( T is Lawson iff T is Refinement of S,LL )
A1: the topology of S = sigma R by YELLOW_9:51;
A2: the carrier of R \/ the carrier of R = the carrier of R ;
A3: the topology of LL = omega R by Def2;
A4: RelStr(# the carrier of LL, the InternalRel of LL #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
A5: ( (omega T) \/ (sigma T) is prebasis of T iff T is Lawson ) by Def3;
A6: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
A7: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then A8: sigma T = sigma R by YELLOW_9:52;
omega T = omega R by A7, Th3;
hence ( T is Lawson iff T is Refinement of S,LL ) by A8, A3, A1, A5, A2, A4, A6, A7, YELLOW_9:def_6; ::_thesis: verum
end;
registration
let R be complete LATTICE;
cluster non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete strict non void Lawson for TopAugmentation of R;
existence
ex b1 being TopAugmentation of R st
( b1 is Lawson & b1 is strict & b1 is correct )
proof
set S = the correct Scott TopAugmentation of R;
set T = the correct lower TopAugmentation of R;
A1: RelStr(# the carrier of the correct Scott TopAugmentation of R, the InternalRel of the correct Scott TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
set RR = the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R;
A2: the carrier of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R = the carrier of the correct Scott TopAugmentation of R \/ the carrier of the correct lower TopAugmentation of R by YELLOW_9:def_6;
A3: RelStr(# the carrier of the correct lower TopAugmentation of R, the InternalRel of the correct lower TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then reconsider O = the topology of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R as Subset-Family of R by A2, A1;
set LL = TopRelStr(# the carrier of R, the InternalRel of R,O #);
RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,O #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,O #) #) = RelStr(# the carrier of R, the InternalRel of R #) ;
then reconsider LL = TopRelStr(# the carrier of R, the InternalRel of R,O #) as TopAugmentation of R by YELLOW_9:def_4;
TopStruct(# the carrier of LL, the topology of LL #) = TopStruct(# the carrier of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R, the topology of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R #) by A3, A1, A2;
then A4: LL is correct by TEX_2:7;
reconsider A = the topology of the correct Scott TopAugmentation of R \/ the topology of the correct lower TopAugmentation of R as prebasis of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by YELLOW_9:def_6;
reconsider A9 = A as Subset-Family of LL by A3, A1, A2;
take LL ; ::_thesis: ( LL is Lawson & LL is strict & LL is correct )
FinMeetCl A is Basis of the Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by YELLOW_9:23;
then UniCl (FinMeetCl A) = O by YELLOW_9:22;
then FinMeetCl A9 is Basis of LL by A3, A1, A2, A4, YELLOW_9:22;
then the topology of the correct Scott TopAugmentation of R \/ the topology of the correct lower TopAugmentation of R is prebasis of LL by A4, YELLOW_9:23;
then LL is Refinement of the correct Scott TopAugmentation of R, the correct lower TopAugmentation of R by A3, A1, A2, A4, YELLOW_9:def_6;
hence ( LL is Lawson & LL is strict & LL is correct ) by Th29; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott non void for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is Scott & b1 is complete & b1 is strict )
proof
set R = the complete LATTICE;
set T = the correct strict Scott TopAugmentation of the complete LATTICE;
take the correct strict Scott TopAugmentation of the complete LATTICE ; ::_thesis: ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict )
thus ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) ; ::_thesis: verum
end;
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() continuous up-complete /\-complete strict non void Lawson for TopRelStr ;
existence
ex b1 being complete strict TopLattice st
( b1 is Lawson & b1 is continuous )
proof
set R = the complete continuous LATTICE;
set T = the correct strict Lawson TopAugmentation of the complete continuous LATTICE;
take the correct strict Lawson TopAugmentation of the complete continuous LATTICE ; ::_thesis: ( the correct strict Lawson TopAugmentation of the complete continuous LATTICE is Lawson & the correct strict Lawson TopAugmentation of the complete continuous LATTICE is continuous )
thus ( the correct strict Lawson TopAugmentation of the complete continuous LATTICE is Lawson & the correct strict Lawson TopAugmentation of the complete continuous LATTICE is continuous ) ; ::_thesis: verum
end;
end;
theorem Th30: :: WAYBEL19:30
for T being complete Lawson TopLattice holds (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T
proof
let T be complete Lawson TopLattice; ::_thesis: (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T
set R = the correct lower TopAugmentation of T;
set S = the Scott TopAugmentation of T;
A1: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
T is TopAugmentation of T by YELLOW_9:44;
then A2: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29;
set K = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } ;
set O = { ((uparrow x) `) where x is Element of T : verum } ;
the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
then sigma T is Basis of the Scott TopAugmentation of T by CANTOR_1:2;
then A3: sigma T is prebasis of the Scott TopAugmentation of T by YELLOW_9:27;
A4: 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;
{ ((uparrow x) `) where x is Element of T : verum } = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } c= { ((uparrow x) `) where x is Element of T : verum }
let a be set ; ::_thesis: ( a in { ((uparrow x) `) where x is Element of T : verum } implies a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum }
then consider x being Element of T such that
A5: a = (uparrow x) ` ;
reconsider y = x as Element of the correct lower TopAugmentation of T by A4;
uparrow x = uparrow y by A4, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } by A4, A5; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } or a in { ((uparrow x) `) where x is Element of T : verum } )
assume a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } ; ::_thesis: a in { ((uparrow x) `) where x is Element of T : verum }
then consider x being Element of the correct lower TopAugmentation of T such that
A6: a = (uparrow x) ` ;
reconsider y = x as Element of T by A4;
uparrow x = uparrow y by A4, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of T : verum } by A4, A6; ::_thesis: verum
end;
then reconsider O = { ((uparrow x) `) where x is Element of T : verum } as prebasis of the correct lower TopAugmentation of T by Def1;
O = O ;
hence (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A3, A2, A1, A4, Th23; ::_thesis: verum
end;
theorem :: WAYBEL19:31
for T being complete Lawson TopLattice holds (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T
proof
let T be complete Lawson TopLattice; ::_thesis: (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T
set R = the correct lower TopAugmentation of T;
reconsider K = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } as prebasis of the correct lower TopAugmentation of T by Def1;
set O = { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } ;
{ (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } or a in bool the carrier of T )
assume a in { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } ; ::_thesis: a in bool the carrier of T
then ex W being Subset of T ex x being Element of T st
( a = W \ (uparrow x) & W in sigma T ) ;
hence a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider O = { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } as Subset-Family of T ;
reconsider O = O as Subset-Family of T ;
set S = the Scott TopAugmentation of T;
A1: 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;
(sigma T) \/ (omega T) is prebasis of T by Def3;
then A2: (sigma T) \/ (omega T) c= the topology of T by TOPS_2:64;
omega T c= (sigma T) \/ (omega T) by XBOOLE_1:7;
then A3: omega T c= the topology of T by A2, XBOOLE_1:1;
sigma T c= (sigma T) \/ (omega T) by XBOOLE_1:7;
then A4: sigma T c= the topology of T by A2, XBOOLE_1:1;
A5: omega T = the topology of the correct lower TopAugmentation of T by Def2;
O c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in O or a in the topology of T )
assume a in O ; ::_thesis: a in the topology of T
then consider W being Subset of T, x being Element of T such that
A6: a = W \ (uparrow x) and
A7: W in sigma T ;
A8: a = W /\ ((uparrow x) `) by A6, SUBSET_1:13;
reconsider y = x as Element of the correct lower TopAugmentation of T by A1;
uparrow x = uparrow y by A1, WAYBEL_0:13;
then A9: (uparrow x) ` in K by A1;
K c= omega T by A5, TOPS_2:64;
then (uparrow x) ` in omega T by A9;
hence a in the topology of T by A4, A3, A7, A8, PRE_TOPC:def_1; ::_thesis: verum
end;
then A10: (sigma T) \/ O c= the topology of T by A4, XBOOLE_1:8;
A11: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A12: sigma T = the topology of the Scott TopAugmentation of T by YELLOW_9:51;
then sigma T is Basis of the Scott TopAugmentation of T by CANTOR_1:2;
then A13: sigma T is prebasis of the Scott TopAugmentation of T by YELLOW_9:27;
A14: the carrier of the Scott TopAugmentation of T in sigma T by A12, PRE_TOPC:def_1;
K c= O
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in K or a in O )
assume a in K ; ::_thesis: a in O
then consider x being Element of the correct lower TopAugmentation of T such that
A15: a = (uparrow x) ` ;
reconsider y = x as Element of T by A1;
a = ([#] T) \ (uparrow y) by A1, A15, WAYBEL_0:13;
hence a in O by A11, A14; ::_thesis: verum
end;
then A16: (sigma T) \/ K c= (sigma T) \/ O by XBOOLE_1:9;
T is TopAugmentation of T by YELLOW_9:44;
then T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29;
hence (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T by A13, A1, A11, Th23, A16, A10, Th22; ::_thesis: verum
end;
theorem :: WAYBEL19:32
for T being complete Lawson TopLattice holds { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T
proof
let T be complete Lawson TopLattice; ::_thesis: { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T
set R = the correct lower TopAugmentation of T;
reconsider B2 = { ((uparrow F) `) where F is Subset of the correct lower TopAugmentation of T : F is finite } as Basis of the correct lower TopAugmentation of T by Th7;
set Z = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ;
set S = the Scott TopAugmentation of T;
A1: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
then reconsider B1 = sigma T as Basis of the Scott TopAugmentation of T by CANTOR_1:2;
A2: 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;
B1 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
proof
set F9 = {} the correct lower TopAugmentation of T;
reconsider G = {} the correct lower TopAugmentation of T as Subset of T by A2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B1 or x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
assume A3: x in B1 ; ::_thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
then reconsider x9 = x as Subset of T ;
uparrow G = uparrow ({} the correct lower TopAugmentation of T) ;
then x9 \ (uparrow G) = x9 ;
hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A3; ::_thesis: verum
end;
then A4: B1 \/ { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by XBOOLE_1:12;
A5: INTERSECTION (B1,B2) = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } c= INTERSECTION (B1,B2)
let x be set ; ::_thesis: ( x in INTERSECTION (B1,B2) implies x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
assume x in INTERSECTION (B1,B2) ; ::_thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
then consider y, z being set such that
A6: y in B1 and
A7: z in B2 and
A8: x = y /\ z by SETFAM_1:def_5;
reconsider y = y as Subset of T by A6;
A9: ([#] T) /\ y = y by XBOOLE_1:28;
consider F being Subset of the correct lower TopAugmentation of T such that
A10: z = (uparrow F) ` and
A11: F is finite by A7;
reconsider G = F as Subset of T by A2;
z = (uparrow G) ` by A2, A10, WAYBEL_0:13;
then x = y \ (uparrow G) by A9, A8, XBOOLE_1:49;
hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A6, A11; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } or x in INTERSECTION (B1,B2) )
assume x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ; ::_thesis: x in INTERSECTION (B1,B2)
then consider W, F being Subset of T such that
A12: x = W \ (uparrow F) and
A13: W in sigma T and
A14: F is finite ;
W /\ ([#] T) = W by XBOOLE_1:28;
then A15: x = W /\ (([#] T) \ (uparrow F)) by A12, XBOOLE_1:49;
reconsider G = F as Subset of the correct lower TopAugmentation of T by A2;
A16: (uparrow G) ` in B2 by A14;
(uparrow F) ` = (uparrow G) ` by A2, WAYBEL_0:13;
hence x in INTERSECTION (B1,B2) by A16, A13, A15, SETFAM_1:def_5; ::_thesis: verum
end;
A17: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
B2 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B2 or x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
assume x in B2 ; ::_thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
then consider F being Subset of the correct lower TopAugmentation of T such that
A18: x = (uparrow F) ` and
A19: F is finite ;
A20: the carrier of the Scott TopAugmentation of T in B1 by A1, PRE_TOPC:def_1;
reconsider G = F as Subset of T by A2;
uparrow F = uparrow G by A2, WAYBEL_0:13;
hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A17, A20, A2, A18, A19; ::_thesis: verum
end;
then A21: B2 \/ { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by XBOOLE_1:12;
T is TopAugmentation of T by YELLOW_9:44;
then T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29;
then (B1 \/ B2) \/ (INTERSECTION (B1,B2)) is Basis of T by YELLOW_9:59;
hence { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T by A4, A5, A21, XBOOLE_1:4; ::_thesis: verum
end;
definition
let T be complete LATTICE;
func lambda T -> Subset-Family of T means :Def4: :: WAYBEL19:def 4
for S being correct Lawson TopAugmentation of T holds it = the topology of S;
uniqueness
for b1, b2 being Subset-Family of T st ( for S being correct Lawson TopAugmentation of T holds b1 = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds b2 = the topology of S ) holds
b1 = b2
proof
set S = the correct Lawson TopAugmentation of T;
let L1, L2 be Subset-Family of T; ::_thesis: ( ( for S being correct Lawson TopAugmentation of T holds L1 = the topology of S ) & ( for S being correct Lawson TopAugmentation of T holds L2 = the topology of S ) implies L1 = L2 )
assume for S being correct Lawson TopAugmentation of T holds L1 = the topology of S ; ::_thesis: ( ex S being correct Lawson TopAugmentation of T st not L2 = the topology of S or L1 = L2 )
then L1 = the topology of the correct Lawson TopAugmentation of T ;
hence ( ex S being correct Lawson TopAugmentation of T st not L2 = the topology of S or L1 = L2 ) ; ::_thesis: verum
end;
existence
ex b1 being Subset-Family of T st
for S being correct Lawson TopAugmentation of T holds b1 = the topology of S
proof
set S = the correct Lawson TopAugmentation of T;
A1: RelStr(# the carrier of the correct Lawson TopAugmentation of T, the InternalRel of the correct Lawson TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider t = the topology of the correct Lawson TopAugmentation of T as Subset-Family of T ;
take t ; ::_thesis: for S being correct Lawson TopAugmentation of T holds t = the topology of S
let S9 be correct Lawson TopAugmentation of T; ::_thesis: t = the topology of S9
A2: RelStr(# the carrier of S9, the InternalRel of S9 #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then A3: sigma S9 = sigma the correct Lawson TopAugmentation of T by A1, YELLOW_9:52;
(omega S9) \/ (sigma S9) is prebasis of S9 by Def3;
then A4: FinMeetCl ((omega S9) \/ (sigma S9)) is Basis of S9 by YELLOW_9:23;
A5: omega S9 = omega the correct Lawson TopAugmentation of T by A2, A1, Th3;
(omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T) is prebasis of the correct Lawson TopAugmentation of T by Def3;
then FinMeetCl ((omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T)) is Basis of the correct Lawson TopAugmentation of T by YELLOW_9:23;
hence t = UniCl (FinMeetCl ((omega the correct Lawson TopAugmentation of T) \/ (sigma the correct Lawson TopAugmentation of T))) by YELLOW_9:22
.= the topology of S9 by A1, A2, A5, A3, A4, YELLOW_9:22 ;
::_thesis: verum
end;
end;
:: deftheorem Def4 defines lambda WAYBEL19:def_4_:_
for T being complete LATTICE
for b2 being Subset-Family of T holds
( b2 = lambda T iff for S being correct Lawson TopAugmentation of T holds b2 = the topology of S );
theorem Th33: :: WAYBEL19:33
for R being complete LATTICE holds lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R)))
proof
let R be complete LATTICE; ::_thesis: lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R)))
set S = the correct Lawson TopAugmentation of R;
A1: RelStr(# the carrier of the correct Lawson TopAugmentation of R, the InternalRel of the correct Lawson TopAugmentation of R #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then A2: sigma R = sigma the correct Lawson TopAugmentation of R by YELLOW_9:52;
(omega the correct Lawson TopAugmentation of R) \/ (sigma the correct Lawson TopAugmentation of R) is prebasis of the correct Lawson TopAugmentation of R by Def3;
then FinMeetCl ((omega the correct Lawson TopAugmentation of R) \/ (sigma the correct Lawson TopAugmentation of R)) is Basis of the correct Lawson TopAugmentation of R by YELLOW_9:23;
then A3: the topology of the correct Lawson TopAugmentation of R = UniCl (FinMeetCl ((omega the correct Lawson TopAugmentation of R) \/ (sigma the correct Lawson TopAugmentation of R))) by YELLOW_9:22;
omega R = omega the correct Lawson TopAugmentation of R by A1, Th3;
hence lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) by A3, A1, A2, Def4; ::_thesis: verum
end;
theorem :: WAYBEL19:34
for R being complete LATTICE
for T being correct lower TopAugmentation of R
for S being correct Scott TopAugmentation of R
for M being Refinement of S,T holds lambda R = the topology of M
proof
let R be complete LATTICE; ::_thesis: for T being correct lower TopAugmentation of R
for S being correct Scott TopAugmentation of R
for M being Refinement of S,T holds lambda R = the topology of M
let T be correct lower TopAugmentation of R; ::_thesis: for S being correct Scott TopAugmentation of R
for M being Refinement of S,T holds lambda R = the topology of M
let S be correct Scott TopAugmentation of R; ::_thesis: for M being Refinement of S,T holds lambda R = the topology of M
let M be Refinement of S,T; ::_thesis: lambda R = the topology of M
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
A2: the carrier of R \/ the carrier of R = the carrier of R ;
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then A3: the carrier of M = the carrier of R by A2, A1, YELLOW_9:def_6;
A4: sigma R = the topology of S by YELLOW_9:51;
omega R = the topology of T by Def2;
then (sigma R) \/ (omega R) is prebasis of M by A4, YELLOW_9:def_6;
then A5: FinMeetCl ((sigma R) \/ (omega R)) is Basis of M by A3, YELLOW_9:23;
thus lambda R = UniCl (FinMeetCl ((sigma R) \/ (omega R))) by Th33
.= the topology of M by A3, A5, YELLOW_9:22 ; ::_thesis: verum
end;
Lm2: for T being LATTICE
for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A is property(S) ) holds
union F is property(S)
proof
let T be LATTICE; ::_thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A is property(S) ) holds
union F is property(S)
let F be Subset-Family of T; ::_thesis: ( ( for A being Subset of T st A in F holds
A is property(S) ) implies union F is property(S) )
assume A1: for A being Subset of T st A in F holds
A is property(S) ; ::_thesis: union F is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in union F or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in union F ) ) ) )
assume sup D in union F ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in union F ) ) )
then consider A being set such that
A2: sup D in A and
A3: A in F by TARSKI:def_4;
reconsider A = A as Subset of T by A3;
A is property(S) by A1, A3;
then consider y being Element of T such that
A4: y in D and
A5: for x being Element of T st x in D & x >= y holds
x in A by A2, WAYBEL11:def_3;
take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in union F ) ) )
thus y in D by A4; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in union F )
let x be Element of T; ::_thesis: ( not x in D or not y <= x or x in union F )
assume that
A6: x in D and
A7: x >= y ; ::_thesis: x in union F
x in A by A6, A7, A5;
hence x in union F by A3, TARSKI:def_4; ::_thesis: verum
end;
Lm3: for T being LATTICE
for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)
proof
let T be LATTICE; ::_thesis: for A1, A2 being Subset of T st A1 is property(S) & A2 is property(S) holds
A1 /\ A2 is property(S)
let A1, A2 be Subset of T; ::_thesis: ( A1 is property(S) & A2 is property(S) implies A1 /\ A2 is property(S) )
assume that
A1: for D being non empty directed Subset of T st sup D in A1 holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A1 ) ) and
A2: for D being non empty directed Subset of T st sup D in A2 holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A2 ) ) ; :: according to WAYBEL11:def_3 ::_thesis: A1 /\ A2 is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in A1 /\ A2 or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in A1 /\ A2 ) ) ) )
assume A3: sup D in A1 /\ A2 ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in A1 /\ A2 ) ) )
then sup D in A1 by XBOOLE_0:def_4;
then consider y1 being Element of T such that
A4: y1 in D and
A5: for x being Element of T st x in D & x >= y1 holds
x in A1 by A1;
sup D in A2 by A3, XBOOLE_0:def_4;
then consider y2 being Element of T such that
A6: y2 in D and
A7: for x being Element of T st x in D & x >= y2 holds
x in A2 by A2;
consider y being Element of T such that
A8: y in D and
A9: y1 <= y and
A10: y2 <= y by A4, A6, WAYBEL_0:def_1;
take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in A1 /\ A2 ) ) )
thus y in D by A8; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in A1 /\ A2 )
let x be Element of T; ::_thesis: ( not x in D or not y <= x or x in A1 /\ A2 )
assume that
A11: x in D and
A12: x >= y ; ::_thesis: x in A1 /\ A2
A13: x in A2 by A12, A10, A7, A11, ORDERS_2:3;
x in A1 by A12, A9, A5, A11, ORDERS_2:3;
hence x in A1 /\ A2 by A13, XBOOLE_0:def_4; ::_thesis: verum
end;
Lm4: for T being LATTICE holds [#] T is property(S)
proof
let T be LATTICE; ::_thesis: [#] T is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in [#] T or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in [#] T ) ) ) )
assume sup D in [#] T ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in [#] T ) ) )
set y = the Element of D;
reconsider y = the Element of D as Element of T ;
take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in [#] T ) ) )
thus ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in [#] T ) ) ) ; ::_thesis: verum
end;
theorem Th35: :: WAYBEL19:35
for T being up-complete lower TopLattice
for A being Subset of T st A is open holds
A is property(S)
proof
let T be up-complete lower TopLattice; ::_thesis: for A being Subset of T st A is open holds
A is property(S)
defpred S1[ Subset of T] means $1 is property(S) ;
A1: ex K being prebasis of T st
for A being Subset of T st A in K holds
S1[A]
proof
reconsider K = { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Def1;
take K ; ::_thesis: for A being Subset of T st A in K holds
S1[A]
let A be Subset of T; ::_thesis: ( A in K implies S1[A] )
assume A in K ; ::_thesis: S1[A]
then consider x being Element of T such that
A2: A = (uparrow x) ` ;
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in A or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in A ) ) ) )
assume A3: sup D in A ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in A ) ) )
set y = the Element of D;
reconsider y = the Element of D as Element of T ;
take y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in A ) ) )
thus y in D ; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in A )
let z be Element of T; ::_thesis: ( not z in D or not y <= z or z in A )
assume that
A4: z in D and
z >= y and
A5: not z in A ; ::_thesis: contradiction
A6: z >= x by A5, A2, YELLOW_9:1;
not x <= sup D by A3, A2, YELLOW_9:1;
then A7: not z <= sup D by A6, ORDERS_2:3;
A8: ex_sup_of D,T by WAYBEL_0:75;
A9: ex_sup_of {z},T by YELLOW_0:38;
{z} c= D by A4, ZFMISC_1:31;
then sup {z} <= sup D by A8, A9, YELLOW_0:34;
hence contradiction by A7, YELLOW_0:39; ::_thesis: verum
end;
A10: for A1, A2 being Subset of T st S1[A1] & S1[A2] holds
S1[A1 /\ A2] by Lm3;
A11: S1[ [#] T] by Lm4;
A12: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
S1[A] ) holds
S1[ union F] by Lm2;
thus for A being Subset of T st A is open holds
S1[A] from WAYBEL19:sch_1(A1, A12, A10, A11); ::_thesis: verum
end;
theorem Th36: :: WAYBEL19:36
for T being complete Lawson TopLattice
for A being Subset of T st A is open holds
A is property(S)
proof
let T be complete Lawson TopLattice; ::_thesis: for A being Subset of T st A is open holds
A is property(S)
defpred S1[ Subset of T] means $1 is property(S) ;
set S = the Scott TopAugmentation of T;
set R = the correct lower TopAugmentation of T;
A1: 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;
A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
A3: ex K being prebasis of T st
for A being Subset of T st A in K holds
S1[A]
proof
reconsider K = (sigma T) \/ (omega T) as prebasis of T by Def3;
take K ; ::_thesis: for A being Subset of T st A in K holds
S1[A]
let A be Subset of T; ::_thesis: ( A in K implies S1[A] )
reconsider AS = A as Subset of the Scott TopAugmentation of T by A2;
reconsider AR = A as Subset of the correct lower TopAugmentation of T by A1;
assume A in K ; ::_thesis: S1[A]
then ( ( A in sigma T & sigma T = the topology of the Scott TopAugmentation of T ) or ( A in omega T & omega T = the topology of the correct lower TopAugmentation of T ) ) by Def2, XBOOLE_0:def_3, YELLOW_9:51;
then ( AS is open or AR is open ) by PRE_TOPC:def_2;
then ( AS is property(S) or AR is property(S) ) by Th35, WAYBEL11:15;
hence S1[A] by A2, A1, YELLOW12:19; ::_thesis: verum
end;
A4: S1[ [#] T] ;
A5: for A1, A2 being Subset of T st S1[A1] & S1[A2] holds
S1[A1 /\ A2] by Lm3;
A6: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
S1[A] ) holds
S1[ union F] by Lm2;
thus for A being Subset of T st A is open holds
S1[A] from WAYBEL19:sch_1(A3, A6, A5, A4); ::_thesis: verum
end;
theorem Th37: :: WAYBEL19:37
for S being complete Scott TopLattice
for T being correct Lawson TopAugmentation of S
for A being Subset of S st A is open holds
for C being Subset of T st C = A holds
C is open
proof
let S be complete Scott TopLattice; ::_thesis: for T being correct Lawson TopAugmentation of S
for A being Subset of S st A is open holds
for C being Subset of T st C = A holds
C is open
let T be correct Lawson TopAugmentation of S; ::_thesis: for A being Subset of S st A is open holds
for C being Subset of T st C = A holds
C is open
let A be Subset of S; ::_thesis: ( A is open implies for C being Subset of T st C = A holds
C is open )
assume A1: A in the topology of S ; :: according to PRE_TOPC:def_2 ::_thesis: for C being Subset of T st C = A holds
C is open
let C be Subset of T; ::_thesis: ( C = A implies C is open )
assume A2: C = A ; ::_thesis: C is open
(sigma T) \/ (omega T) is prebasis of T by Def3;
then A3: (sigma T) \/ (omega T) c= the topology of T by TOPS_2:64;
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then S is Scott TopAugmentation of T by YELLOW_9:def_4;
then A in sigma T by A1, YELLOW_9:51;
then C in (sigma T) \/ (omega T) by A2, XBOOLE_0:def_3;
hence C in the topology of T by A3; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
theorem Th38: :: WAYBEL19:38
for T being complete Lawson TopLattice
for x being Element of T holds
( uparrow x is closed & downarrow x is closed & {x} is closed )
proof
let T be complete Lawson TopLattice; ::_thesis: for x being Element of T holds
( uparrow x is closed & downarrow x is closed & {x} is closed )
set S = the Scott TopAugmentation of T;
set R = the correct lower TopAugmentation of T;
let x be Element of T; ::_thesis: ( uparrow x is closed & downarrow x is closed & {x} is closed )
A1: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider y = x as Element of the Scott TopAugmentation of T ;
A2: downarrow y is closed by WAYBEL11:11;
T is TopAugmentation of T by YELLOW_9:44;
then A3: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29;
A4: 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;
then reconsider z = x as Element of the correct lower TopAugmentation of T ;
A5: uparrow z = uparrow x by A4, WAYBEL_0:13;
downarrow y = downarrow x by A1, WAYBEL_0:13;
hence ( uparrow x is closed & downarrow x is closed ) by A2, A5, Th4, A1, A4, A3, Th21; ::_thesis: {x} is closed
then (uparrow x) /\ (downarrow x) is closed ;
hence {x} is closed by Th28; ::_thesis: verum
end;
theorem Th39: :: WAYBEL19:39
for T being complete Lawson TopLattice
for x being Element of T holds
( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )
proof
let T be complete Lawson TopLattice; ::_thesis: for x being Element of T holds
( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )
let x be Element of T; ::_thesis: ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open )
A1: downarrow x is closed by Th38;
A2: {x} is closed by Th38;
uparrow x is closed by Th38;
hence ( (uparrow x) ` is open & (downarrow x) ` is open & {x} ` is open ) by A1, A2; ::_thesis: verum
end;
theorem Th40: :: WAYBEL19:40
for T being complete continuous Lawson TopLattice
for x being Element of T holds
( wayabove x is open & (wayabove x) ` is closed )
proof
let T be complete continuous Lawson TopLattice; ::_thesis: for x being Element of T holds
( wayabove x is open & (wayabove x) ` is closed )
let x be Element of T; ::_thesis: ( wayabove x is open & (wayabove x) ` is closed )
set S = the Scott TopAugmentation of T;
A1: T is TopAugmentation of the Scott TopAugmentation of T by YELLOW_9:45;
A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider v = x as Element of the Scott TopAugmentation of T ;
wayabove v is open by WAYBEL11:36;
hence wayabove x is open by A2, A1, Th37, YELLOW12:13; ::_thesis: (wayabove x) ` is closed
hence (wayabove x) ` is closed ; ::_thesis: verum
end;
theorem :: WAYBEL19:41
for S being complete Scott TopLattice
for T being correct Lawson TopAugmentation of S
for A being upper Subset of T st A is open holds
for C being Subset of S st C = A holds
C is open
proof
let S be complete Scott TopLattice; ::_thesis: for T being correct Lawson TopAugmentation of S
for A being upper Subset of T st A is open holds
for C being Subset of S st C = A holds
C is open
let T be correct Lawson TopAugmentation of S; ::_thesis: for A being upper Subset of T st A is open holds
for C being Subset of S st C = A holds
C is open
let A be upper Subset of T; ::_thesis: ( A is open implies for C being Subset of S st C = A holds
C is open )
assume A1: A is open ; ::_thesis: for C being Subset of S st C = A holds
C is open
let C be Subset of S; ::_thesis: ( C = A implies C is open )
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4;
assume C = A ; ::_thesis: C is open
then ( C is upper & C is property(S) ) by A1, Th36, A2, WAYBEL_0:25, YELLOW12:19;
hence C is open by WAYBEL11:15; ::_thesis: verum
end;
theorem :: WAYBEL19:42
for T being complete Lawson TopLattice
for A being lower Subset of T holds
( A is closed iff A is closed_under_directed_sups )
proof
let T be complete Lawson TopLattice; ::_thesis: for A being lower Subset of T holds
( A is closed iff A is closed_under_directed_sups )
let A be lower Subset of T; ::_thesis: ( A is closed iff A is closed_under_directed_sups )
set S = the Scott TopAugmentation of T;
hereby ::_thesis: ( A is closed_under_directed_sups implies A is closed )
assume A is closed ; ::_thesis: A is directly_closed
then A ` is open ;
then reconsider mA = A ` as property(S) Subset of T by Th36;
mA ` = A ;
hence A is directly_closed ; ::_thesis: verum
end;
assume A is directly_closed ; ::_thesis: A is closed
then reconsider dA = A as lower directly_closed Subset of T ;
A1: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider mA = dA ` as Subset of the Scott TopAugmentation of T ;
( mA is upper & mA is inaccessible ) by A1, WAYBEL_0:25, YELLOW_9:47;
then A2: mA is open by WAYBEL11:def_4;
T is TopAugmentation of the Scott TopAugmentation of T by A1, YELLOW_9:def_4;
then dA ` is open by A2, Th37;
hence A is closed by TOPS_1:3; ::_thesis: verum
end;
theorem :: WAYBEL19:43
for T being complete Lawson TopLattice
for F being non empty filtered Subset of T holds Lim (F opp+id) = {(inf F)}
proof
let T be complete Lawson TopLattice; ::_thesis: for F being non empty filtered Subset of T holds Lim (F opp+id) = {(inf F)}
reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by Th30;
set S = the Scott TopAugmentation of T;
let F be non empty filtered Subset of T; ::_thesis: Lim (F opp+id) = {(inf F)}
set N = F opp+id ;
A1: the carrier of (F opp+id) = F by YELLOW_9:7;
A2: F opp+id is full SubRelStr of T opp by YELLOW_9:7;
thus Lim (F opp+id) c= {(inf F)} :: according to XBOOLE_0:def_10 ::_thesis: {(inf F)} c= Lim (F opp+id)
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Lim (F opp+id) or p in {(inf F)} )
assume A3: p in Lim (F opp+id) ; ::_thesis: p in {(inf F)}
then reconsider p = p as Element of T ;
the mapping of (F opp+id) = id F by Th27;
then rng the mapping of (F opp+id) = F by RELAT_1:45;
then A4: p in Cl F by A3, WAYBEL_9:24;
p is_<=_than F
proof
let u be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not u in F or p <= u )
assume A5: u in F ; ::_thesis: p <= u
A6: F opp+id is_eventually_in downarrow u
proof
reconsider i = u as Element of (F opp+id) by A5, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds
( not i <= b1 or (F opp+id) . b1 in downarrow u )
let j be Element of (F opp+id); ::_thesis: ( not i <= j or (F opp+id) . j in downarrow u )
j in F by A1;
then reconsider z = j as Element of T ;
assume j >= i ; ::_thesis: (F opp+id) . j in downarrow u
then z ~ >= u ~ by A2, YELLOW_0:59;
then z <= u by LATTICE3:9;
then z in downarrow u by WAYBEL_0:17;
hence (F opp+id) . j in downarrow u by YELLOW_9:7; ::_thesis: verum
end;
downarrow u is closed by Th38;
then Cl (downarrow u) = downarrow u by PRE_TOPC:22;
then Lim (F opp+id) c= downarrow u by A6, Th26;
hence p <= u by A3, WAYBEL_0:17; ::_thesis: verum
end;
then A7: p <= inf F by YELLOW_0:33;
inf F is_<=_than F by YELLOW_0:33;
then A8: F c= uparrow (inf F) by YELLOW_2:2;
uparrow (inf F) is closed by Th38;
then Cl (uparrow (inf F)) = uparrow (inf F) by PRE_TOPC:22;
then Cl F c= uparrow (inf F) by A8, PRE_TOPC:19;
then p >= inf F by A4, WAYBEL_0:18;
then p = inf F by A7, ORDERS_2:2;
hence p in {(inf F)} by TARSKI:def_1; ::_thesis: verum
end;
A9: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
A10: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
now__::_thesis:_for_A_being_Subset_of_T_st_inf_F_in_A_&_A_in_K_holds_
F_opp+id_is_eventually_in_A
let A be Subset of T; ::_thesis: ( inf F in A & A in K implies F opp+id is_eventually_in b1 )
assume that
A11: inf F in A and
A12: A in K ; ::_thesis: F opp+id is_eventually_in b1
percases ( A in sigma T or A in { ((uparrow x) `) where x is Element of T : verum } ) by A12, XBOOLE_0:def_3;
supposeA13: A in sigma T ; ::_thesis: F opp+id is_eventually_in b1
then reconsider a = A as Subset of the Scott TopAugmentation of T by A9;
set i = the Element of (F opp+id);
a is open by A9, A13, PRE_TOPC:def_2;
then a is upper by WAYBEL11:def_4;
then A14: A is upper by A10, WAYBEL_0:25;
thus F opp+id is_eventually_in A ::_thesis: verum
proof
take the Element of (F opp+id) ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds
( not the Element of (F opp+id) <= b1 or (F opp+id) . b1 in A )
let j be Element of (F opp+id); ::_thesis: ( not the Element of (F opp+id) <= j or (F opp+id) . j in A )
j in F by A1;
then reconsider z = j as Element of T ;
z >= inf F by A1, YELLOW_2:22;
then z in A by A11, A14, WAYBEL_0:def_20;
hence ( not the Element of (F opp+id) <= j or (F opp+id) . j in A ) by YELLOW_9:7; ::_thesis: verum
end;
end;
suppose A in { ((uparrow x) `) where x is Element of T : verum } ; ::_thesis: F opp+id is_eventually_in b1
then consider x being Element of T such that
A15: A = (uparrow x) ` ;
not inf F >= x by A11, A15, YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A16: y in F and
A17: not y >= x by LATTICE3:def_8;
thus F opp+id is_eventually_in A ::_thesis: verum
proof
reconsider i = y as Element of (F opp+id) by A16, YELLOW_9:7;
take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (F opp+id) holds
( not i <= b1 or (F opp+id) . b1 in A )
let j be Element of (F opp+id); ::_thesis: ( not i <= j or (F opp+id) . j in A )
j in F by A1;
then reconsider z = j as Element of T ;
assume j >= i ; ::_thesis: (F opp+id) . j in A
then z ~ >= y ~ by A2, YELLOW_0:59;
then z <= y by LATTICE3:9;
then not z >= x by A17, ORDERS_2:3;
then z in A by A15, YELLOW_9:1;
hence (F opp+id) . j in A by YELLOW_9:7; ::_thesis: verum
end;
end;
end;
end;
then inf F in Lim (F opp+id) by Th25;
hence {(inf F)} c= Lim (F opp+id) by ZFMISC_1:31; ::_thesis: verum
end;
registration
cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Lawson -> T_1 complete compact for TopRelStr ;
coherence
for b1 being complete TopLattice st b1 is Lawson holds
( b1 is T_1 & b1 is compact )
proof
let T be complete TopLattice; ::_thesis: ( T is Lawson implies ( T is T_1 & T is compact ) )
assume A1: T is Lawson ; ::_thesis: ( T is T_1 & T is compact )
for x being Point of T holds {x} is closed by A1, Th38;
hence T is T_1 by URYSOHN1:19; ::_thesis: T is compact
set O1 = sigma T;
set O2 = { ((uparrow x) `) where x is Element of T : verum } ;
reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by A1, Th30;
set S = the Scott TopAugmentation of T;
the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then reconsider X = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:def_1;
A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
for F being Subset of K st X c= union F holds
ex G being finite Subset of F st X c= union G
proof
deffunc H1( Element of T) -> Element of bool the carrier of T = (uparrow c1) ` ;
let F be Subset of K; ::_thesis: ( X c= union F implies ex G being finite Subset of F st X c= union G )
set I2 = { x where x is Element of T : (uparrow x) ` in F } ;
set x = "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T);
A3: { x where x is Element of T : (uparrow x) ` in F } c= the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { x where x is Element of T : (uparrow x) ` in F } or a in the carrier of T )
assume a in { x where x is Element of T : (uparrow x) ` in F } ; ::_thesis: a in the carrier of T
then ex x being Element of T st
( a = x & (uparrow x) ` in F ) ;
hence a in the carrier of T ; ::_thesis: verum
end;
reconsider z = "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) as Element of the Scott TopAugmentation of T by A2;
assume A4: X c= union F ; ::_thesis: ex G being finite Subset of F st X c= union G
"\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) in X ;
then consider Y being set such that
A5: "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) in Y and
A6: Y in F by A4, TARSKI:def_4;
Y in K by A6;
then reconsider I2 = { x where x is Element of T : (uparrow x) ` in F } , Y = Y as Subset of T by A3;
reconsider Z = Y, J2 = I2 as Subset of the Scott TopAugmentation of T by A2;
now__::_thesis:_Y_in_sigma_T
assume not Y in sigma T ; ::_thesis: contradiction
then Y in { ((uparrow x) `) where x is Element of T : verum } by A6, XBOOLE_0:def_3;
then consider y being Element of T such that
A7: Y = (uparrow y) ` ;
y in I2 by A6, A7;
then y <= "\/" ( { x where x is Element of T : (uparrow x) ` in F } ,T) by YELLOW_2:22;
hence contradiction by A5, A7, YELLOW_9:1; ::_thesis: verum
end;
then Z in the topology of the Scott TopAugmentation of T by YELLOW_9:51;
then A8: Z is open by PRE_TOPC:def_2;
then A9: Z is upper by WAYBEL11:15;
A10: z = sup J2 by A2, YELLOW_0:17, YELLOW_0:26
.= sup (finsups J2) by WAYBEL_0:55 ;
Z is property(S) by A8, WAYBEL11:15;
then consider y being Element of the Scott TopAugmentation of T such that
A11: y in finsups J2 and
A12: for x being Element of the Scott TopAugmentation of T st x in finsups J2 & x >= y holds
x in Z by A10, A5, WAYBEL11:def_3;
consider a being finite Subset of J2 such that
A13: y = "\/" (a, the Scott TopAugmentation of T) and
ex_sup_of a, the Scott TopAugmentation of T by A11;
set AA = { ((uparrow c) `) where c is Element of T : c in a } ;
set G = {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } ;
A14: {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } c= F
proof
let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } or i in F )
assume that
A15: i in {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } and
A16: not i in F ; ::_thesis: contradiction
( i in {Y} or i in { ((uparrow c) `) where c is Element of T : c in a } ) by A15, XBOOLE_0:def_3;
then consider c being Element of T such that
A17: i = (uparrow c) ` and
A18: c in a by A6, A16, TARSKI:def_1;
c in J2 by A18;
then ex c9 being Element of T st
( c = c9 & (uparrow c9) ` in F ) ;
hence contradiction by A16, A17; ::_thesis: verum
end;
A19: a is finite ;
{ H1(c) where c is Element of T : c in a } is finite from FRAENKEL:sch_21(A19);
then reconsider G = {Y} \/ { ((uparrow c) `) where c is Element of T : c in a } as finite Subset of F by A14;
take G ; ::_thesis: X c= union G
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in X or u in union G )
assume that
A20: u in X and
A21: not u in union G ; ::_thesis: contradiction
reconsider u = u as Element of the Scott TopAugmentation of T by A20, A2;
A22: union G = (union {Y}) \/ (union { ((uparrow c) `) where c is Element of T : c in a } ) by ZFMISC_1:78
.= Y \/ (union { ((uparrow c) `) where c is Element of T : c in a } ) by ZFMISC_1:25 ;
then A23: not u in Y by A21, XBOOLE_0:def_3;
A24: not u in union { ((uparrow c) `) where c is Element of T : c in a } by A22, A21, XBOOLE_0:def_3;
A25: ( y <= y & u is_>=_than a )
proof
thus y <= y ; ::_thesis: u is_>=_than a
let v be Element of the Scott TopAugmentation of T; :: according to LATTICE3:def_9 ::_thesis: ( not v in a or v <= u )
assume A26: v in a ; ::_thesis: v <= u
then v in J2 ;
then consider c being Element of T such that
A27: v = c and
(uparrow c) ` in F ;
(uparrow c) ` in { ((uparrow c) `) where c is Element of T : c in a } by A26, A27;
then A28: not u in (uparrow c) ` by A24, TARSKI:def_4;
(uparrow c) ` = (uparrow v) ` by A2, A27, WAYBEL_0:13;
hence v <= u by A28, YELLOW_9:1; ::_thesis: verum
end;
then A29: u >= y by A13, YELLOW_0:32;
y in Z by A25, A11, A12;
hence contradiction by A29, A9, A23, WAYBEL_0:def_20; ::_thesis: verum
end;
then X << X by WAYBEL_7:31;
then X is compact by WAYBEL_3:def_2;
hence T is compact by WAYBEL_3:37; ::_thesis: verum
end;
end;
registration
cluster TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete continuous Lawson -> Hausdorff complete continuous for TopRelStr ;
coherence
for b1 being complete continuous TopLattice st b1 is Lawson holds
b1 is Hausdorff
proof
let T be complete continuous TopLattice; ::_thesis: ( T is Lawson implies T is Hausdorff )
assume A1: T is Lawson ; ::_thesis: T is Hausdorff
let x, y be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( x = y or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 ) )
assume A2: x <> y ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 )
reconsider x9 = x, y9 = y as Element of T ;
A3: for x being Element of T holds
( not waybelow x is empty & waybelow x is directed ) ;
percases ( not y9 <= x9 or not x9 <= y9 ) by A2, ORDERS_2:2;
suppose not y9 <= x9 ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 )
then consider u being Element of T such that
A4: u << y9 and
A5: not u <= x9 by A3, WAYBEL_3:24;
take V = (uparrow u) ` ; ::_thesis: ex b1 being Element of bool the carrier of T st
( V is open & b1 is open & x in V & y in b1 & V misses b1 )
take W = wayabove u; ::_thesis: ( V is open & W is open & x in V & y in W & V misses W )
thus ( V is open & W is open ) by A1, Th39, Th40; ::_thesis: ( x in V & y in W & V misses W )
thus x in V by A5, YELLOW_9:1; ::_thesis: ( y in W & V misses W )
thus y in W by A4; ::_thesis: V misses W
A6: V ` = uparrow u ;
W c= uparrow u by WAYBEL_3:11;
hence V misses W by A6, SUBSET_1:23; ::_thesis: verum
end;
suppose not x9 <= y9 ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & x in b1 & y in b2 & b1 misses b2 )
then consider u being Element of T such that
A7: u << x9 and
A8: not u <= y9 by A3, WAYBEL_3:24;
take W = wayabove u; ::_thesis: ex b1 being Element of bool the carrier of T st
( W is open & b1 is open & x in W & y in b1 & W misses b1 )
take V = (uparrow u) ` ; ::_thesis: ( W is open & V is open & x in W & y in V & W misses V )
thus ( W is open & V is open ) by A1, Th39, Th40; ::_thesis: ( x in W & y in V & W misses V )
thus x in W by A7; ::_thesis: ( y in V & W misses V )
thus y in V by A8, YELLOW_9:1; ::_thesis: W misses V
A9: V ` = uparrow u ;
W c= uparrow u by WAYBEL_3:11;
hence W misses V by A9, SUBSET_1:23; ::_thesis: verum
end;
end;
end;
end;