:: Lim-inf Convergence
:: by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: WAYBEL28:1
for L being complete LATTICE
for N being net of L holds inf N <= lim_inf N
proofend;

theorem :: WAYBEL28:2
for L being complete LATTICE
for N being net of L
for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds
( x = lim_inf N &amp; ( for M being subnet of N holds x >= inf M ) )
proofend;

theorem Th3: :: WAYBEL28:3
for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L &amp; ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) holds
( x = lim_inf N &amp; ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) )
proofend;

definition
let N be non empty RelStr ;
let f be Function of N,N;
attrf is greater_or_equal_to_id  means :Def1: :: WAYBEL28:def 1
 for j being Element of N holds j <= f . j;
end;

:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def_1_:_
 for N being non empty RelStr
for f being Function of N,N holds
( f is greater_or_equal_to_id iff for j being Element of N holds j <= f . j );

theorem Th4: :: WAYBEL28:4
for N being non empty reflexive RelStr holds id N is greater_or_equal_to_id
proofend;

theorem Th5: :: WAYBEL28:5
for N being non empty directed RelStr
for x, y being Element of N ex z being Element of N st
( x <= z &amp; y <= z )
proofend;

registration
let N be non empty directed RelStr ;
cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:];
existence
 ex b1 being Function of N,N st b1 is greater_or_equal_to_id
proofend;
end;

registration
let N be non empty reflexive RelStr ;
cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:];
existence
 ex b1 being Function of N,N st b1 is greater_or_equal_to_id
proofend;
end;

definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let f be Function of N,N;
funcN * f ->  non empty strict NetStr over L means :Def2: :: WAYBEL28:def 2
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; the mapping of it = the mapping of N * f );
existence
 ex b1 being non empty strict NetStr over L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; the mapping of b1 = the mapping of N * f )
proofend;
uniqueness
 for b1, b2 being non empty strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; the mapping of b1 = the mapping of N * f &amp; RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; the mapping of b2 = the mapping of N * f holds
b1 = b2 ;
end;

:: deftheorem Def2 defines * WAYBEL28:def_2_:_
 for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N
for b4 being non empty strict NetStr over L holds
( b4 = N * f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) &amp; the mapping of b4 = the mapping of N * f ) );

theorem Th6: :: WAYBEL28:6
for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N holds the carrier of (N * f) = the carrier of N
proofend;

theorem Th7: :: WAYBEL28:7
for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
proofend;

theorem Th8: :: WAYBEL28:8
for L being non empty 1-sorted
for N being non empty transitive directed RelStr
for 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
proofend;

registration
let L be non empty 1-sorted ;
let N be non empty transitive directed RelStr ;
let f be Function of the carrier of N, the carrier of L;
cluster NetStr(# the carrier of N, the InternalRel of N,f #) ->  non empty transitive directed ;
correctness
coherence
( NetStr(# the carrier of N, the InternalRel of N,f #) is transitive &amp; NetStr(# the carrier of N, the InternalRel of N,f #) is directed &amp; not NetStr(# the carrier of N, the InternalRel of N,f #) is empty );
by Th8;
end;

theorem Th9: :: WAYBEL28:9
for L being non empty 1-sorted
for N being net of L
for p being Function of N,N holds N * p is net of L
proofend;

registration
let L be non empty 1-sorted ;
let N be net of L;
let p be Function of N,N;
clusterN * p ->  non empty transitive strict directed ;
correctness
coherence
( N * p is transitive &amp; N * p is directed );
by Th9;
end;

theorem Th10: :: WAYBEL28:10
for L being non empty 1-sorted
for N being net of L
for p being Function of N,N st N in NetUniv L holds
N * p in NetUniv L
proofend;

theorem :: WAYBEL28:11
for L being non empty 1-sorted
for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds
M is subnet of N
proofend;

theorem Th12: :: WAYBEL28:12
for L being non empty 1-sorted
for N being net of L
for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N
proofend;

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;
:: original:*
redefine funcN * p ->  strict subnet of N;
correctness
coherence
N * p is strict subnet of N;
by Th12;
end;

theorem :: WAYBEL28:13
for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L &amp; x = lim_inf N &amp; ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) holds
( x = lim_inf N &amp; ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) ) by Th10;

theorem Th14: :: WAYBEL28:14
for L being complete LATTICE
for N being net of L
for x being Element of L st x = lim_inf N &amp; ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
proofend;

definition
let L be non empty RelStr ;
func lim_inf-Convergence L ->  Convergence-Class of L means :Def3: :: WAYBEL28:def 3
 for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in it iff for M being subnet of N holds x = lim_inf M );
