:: Lim-inf Convergence
:: by Bart{\l}omiej Skorulski
::
:: Received January 6, 2000
:: Copyright (c) 2000-2011 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
proof end;

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 & ( for M being subnet of N holds x >= inf M ) )
proof end;

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 & ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) )
proof 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: :: 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
proof end;

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 & y <= z )
proof end;

theorem Th6: :: WAYBEL28:6
for N being non empty directed RelStr ex p being Function of N,N st p is greater_or_equal_to_id
proof end;

registration
let N be non empty directed RelStr ;
cluster non empty Relation-like Function-like V31( the carrier of N) V32( the carrier of N, the carrier of N) greater_or_equal_to_id 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 by Th6;
end;

registration
let N be non empty reflexive RelStr ;
cluster non empty Relation-like Function-like V31( the carrier of N) V32( the carrier of N, the carrier of N) greater_or_equal_to_id 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
proof end;
end;

definition
let L be non empty 1-sorted ;
let N be non empty NetStr of L;
let f be Function of N,N;
func N * f -> non empty strict NetStr of L means :Def2: :: WAYBEL28:def 2
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = the mapping of N * f );
existence
ex b1 being non empty strict NetStr of L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = the mapping of N * f )
proof end;
uniqueness
for b1, b2 being non empty strict NetStr of L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = the mapping of N * f & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & 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 of L
for f being Function of N,N
for b4 being non empty strict NetStr of L holds
( b4 = N * f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b4 = the mapping of N * f ) );

theorem Th7: :: WAYBEL28:7
for L being non empty 1-sorted
for N being non empty NetStr of L
for f being Function of N,N holds the carrier of (N * f) = the carrier of N
proof end;

theorem Th8: :: WAYBEL28:8
for L being non empty 1-sorted
for N being non empty NetStr of 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) #)
proof end;

theorem Th9: :: WAYBEL28:9
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
proof end;

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 & NetStr(# the carrier of N, the InternalRel of N,f #) is directed & not NetStr(# the carrier of N, the InternalRel of N,f #) is empty );
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 holds N * p is net of L
proof end;

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

theorem Th11: :: WAYBEL28:11
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
proof end;

theorem :: WAYBEL28:12
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
proof end;

theorem Th13: :: WAYBEL28:13
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
proof 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;
:: original: *
redefine func N * p -> strict subnet of N;
correctness
coherence
N * p is strict subnet of N;
by Th13;
end;

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

theorem Th15: :: WAYBEL28:15
for L being complete LATTICE
for N being net of L
for x being Element of L st x = lim_inf N & ( 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
proof end;

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 )
proof end;
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 ) ) & ( 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
proof end;
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:16
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 )
proof end;

theorem Th17: :: WAYBEL28:17
for L being non empty RelStr
for N being constant net of L
for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )
proof end;

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 27;
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:18
for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS)
proof end;

theorem :: WAYBEL28:19
for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS)
proof end;

theorem :: WAYBEL28:20
for L being continuous complete LATTICE holds lim_inf-Convergence L is (DIVERGENCE)
proof end;

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

theorem Th22: :: WAYBEL28:22
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)
proof end;

theorem Th23: :: WAYBEL28:23
for L being non empty reflexive RelStr holds lim_inf-Convergence L c= Scott-Convergence L
proof end;

theorem Th24: :: WAYBEL28:24
for X, Y being set st X c= Y holds
X in the_universe_of Y
proof end;

theorem Th25: :: WAYBEL28:25
for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of L holds Net-Str D in NetUniv L
proof end;

theorem Th26: :: WAYBEL28:26
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
proof end;

theorem Th27: :: WAYBEL28:27
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
proof end;

theorem Th28: :: WAYBEL28:28
for L being complete LATTICE
for U1 being Subset of L st U1 in xi L holds
U1 is property(S)
proof end;

theorem Th29: :: WAYBEL28:29
for L being non empty reflexive RelStr
for A being Subset of L st A in sigma L holds
A in xi L
proof end;

theorem Th30: :: WAYBEL28:30
for L being complete LATTICE
for A being Subset of L st A is upper & A in xi L holds
A in sigma L
proof end;

theorem :: WAYBEL28:31
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 )
proof end;