:: Lim-inf Convergence
:: by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REWRITE1, WAYBEL_0, ORDINAL2, XXREAL_0, LATTICES, FUNCT_1,
SUBSET_1, TARSKI, STRUCT_0, RELAT_1, YELLOW_0, YELLOW_2, LATTICE3,
EQREL_1, YELLOW_6, XBOOLE_0, ORDERS_2, RELAT_2, ZFMISC_1, SETFAM_1,
PRE_TOPC, WAYBEL11, CLASSES1, CAT_1, PROB_1, YELLOW_9, RCOMP_1, WAYBEL28;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, STRUCT_0, CLASSES1, PRE_TOPC, ORDERS_2, LATTICE3,
YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_3, YELLOW_6, YELLOW_9, WAYBEL_9,
WAYBEL11, WAYBEL17;
constructors CLASSES1, YELLOW_2, WAYBEL_3, WAYBEL17, YELLOW_9, RELSET_1;
registrations RELAT_1, FUNCT_1, FUNCT_2, CLASSES2, STRUCT_0, LATTICE3,
YELLOW_0, WAYBEL_0, WAYBEL_3, YELLOW_6, WAYBEL_9, WAYBEL11, WAYBEL17,
YELLOW_9, RELSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RELAT_1, YELLOW_6, WAYBEL11;
equalities XBOOLE_0, YELLOW_6, WAYBEL11, STRUCT_0;
expansions TARSKI, YELLOW_6, WAYBEL11;
theorems ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, ORDERS_2,
CLASSES1, WAYBEL_0, YELLOW_0, LATTICE3, YELLOW_2, YELLOW_4, YELLOW_6,
WAYBEL_8, YELLOW_9, WAYBEL_9, WAYBEL11, YELLOW12, WAYBEL17, WAYBEL21;
schemes RELSET_1, FUNCT_1;
begin
theorem Th1:
for L being complete LATTICE, N being net of L holds inf N <= lim_inf N
proof
let L be complete LATTICE, N be net of L;
set X = the set of all
"/\"({N.i where i is Element of N :i >= j1},L) where j1 is Element
of N;
X c= the carrier of L
proof
let x be object;
assume x in X;
then ex j1 being Element of N st x = "/\"({N.i where i is Element of N :i
>= j1},L);
hence thesis;
end;
then reconsider X as Subset of L;
set j = the Element of N;
A1: {N.i where i is Element of N:i >= j} c= rng the mapping of N
proof
let x be object;
A2: dom(the mapping of N) = the carrier of N by FUNCT_2:def 1;
assume x in {N.i where i is Element of N:i >= j};
then consider i being Element of N such that
A3: x = N.i and
i >= j;
x = (the mapping of N).i by A3,WAYBEL_0:def 8;
hence thesis by A2,FUNCT_1:def 3;
end;
reconsider X as Subset of L;
set x = "/\"({N.i where i is Element of N:i >= j},L);
ex_inf_of {N.i where i is Element of N:i >= j},L & ex_inf_of rng the
mapping of N,L by YELLOW_0:17;
then
"/\"({N.i where i is Element of N:i >= j},L) >= "/\"(rng the mapping of
N,L) by A1,YELLOW_0:35;
then x >= Inf(the mapping of N) by YELLOW_2:def 6;
then
A4: inf N <= x by WAYBEL_9:def 2;
ex_sup_of X,L by YELLOW_0:17;
then x in X & X is_<=_than "\/"(X,L) by YELLOW_0:def 9;
then x <= "\/"(X,L) by LATTICE3:def 9;
hence thesis by A4,YELLOW_0:def 2;
end;
theorem ::3.1 Proposition (1)=>(2)
for L being complete LATTICE, N being net of L, x being Element of L
holds (for M being subnet of N holds x = lim_inf M) implies (x=lim_inf N & for
M being subnet of N holds x >= inf M)
proof
let L be complete LATTICE, N be net of L, x be Element of L;
assume
A1: for M being subnet of N holds x = lim_inf M;
N is subnet of N by YELLOW_6:14;
hence x=lim_inf N by A1;
let M be subnet of N;
x = lim_inf M by A1;
hence thesis by Th1;
end;
theorem Th3:
for L being complete LATTICE, N being net of L, x being Element
of L st N in NetUniv L holds (for M being subnet of N st M in NetUniv L holds x
= lim_inf M) implies (x=lim_inf N & for M being subnet of N st M in NetUniv L
holds x >= inf M)
proof
let L be complete LATTICE, N be net of L, x be Element of L;
assume
A1: N in NetUniv L;
assume
A2: for M being subnet of N st M in NetUniv L holds x = lim_inf M;
N is subnet of N by YELLOW_6:14;
hence x=lim_inf N by A1,A2;
let M be subnet of N;
assume M in NetUniv L;
then x = lim_inf M by A2;
hence thesis by Th1;
end;
definition
let N be non empty RelStr;
let f be Function of N,N;
attr f is greater_or_equal_to_id means
:Def1:
for j being Element of N holds j <= f.j;
end;
theorem Th4:
for N being reflexive non empty RelStr holds id N is greater_or_equal_to_id
proof
let N be reflexive non empty RelStr;
let j be Element of N;
reconsider n=j as Element of N;
n <= (id N).n;
hence thesis;
end;
theorem Th5:
for N being directed non empty RelStr, x,y being Element of N ex
z being Element of N st x <= z & y <= z
proof
let N be directed non empty RelStr, x,y be Element of N;
[#]N is directed by WAYBEL_0:def 6;
then ex z being Element of N st z in [#]N & x <= z & y <= z by WAYBEL_0:def 1
;
hence thesis;
end;
registration
let N be directed non empty RelStr;
cluster greater_or_equal_to_id for Function of N,N;
existence
proof
defpred P[object,object] means
for n,m being Element of N st $1=n & $2=m holds n
<= m;
A1: for e being object st e in the carrier of N
ex u being object st u in the carrier of N & P[e,u]
proof
let e be object;
assume e in the carrier of N;
then reconsider e9=e as Element of N;
consider u9 being Element of N such that
A2: e9<= u9 and
e9 <= u9 by Th5;
take u9;
thus u9 in the carrier of N;
let n,m be Element of N;
assume e=n & u9=m;
hence thesis by A2;
end;
consider p being Function such that
A3: dom p = the carrier of N & rng p c= the carrier of N and
A4: for e being object st e in the carrier of N holds P[e,p.e] from
FUNCT_1:sch 6(A1);
reconsider p as Function of N,N by A3,FUNCT_2:2;
take p;
let j be Element of N;
thus thesis by A4;
end;
end;
registration
let N be reflexive non empty RelStr;
cluster greater_or_equal_to_id for Function of N,N;
existence
proof
take id N;
thus thesis by Th4;
end;
end;
definition
let L be non empty 1-sorted;
let N be non empty NetStr over L;
let f be Function of N,N;
func N * f -> strict non empty NetStr over L means
:Def2:
the RelStr of it =
the RelStr of N & the mapping of it = (the mapping of N) * f;
existence
proof
take NetStr (# the carrier of N,the InternalRel of N,(the mapping of N)*f
#);
thus thesis;
end;
uniqueness;
end;
theorem Th6:
for L being non empty 1-sorted, N being non empty NetStr over L,
f being Function of N, N holds the carrier of N * f = the carrier of N
proof
let L be non empty 1-sorted, N be non empty NetStr over L, f be Function of
N, N;
the RelStr of N * f = the RelStr of N by Def2;
hence thesis;
end;
theorem Th7:
for L being non empty 1-sorted, N being non empty NetStr over L,
f being Function of N,N holds N * f = NetStr(#the carrier of N,the InternalRel
of N,(the mapping of N)*f#)
proof
let L be non empty 1-sorted, N be non empty NetStr over L, f be Function of
N,N;
the RelStr of N*f=the RelStr of N by Def2;
hence thesis by Def2;
end;
theorem Th8:
for L being non empty 1-sorted, N being transitive directed non
empty RelStr, f being Function of the carrier of N,the carrier of L holds
NetStr (#the carrier of N,the InternalRel of N,f#) is net of L
proof
let L be non empty 1-sorted, N be transitive directed non empty RelStr, f be
Function of the carrier of N,the carrier of L;
set N2 = NetStr(#the carrier of N,the InternalRel of N,f#);
A1: the RelStr of N = the RelStr of N2;
[#]N is directed by WAYBEL_0:def 6;
then [#]N2 is directed by A1,WAYBEL_0:3;
hence thesis by A1,WAYBEL_0:def 6,WAYBEL_8:13;
end;
registration
let L be non empty 1-sorted, N be transitive directed non empty RelStr, f be
Function of the carrier of N,the carrier of L;
cluster NetStr (#the carrier of N,the InternalRel of N,f#) -> transitive
directed non empty;
correctness by Th8;
end;
theorem Th9:
for L being non empty 1-sorted, N being net of L, p being
Function of N,N holds N * p is net of L
proof
let L be non empty 1-sorted, N be net of L, p be Function of N,N;
N * p = NetStr(#the carrier of N,the InternalRel of N,(the mapping of N
) * p #) by Th7;
hence thesis;
end;
registration
let L be non empty 1-sorted, N be net of L;
let p be Function of N,N;
cluster N * p -> transitive directed;
correctness by Th9;
end;
theorem Th10:
for L being non empty 1-sorted, N being net of L, p being
Function of N,N st N in NetUniv L holds N * p in NetUniv L
proof
let L be non empty 1-sorted, N be net of L, p be Function of N,N;
assume N in NetUniv L;
then
A1: 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;
the carrier of N * p = the carrier of N by Th6;
hence thesis by A1,YELLOW_6:def 11;
end;
theorem
for L being non empty 1-sorted, N,M being net of L st the NetStr of N
= the NetStr of M holds M is subnet of N
proof
let L be non empty 1-sorted, N,M be net of L;
assume
A1: the NetStr of N = the NetStr of M;
A2: N is subnet of N by YELLOW_6:14;
ex f being Function of M, N st the mapping of M = (the mapping of N)*f &
for m being Element of N ex n being Element of M st for p being Element of M st
n <= p holds m <= f.p
proof
consider f being Function of N, N such that
A3: the mapping of N = (the mapping of N)*f and
A4: for m being Element of N ex n being Element of N st for p being
Element of N st n <= p holds m <= f.p by A2,YELLOW_6:def 9;
reconsider f2=f as Function of M,N by A1;
take f2;
thus the mapping of M = (the mapping of N)*f2 by A1,A3;
let m be Element of N;
consider n being Element of N such that
A5: for p being Element of N st n <= p holds m <= f.p by A4;
reconsider n2=n as Element of M by A1;
take n2;
let p be Element of M;
reconsider p1=p as Element of N by A1;
assume n2 <= p;
then [n2,p] in the InternalRel of M by ORDERS_2:def 5;
then n <= p1 by A1,ORDERS_2:def 5;
hence thesis by A5;
end;
hence thesis by YELLOW_6:def 9;
end;
theorem Th12:
for L being non empty 1-sorted, N being net of L, p being
greater_or_equal_to_id Function of N,N holds N * p is subnet of N
proof
let L be non empty 1-sorted;
let N be net of L;
let p be greater_or_equal_to_id Function of N,N;
ex f being Function of (N * p), N st the mapping of (N * p) = (the
mapping of N)*f & for m being Element of N ex n being Element of (N * p) st for
k being Element of (N * p) st n <= k holds m <= f.k
proof
the carrier of N * p = the carrier of N by Th6;
then reconsider f=p as Function of (N * p), N;
take f;
thus the mapping of (N * p) = (the mapping of N)*f by Def2;
let m be Element of N;
reconsider n=m as Element of (N * p) by Th6;
take n;
let k be Element of (N * p);
assume
A1: n <= k;
reconsider k1 = k as Element of N by Th6;
A2: k1 <= p.k1 by Def1;
the RelStr of N*p = the RelStr of N by Def2;
then m <= k1 by A1,YELLOW_0:1;
hence thesis by A2,YELLOW_0:def 2;
end;
hence thesis by YELLOW_6:def 9;
end;
definition
let L be non empty 1-sorted;
let N be net of L;
let p be greater_or_equal_to_id Function of N,N;
redefine func N * p -> strict subnet of N;
correctness by Th12;
end;
theorem ::3.1 Proposition (2)=>(3)
for L being complete LATTICE, N being net of L, x being Element of L
st N in NetUniv L holds (x=lim_inf N & for M being subnet of N st M in NetUniv
L holds x >= inf M) implies x=lim_inf N & for p being greater_or_equal_to_id
Function of N,N holds x >= inf (N * p) by Th10;
theorem Th14:
for L being complete LATTICE, N being net of L, x being Element
of L holds (x=lim_inf N & for p being greater_or_equal_to_id Function of N,N
holds x >= inf (N * p) ) implies for M being subnet of N holds x = lim_inf M
proof
let L be complete LATTICE, N be net of L, x be Element of L;
assume that
A1: x=lim_inf N and
A2: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p);
let M be subnet of N;
consider f being Function of M, N such that
A3: the mapping of M = (the mapping of N)*f and
A4: for j being Element of N ex k being Element of M st for m being
Element of M st k <= m holds j <= f.m by YELLOW_6:def 9;
A5: x <= lim_inf M by A1,WAYBEL21:37;
A6: for k0 being Element of M holds "/\"({M.k where k is Element of M:k >=
k0},L)<=x
proof
let k0 be Element of M;
defpred P[object,object] means
for j being Element of N, v,v9 being Element of M
st $1=j & $2=v & v9>= v holds v >= k0 & f.(v9)>=j & f.v >= j;
A7: for j being Element of N ex v being Element of M st v >= k0 & for v9
being Element of M st v9>= v holds f.(v9)>=j & f.v >= j
proof
let j be Element of N;
consider w being Element of M such that
A8: for w9 being Element of M st w <= w9 holds j <= f.(w9) by A4;
consider v being Element of M such that
A9: v >= k0 and
A10: v >= w by Th5;
take v;
thus v >= k0 by A9;
let v9 be Element of M;
assume v9>= v;
then v9 >= w by A10,YELLOW_0:def 2;
hence f.(v9)>=j by A8;
thus thesis by A8,A10;
end;
A11: for e being object st e in the carrier of N
ex u being object st u in the
carrier of M & P[e,u]
proof
let e be object;
assume e in the carrier of N;
then reconsider e9=e as Element of N;
consider u being Element of M such that
A12: u >= k0 and
A13: for v9 being Element of M st v9>= u holds f.(v9)>=e9 & f.u >= e9 by A7;
take u;
thus u in the carrier of M;
let j be Element of N, v,v9 be Element of M;
assume that
A14: e=j and
A15: u=v and
A16: v9>= v;
thus v >= k0 by A12,A15;
thus f.(v9)>=j by A13,A14,A15,A16;
thus thesis by A13,A14,A15,A16;
end;
consider g being Function such that
A17: dom g = the carrier of N and
A18: rng g c= the carrier of M and
A19: for e being object st e in the carrier of N holds P[e,g.e] from
FUNCT_1:sch 6(A11);
reconsider g as Function of the carrier of N,the carrier of M by A17,A18,
FUNCT_2:2;
A20: for j being Element of N holds g.j >= k0
proof
let j be Element of N;
reconsider v=g.j as Element of M;
ex v9 being Element of M st v9>= v & v9>= v by Th5;
hence thesis by A19;
end;
reconsider g as Function of N,M;
reconsider p=f*g as Function of N,N;
for j being Element of N holds j <= p.j
proof
let j be Element of N;
reconsider v=g.j as Element of M;
[#]M is directed by WAYBEL_0:def 6;
then ex v9 being Element of M st v9 in [#]M & v <= v9 & v <= v9 by
WAYBEL_0:def 1;
then j <= f.(g.j) by A19;
hence thesis by A17,FUNCT_1:13;
end;
then reconsider p as greater_or_equal_to_id Function of N,N by Def1;
A21: the set of all (N*p).j where j is Element of (N*p) c= {M.k where
k is Element of M:k >= k0}
proof
let y be object;
assume y in the set of all (N*p).j where j is Element of (N*p);
then consider j being Element of (N*p) such that
A22: y = (N*p).j;
reconsider j9=j as Element of N by Th6;
A23: the carrier of (N*p)= the carrier of N by Th6;
y = (the mapping of (N*p)).j by A22,WAYBEL_0:def 8
.= ((the mapping of N)*(f*g)).j by Def2
.= ((the mapping of M)*g).j by A3,RELAT_1:36
.= (the mapping of M).(g.j) by A17,A23,FUNCT_1:13;
then
A24: y = M.(g.j9) by WAYBEL_0:def 8;
g.j9 >= k0 by A20;
hence thesis by A24;
end;
A25: ex_inf_of (the set of all (N*p).j where j is Element of (N*p)),L
& ex_inf_of {M.k where k is Element of M:k >= k0},L by YELLOW_0:17;
A26: dom (the mapping of (N*p)) = the carrier of (N*p) by FUNCT_2:def 1;
A27: rng the mapping of (N*p) = the set of all
(N*p).j where j is Element of (N*p)
proof
thus rng the mapping of (N*p) c= the set of all
(N*p).j where j is Element of (N*p)
proof
let y be object;
assume y in rng the mapping of (N*p);
then consider j1 being object such that
A28: j1 in dom (the mapping of (N*p)) and
A29: (the mapping of (N*p)).j1 = y by FUNCT_1:def 3;
reconsider j1 as Element of (N*p) by A28;
y = (N*p).j1 by A29,WAYBEL_0:def 8;
hence thesis;
end;
let y be object;
assume y in the set of all (N*p).j where j is Element of (N*p);
then consider j being Element of (N*p) such that
A30: y = (N*p).j;
y = (the mapping of (N*p)).j by A30,WAYBEL_0:def 8;
hence thesis by A26,FUNCT_1:def 3;
end;
A31: inf (N * p) <= x by A2;
inf (N*p) = Inf the mapping of (N*p) by WAYBEL_9:def 2
.= "/\"((the set of all (N*p).j where j is Element of (N*p)),L)
by A27,YELLOW_2:def 6;
then
"/\"({M.k where k is Element of M:k >= k0},L)<= inf (N*p) by A25,A21,
YELLOW_0:35;
hence thesis by A31,YELLOW_0:def 2;
end;
for b being Element of L st b in the set of all
"/\"({M.k where k is Element of M:k
>= k0},L) where k0 is Element of M holds b <= x
proof
let b be Element of L;
assume b in the set of all
"/\"({M.k where k is Element of M:k >= k0},L) where k0 is
Element of M;
then
ex k0 being Element of M st b = "/\"({M.k where k is Element of M:k >=
k0},L);
hence thesis by A6;
end;
then
A32: x is_>=_than the set of all
"/\" ({M.k where k is Element of M:k >= k0},L) where k0
is Element of M by LATTICE3:def 9;
ex_sup_of (the set of all "/\"({M.k where k is Element of M:k >= k0},L)
where k0 is Element of M),L by YELLOW_0:17;
then "\/"((the set of all "/\"({M.k where k is Element of M:k >= k0},L)
where k0 is Element of M),L)<=x by A32,YELLOW_0:def 9;
hence thesis by A5,ORDERS_2:2;
end;
definition
let L be non empty RelStr;
func lim_inf-Convergence L -> Convergence-Class of L means
:Def3:
for N being net of L st N in NetUniv L for x being Element of L holds
[N,x] in it iff for M being subnet of N holds x = lim_inf M;
existence
proof
defpred P[set,set] means ex N being strict net of L st $1=N & for M being
subnet of N holds $2 = lim_inf M;
consider C being Relation of NetUniv L,the carrier of L such that
A1: for N9 being Element of NetUniv L, x being Element of L holds [N9,
x] in C iff P[N9, x] from RELSET_1:sch 2;
reconsider C as Convergence-Class of L by YELLOW_6:def 18;
take C;
let N be net of L;
assume N in NetUniv L;
then reconsider N1=N as Element of NetUniv L;
let x be Element of L;
thus [N,x] in C implies for M being subnet of N holds x = lim_inf M
proof
assume
A2: [N,x] in C;
let M be subnet of N;
ex N2 being strict net of L st N1=N2 & for M being subnet of N2 holds
x = lim_inf M by A1,A2;
hence thesis;
end;
A3: ex N2 being strict net of L st N2=N1 & the carrier of N2 in
the_universe_of the carrier of L by YELLOW_6:def 11;
assume for M being subnet of N holds x = lim_inf M;
hence thesis by A1,A3;
end;
uniqueness
proof
let C1,C2 be Convergence-Class of L such that
A4: for N being net of L st N in NetUniv L for x being Element of L
holds [N,x] in C1 iff for M being subnet of N holds x = lim_inf M and
A5: for N being net of L st N in NetUniv L for x being Element of L
holds [N,x] in C2 iff for M being subnet of N holds x = lim_inf M;
let Ns,xs be object;
A6: C1 c= [:NetUniv L,the carrier of L:] by YELLOW_6:def 18;
thus [Ns,xs] in C1 implies [Ns,xs] in C2
proof
assume
A7: [Ns,xs] in C1;
then reconsider x=xs as Element of L by A6,ZFMISC_1:87;
Ns in NetUniv L by A6,A7,ZFMISC_1:87;
then consider N being strict net of L such that
A8: N = Ns and
the carrier of N in the_universe_of the carrier of L by YELLOW_6:def 11;
A9: N in NetUniv L by A6,A7,A8,ZFMISC_1:87;
then for M being subnet of N holds x = lim_inf M by A4,A7,A8;
hence thesis by A5,A8,A9;
end;
assume
A10: [Ns,xs] in C2;
A11: C2 c= [:NetUniv L,the carrier of L:] by YELLOW_6:def 18;
then reconsider x=xs as Element of L by A10,ZFMISC_1:87;
Ns in NetUniv L by A11,A10,ZFMISC_1:87;
then consider N being strict net of L such that
A12: N = Ns and
the carrier of N in the_universe_of the carrier of L by YELLOW_6:def 11;
A13: N in NetUniv L by A11,A10,A12,ZFMISC_1:87;
then for M being subnet of N holds x = lim_inf M by A5,A10,A12;
hence thesis by A4,A12,A13;
end;
end;
theorem
for L being complete LATTICE, N being net of L, x being Element of L
st N in NetUniv L holds [N,x] in lim_inf-Convergence L iff for M being subnet
of N st M in NetUniv L holds x = lim_inf M
proof
let L be complete LATTICE;
let N be net of L;
let x be Element of L;
assume
A1: N in NetUniv L;
hence [N,x] in lim_inf-Convergence L implies for M being subnet of N st M in
NetUniv L holds x = lim_inf M by Def3;
assume
A2: for M being subnet of N st M in NetUniv L holds x = lim_inf M;
then for M being subnet of N st M in NetUniv L holds x >= inf M by A1,Th3;
then
A3: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p
) by A1,Th10;
x=lim_inf N by A1,A2,Th3;
then for M being subnet of N holds x = lim_inf M by A3,Th14;
hence thesis by A1,Def3;
end;
theorem Th16:
for L being non empty RelStr, N being constant net of L, M being
subnet of N holds M is constant & the_value_of N = the_value_of M
proof
let L be non empty RelStr, N be constant net of L, M be subnet of N;
consider f being Function of M, N such that
A1: the mapping of M = (the mapping of N)*f and
for m being Element of N ex n being Element of M st for p being Element
of M st n <= p holds m <= f.p by YELLOW_6:def 9;
set y = the Element of dom (the mapping of M);
A2: dom (the mapping of N) = the carrier of N by FUNCT_2:def 1;
then
A3: the_value_of the mapping of N= (the mapping of N).(f.y) by FUNCT_1:def 12
.= (the mapping of M).y by A1,FUNCT_1:12;
A4: dom f = the carrier of M by FUNCT_2:def 1;
for n1,n2 being object st n1 in dom (the mapping of M) & n2 in dom (the
mapping of M) holds (the mapping of M).n1=(the mapping of M).n2
proof
let n1,n2 be object;
assume that
A5: n1 in dom (the mapping of M) and
A6: n2 in dom (the mapping of M);
A7: f.n1 in rng f & f.n2 in rng f by A4,A5,A6,FUNCT_1:def 3;
thus (the mapping of M).n1= (the mapping of N).(f.n1) by A1,A4,A5,
FUNCT_1:13
.= (the mapping of N).(f.n2) by A2,A7,FUNCT_1:def 10
.= (the mapping of M).n2 by A1,A4,A6,FUNCT_1:13;
end;
then
A8: the mapping of M is constant by FUNCT_1:def 10;
hence
A9: M is constant;
thus the_value_of N = the_value_of the mapping of N by YELLOW_6:def 8
.= the_value_of the mapping of M by A8,A3,FUNCT_1:def 12
.= the_value_of M by A9,YELLOW_6:def 8;
end;
definition
let L be non empty RelStr;
func xi L -> Subset-Family of L equals
the topology of ConvergenceSpace
lim_inf-Convergence L;
correctness by YELLOW_6:def 24;
end;
theorem
for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS)
proof
let L be complete LATTICE;
let N be constant net of L;
A1: for M being subnet of N holds the_value_of N = lim_inf M
proof
let M be subnet of N;
A2: M is constant by Th16;
thus the_value_of N = the_value_of M by Th16
.= lim_inf M by A2,WAYBEL11:23;
end;
assume N in NetUniv L;
hence thesis by A1,Def3;
end;
theorem
for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS)
proof
let L be non empty RelStr;
let N be net of L, M be subnet of N;
assume
A1: M in NetUniv L;
let x be Element of L;
assume
A2: [N,x] in lim_inf-Convergence L;
lim_inf-Convergence L c= [:NetUniv L,the carrier of L:] by YELLOW_6:def 18;
then
A3: N in NetUniv L by A2,ZFMISC_1:87;
for M1 being subnet of M holds x = lim_inf M1
proof
let M1 be subnet of M;
reconsider M19=M1 as subnet of N by YELLOW_6:15;
x = lim_inf M19 by A2,A3,Def3;
hence thesis;
end;
hence thesis by A1,Def3;
end;
theorem
for L being continuous complete LATTICE holds lim_inf-Convergence L is
(DIVERGENCE)
proof
let L be continuous complete LATTICE;
let N be net of L, x be Element of L;
assume that
A1: N in NetUniv L and
A2: not [N,x] in lim_inf-Convergence L;
A3: ex N1 being strict net of L st N1=N & the carrier of N1 in
the_universe_of the carrier of L by A1,YELLOW_6:def 11;
not for M being subnet of N holds x = lim_inf M by A1,A2,Def3;
then
A4: not (x=lim_inf N & for p being greater_or_equal_to_id Function of N,N
holds x >= inf (N * p)) by Th14;
A5: lim_inf-Convergence L c= [:NetUniv L,the carrier of L:] by YELLOW_6:def 18;
per cases by A1,A4,Th10;
suppose
A6: not x=lim_inf N & x<=lim_inf N;
reconsider N9=N as subnet of N by YELLOW_6:14;
take N9;
thus N9 in NetUniv L by A1;
given M2 being subnet of N9 such that
A7: [M2,x] in lim_inf-Convergence L;
A8: lim_inf N <= lim_inf M2 by WAYBEL21:37;
A9: M2 is subnet of M2 by YELLOW_6:14;
M2 in NetUniv L by A5,A7,ZFMISC_1:87;
then lim_inf M2 =x by A7,A9,Def3;
hence contradiction by A6,A8,YELLOW_0:def 3;
end;
suppose
not x=lim_inf N & not x<=lim_inf N;
then not x is_S-limit_of N;
then not [N,x] in Scott-Convergence L by A1,A3,WAYBEL11:def 8;
then consider M being subnet of N such that
A10: M in NetUniv L and
A11: not ex M1 being subnet of M st [M1,x] in Scott-Convergence L by A1,
YELLOW_6:def 22;
take M;
thus M in NetUniv L by A10;
for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L
proof
let M1 be subnet of M;
A12: not [M1,x] in Scott-Convergence L by A11;
assume
A13: [M1,x] in lim_inf-Convergence L;
then
A14: M1 in NetUniv L by A5,ZFMISC_1:87;
then ex M11 being strict net of L st M11=M1 & the carrier of M11 in
the_universe_of the carrier of L by YELLOW_6:def 11;
then
A15: not x is_S-limit_of M1 by A14,A12,WAYBEL11:def 8;
M1 is subnet of M1 by YELLOW_6:14;
then x = lim_inf M1 by A13,A14,Def3;
hence contradiction by A15;
end;
hence thesis;
end;
suppose
not (for M being subnet of N st M in NetUniv L holds x >= inf M);
then consider M being subnet of N such that
A16: M in NetUniv L and
A17: not x >= inf M;
take M;
thus M in NetUniv L by A16;
for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L
proof
let M1 be subnet of M;
A18: M1 is subnet of M1 by YELLOW_6:14;
A19: lim_inf M1 >= lim_inf M & lim_inf M >= inf M by Th1,WAYBEL21:37;
assume
A20: [M1,x] in lim_inf-Convergence L;
then M1 in NetUniv L by A5,ZFMISC_1:87;
then x = lim_inf M1 by A20,A18,Def3;
hence contradiction by A17,A19,YELLOW_0:def 2;
end;
hence thesis;
end;
end;
theorem
for L being non empty RelStr, N,x being set holds [N,x] in
lim_inf-Convergence L implies N in NetUniv L
proof
let L be non empty RelStr, N,x be set;
A1: lim_inf-Convergence L c= [:NetUniv L,the carrier of L:] by YELLOW_6:def 18;
assume [N,x] in lim_inf-Convergence L;
hence thesis by A1,ZFMISC_1:87;
end;
theorem Th21:
for L being non empty 1-sorted, C1,C2 being Convergence-Class of
L holds C1 c= C2 implies the topology of ConvergenceSpace C2 c= the topology of
ConvergenceSpace C1
proof
let L be non empty 1-sorted, C1,C2 be Convergence-Class of L;
assume
A1: C1 c= C2;
let A be object;
assume A in the topology of ConvergenceSpace C2;
then
A in { V where V is Subset of L: for p being Element of L st p in V for
N being net of L st [N,p] in C2 holds N is_eventually_in V} by
YELLOW_6:def 24;
then consider V1 being Subset of L such that
A2: A=V1 and
A3: for p being Element of L st p in V1 for N being net of L st [N,p] in
C2 holds N is_eventually_in V1;
ex V being Subset of L st A=V & for p being Element of L st p in V for N
being net of L st [N,p] in C1 holds N is_eventually_in V
proof
take V1;
thus A=V1 by A2;
let p be Element of L;
assume
A4: p in V1;
let N be net of L;
assume [N,p] in C1;
hence thesis by A1,A3,A4;
end;
then
A in { V where V is Subset of L: for p being Element of L st p in V for
N being net of L st [N,p] in C1 holds N is_eventually_in V};
hence thesis by YELLOW_6:def 24;
end;
theorem Th22:
for L being non empty reflexive RelStr holds lim_inf-Convergence
L c= Scott-Convergence L
proof
let L be non empty reflexive RelStr;
let Ns,xs be object;
assume
A1: [Ns,xs] in lim_inf-Convergence L;
A2: lim_inf-Convergence L c= [:NetUniv L,the carrier of L:] by YELLOW_6:def 18;
then reconsider x=xs as Element of L by A1,ZFMISC_1:87;
Ns in NetUniv L by A2,A1,ZFMISC_1:87;
then consider N being strict net of L such that
A3: N = Ns and
the carrier of N in the_universe_of the carrier of L by YELLOW_6:def 11;
A4: N in NetUniv L by A2,A1,A3,ZFMISC_1:87;
N is subnet of N by YELLOW_6:14;
then x = lim_inf N by A1,A3,A4,Def3;
then x is_S-limit_of N;
hence thesis by A3,A4,WAYBEL11:def 8;
end;
theorem Th23:
for X,Y being set holds X c= Y implies X in the_universe_of Y
proof
let X,Y be set;
A1: Y c= the_transitive-closure_of Y by CLASSES1:52;
Tarski-Class the_transitive-closure_of Y is_Tarski-Class_of
the_transitive-closure_of Y by CLASSES1:def 4;
then
A2: the_transitive-closure_of Y in Tarski-Class the_transitive-closure_of Y
by CLASSES1:def 3;
assume X c= Y;
then X c= the_transitive-closure_of Y by A1;
hence thesis by A2,CLASSES1:def 1;
end;
theorem Th24:
for L being non empty transitive reflexive RelStr, D being
directed non empty Subset of L holds Net-Str D in NetUniv L
proof
let L be non empty transitive reflexive RelStr;
let D be directed non empty Subset of L;
D in the_universe_of the carrier of L & the carrier of Net-Str D = D by Th23,
WAYBEL21:32;
hence thesis by YELLOW_6:def 11;
end;
theorem Th25:
for L being complete LATTICE, D being directed non empty Subset
of L holds for M being subnet of Net-Str D holds lim_inf M = sup D
proof
let L be complete LATTICE;
let D be directed non empty Subset of L;
for M being subnet of Net-Str D holds sup D >= inf M
proof
let M be subnet of Net-Str D;
set i = the Element of M;
set f=the mapping of M;
consider g being Function of M, Net-Str D such that
A1: the mapping of M = (the mapping of Net-Str D)*g and
for m being Element of Net-Str D ex n being Element of M st for p
being Element of M st n <= p holds m <= g.p by YELLOW_6:def 9;
A2: dom f = the carrier of M by FUNCT_2:def 1;
then f.i in rng f by FUNCT_1:def 3;
then
A3: "/\"(rng f,L) <= f.i by YELLOW_0:17,YELLOW_4:2;
g.i in the carrier of Net-Str D;
then
A4: g.i in D by WAYBEL21:32;
then g.i = (id D).(g.i) by FUNCT_1:18
.= (the mapping of Net-Str D).(g.i) by WAYBEL21:32
.= f.i by A1,A2,FUNCT_1:12;
then f.i <= sup D by A4,YELLOW_2:22;
then sup D >= "/\"(rng f,L) by A3,YELLOW_0:def 2;
then sup D >= Inf the mapping of M by YELLOW_2:def 6;
hence thesis by WAYBEL_9:def 2;
end;
then lim_inf Net-Str D =sup D & for p being greater_or_equal_to_id Function
of Net-Str(D),Net-Str(D) holds sup D >= inf (Net-Str(D)*p) by WAYBEL17:10;
hence thesis by Th14;
end;
theorem Th26:
for L being non empty complete LATTICE, D being directed non
empty Subset of L holds [Net-Str D,sup D] in lim_inf-Convergence L
proof
let L be non empty complete LATTICE;
let D be directed non empty Subset of L;
Net-Str D in NetUniv L & for M being subnet of Net-Str D holds lim_inf M
= sup D by Th24,Th25;
hence thesis by Def3;
end;
theorem Th27:
for L being complete LATTICE, U1 being Subset of L holds U1 in
xi(L) implies U1 is property(S)
proof
let L be complete LATTICE;
let U1 be Subset of L;
assume U1 in xi(L);
then
U1 in { V where V is Subset of L: for p being Element of L st p in V 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;
then
A1: ex V being Subset of L st U1=V & for p being Element of L st p in V for N
being net of L st [N,p] in lim_inf-Convergence L holds N is_eventually_in V;
let D be non empty directed Subset of L;
assume
A2: sup D in U1;
[Net-Str D,sup D] in lim_inf-Convergence L by Th26;
then (Net-Str D) is_eventually_in U1 by A1,A2;
then consider y being Element of (Net-Str D) such that
A3: for x being Element of (Net-Str D) st y <= x holds (Net-Str D).x in
U1 by WAYBEL_0:def 11;
A4: y in the carrier of Net-Str D;
then y in D by WAYBEL21:32;
then reconsider y1=y as Element of L;
reconsider y1 as Element of L;
take y1;
thus y1 in D by A4,WAYBEL21:32;
let x1 be Element of L;
assume that
A5: x1 in D and
A6: x1 >= y1;
A7: Net-Str D is full SubRelStr of L by WAYBEL21:32;
reconsider x=x1 as Element of Net-Str D by A5,WAYBEL21:32;
reconsider x as Element of Net-Str D;
(Net-Str D).x = (the mapping of Net-Str D).x by WAYBEL_0:def 8
.= (id D).x by WAYBEL21:32
.= x by A5,FUNCT_1:18;
hence thesis by A3,A6,A7,YELLOW_0:60;
end;
theorem Th28:
for L being non empty reflexive RelStr, A being Subset of L
holds A in sigma L implies A in xi L
proof
let L be non empty reflexive RelStr, A be Subset of L;
assume
A1: A in sigma L;
the topology of ConvergenceSpace Scott-Convergence L c= the topology of
ConvergenceSpace lim_inf-Convergence L by Th21,Th22;
hence thesis by A1;
end;
theorem Th29:
for L being complete LATTICE, A being Subset of L st A is upper
holds A in xi L implies A in sigma L
proof
let L be complete LATTICE, A be Subset of L;
set T = the Scott TopAugmentation of L;
A1: the RelStr of T = the RelStr of L by YELLOW_9:def 4;
then reconsider A9=A as Subset of T;
reconsider A9 as Subset of T;
assume A is upper;
then
A2: A9 is upper by A1,WAYBEL_0:25;
assume A in xi L;
then A9 is property(S) by A1,Th27,YELLOW12:19;
then A9 is open by A2,WAYBEL11:15;
then A9 in the topology of T by PRE_TOPC:def 2;
hence thesis by YELLOW_9:51;
end;
theorem ::3.3 Proposition (ii)
for L being complete LATTICE , A being Subset of L st A is lower holds
A` in xi L iff A is closed_under_directed_sups
proof
let L be complete LATTICE, A be Subset of L;
set T = the Scott TopAugmentation of L;
assume
A1: A is lower;
then reconsider A1=A as lower Subset of L;
A2: the RelStr of L = the RelStr of T by YELLOW_9:def 4;
then reconsider A9=A as Subset of T;
reconsider A9 as Subset of T;
A3: A1` is upper;
thus A` in xi L implies A is closed_under_directed_sups
proof
assume A` in xi L;
then A9` in sigma L by A3,A2,Th29;
then A9` in the topology of T by YELLOW_9:51;
then A9` is open by PRE_TOPC:def 2;
then A9 is closed by TOPS_1:3;
then A9 is directly_closed by WAYBEL11:7;
hence thesis by A2,YELLOW12:20;
end;
assume A is closed_under_directed_sups;
then
A4: A9 is directly_closed by A2,YELLOW12:20;
A9 is lower by A1,A2,WAYBEL_0:25;
then A9 is closed by A4,WAYBEL11:7;
then A9` is open by TOPS_1:3;
then A9` in the topology of T by PRE_TOPC:def 2;
then A` in sigma L by A2,YELLOW_9:51;
hence thesis by Th28;
end;