existence
 ex b1 being Convergence-Class of L st
for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b1 iff for M being subnet of N holds x = lim_inf M )
proofend;
uniqueness
 for b1, b2 being Convergence-Class of L st ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b1 iff for M being subnet of N holds x = lim_inf M ) ) &amp; ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b2 iff for M being subnet of N holds x = lim_inf M ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines lim_inf-Convergence WAYBEL28:def_3_:_
 for L being non empty RelStr
for b2 being Convergence-Class of L holds
( b2 = lim_inf-Convergence L iff for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b2 iff for M being subnet of N holds x = lim_inf M ) );

theorem :: WAYBEL28:15
for L being complete LATTICE
for N being net of L
for 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 )
proofend;

theorem Th16: :: WAYBEL28:16
for L being non empty RelStr
for N being constant net of L
for M being subnet of N holds
( M is constant &amp; the_value_of N = the_value_of M )
proofend;

definition
let L be non empty RelStr ;
func xi L ->  Subset-Family of L equals :: WAYBEL28:def 4
 the topology of (ConvergenceSpace (lim_inf-Convergence L));
correctness
coherence
the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Subset-Family of L;
by YELLOW_6:def_24;
end;

:: deftheorem  defines xi WAYBEL28:def_4_:_
 for L being non empty RelStr holds xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L));

theorem :: WAYBEL28:17
for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS)
proofend;

theorem :: WAYBEL28:18
for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS)
proofend;

theorem :: WAYBEL28:19
for L being continuous complete LATTICE holds lim_inf-Convergence L is (DIVERGENCE)
proofend;

theorem :: WAYBEL28:20
for L being non empty RelStr
for N, x being set st [N,x] in lim_inf-Convergence L holds
N in NetUniv L
proofend;

theorem Th21: :: WAYBEL28:21
for L being non empty 1-sorted
for C1, C2 being Convergence-Class of L st C1 c= C2 holds
the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)
proofend;

theorem Th22: :: WAYBEL28:22
for L being non empty reflexive RelStr holds lim_inf-Convergence L c= Scott-Convergence L
proofend;

theorem Th23: :: WAYBEL28:23
for X, Y being set st X c= Y holds
X in the_universe_of Y
proofend;

theorem Th24: :: WAYBEL28:24
for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of L holds Net-Str D in NetUniv L
proofend;

theorem Th25: :: WAYBEL28:25
for L being complete LATTICE
for D being non empty directed Subset of L
for M being subnet of Net-Str D holds lim_inf M = sup D
proofend;

theorem Th26: :: WAYBEL28:26
for L being non empty complete LATTICE
for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L
proofend;

theorem Th27: :: WAYBEL28:27
for L being complete LATTICE
for U1 being Subset of L st U1 in xi L holds
U1 is property(S)
proofend;

theorem Th28: :: WAYBEL28:28
for L being non empty reflexive RelStr
for A being Subset of L st A in sigma L holds
A in xi L
proofend;

theorem Th29: :: WAYBEL28:29
for L being complete LATTICE
for A being Subset of L st A is upper &amp; A in xi L holds
A in sigma L
proofend;

theorem :: WAYBEL28:30
for L being complete LATTICE
for A being Subset of L st A is lower holds
( A ` in xi L iff A is closed_under_directed_sups )
proofend;