:: WAYBEL33 semantic presentation
begin
definition
let L be non empty Poset;
let X be non empty Subset of L;
let F be Filter of (BoolePoset X);
func lim_inf F -> Element of L equals :: WAYBEL33:def 1
"\/" ( { (inf B) where B is Subset of L : B in F } ,L);
correctness
coherence
"\/" ( { (inf B) where B is Subset of L : B in F } ,L) is Element of L;
;
end;
:: deftheorem defines lim_inf WAYBEL33:def_1_:_
for L being non empty Poset
for X being non empty Subset of L
for F being Filter of (BoolePoset X) holds lim_inf F = "\/" ( { (inf B) where B is Subset of L : B in F } ,L);
theorem :: WAYBEL33:1
for L1, L2 being complete LATTICE st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
proof
let L1, L2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2 )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being non empty Subset of L1
for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let X1 be non empty Subset of L1; ::_thesis: for X2 being non empty Subset of L2
for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let X2 be non empty Subset of L2; ::_thesis: for F1 being Filter of (BoolePoset X1)
for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let F1 be Filter of (BoolePoset X1); ::_thesis: for F2 being Filter of (BoolePoset X2) st F1 = F2 holds
lim_inf F1 = lim_inf F2
let F2 be Filter of (BoolePoset X2); ::_thesis: ( F1 = F2 implies lim_inf F1 = lim_inf F2 )
assume A2: F1 = F2 ; ::_thesis: lim_inf F1 = lim_inf F2
set Y2 = { (inf B2) where B2 is Subset of L2 : B2 in F2 } ;
set Y1 = { (inf B1) where B1 is Subset of L1 : B1 in F1 } ;
A3: { (inf B2) where B2 is Subset of L2 : B2 in F2 } c= { (inf B1) where B1 is Subset of L1 : B1 in F1 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } or x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } )
assume x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } ; ::_thesis: x in { (inf B1) where B1 is Subset of L1 : B1 in F1 }
then consider B2 being Subset of L2 such that
A4: x = inf B2 and
A5: B2 in F2 ;
F1 c= the carrier of (BoolePoset X1) ;
then F1 c= bool X1 by WAYBEL_7:2;
then reconsider B1 = B2 as Subset of L1 by A2, A5, XBOOLE_1:1;
inf B1 = inf B2 by A1, YELLOW_0:17, YELLOW_0:27;
hence x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } by A2, A4, A5; ::_thesis: verum
end;
{ (inf B1) where B1 is Subset of L1 : B1 in F1 } c= { (inf B2) where B2 is Subset of L2 : B2 in F2 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } or x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } )
assume x in { (inf B1) where B1 is Subset of L1 : B1 in F1 } ; ::_thesis: x in { (inf B2) where B2 is Subset of L2 : B2 in F2 }
then consider B1 being Subset of L1 such that
A6: x = inf B1 and
A7: B1 in F1 ;
F2 c= the carrier of (BoolePoset X2) ;
then F2 c= bool X2 by WAYBEL_7:2;
then reconsider B2 = B1 as Subset of L2 by A2, A7, XBOOLE_1:1;
inf B1 = inf B2 by A1, YELLOW_0:17, YELLOW_0:27;
hence x in { (inf B2) where B2 is Subset of L2 : B2 in F2 } by A2, A6, A7; ::_thesis: verum
end;
then { (inf B1) where B1 is Subset of L1 : B1 in F1 } = { (inf B2) where B2 is Subset of L2 : B2 in F2 } by A3, XBOOLE_0:def_10;
hence lim_inf F1 = lim_inf F2 by A1, YELLOW_0:17, YELLOW_0:26; ::_thesis: verum
end;
definition
let L be non empty TopRelStr ;
attrL is lim-inf means :Def2: :: WAYBEL33:def 2
the topology of L = xi L;
end;
:: deftheorem Def2 defines lim-inf WAYBEL33:def_2_:_
for L being non empty TopRelStr holds
( L is lim-inf iff the topology of L = xi L );
registration
cluster non empty lim-inf -> non empty TopSpace-like for TopRelStr ;
coherence
for b1 being non empty TopRelStr st b1 is lim-inf holds
b1 is TopSpace-like
proof
let L be non empty TopRelStr ; ::_thesis: ( L is lim-inf implies L is TopSpace-like )
set T = ConvergenceSpace (lim_inf-Convergence L);
assume L is lim-inf ; ::_thesis: L is TopSpace-like
then A1: the topology of L = xi L by Def2
.= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def_4 ;
A2: for a being Subset-Family of L st a c= the topology of L holds
union a in the topology of L
proof
let a be Subset-Family of L; ::_thesis: ( a c= the topology of L implies union a in the topology of L )
reconsider b = a as Subset-Family of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def_24;
assume a c= the topology of L ; ::_thesis: union a in the topology of L
then union b in the topology of (ConvergenceSpace (lim_inf-Convergence L)) by A1, PRE_TOPC:def_1;
hence union a in the topology of L by A1; ::_thesis: verum
end;
the carrier of L = the carrier of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def_24;
then A3: the carrier of L in the topology of L by A1, PRE_TOPC:def_1;
for a, b being Subset of L st a in the topology of L & b in the topology of L holds
a /\ b in the topology of L by A1, PRE_TOPC:def_1;
hence L is TopSpace-like by A3, A2, PRE_TOPC:def_1; ::_thesis: verum
end;
end;
registration
cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima -> lim-inf for TopRelStr ;
coherence
for b1 being TopLattice st b1 is trivial holds
b1 is lim-inf
proof
let L be TopLattice; ::_thesis: ( L is trivial implies L is lim-inf )
assume L is trivial ; ::_thesis: L is lim-inf
then the carrier of L is 1 -element ;
then reconsider L9 = L as 1 -element TopLattice by STRUCT_0:def_19;
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) = the carrier of L9 by YELLOW_6:def_24;
then reconsider S = ConvergenceSpace (lim_inf-Convergence L) as 1 -element TopSpace by STRUCT_0:def_19;
set x = the Point of L9;
reconsider y = the Point of L9 as Point of S by YELLOW_6:def_24;
thus the topology of L = {{},{y}} by YELLOW_9:9
.= the topology of S by YELLOW_9:9
.= xi L by WAYBEL28:def_4 ; :: according to WAYBEL33:def_2 ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like reflexive transitive antisymmetric continuous with_suprema with_infima complete lim-inf for TopRelStr ;
existence
ex b1 being TopLattice st
( b1 is lim-inf & b1 is continuous & b1 is complete )
proof
take the 1 -element TopLattice ; ::_thesis: ( the 1 -element TopLattice is lim-inf & the 1 -element TopLattice is continuous & the 1 -element TopLattice is complete )
thus ( the 1 -element TopLattice is lim-inf & the 1 -element TopLattice is continuous & the 1 -element TopLattice is complete ) ; ::_thesis: verum
end;
end;
theorem Th2: :: WAYBEL33:2
for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
proof
let L1, L2 be non empty 1-sorted ; ::_thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) )
assume A1: the carrier of L1 = the carrier of L2 ; ::_thesis: for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
let N1 be NetStr over L1; ::_thesis: ex N2 being strict NetStr over L2 st
( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
reconsider f = the mapping of N1 as Function of the carrier of N1, the carrier of L2 by A1;
take NetStr(# the carrier of N1, the InternalRel of N1,f #) ; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N1, the InternalRel of N1,f #), the InternalRel of NetStr(# the carrier of N1, the InternalRel of N1,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N1, the InternalRel of N1,f #) )
thus ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N1, the InternalRel of N1,f #), the InternalRel of NetStr(# the carrier of N1, the InternalRel of N1,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N1, the InternalRel of N1,f #) ) ; ::_thesis: verum
end;
theorem Th3: :: WAYBEL33:3
for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being NetStr over L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
proof
let L1, L2 be non empty 1-sorted ; ::_thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being NetStr over L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) )
assume A1: the carrier of L1 = the carrier of L2 ; ::_thesis: for N1 being NetStr over L1 st N1 in NetUniv L1 holds
ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
let N1 be NetStr over L1; ::_thesis: ( N1 in NetUniv L1 implies ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) )
assume N1 in NetUniv L1 ; ::_thesis: ex N2 being strict net of L2 st
( N2 in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
then consider N being strict net of L1 such that
A2: ( N = N1 & the carrier of N in the_universe_of the carrier of L1 ) by YELLOW_6:def_11;
reconsider f = the mapping of N as Function of the carrier of N, the carrier of L2 by A1;
take NetStr(# the carrier of N, the InternalRel of N,f #) ; ::_thesis: ( NetStr(# the carrier of N, the InternalRel of N,f #) in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N, the InternalRel of N,f #) )
thus ( NetStr(# the carrier of N, the InternalRel of N,f #) in NetUniv L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) & the mapping of N1 = the mapping of NetStr(# the carrier of N, the InternalRel of N,f #) ) by A1, A2, YELLOW_6:def_11; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_L1,_L2_being_non_empty_RelStr_
for_N1_being_net_of_L1
for_N2_being_net_of_L2_st_RelStr(#_the_carrier_of_N1,_the_InternalRel_of_N1_#)_=_RelStr(#_the_carrier_of_N2,_the_InternalRel_of_N2_#)_&_the_mapping_of_N1_=_the_mapping_of_N2_holds_
for_j1_being_Element_of_N1
for_j2_being_Element_of_N2_st_j1_=_j2_holds_
H2(j1)_c=_H1(j2)
let L1, L2 be non empty RelStr ; ::_thesis: for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2) )
assume that
A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A2: the mapping of N1 = the mapping of N2 ; ::_thesis: for j1 being Element of N1
for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
let j1 be Element of N1; ::_thesis: for j2 being Element of N2 st j1 = j2 holds
H2(j1) c= H1(j2)
deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
let j2 be Element of N2; ::_thesis: ( j1 = j2 implies H2(j1) c= H1(j2) )
assume A3: j1 = j2 ; ::_thesis: H2(j1) c= H1(j2)
thus H2(j1) c= H1(j2) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in H2(j1) or y in H1(j2) )
assume y in H2(j1) ; ::_thesis: y in H1(j2)
then consider i1 being Element of N1 such that
A4: y = N1 . i1 and
A5: i1 >= j1 ;
reconsider i1 = i1 as Element of N1 ;
reconsider i2 = i1, j2 = j2 as Element of N2 by A1;
A6: N1 . i1 = N2 . i2 by A2;
i2 >= j2 by A1, A3, A5, YELLOW_0:1;
hence y in H1(j2) by A4, A6; ::_thesis: verum
end;
end;
Lm2: now__::_thesis:_for_L1,_L2_being_/\-complete_Semilattice_st_RelStr(#_the_carrier_of_L1,_the_InternalRel_of_L1_#)_=_RelStr(#_the_carrier_of_L2,_the_InternalRel_of_L2_#)_holds_
for_N1_being_net_of_L1
for_N2_being_net_of_L2_st_RelStr(#_the_carrier_of_N1,_the_InternalRel_of_N1_#)_=_RelStr(#_the_carrier_of_N2,_the_InternalRel_of_N2_#)_&_the_mapping_of_N1_=_the_mapping_of_N2_holds_
{__("/\"_(H2(j),L1))_where_j_is_Element_of_N1_:_verum__}__c=__{__("/\"_(H1(j),L2))_where_j_is_Element_of_N2_:_verum__}_
let L1, L2 be /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
{ ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
{ ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
{ ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } )
assume that
A2: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A3: the mapping of N1 = the mapping of N2 ; ::_thesis: { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
set U1 = { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ;
set U2 = { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ;
thus { ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } or x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum } )
assume x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ; ::_thesis: x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum }
then consider j1 being Element of N1 such that
A4: x = "/\" (H2(j1),L1) ;
reconsider j2 = j1 as Element of N2 by A2;
( H2(j1) c= H1(j2) & H1(j2) c= H2(j1) ) by A2, A3, Lm1;
then A5: H2(j1) = H1(j2) by XBOOLE_0:def_10;
reconsider j1 = j1 as Element of N1 ;
A6: H2(j1) c= the carrier of L1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H2(j1) or x in the carrier of L1 )
assume x in H2(j1) ; ::_thesis: x in the carrier of L1
then ex i being Element of N1 st
( x = N1 . i & i >= j1 ) ;
hence x in the carrier of L1 ; ::_thesis: verum
end;
[#] N1 is directed by WAYBEL_0:def_6;
then consider j0 being Element of N1 such that
j0 in the carrier of N1 and
A7: j1 <= j0 and
j1 <= j0 by WAYBEL_0:def_1;
N1 . j0 in H2(j1) by A7;
then reconsider S = H2(j1) as non empty Subset of L1 by A6;
ex_inf_of S,L1 by WAYBEL_0:76;
then x = "/\" (H1(j2),L2) by A1, A4, A5, YELLOW_0:27;
hence x in { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ; ::_thesis: verum
end;
end;
theorem Th4: :: WAYBEL33:4
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
lim_inf N1 = lim_inf N2
proof
let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
lim_inf N1 = lim_inf N2 )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
lim_inf N1 = lim_inf N2
let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
lim_inf N1 = lim_inf N2
let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies lim_inf N1 = lim_inf N2 )
assume A2: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) ; ::_thesis: lim_inf N1 = lim_inf N2
deffunc H1( Element of N2) -> set = { (N2 . i) where i is Element of N2 : i >= $1 } ;
deffunc H2( Element of N1) -> set = { (N1 . i) where i is Element of N1 : i >= $1 } ;
set U1 = { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ;
set U2 = { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ;
A3: ( lim_inf N1 = "\/" ( { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ,L1) & lim_inf N2 = "\/" ( { ("/\" (H1(j),L2)) where j is Element of N2 : verum } ,L2) ) by WAYBEL11:def_6;
{ ("/\" (H2(j),L1)) where j is Element of N1 : verum } c= the carrier of L1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } or x in the carrier of L1 )
assume x in { ("/\" (H2(j),L1)) where j is Element of N1 : verum } ; ::_thesis: x in the carrier of L1
then ex j being Element of N1 st x = "/\" (H2(j),L1) ;
hence x in the carrier of L1 ; ::_thesis: verum
end;
then reconsider U1 = { ("/\" (H2(j),L1)) where j is Element of N1 : verum } as Subset of L1 ;
( not U1 is empty & U1 is directed ) by WAYBEL32:7;
then A4: ex_sup_of U1,L1 by WAYBEL_0:75;
( U1 c= { ("/\" (H1(j),L2)) where j is Element of N2 : verum } & { ("/\" (H1(j),L2)) where j is Element of N2 : verum } c= U1 ) by A1, A2, Lm2;
then U1 = { ("/\" (H1(j),L2)) where j is Element of N2 : verum } by XBOOLE_0:def_10;
hence lim_inf N1 = lim_inf N2 by A1, A3, A4, YELLOW_0:26; ::_thesis: verum
end;
theorem Th5: :: WAYBEL33:5
for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 holds
for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
proof
let L1, L2 be non empty 1-sorted ; ::_thesis: ( the carrier of L1 = the carrier of L2 implies for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) )
assume A1: the carrier of L1 = the carrier of L2 ; ::_thesis: for N1 being net of L1
for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
let N1 be net of L1; ::_thesis: for N2 being net of L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
let N2 be net of L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) )
assume that
A2: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A3: the mapping of N1 = the mapping of N2 ; ::_thesis: for S1 being subnet of N1 ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
let S1 be subnet of N1; ::_thesis: ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 )
consider S2 being strict NetStr over L2 such that
A4: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) and
A5: the mapping of S1 = the mapping of S2 by A1, Th2;
reconsider S2 = S2 as strict net of L2 by A4;
consider f being Function of S1,N1 such that
A6: the mapping of S1 = the mapping of N1 * f and
A7: for B5 being Element of N1 ex B6 being Element of S1 st
for B7 being Element of S1 st B6 <= B7 holds
B5 <= f . B7 by YELLOW_6:def_9;
reconsider g = f as Function of S2,N2 by A2, A4;
S2 is subnet of N2
proof
take g ; :: according to YELLOW_6:def_9 ::_thesis: ( the mapping of S2 = the mapping of N2 * g & ( for b1 being Element of the carrier of N2 ex b2 being Element of the carrier of S2 st
for b3 being Element of the carrier of S2 holds
( not b2 <= b3 or b1 <= g . b3 ) ) )
thus the mapping of S2 = the mapping of N2 * g by A3, A5, A6; ::_thesis: for b1 being Element of the carrier of N2 ex b2 being Element of the carrier of S2 st
for b3 being Element of the carrier of S2 holds
( not b2 <= b3 or b1 <= g . b3 )
let B2 be Element of N2; ::_thesis: ex b1 being Element of the carrier of S2 st
for b2 being Element of the carrier of S2 holds
( not b1 <= b2 or B2 <= g . b2 )
reconsider b2 = B2 as Element of N1 by A2;
consider b6 being Element of S1 such that
A8: for b7 being Element of S1 st b6 <= b7 holds
b2 <= f . b7 by A7;
reconsider B3 = b6 as Element of S2 by A4;
take B3 ; ::_thesis: for b1 being Element of the carrier of S2 holds
( not B3 <= b1 or B2 <= g . b1 )
let B4 be Element of S2; ::_thesis: ( not B3 <= B4 or B2 <= g . B4 )
reconsider b4 = B4 as Element of S1 by A4;
assume B3 <= B4 ; ::_thesis: B2 <= g . B4
then b6 <= b4 by A4, YELLOW_0:1;
then b2 <= f . b4 by A8;
hence B2 <= g . B4 by A2, YELLOW_0:1; ::_thesis: verum
end;
hence ex S2 being strict subnet of N2 st
( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & the mapping of S1 = the mapping of S2 ) by A4, A5; ::_thesis: verum
end;
theorem Th6: :: WAYBEL33:6
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for N1 being NetStr over L1
for a being set st [N1,a] in lim_inf-Convergence L1 holds
ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
proof
let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for N1 being NetStr over L1
for a being set st [N1,a] in lim_inf-Convergence L1 holds
ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for N1 being NetStr over L1
for a being set st [N1,a] in lim_inf-Convergence L1 holds
ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
let N1 be NetStr over L1; ::_thesis: for a being set st [N1,a] in lim_inf-Convergence L1 holds
ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
let a be set ; ::_thesis: ( [N1,a] in lim_inf-Convergence L1 implies ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) )
assume A2: [N1,a] in lim_inf-Convergence L1 ; ::_thesis: ex N2 being strict net of L2 st
( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
lim_inf-Convergence L1 c= [:(NetUniv L1), the carrier of L1:] by YELLOW_6:def_18;
then consider N, x being set such that
A3: N in NetUniv L1 and
A4: x in the carrier of L1 and
A5: [N1,a] = [N,x] by A2, ZFMISC_1:def_2;
reconsider x = x as Element of L1 by A4;
A6: N = N1 by A5, XTUPLE_0:1;
then consider N2 being strict net of L2 such that
A7: N2 in NetUniv L2 and
A8: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) by A1, A3, Th3;
ex N being strict net of L1 st
( N = N1 & the carrier of N in the_universe_of the carrier of L1 ) by A3, A6, YELLOW_6:def_11;
then reconsider N1 = N1 as strict net of L1 ;
A9: now__::_thesis:_for_M_being_subnet_of_N2_holds_x_=_lim_inf_M
let M be subnet of N2; ::_thesis: x = lim_inf M
consider M1 being strict subnet of N1 such that
A10: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of M1, the InternalRel of M1 #) & the mapping of M = the mapping of M1 ) by A1, A8, Th5;
thus x = lim_inf M1 by A2, A3, A5, A6, WAYBEL28:def_3
.= lim_inf M by A1, A10, Th4 ; ::_thesis: verum
end;
take N2 ; ::_thesis: ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 )
x = a by A5, XTUPLE_0:1;
hence ( [N2,a] in lim_inf-Convergence L2 & RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 ) by A1, A7, A8, A9, WAYBEL28:def_3; ::_thesis: verum
end;
theorem Th7: :: WAYBEL33:7
for L1, L2 being non empty 1-sorted
for N1 being non empty NetStr over L1
for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X
proof
let L1, L2 be non empty 1-sorted ; ::_thesis: for N1 being non empty NetStr over L1
for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X
let N1 be non empty NetStr over L1; ::_thesis: for N2 being non empty NetStr over L2 st RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 holds
for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X
let N2 be non empty NetStr over L2; ::_thesis: ( RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) & the mapping of N1 = the mapping of N2 implies for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X )
assume that
A1: RelStr(# the carrier of N1, the InternalRel of N1 #) = RelStr(# the carrier of N2, the InternalRel of N2 #) and
A2: the mapping of N1 = the mapping of N2 ; ::_thesis: for X being set st N1 is_eventually_in X holds
N2 is_eventually_in X
let X be set ; ::_thesis: ( N1 is_eventually_in X implies N2 is_eventually_in X )
given i1 being Element of N1 such that A3: for j being Element of N1 st i1 <= j holds
N1 . j in X ; :: according to WAYBEL_0:def_11 ::_thesis: N2 is_eventually_in X
reconsider i2 = i1 as Element of N2 by A1;
take i2 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds
( not i2 <= b1 or N2 . b1 in X )
let j2 be Element of N2; ::_thesis: ( not i2 <= j2 or N2 . j2 in X )
reconsider j1 = j2 as Element of N1 by A1;
assume i2 <= j2 ; ::_thesis: N2 . j2 in X
then N1 . j1 in X by A1, A3, YELLOW_0:1;
hence N2 . j2 in X by A2; ::_thesis: verum
end;
Lm3: for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2))
proof
let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence 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 (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of (ConvergenceSpace (lim_inf-Convergence L1)) or x in the topology of (ConvergenceSpace (lim_inf-Convergence L2)) )
A2: the topology of (ConvergenceSpace (lim_inf-Convergence L2)) = { V where V is Subset of L2 : for p being Element of L2 st p in V holds
for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V } by YELLOW_6:def_24;
A3: the topology of (ConvergenceSpace (lim_inf-Convergence L1)) = { V where V is Subset of L1 : for p being Element of L1 st p in V holds
for N being net of L1 st [N,p] in lim_inf-Convergence L1 holds
N is_eventually_in V } by YELLOW_6:def_24;
assume x in the topology of (ConvergenceSpace (lim_inf-Convergence L1)) ; ::_thesis: x in the topology of (ConvergenceSpace (lim_inf-Convergence L2))
then consider V being Subset of L1 such that
A4: x = V and
A5: for p being Element of L1 st p in V holds
for N being net of L1 st [N,p] in lim_inf-Convergence L1 holds
N is_eventually_in V by A3;
reconsider V2 = V as Subset of L2 by A1;
now__::_thesis:_for_p_being_Element_of_L2_st_p_in_V2_holds_
for_N_being_net_of_L2_st_[N,p]_in_lim_inf-Convergence_L2_holds_
N_is_eventually_in_V2
let p be Element of L2; ::_thesis: ( p in V2 implies for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V2 )
assume A6: p in V2 ; ::_thesis: for N being net of L2 st [N,p] in lim_inf-Convergence L2 holds
N is_eventually_in V2
let N be net of L2; ::_thesis: ( [N,p] in lim_inf-Convergence L2 implies N is_eventually_in V2 )
assume [N,p] in lim_inf-Convergence L2 ; ::_thesis: N is_eventually_in V2
then ex N1 being strict net of L1 st
( [N1,p] in lim_inf-Convergence L1 & RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N1, the InternalRel of N1 #) & the mapping of N = the mapping of N1 ) by A1, Th6;
hence N is_eventually_in V2 by A5, A6, Th7; ::_thesis: verum
end;
hence x in the topology of (ConvergenceSpace (lim_inf-Convergence L2)) by A2, A4; ::_thesis: verum
end;
theorem :: WAYBEL33:8
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2)
proof
let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2)
set C2 = lim_inf-Convergence L2;
set C1 = lim_inf-Convergence L1;
set T1 = ConvergenceSpace (lim_inf-Convergence L1);
set T2 = ConvergenceSpace (lim_inf-Convergence L2);
( the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) & the topology of (ConvergenceSpace (lim_inf-Convergence L2)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L1)) ) by A1, Lm3;
then ( the carrier of (ConvergenceSpace (lim_inf-Convergence L2)) = the carrier of L2 & the topology of (ConvergenceSpace (lim_inf-Convergence L1)) = the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) by XBOOLE_0:def_10, YELLOW_6:def_24;
hence ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) by A1, YELLOW_6:def_24; ::_thesis: verum
end;
theorem Th9: :: WAYBEL33:9
for L1, L2 being up-complete /\-complete Semilattice st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
xi L1 = xi L2
proof
let L1, L2 be up-complete /\-complete Semilattice; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies xi L1 = xi L2 )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: xi L1 = xi L2
( xi L1 = the topology of (ConvergenceSpace (lim_inf-Convergence L1)) & xi L2 = the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) by WAYBEL28:def_4;
hence ( xi L1 c= xi L2 & xi L2 c= xi L1 ) by A1, Lm3; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
registration
let R be non empty reflexive /\-complete RelStr ;
cluster -> /\-complete for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is /\-complete
proof
let T be TopAugmentation of R; ::_thesis: T is /\-complete
let X be non empty Subset of T; :: according to WAYBEL_0:def_40 ::_thesis: ex b1 being Element of the carrier of T st
( b1 is_<=_than X & ( for b2 being Element of the carrier of T holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then reconsider Y = X as non empty Subset of R ;
consider x being Element of R such that
A2: x is_<=_than Y and
A3: for y being Element of R st y is_<=_than Y holds
x >= y by WAYBEL_0:def_40;
reconsider y = x as Element of T by A1;
take y ; ::_thesis: ( y is_<=_than X & ( for b1 being Element of the carrier of T holds
( not b1 is_<=_than X or b1 <= y ) ) )
thus y is_<=_than X by A1, A2, YELLOW_0:2; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 is_<=_than X or b1 <= y )
let z be Element of T; ::_thesis: ( not z is_<=_than X or z <= y )
reconsider v = z as Element of R by A1;
assume z is_<=_than X ; ::_thesis: z <= y
then x >= v by A1, A3, YELLOW_0:2;
hence z <= y by A1, YELLOW_0:1; ::_thesis: verum
end;
end;
registration
let R be Semilattice;
cluster -> with_infima for TopAugmentation of R;
coherence
for b1 being TopAugmentation of R holds b1 is with_infima
proof
let T be TopAugmentation of R; ::_thesis: T is with_infima
let x, y be Element of T; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of T st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of T holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then reconsider x9 = x, y9 = y as Element of R ;
consider z9 being Element of R such that
A2: ( z9 <= x9 & z9 <= y9 ) and
A3: for v9 being Element of R st v9 <= x9 & v9 <= y9 holds
v9 <= z9 by LATTICE3:def_11;
reconsider z = z9 as Element of T by A1;
take z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of T holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
thus ( z <= x & z <= y ) by A1, A2, YELLOW_0:1; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 <= x or not b1 <= y or b1 <= z )
let v be Element of T; ::_thesis: ( not v <= x or not v <= y or v <= z )
reconsider v9 = v as Element of R by A1;
assume ( v <= x & v <= y ) ; ::_thesis: v <= z
then ( v9 <= x9 & v9 <= y9 ) by A1, YELLOW_0:1;
then v9 <= z9 by A3;
hence v <= z by A1, YELLOW_0:1; ::_thesis: verum
end;
end;
registration
let L be up-complete /\-complete Semilattice;
cluster non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict lim-inf for TopAugmentation of L;
existence
ex b1 being TopAugmentation of L st
( b1 is strict & b1 is lim-inf )
proof
set T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #);
A1: RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) ;
then reconsider T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) as TopAugmentation of L by YELLOW_9:def_4;
take T ; ::_thesis: ( T is strict & T is lim-inf )
thus T is strict ; ::_thesis: T is lim-inf
thus the topology of T = xi T by A1, Th9; :: according to WAYBEL33:def_2 ::_thesis: verum
end;
end;
theorem Th10: :: WAYBEL33:10
for L being up-complete /\-complete Semilattice
for X being lim-inf TopAugmentation of L holds xi L = the topology of X
proof
let L be up-complete /\-complete Semilattice; ::_thesis: for X being lim-inf TopAugmentation of L holds xi L = the topology of X
let X be lim-inf TopAugmentation of L; ::_thesis: xi L = the topology of X
( the topology of X = xi X & RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of L, the InternalRel of L #) ) by Def2, YELLOW_9:def_4;
hence xi L = the topology of X by Th9; ::_thesis: verum
end;
definition
let L be up-complete /\-complete Semilattice;
func Xi L -> strict TopAugmentation of L means :Def3: :: WAYBEL33:def 3
it is lim-inf ;
uniqueness
for b1, b2 being strict TopAugmentation of L st b1 is lim-inf & b2 is lim-inf holds
b1 = b2
proof
let T1, T2 be strict TopAugmentation of L; ::_thesis: ( T1 is lim-inf & T2 is lim-inf implies T1 = T2 )
assume A1: ( the topology of T1 = xi T1 & the topology of T2 = xi T2 ) ; :: according to WAYBEL33:def_2 ::_thesis: T1 = T2
( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of T2, the InternalRel of T2 #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4;
hence T1 = T2 by A1, Th9; ::_thesis: verum
end;
existence
ex b1 being strict TopAugmentation of L st b1 is lim-inf
proof
set T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #);
A2: RelStr(# the carrier of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #), the InternalRel of TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) #) = RelStr(# the carrier of L, the InternalRel of L #) ;
then reconsider T = TopRelStr(# the carrier of L, the InternalRel of L,(xi L) #) as strict TopAugmentation of L by YELLOW_9:def_4;
take T ; ::_thesis: T is lim-inf
thus the topology of T = xi T by A2, Th9; :: according to WAYBEL33:def_2 ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Xi WAYBEL33:def_3_:_
for L being up-complete /\-complete Semilattice
for b2 being strict TopAugmentation of L holds
( b2 = Xi L iff b2 is lim-inf );
registration
let L be up-complete /\-complete Semilattice;
cluster Xi L -> strict lim-inf ;
coherence
Xi L is lim-inf by Def3;
end;
theorem Th11: :: WAYBEL33:11
for L being complete LATTICE
for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)
proof
let L be complete LATTICE; ::_thesis: for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)
let N be net of L; ::_thesis: lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ;
set Y = { (inf (N | i)) where i is Element of N : verum } ;
for x being set st x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } holds
x in { (inf (N | i)) where i is Element of N : verum }
proof
let x be set ; ::_thesis: ( x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } implies x in { (inf (N | i)) where i is Element of N : verum } )
assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ; ::_thesis: x in { (inf (N | i)) where i is Element of N : verum }
then consider j being Element of N such that
A1: x = "/\" ( { (N . i) where i is Element of N : i >= j } ,L) ;
reconsider x = x as Element of L by A1;
set S = { (N . i) where i is Element of N : i >= j } ;
reconsider i = j as Element of N ;
for b being set st b in rng the mapping of (N | i) holds
b in { (N . i) where i is Element of N : i >= j }
proof
let b be set ; ::_thesis: ( b in rng the mapping of (N | i) implies b in { (N . i) where i is Element of N : i >= j } )
assume b in rng the mapping of (N | i) ; ::_thesis: b in { (N . i) where i is Element of N : i >= j }
then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;
then consider k being Element of (N | i) such that
A2: b = (N | i) . k ;
the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;
then reconsider l = k as Element of N by TARSKI:def_3;
k in the carrier of (N | i) ;
then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;
then A3: ex y being Element of N st
( k = y & i <= y ) ;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
hence b in { (N . i) where i is Element of N : i >= j } by A2, A3; ::_thesis: verum
end;
then A4: rng the mapping of (N | i) c= { (N . i) where i is Element of N : i >= j } by TARSKI:def_3;
A5: ex_inf_of { (N . i) where i is Element of N : i >= j } ,L by YELLOW_0:17;
then A6: { (N . i) where i is Element of N : i >= j } is_>=_than x by A1, YELLOW_0:def_10;
A7: rng the mapping of (N | i) is_>=_than x
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in rng the mapping of (N | i) or x <= b )
thus ( not b in rng the mapping of (N | i) or x <= b ) by A6, A4, LATTICE3:def_8; ::_thesis: verum
end;
for b being set st b in { (N . i) where i is Element of N : i >= j } holds
b in rng the mapping of (N | i)
proof
let b be set ; ::_thesis: ( b in { (N . i) where i is Element of N : i >= j } implies b in rng the mapping of (N | i) )
assume b in { (N . i) where i is Element of N : i >= j } ; ::_thesis: b in rng the mapping of (N | i)
then consider k being Element of N such that
A8: b = N . k and
A9: k >= j ;
reconsider l = k as Element of N ;
l in { y where y is Element of N : i <= y } by A9;
then reconsider k = k as Element of (N | i) by WAYBEL_9:12;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A8;
hence b in rng the mapping of (N | i) by WAYBEL11:19; ::_thesis: verum
end;
then { (N . i) where i is Element of N : i >= j } c= rng the mapping of (N | i) by TARSKI:def_3;
then { (N . i) where i is Element of N : i >= j } = rng the mapping of (N | i) by A4, XBOOLE_0:def_10;
then for a being Element of L st rng the mapping of (N | i) is_>=_than a holds
a <= x by A1, A5, YELLOW_0:def_10;
then consider i being Element of N such that
A10: ( ex_inf_of rng the mapping of (N | i),L & rng the mapping of (N | i) is_>=_than x & ( for a being Element of L st rng the mapping of (N | i) is_>=_than a holds
a <= x ) ) by A7, YELLOW_0:17;
A11: inf (N | i) = Inf by WAYBEL_9:def_2
.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def_6 ;
x = "/\" ((rng the mapping of (N | i)),L) by A10, YELLOW_0:def_10;
hence x in { (inf (N | i)) where i is Element of N : verum } by A11; ::_thesis: verum
end;
then A12: ( lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ,L) & { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } c= { (inf (N | i)) where i is Element of N : verum } ) by TARSKI:def_3, WAYBEL11:def_6;
for x being set st x in { (inf (N | i)) where i is Element of N : verum } holds
x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }
proof
let x be set ; ::_thesis: ( x in { (inf (N | i)) where i is Element of N : verum } implies x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } )
assume x in { (inf (N | i)) where i is Element of N : verum } ; ::_thesis: x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }
then consider i being Element of N such that
A13: x = inf (N | i) ;
set S = { (N . j) where j is Element of N : j >= i } ;
for b being set st b in rng the mapping of (N | i) holds
b in { (N . j) where j is Element of N : j >= i }
proof
let b be set ; ::_thesis: ( b in rng the mapping of (N | i) implies b in { (N . j) where j is Element of N : j >= i } )
assume b in rng the mapping of (N | i) ; ::_thesis: b in { (N . j) where j is Element of N : j >= i }
then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;
then consider k being Element of (N | i) such that
A14: b = (N | i) . k ;
the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;
then reconsider l = k as Element of N by TARSKI:def_3;
k in the carrier of (N | i) ;
then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;
then A15: ex y being Element of N st
( k = y & i <= y ) ;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
hence b in { (N . j) where j is Element of N : j >= i } by A14, A15; ::_thesis: verum
end;
then A16: rng the mapping of (N | i) c= { (N . j) where j is Element of N : j >= i } by TARSKI:def_3;
reconsider x = x as Element of L by A13;
A17: x = Inf by A13, WAYBEL_9:def_2
.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def_6 ;
for b being set st b in { (N . j) where j is Element of N : j >= i } holds
b in rng the mapping of (N | i)
proof
let b be set ; ::_thesis: ( b in { (N . j) where j is Element of N : j >= i } implies b in rng the mapping of (N | i) )
assume b in { (N . j) where j is Element of N : j >= i } ; ::_thesis: b in rng the mapping of (N | i)
then consider k being Element of N such that
A18: b = N . k and
A19: k >= i ;
reconsider l = k as Element of N ;
l in { y where y is Element of N : i <= y } by A19;
then reconsider k = k as Element of (N | i) by WAYBEL_9:12;
reconsider k = k as Element of (N | i) ;
N . l = (N | i) . k by WAYBEL_9:16;
then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A18;
hence b in rng the mapping of (N | i) by WAYBEL11:19; ::_thesis: verum
end;
then { (N . j) where j is Element of N : j >= i } c= rng the mapping of (N | i) by TARSKI:def_3;
then rng the mapping of (N | i) = { (N . j) where j is Element of N : j >= i } by A16, XBOOLE_0:def_10;
hence x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } by A17; ::_thesis: verum
end;
then { (inf (N | i)) where i is Element of N : verum } c= { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } by TARSKI:def_3;
hence lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) by A12, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th12: :: WAYBEL33:12
for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L))
for f being Subset of L st f in F holds
for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
proof
let L be complete LATTICE; ::_thesis: for F being proper Filter of (BoolePoset ([#] L))
for f being Subset of L st f in F holds
for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let F be proper Filter of (BoolePoset ([#] L)); ::_thesis: for f being Subset of L st f in F holds
for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let f be Subset of L; ::_thesis: ( f in F implies for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i) )
assume A1: f in F ; ::_thesis: for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let i be Element of (a_net F); ::_thesis: ( i `2 = f implies inf f = inf ((a_net F) | i) )
assume A2: i `2 = f ; ::_thesis: inf f = inf ((a_net F) | i)
for b being set st b in f holds
b in rng the mapping of ((a_net F) | i)
proof
let b be set ; ::_thesis: ( b in f implies b in rng the mapping of ((a_net F) | i) )
assume A3: b in f ; ::_thesis: b in rng the mapping of ((a_net F) | i)
then reconsider b = b as Element of L ;
reconsider f = f as Element of F by A1;
[b,f] in { [a,g] where a is Element of L, g is Element of F : a in g } by A3;
then reconsider k = [b,f] as Element of (a_net F) by YELLOW19:def_4;
reconsider l = k as Element of (a_net F) ;
[b,f] `1 = b ;
then A4: b = (a_net F) . k by YELLOW19:def_4;
[b,f] `2 = f ;
then k `2 c= i `2 by A2;
then i <= k by YELLOW19:def_4;
then l in { y where y is Element of (a_net F) : i <= y } ;
then reconsider k = k as Element of ((a_net F) | i) by WAYBEL_9:12;
reconsider k = k as Element of ((a_net F) | i) ;
(a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16;
then b in { (((a_net F) | i) . m) where m is Element of ((a_net F) | i) : verum } by A4;
hence b in rng the mapping of ((a_net F) | i) by WAYBEL11:19; ::_thesis: verum
end;
then A5: f c= rng the mapping of ((a_net F) | i) by TARSKI:def_3;
for b being set st b in rng the mapping of ((a_net F) | i) holds
b in f
proof
let b be set ; ::_thesis: ( b in rng the mapping of ((a_net F) | i) implies b in f )
assume b in rng the mapping of ((a_net F) | i) ; ::_thesis: b in f
then b in { (((a_net F) | i) . k) where k is Element of ((a_net F) | i) : verum } by WAYBEL11:19;
then consider k being Element of ((a_net F) | i) such that
A6: b = ((a_net F) | i) . k ;
A7: the carrier of ((a_net F) | i) c= the carrier of (a_net F) by WAYBEL_9:13;
then reconsider l = k as Element of (a_net F) by TARSKI:def_3;
k in the carrier of (a_net F) by A7, TARSKI:def_3;
then A8: k in { [c,g] where c is Element of L, g is Element of F : c in g } by YELLOW19:def_4;
k in the carrier of ((a_net F) | i) ;
then k in { y where y is Element of (a_net F) : i <= y } by WAYBEL_9:12;
then ex y being Element of (a_net F) st
( k = y & i <= y ) ;
then A9: l `2 c= f by A2, YELLOW19:def_4;
consider c being Element of L, g being Element of F such that
A10: k = [c,g] and
A11: c in g by A8;
A12: ( [c,g] `1 = c & [c,g] `2 = g ) ;
reconsider k = k as Element of ((a_net F) | i) ;
(a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16;
then b = l `1 by A6, YELLOW19:def_4;
hence b in f by A11, A12, A9, A10; ::_thesis: verum
end;
then A13: rng the mapping of ((a_net F) | i) c= f by TARSKI:def_3;
inf ((a_net F) | i) = Inf by WAYBEL_9:def_2
.= "/\" ((rng the mapping of ((a_net F) | i)),L) by YELLOW_2:def_6 ;
hence inf f = inf ((a_net F) | i) by A13, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th13: :: WAYBEL33:13
for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf (a_net F)
proof
let L be complete LATTICE; ::_thesis: for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf (a_net F)
let F be proper Filter of (BoolePoset ([#] L)); ::_thesis: lim_inf F = lim_inf (a_net F)
set X = { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ;
set Y = { (inf B) where B is Subset of L : B in F } ;
for x being set st x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } holds
x in { (inf B) where B is Subset of L : B in F }
proof
let x be set ; ::_thesis: ( x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } implies x in { (inf B) where B is Subset of L : B in F } )
assume x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; ::_thesis: x in { (inf B) where B is Subset of L : B in F }
then consider i being Element of (a_net F) such that
A1: x = inf ((a_net F) | i) ;
reconsider i = i as Element of (a_net F) ;
i in the carrier of (a_net F) ;
then i in { [b,g] where b is Element of L, g is Element of F : b in g } by YELLOW19:def_4;
then consider a being Element of L, f being Element of F such that
A2: i = [a,f] and
a in f ;
reconsider i = i as Element of (a_net F) ;
reconsider f = f as Element of (BoolePoset ([#] L)) ;
reconsider f = f as Subset of L by WAYBEL_7:2;
[a,f] `2 = f ;
then inf f = inf ((a_net F) | i) by Th12, A2;
hence x in { (inf B) where B is Subset of L : B in F } by A1; ::_thesis: verum
end;
then A3: { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } c= { (inf B) where B is Subset of L : B in F } by TARSKI:def_3;
for x being set st x in { (inf B) where B is Subset of L : B in F } holds
x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum }
proof
let x be set ; ::_thesis: ( x in { (inf B) where B is Subset of L : B in F } implies x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } )
assume x in { (inf B) where B is Subset of L : B in F } ; ::_thesis: x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum }
then consider B being Subset of L such that
A4: x = inf B and
A5: B in F ;
not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;
then B <> {} by A5, YELLOW_1:18;
then consider a being Element of L such that
A6: a in B by SUBSET_1:4;
reconsider B = B as Element of F by A5;
[a,B] in { [b,f] where b is Element of L, f is Element of F : b in f } by A6;
then reconsider i = [a,B] as Element of (a_net F) by YELLOW19:def_4;
[a,B] `2 = B ;
then x = inf ((a_net F) | i) by A4, Th12;
hence x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; ::_thesis: verum
end;
then A7: { (inf B) where B is Subset of L : B in F } c= { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } by TARSKI:def_3;
lim_inf (a_net F) = "\/" ( { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ,L) by Th11;
hence lim_inf F = lim_inf (a_net F) by A3, A7, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm4: for L being LATTICE
for F being non empty Subset of (BoolePoset ([#] L)) holds { [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):]
proof
let L be LATTICE; ::_thesis: for F being non empty Subset of (BoolePoset ([#] L)) holds { [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):]
let F be non empty Subset of (BoolePoset ([#] L)); ::_thesis: { [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [a,f] where a is Element of L, f is Element of F : a in f } or x in [: the carrier of L,(bool the carrier of L):] )
assume x in { [a,f] where a is Element of L, f is Element of F : a in f } ; ::_thesis: x in [: the carrier of L,(bool the carrier of L):]
then consider a being Element of L, f being Element of F such that
A1: x = [a,f] and
a in f ;
f is Subset of ([#] L) by WAYBEL_7:2;
hence x in [: the carrier of L,(bool the carrier of L):] by A1, ZFMISC_1:def_2; ::_thesis: verum
end;
theorem Th14: :: WAYBEL33:14
for L being complete LATTICE
for F being proper Filter of (BoolePoset ([#] L)) holds a_net F in NetUniv L
proof
let L be complete LATTICE; ::_thesis: for F being proper Filter of (BoolePoset ([#] L)) holds a_net F in NetUniv L
let F be proper Filter of (BoolePoset ([#] L)); ::_thesis: a_net F in NetUniv L
set S = { [a,f] where a is Element of L, f is Element of F : a in f } ;
set UN = the_universe_of the carrier of L;
reconsider UN = the_universe_of the carrier of L as universal set ;
the_transitive-closure_of the carrier of L in UN by CLASSES1:2;
then A1: the carrier of L in UN by CLASSES1:3, CLASSES1:52;
then bool the carrier of L in UN by CLASSES2:59;
then A2: [: the carrier of L,(bool the carrier of L):] in UN by A1, CLASSES2:61;
{ [a,f] where a is Element of L, f is Element of F : a in f } c= [: the carrier of L,(bool the carrier of L):] by Lm4;
then ( { [a,f] where a is Element of L, f is Element of F : a in f } = the carrier of (a_net F) & { [a,f] where a is Element of L, f is Element of F : a in f } in UN ) by A2, CLASSES1:def_1, YELLOW19:def_4;
hence a_net F in NetUniv L by YELLOW_6:def_11; ::_thesis: verum
end;
theorem Th15: :: WAYBEL33:15
for L being complete LATTICE
for F being ultra Filter of (BoolePoset ([#] L))
for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)
proof
let L be complete LATTICE; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L))
for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)
let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)
let p be greater_or_equal_to_id Function of (a_net F),(a_net F); ::_thesis: lim_inf F >= inf ((a_net F) * p)
set M = (a_net F) * p;
set rM = rng the mapping of ((a_net F) * p);
set C = the Element of F;
A1: inf ((a_net F) * p) = Inf by WAYBEL_9:def_2
.= "/\" ((rng the mapping of ((a_net F) * p)),L) by YELLOW_2:def_6 ;
F c= the carrier of (BoolePoset ([#] L)) ;
then F c= bool ([#] L) by WAYBEL_7:2;
then the Element of F in bool ([#] L) by TARSKI:def_3;
then A2: the Element of F \ (rng the mapping of ((a_net F) * p)) c= [#] L by XBOOLE_1:1;
then reconsider D = the Element of F \ (rng the mapping of ((a_net F) * p)), A = the Element of F /\ (rng the mapping of ((a_net F) * p)) as Element of (BoolePoset ([#] L)) by WAYBEL_7:2;
A3: the carrier of ((a_net F) * p) = the carrier of (a_net F) by WAYBEL28:6;
then reconsider g = p as Function of ((a_net F) * p),(a_net F) ;
A4: now__::_thesis:_not_D_in_F
set d = the Element of D;
assume A5: D in F ; ::_thesis: contradiction
not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;
then A6: D <> {} by A5, YELLOW_1:18;
then A7: the Element of D in D ;
reconsider D = D as Element of F by A5;
reconsider d = the Element of D as Element of L by A2, A7;
[d,D] in { [a,f] where a is Element of L, f is Element of F : a in f } by A6;
then reconsider dD = [d,D] as Element of (a_net F) by YELLOW19:def_4;
reconsider dD9 = dD as Element of ((a_net F) * p) by WAYBEL28:6;
A8: dom p = the carrier of (a_net F) by FUNCT_2:52;
ex i being Element of ((a_net F) * p) st
for j being Element of ((a_net F) * p) st j >= i holds
g . j >= dD
proof
consider i being Element of ((a_net F) * p) such that
A9: i = dD9 ;
take i ; ::_thesis: for j being Element of ((a_net F) * p) st j >= i holds
g . j >= dD
for j being Element of ((a_net F) * p) st j >= i holds
g . j >= dD
proof
reconsider i9 = i as Element of (a_net F) by WAYBEL28:6;
let j be Element of ((a_net F) * p); ::_thesis: ( j >= i implies g . j >= dD )
reconsider j9 = j as Element of (a_net F) by WAYBEL28:6;
A10: j9 <= g . j by WAYBEL28:def_1;
reconsider i9 = i9 as Element of (a_net F) ;
reconsider j9 = j9 as Element of (a_net F) ;
A11: RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def_2;
assume j >= i ; ::_thesis: g . j >= dD
then i9 <= j9 by A11, YELLOW_0:1;
hence g . j >= dD by A9, A10, YELLOW_0:def_2; ::_thesis: verum
end;
hence for j being Element of ((a_net F) * p) st j >= i holds
g . j >= dD ; ::_thesis: verum
end;
then consider i being Element of ((a_net F) * p) such that
A12: for j being Element of ((a_net F) * p) st j >= i holds
g . j >= dD ;
RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def_2;
then (a_net F) * p is reflexive by WAYBEL_8:12;
then i >= i by YELLOW_0:def_1;
then A13: g . i >= dD by A12;
[d,D] `2 = D ;
then A14: (p . i) `2 c= D by A13, YELLOW19:def_4;
reconsider G = g . i as Element of (a_net F) ;
g . i in the carrier of (a_net F) ;
then g . i in { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def_4;
then consider a being Element of L, f being Element of F such that
A15: g . i = [a,f] and
A16: a in f ;
( [a,f] `1 = a & [a,f] `2 = f ) ;
then A17: (p . i) `1 in (p . i) `2 by A15, A16;
((a_net F) * p) . i = ( the mapping of (a_net F) * p) . i by WAYBEL28:def_2
.= (a_net F) . G by A3, A8, FUNCT_1:13
.= (p . i) `1 by YELLOW19:def_4 ;
then not ((a_net F) * p) . i in rng the mapping of ((a_net F) * p) by A14, A17, XBOOLE_0:def_5;
hence contradiction by FUNCT_2:4; ::_thesis: verum
end;
set Y = { (inf B) where B is Subset of L : B in F } ;
reconsider A9 = A as Subset of L ;
A18: D "\/" A = D \/ A by YELLOW_1:17
.= the Element of F by XBOOLE_1:51 ;
F is prime by WAYBEL_7:22;
then A in F by A18, A4, WAYBEL_7:def_2;
then inf A9 in { (inf B) where B is Subset of L : B in F } ;
then A19: inf A9 <= lim_inf F by YELLOW_0:17, YELLOW_4:1;
A c= rng the mapping of ((a_net F) * p) by XBOOLE_1:17;
then inf ((a_net F) * p) <= inf A9 by A1, WAYBEL_7:1;
hence lim_inf F >= inf ((a_net F) * p) by A19, YELLOW_0:def_2; ::_thesis: verum
end;
theorem Th16: :: WAYBEL33:16
for L being complete LATTICE
for F being ultra Filter of (BoolePoset ([#] L))
for M being subnet of a_net F holds lim_inf F = lim_inf M
proof
let L be complete LATTICE; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L))
for M being subnet of a_net F holds lim_inf F = lim_inf M
let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: for M being subnet of a_net F holds lim_inf F = lim_inf M
let M be subnet of a_net F; ::_thesis: lim_inf F = lim_inf M
( lim_inf F = lim_inf (a_net F) & ( for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p) ) ) by Th13, Th15;
hence lim_inf F = lim_inf M by WAYBEL28:14; ::_thesis: verum
end;
theorem Th17: :: WAYBEL33:17
for L being non empty 1-sorted
for N being net of L
for A being set st N is_often_in A holds
ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
proof
let L be non empty 1-sorted ; ::_thesis: for N being net of L
for A being set st N is_often_in A holds
ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
let N be net of L; ::_thesis: for A being set st N is_often_in A holds
ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
let A be set ; ::_thesis: ( N is_often_in A implies ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N ) )
assume N is_often_in A ; ::_thesis: ex N9 being strict subnet of N st
( rng the mapping of N9 c= A & N9 is SubNetStr of N )
then reconsider N9 = N " A as strict subnet of N by YELLOW_6:22;
take N9 ; ::_thesis: ( rng the mapping of N9 c= A & N9 is SubNetStr of N )
rng the mapping of N9 c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of N9 or y in A )
assume y in rng the mapping of N9 ; ::_thesis: y in A
then consider x being set such that
A1: x in dom the mapping of N9 and
A2: y = the mapping of N9 . x by FUNCT_1:def_3;
A3: x in dom ( the mapping of N | the carrier of N9) by A1, YELLOW_6:def_6;
then x in (dom the mapping of N) /\ the carrier of N9 by RELAT_1:61;
then x in the carrier of N9 by XBOOLE_0:def_4;
then A4: x in the mapping of N " A by YELLOW_6:def_10;
y = ( the mapping of N | the carrier of N9) . x by A2, YELLOW_6:def_6;
then y = the mapping of N . x by A3, FUNCT_1:47;
hence y in A by A4, FUNCT_1:def_7; ::_thesis: verum
end;
hence ( rng the mapping of N9 c= A & N9 is SubNetStr of N ) ; ::_thesis: verum
end;
theorem Th18: :: WAYBEL33:18
for L being complete lim-inf TopLattice
for A being non empty Subset of L holds
( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A )
proof
let L be complete lim-inf TopLattice; ::_thesis: for A being non empty Subset of L holds
( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A )
let A be non empty Subset of L; ::_thesis: ( A is closed iff for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A )
xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def_4;
then A1: xi L = { V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in V } by YELLOW_6:def_24;
set V = A ` ;
A2: the topology of L = xi L by Def2;
hereby ::_thesis: ( ( for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A ) implies A is closed )
assume A is closed ; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A
then A ` in xi L by A2, PRE_TOPC:def_2;
then A3: ex V being Subset of L st
( V = A ` & ( for p being Element of L st p in V holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in V ) ) by A1;
let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: ( A in F implies lim_inf F in A )
assume A4: A in F ; ::_thesis: lim_inf F in A
( ( for M being subnet of a_net F holds lim_inf F = lim_inf M ) & a_net F in NetUniv L ) by Th14, Th16;
then A5: [(a_net F),(lim_inf F)] in lim_inf-Convergence L by WAYBEL28:def_3;
assume not lim_inf F in A ; ::_thesis: contradiction
then lim_inf F in A ` by XBOOLE_0:def_5;
then a_net F is_eventually_in A ` by A3, A5;
then consider i being Element of (a_net F) such that
A6: for j being Element of (a_net F) st i <= j holds
(a_net F) . j in A ` by WAYBEL_0:def_11;
A7: the carrier of (a_net F) = { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def_4;
i in the carrier of (a_net F) ;
then consider a being Element of L, f being Element of F such that
A8: i = [a,f] and
a in f by A7;
reconsider A9 = A, f9 = f as Element of (BoolePoset ([#] L)) by A4;
consider B being Element of (BoolePoset ([#] L)) such that
A9: B in F and
A10: A9 >= B and
A11: f9 >= B by A4, WAYBEL_0:def_2;
set b = the Element of B;
not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;
then not B is empty by A9, YELLOW_1:18;
then A12: the Element of B in B ;
the carrier of (BoolePoset ([#] L)) = bool the carrier of L by WAYBEL_7:2;
then [ the Element of B,B] in the carrier of (a_net F) by A7, A9, A12;
then reconsider j = [ the Element of B,B] as Element of (a_net F) ;
B c= f by A11, YELLOW_1:2;
then j `2 c= f by MCART_1:7;
then j `2 c= i `2 by A8, MCART_1:7;
then j >= i by YELLOW19:def_4;
then (a_net F) . j in A ` by A6;
then j `1 in A ` by YELLOW19:def_4;
then A13: the Element of B in A ` by MCART_1:7;
B c= A by A10, YELLOW_1:2;
hence contradiction by A12, A13, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A14: for F being ultra Filter of (BoolePoset ([#] L)) st A in F holds
lim_inf F in A ; ::_thesis: A is closed
now__::_thesis:_for_p_being_Element_of_L_st_p_in_A_`_holds_
for_N_being_net_of_L_st_[N,p]_in_lim_inf-Convergence_L_holds_
N_is_eventually_in_A_`
let p be Element of L; ::_thesis: ( p in A ` implies for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in A ` )
assume p in A ` ; ::_thesis: for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in A `
then A15: not p in (A `) ` by XBOOLE_0:def_5;
reconsider x = p as Element of L ;
let N be net of L; ::_thesis: ( [N,p] in lim_inf-Convergence L implies N is_eventually_in A ` )
assume A16: [N,p] in lim_inf-Convergence L ; ::_thesis: N is_eventually_in A `
assume not N is_eventually_in A ` ; ::_thesis: contradiction
then N is_often_in A by WAYBEL_0:10;
then consider N9 being strict subnet of N such that
A17: rng the mapping of N9 c= A and
A18: N9 is SubNetStr of N by Th17;
lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
then A19: N in NetUniv L by A16, ZFMISC_1:87;
then A20: ex N1 being strict net of L st
( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def_11;
set j0 = the Element of N9;
reconsider rj = rng the mapping of (N9 | the Element of N9), a = A as Element of (BoolePoset ([#] L)) by WAYBEL_7:2;
set j2 = the Element of N9;
set G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ;
set g = rng the mapping of (N9 | the Element of N9);
A21: rng the mapping of (N9 | the Element of N9) in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ;
for g being set st g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } holds
g in the carrier of (BoolePoset ([#] L))
proof
let g be set ; ::_thesis: ( g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } implies g in the carrier of (BoolePoset ([#] L)) )
assume g in { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } ; ::_thesis: g in the carrier of (BoolePoset ([#] L))
then ex j3 being Element of N9 st g = rng the mapping of (N9 | j3) ;
then g in bool ([#] L) ;
hence g in the carrier of (BoolePoset ([#] L)) by WAYBEL_7:2; ::_thesis: verum
end;
then reconsider G = { (rng the mapping of (N9 | j)) where j is Element of N9 : verum } as non empty Subset of (BoolePoset ([#] L)) by A21, TARSKI:def_3;
A22: G c= fininfs G by WAYBEL_0:50;
now__::_thesis:_for_p_being_set_st_p_in_rj_holds_
p_in_rng_the_mapping_of_N9
let p be set ; ::_thesis: ( p in rj implies p in rng the mapping of N9 )
assume p in rj ; ::_thesis: p in rng the mapping of N9
then p in rng ( the mapping of N9 | the carrier of (N9 | the Element of N9)) by WAYBEL_9:def_7;
then consider q being set such that
A23: q in dom ( the mapping of N9 | the carrier of (N9 | the Element of N9)) and
A24: p = ( the mapping of N9 | the carrier of (N9 | the Element of N9)) . q by FUNCT_1:def_3;
q in (dom the mapping of N9) /\ the carrier of (N9 | the Element of N9) by A23, RELAT_1:61;
then A25: q in dom the mapping of N9 by XBOOLE_0:def_4;
p = the mapping of N9 . q by A23, A24, FUNCT_1:47;
hence p in rng the mapping of N9 by A25, FUNCT_1:3; ::_thesis: verum
end;
then rj c= rng the mapping of N9 by TARSKI:def_3;
then rj c= a by A17, XBOOLE_1:1;
then ( rng the mapping of (N9 | the Element of N9) in G & rj <= a ) by YELLOW_1:2;
then A26: a in uparrow (fininfs G) by A22, WAYBEL_0:def_16;
A27: x = lim_inf N9 by A16, A19, WAYBEL28:def_3;
then A28: x = "\/" ( { (inf (N9 | j)) where j is Element of N9 : verum } ,L) by Th11;
the carrier of N9 c= the carrier of N by A18, YELLOW_6:10;
then the carrier of N9 in the_universe_of the carrier of L by A20, CLASSES1:def_1;
then A29: N9 in NetUniv L by YELLOW_6:def_11;
A30: not {} in fininfs G
proof
assume {} in fininfs G ; ::_thesis: contradiction
then consider Y being finite Subset of G such that
A31: {} = "/\" (Y,(BoolePoset ([#] L))) and
ex_inf_of Y, BoolePoset ([#] L) ;
defpred S1[ set , set ] means ex j being Element of N9 st
( j = $2 & $1 = rng the mapping of (N9 | j) );
A32: "/\" ({},(BoolePoset ([#] L))) = Top (BoolePoset ([#] L)) by YELLOW_0:def_12
.= [#] L by YELLOW_1:19 ;
reconsider Y = Y as finite Subset of (BoolePoset ([#] L)) by XBOOLE_1:1;
A33: for x being set st x in Y holds
ex y being set st
( y in the carrier of N9 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Y implies ex y being set st
( y in the carrier of N9 & S1[x,y] ) )
assume x in Y ; ::_thesis: ex y being set st
( y in the carrier of N9 & S1[x,y] )
then x in G ;
then A34: ex j being Element of N9 st x = rng the mapping of (N9 | j) ;
assume for y being set st y in the carrier of N9 holds
not S1[x,y] ; ::_thesis: contradiction
hence contradiction by A34; ::_thesis: verum
end;
consider f being Function such that
A35: ( dom f = Y & rng f c= the carrier of N9 ) and
A36: for x being set st x in Y holds
S1[x,f . x] from FUNCT_1:sch_5(A33);
reconsider C = rng f as finite Subset of ([#] N9) by A35, FINSET_1:8;
[#] N9 is directed by WAYBEL_0:def_6;
then consider j0 being Element of N9 such that
j0 in [#] N9 and
A37: j0 is_>=_than C by WAYBEL_0:1;
for y being set st y in Y holds
rng the mapping of (N9 | j0) c= y
proof
let y be set ; ::_thesis: ( y in Y implies rng the mapping of (N9 | j0) c= y )
assume A38: y in Y ; ::_thesis: rng the mapping of (N9 | j0) c= y
consider j1 being Element of N9 such that
A39: j1 = f . y and
A40: y = rng the mapping of (N9 | j1) by A36, A38;
A41: f . y in rng f by A35, A38, FUNCT_1:3;
then reconsider f1 = f . y as Element of N9 by A35;
A42: f1 <= j0 by A37, A41, LATTICE3:def_9;
for p being set st p in rng the mapping of (N9 | j0) holds
p in y
proof
let p be set ; ::_thesis: ( p in rng the mapping of (N9 | j0) implies p in y )
assume p in rng the mapping of (N9 | j0) ; ::_thesis: p in y
then p in rng ( the mapping of N9 | the carrier of (N9 | j0)) by WAYBEL_9:def_7;
then consider q being set such that
A43: q in dom ( the mapping of N9 | the carrier of (N9 | j0)) and
A44: p = ( the mapping of N9 | the carrier of (N9 | j0)) . q by FUNCT_1:def_3;
A45: q in (dom the mapping of N9) /\ the carrier of (N9 | j0) by A43, RELAT_1:61;
then q in the carrier of (N9 | j0) by XBOOLE_0:def_4;
then q in { n9 where n9 is Element of N9 : j0 <= n9 } by WAYBEL_9:12;
then consider n9 being Element of N9 such that
A46: q = n9 and
A47: j0 <= n9 ;
f1 <= n9 by A42, A47, YELLOW_0:def_2;
then q in { m9 where m9 is Element of N9 : j1 <= m9 } by A39, A46;
then A48: q in the carrier of (N9 | j1) by WAYBEL_9:12;
q in dom the mapping of N9 by A45, XBOOLE_0:def_4;
then q in (dom the mapping of N9) /\ the carrier of (N9 | j1) by A48, XBOOLE_0:def_4;
then A49: q in dom ( the mapping of N9 | the carrier of (N9 | j1)) by RELAT_1:61;
p = the mapping of N9 . q by A43, A44, FUNCT_1:47;
then p = ( the mapping of N9 | the carrier of (N9 | j1)) . q by A49, FUNCT_1:47;
then p in rng ( the mapping of N9 | the carrier of (N9 | j1)) by A49, FUNCT_1:3;
hence p in y by A40, WAYBEL_9:def_7; ::_thesis: verum
end;
hence rng the mapping of (N9 | j0) c= y by TARSKI:def_3; ::_thesis: verum
end;
then rng the mapping of (N9 | j0) c= meet Y by A31, A32, SETFAM_1:5;
then rng the mapping of (N9 | j0) c= {} by A31, A32, YELLOW_1:20;
hence contradiction ; ::_thesis: verum
end;
for y being Element of (BoolePoset ([#] L)) st Bottom (BoolePoset ([#] L)) >= y holds
not y in fininfs G
proof
let y be Element of (BoolePoset ([#] L)); ::_thesis: ( Bottom (BoolePoset ([#] L)) >= y implies not y in fininfs G )
assume Bottom (BoolePoset ([#] L)) >= y ; ::_thesis: not y in fininfs G
then ( {} = Bottom (BoolePoset ([#] L)) & y c= Bottom (BoolePoset ([#] L)) ) by YELLOW_1:2, YELLOW_1:18;
hence not y in fininfs G by A30; ::_thesis: verum
end;
then not Bottom (BoolePoset ([#] L)) in uparrow (fininfs G) by WAYBEL_0:def_16;
then uparrow (fininfs G) is proper by WAYBEL_7:4;
then consider F being Filter of (BoolePoset ([#] L)) such that
A50: uparrow (fininfs G) c= F and
A51: F is ultra by WAYBEL_7:26;
A52: fininfs G c= uparrow (fininfs G) by WAYBEL_0:16;
A53: { (inf (N9 | j)) where j is Element of N9 : verum } c= { (inf f) where f is Subset of L : f in F }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (inf (N9 | j)) where j is Element of N9 : verum } or x in { (inf f) where f is Subset of L : f in F } )
assume x in { (inf (N9 | j)) where j is Element of N9 : verum } ; ::_thesis: x in { (inf f) where f is Subset of L : f in F }
then consider j3 being Element of N9 such that
A54: x = inf (N9 | j3) ;
reconsider f1 = rng the mapping of (N9 | j3) as Subset of L ;
fininfs G c= F by A50, A52, XBOOLE_1:1;
then A55: ( f1 in G & G c= F ) by A22, XBOOLE_1:1;
x = Inf by A54, WAYBEL_9:def_2
.= "/\" ((rng the mapping of (N9 | j3)),L) by YELLOW_2:def_6 ;
hence x in { (inf f) where f is Subset of L : f in F } by A55; ::_thesis: verum
end;
now__::_thesis:_for_M_being_subnet_of_N9_holds_x_=_lim_inf_M
let M be subnet of N9; ::_thesis: x = lim_inf M
M is subnet of N by YELLOW_6:15;
hence x = lim_inf M by A16, A19, WAYBEL28:def_3; ::_thesis: verum
end;
then A56: for M being subnet of N9 st M in NetUniv L holds
x = lim_inf M ;
{ (inf f) where f is Subset of L : f in F } is_<=_than x
proof
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in { (inf f) where f is Subset of L : f in F } or y <= x )
assume y in { (inf f) where f is Subset of L : f in F } ; ::_thesis: y <= x
then consider f0 being Subset of L such that
A57: y = inf f0 and
A58: f0 in F ;
defpred S1[ Element of N9, Element of N9] means ( $1 <= $2 & N9 . $2 in f0 );
A59: now__::_thesis:_for_j_being_Element_of_N9_ex_pj_being_Element_of_N9_st_S1[j,pj]
let j be Element of N9; ::_thesis: ex pj being Element of N9 st S1[j,pj]
not Bottom (BoolePoset ([#] L)) in F by A51, WAYBEL_7:4;
then A60: not {} in F by YELLOW_1:18;
G c= uparrow (fininfs G) by A22, A52, XBOOLE_1:1;
then A61: G c= F by A50, XBOOLE_1:1;
rng the mapping of (N9 | j) in G ;
then f0 /\ (rng the mapping of (N9 | j)) in F by A58, A61, WAYBEL_7:9;
then consider nj being Element of L such that
A62: nj in f0 /\ (rng the mapping of (N9 | j)) by A60, SUBSET_1:4;
nj in rng the mapping of (N9 | j) by A62, XBOOLE_0:def_4;
then consider pj9 being set such that
A63: pj9 in dom the mapping of (N9 | j) and
A64: nj = the mapping of (N9 | j) . pj9 by FUNCT_1:def_3;
pj9 in the carrier of (N9 | j) by A63;
then pj9 in { y9 where y9 is Element of N9 : j <= y9 } by WAYBEL_9:12;
then consider pj being Element of N9 such that
A65: pj = pj9 and
A66: j <= pj ;
reconsider pj9 = pj9 as Element of (N9 | j) by A63;
take pj = pj; ::_thesis: S1[j,pj]
N9 . pj = (N9 | j) . pj9 by A65, WAYBEL_9:16
.= the mapping of (N9 | j) . pj9 ;
hence S1[j,pj] by A62, A64, A66, XBOOLE_0:def_4; ::_thesis: verum
end;
consider p being Function of N9,N9 such that
A67: for j being Element of N9 holds S1[j,p . j] from FUNCT_2:sch_3(A59);
for b being set st b in rng the mapping of (N9 * p) holds
b in f0
proof
let b be set ; ::_thesis: ( b in rng the mapping of (N9 * p) implies b in f0 )
assume b in rng the mapping of (N9 * p) ; ::_thesis: b in f0
then b in { ((N9 * p) . k) where k is Element of (N9 * p) : verum } by WAYBEL11:19;
then consider k being Element of (N9 * p) such that
A68: b = (N9 * p) . k ;
reconsider l = k as Element of N9 by WAYBEL28:6;
the carrier of (N9 * p) = the carrier of N9 by WAYBEL28:6;
then k in the carrier of N9 ;
then A69: k in dom p by FUNCT_2:52;
(N9 * p) . k = ( the mapping of N9 * p) . k by WAYBEL28:def_2
.= N9 . (p . l) by A69, FUNCT_1:13 ;
hence b in f0 by A67, A68; ::_thesis: verum
end;
then rng the mapping of (N9 * p) c= f0 by TARSKI:def_3;
then A70: "/\" (f0,L) <= "/\" ((rng the mapping of (N9 * p)),L) by WAYBEL_7:1;
A71: for M being subnet of N9 st M in NetUniv L holds
x >= inf M by A29, A56, WAYBEL28:3;
p is greater_or_equal_to_id by A67, WAYBEL28:def_1;
then A72: inf (N9 * p) <= x by A29, A27, A71, WAYBEL28:13;
inf (N9 * p) = Inf by WAYBEL_9:def_2
.= "/\" ((rng the mapping of (N9 * p)),L) by YELLOW_2:def_6 ;
hence y <= x by A57, A72, A70, YELLOW_0:def_2; ::_thesis: verum
end;
then A73: lim_inf F <= x by YELLOW_0:32;
( ex_sup_of { (inf f) where f is Subset of L : f in F } ,L & ex_sup_of { (inf (N9 | j)) where j is Element of N9 : verum } ,L ) by YELLOW_0:17;
then x <= lim_inf F by A28, A53, YELLOW_0:34;
then x = lim_inf F by A73, YELLOW_0:def_3;
hence contradiction by A14, A50, A51, A26, A15; ::_thesis: verum
end;
then A ` in xi L by A1;
then A ` is open by A2, PRE_TOPC:def_2;
hence A is closed by WAYBEL12:def_1; ::_thesis: verum
end;
theorem Th19: :: WAYBEL33:19
for L being non empty reflexive RelStr holds sigma L c= xi L
proof
let L be non empty reflexive RelStr ; ::_thesis: sigma L c= xi L
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sigma L or x in xi L )
assume x in sigma L ; ::_thesis: x in xi L
hence x in xi L by WAYBEL28:28; ::_thesis: verum
end;
theorem Th20: :: WAYBEL33:20
for T1, T2 being non empty TopSpace
for B being prebasis of T1 st B c= the topology of T2 & the carrier of T1 in the topology of T2 holds
the topology of T1 c= the topology of T2
proof
let T1, T2 be non empty TopSpace; ::_thesis: for B being prebasis of T1 st B c= the topology of T2 & the carrier of T1 in the topology of T2 holds
the topology of T1 c= the topology of T2
let B be prebasis of T1; ::_thesis: ( B c= the topology of T2 & the carrier of T1 in the topology of T2 implies the topology of T1 c= the topology of T2 )
assume that
A1: B c= the topology of T2 and
A2: the carrier of T1 in the topology of T2 ; ::_thesis: the topology of T1 c= the topology of T2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of T1 or x in the topology of T2 )
FinMeetCl B is Basis of T1 by YELLOW_9:23;
then A3: the topology of T1 = UniCl (FinMeetCl B) by YELLOW_9:22;
assume x in the topology of T1 ; ::_thesis: x in the topology of T2
then consider Y being Subset-Family of T1 such that
A4: Y c= FinMeetCl B and
A5: x = union Y by A3, CANTOR_1:def_1;
A6: Y c= the topology of T2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in the topology of T2 )
assume y in Y ; ::_thesis: y in the topology of T2
then consider Z being Subset-Family of T1 such that
A7: Z c= B and
A8: Z is finite and
A9: y = Intersect Z by A4, CANTOR_1:def_3;
Z c= the topology of T2 by A1, A7, XBOOLE_1:1;
then reconsider Z9 = Z as Subset-Family of T2 by XBOOLE_1:1;
( y = the carrier of T1 or ( Z9 c= the topology of T2 & y = meet Z9 & meet Z9 = Intersect Z9 ) ) by A1, A7, A9, SETFAM_1:def_9, XBOOLE_1:1;
then ( y = the carrier of T1 or y in FinMeetCl the topology of T2 ) by A8, CANTOR_1:def_3;
hence y in the topology of T2 by A2, CANTOR_1:5; ::_thesis: verum
end;
then reconsider Y = Y as Subset-Family of T2 by XBOOLE_1:1;
union Y in UniCl the topology of T2 by A6, CANTOR_1:def_1;
hence x in the topology of T2 by A5, CANTOR_1:6; ::_thesis: verum
end;
theorem Th21: :: WAYBEL33:21
for L being complete LATTICE holds omega L c= xi L
proof
let L be complete LATTICE; ::_thesis: omega L c= xi L
set S = the correct lower TopAugmentation of L;
set X = the lim-inf TopAugmentation of L;
reconsider B = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of L : verum } as prebasis of the correct lower TopAugmentation of L by WAYBEL19:def_1;
A1: ( RelStr(# the carrier of the correct lower TopAugmentation of L, the InternalRel of the correct lower TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of the lim-inf TopAugmentation of L, the InternalRel of the lim-inf TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4;
A2: B c= the topology of the lim-inf TopAugmentation of L
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in B or b in the topology of the lim-inf TopAugmentation of L )
assume b in B ; ::_thesis: b in the topology of the lim-inf TopAugmentation of L
then consider x being Element of the correct lower TopAugmentation of L such that
A3: b = (uparrow x) ` ;
reconsider y = x as Element of the lim-inf TopAugmentation of L by A1;
set A = uparrow y;
the lim-inf TopAugmentation of L is SubRelStr of the lim-inf TopAugmentation of L by YELLOW_6:6;
then the correct lower TopAugmentation of L is SubRelStr of the lim-inf TopAugmentation of L by A1, WAYBEL21:12;
then A4: uparrow x c= uparrow y by WAYBEL23:14;
A5: inf (uparrow y) = y by WAYBEL_0:39;
now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_([#]_the_lim-inf_TopAugmentation_of_L))_st_uparrow_y_in_F_holds_
lim_inf_F_in_uparrow_y
let F be ultra Filter of (BoolePoset ([#] the lim-inf TopAugmentation of L)); ::_thesis: ( uparrow y in F implies lim_inf F in uparrow y )
assume uparrow y in F ; ::_thesis: lim_inf F in uparrow y
then inf (uparrow y) in { (inf C) where C is Subset of the lim-inf TopAugmentation of L : C in F } ;
then inf (uparrow y) <= "\/" ( { (inf C) where C is Subset of the lim-inf TopAugmentation of L : C in F } , the lim-inf TopAugmentation of L) by YELLOW_2:22;
hence lim_inf F in uparrow y by A5, WAYBEL_0:18; ::_thesis: verum
end;
then A6: uparrow y is closed by Th18;
the correct lower TopAugmentation of L is SubRelStr of the correct lower TopAugmentation of L by YELLOW_6:6;
then the lim-inf TopAugmentation of L is SubRelStr of the correct lower TopAugmentation of L by A1, WAYBEL21:12;
then uparrow y c= uparrow x by WAYBEL23:14;
then uparrow y = uparrow x by A4, XBOOLE_0:def_10;
hence b in the topology of the lim-inf TopAugmentation of L by A1, A3, A6, PRE_TOPC:def_2; ::_thesis: verum
end;
the carrier of the correct lower TopAugmentation of L in the topology of the lim-inf TopAugmentation of L by A1, PRE_TOPC:def_1;
then the topology of the correct lower TopAugmentation of L c= the topology of the lim-inf TopAugmentation of L by A2, Th20;
then omega L c= the topology of the lim-inf TopAugmentation of L by WAYBEL19:def_2;
hence omega L c= xi L by Th10; ::_thesis: verum
end;
theorem Th22: :: WAYBEL33:22
for T1, T2 being TopSpace
for T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds
for R being Refinement of T1,T2 holds T is TopExtension of R
proof
let T1, T2 be TopSpace; ::_thesis: for T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 holds
for R being Refinement of T1,T2 holds T is TopExtension of R
let T be non empty TopSpace; ::_thesis: ( T is TopExtension of T1 & T is TopExtension of T2 implies for R being Refinement of T1,T2 holds T is TopExtension of R )
assume that
A1: the carrier of T1 = the carrier of T and
A2: the topology of T1 c= the topology of T and
A3: the carrier of T2 = the carrier of T and
A4: the topology of T2 c= the topology of T ; :: according to YELLOW_9:def_5 ::_thesis: for R being Refinement of T1,T2 holds T is TopExtension of R
let R be Refinement of T1,T2; ::_thesis: T is TopExtension of R
A5: the carrier of R = the carrier of T \/ the carrier of T by A1, A3, YELLOW_9:def_6;
hence the carrier of R = the carrier of T ; :: according to YELLOW_9:def_5 ::_thesis: the topology of R c= the topology of T
reconsider S = the topology of T1 \/ the topology of T2 as prebasis of R by YELLOW_9:def_6;
FinMeetCl S is Basis of R by YELLOW_9:23;
then A6: UniCl (FinMeetCl S) = the topology of R by YELLOW_9:22;
S c= the topology of T by A2, A4, XBOOLE_1:8;
then FinMeetCl S c= FinMeetCl the topology of T by A5, CANTOR_1:14;
then the topology of R c= UniCl (FinMeetCl the topology of T) by A5, A6, CANTOR_1:9;
hence the topology of R c= the topology of T by CANTOR_1:7; ::_thesis: verum
end;
theorem Th23: :: WAYBEL33:23
for T1 being TopSpace
for T2 being TopExtension of T1
for A being Subset of T1 holds
( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) )
proof
let T1 be TopSpace; ::_thesis: for T2 being TopExtension of T1
for A being Subset of T1 holds
( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) )
let T2 be TopExtension of T1; ::_thesis: for A being Subset of T1 holds
( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) )
let A be Subset of T1; ::_thesis: ( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) )
A1: the carrier of T1 = the carrier of T2 by YELLOW_9:def_5;
reconsider B = A as Subset of T2 by YELLOW_9:def_5;
reconsider C = ([#] T2) \ B as Subset of T2 ;
A2: the topology of T1 c= the topology of T2 by YELLOW_9:def_5;
thus ( A is open implies A is open Subset of T2 ) ::_thesis: ( A is closed implies A is closed Subset of T2 )
proof
assume A in the topology of T1 ; :: according to PRE_TOPC:def_2 ::_thesis: A is open Subset of T2
then A in the topology of T2 by A2;
hence A is open Subset of T2 by PRE_TOPC:def_2; ::_thesis: verum
end;
assume ([#] T1) \ A in the topology of T1 ; :: according to PRE_TOPC:def_2,PRE_TOPC:def_3 ::_thesis: A is closed Subset of T2
then C is open by A2, A1, PRE_TOPC:def_2;
hence A is closed Subset of T2 by PRE_TOPC:def_3; ::_thesis: verum
end;
theorem Th24: :: WAYBEL33:24
for L being complete LATTICE holds lambda L c= xi L
proof
let L be complete LATTICE; ::_thesis: lambda L c= xi L
set T = the correct Lawson TopAugmentation of L;
set S = the Scott TopAugmentation of L;
set LL = the correct lower TopAugmentation of L;
set LI = the lim-inf TopAugmentation of L;
A1: RelStr(# the carrier of the lim-inf TopAugmentation of L, the InternalRel of the lim-inf TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4;
A2: xi L = the topology of the lim-inf TopAugmentation of L by Th10;
omega L = the topology of the correct lower TopAugmentation of L by WAYBEL19:def_2;
then ( RelStr(# the carrier of the correct lower TopAugmentation of L, the InternalRel of the correct lower TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) & the topology of the correct lower TopAugmentation of L c= xi L ) by Th21, YELLOW_9:def_4;
then A3: the lim-inf TopAugmentation of L is TopExtension of the correct lower TopAugmentation of L by A2, A1, YELLOW_9:def_5;
sigma L = the topology of the Scott TopAugmentation of L by YELLOW_9:51;
then ( RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) & the topology of the Scott TopAugmentation of L c= xi L ) by Th19, YELLOW_9:def_4;
then ( the correct Lawson TopAugmentation of L is Refinement of the Scott TopAugmentation of L, the correct lower TopAugmentation of L & the lim-inf TopAugmentation of L is TopExtension of the Scott TopAugmentation of L ) by A2, A1, WAYBEL19:29, YELLOW_9:def_5;
then ( lambda L = the topology of the correct Lawson TopAugmentation of L & the lim-inf TopAugmentation of L is TopExtension of the correct Lawson TopAugmentation of L ) by A3, Th22, WAYBEL19:def_4;
hence lambda L c= xi L by A2, YELLOW_9:def_5; ::_thesis: verum
end;
theorem Th25: :: WAYBEL33:25
for L being complete LATTICE
for T being lim-inf TopAugmentation of L
for S being correct Lawson TopAugmentation of L holds T is TopExtension of S
proof
let L be complete LATTICE; ::_thesis: for T being lim-inf TopAugmentation of L
for S being correct Lawson TopAugmentation of L holds T is TopExtension of S
let T be lim-inf TopAugmentation of L; ::_thesis: for S being correct Lawson TopAugmentation of L holds T is TopExtension of S
let S be correct Lawson TopAugmentation of L; ::_thesis: T is TopExtension of S
( lambda L = the topology of S & xi L = the topology of T ) by Th10, WAYBEL19:def_4;
then A1: the topology of S c= the topology of T by Th24;
( RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of L, the InternalRel of L #) & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of L, the InternalRel of L #) ) by YELLOW_9:def_4;
hence T is TopExtension of S by A1, YELLOW_9:def_5; ::_thesis: verum
end;
theorem Th26: :: WAYBEL33:26
for L being complete lim-inf TopLattice
for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L
proof
let L be complete lim-inf TopLattice; ::_thesis: for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L
let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: lim_inf F is_a_convergence_point_of F,L
set x = lim_inf F;
let A be Subset of L; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not lim_inf F in A or A in F )
assume that
A1: A is open and
A2: lim_inf F in A and
A3: not A in F ; ::_thesis: contradiction
F is prime by WAYBEL_7:22;
then A4: ([#] L) \ A in F by A3, WAYBEL_7:21;
then A ` <> {} by YELLOW19:1;
then lim_inf F in A ` by A1, A4, Th18;
hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: WAYBEL33:27
for L being complete lim-inf TopLattice holds
( L is compact & L is T_1 )
proof
let L be complete lim-inf TopLattice; ::_thesis: ( L is compact & L is T_1 )
set T = the correct Lawson TopAugmentation of L;
now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_([#]_L))_ex_x_being_Point_of_L_st_x_is_a_convergence_point_of_F,L
let F be ultra Filter of (BoolePoset ([#] L)); ::_thesis: ex x being Point of L st x is_a_convergence_point_of F,L
reconsider x = lim_inf F as Point of L ;
take x = x; ::_thesis: x is_a_convergence_point_of F,L
thus x is_a_convergence_point_of F,L by Th26; ::_thesis: verum
end;
hence L is compact by YELLOW19:31; ::_thesis: L is T_1
now__::_thesis:_for_x_being_Point_of_L_holds_Cl_{x}_=_{x}
let x be Point of L; ::_thesis: Cl {x} = {x}
reconsider y = x as Element of L ;
RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of the correct Lawson TopAugmentation of L, the InternalRel of the correct Lawson TopAugmentation of L #) by YELLOW_9:def_4;
then reconsider z = y as Element of the correct Lawson TopAugmentation of L ;
L is TopAugmentation of L by YELLOW_9:44;
then A1: L is TopExtension of the correct Lawson TopAugmentation of L by Th25;
{z} is closed ;
then {y} is closed by A1, Th23;
hence Cl {x} = {x} by PRE_TOPC:22; ::_thesis: verum
end;
hence L is T_1 by FRECHET2:43; ::_thesis: verum
end;