Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Lim-Inf Convergence

**by****Bartlomiej Skorulski**- Received January 6, 2000
- MML identifier: WAYBEL28

- [ Mizar article, MML identifier index ]

environ vocabulary BHSP_3, WAYBEL_0, ORDINAL2, YELLOW_0, FUNCT_1, RELAT_1, LATTICES, YELLOW_2, LATTICE3, YELLOW_6, ORDERS_1, PRE_TOPC, RELAT_2, QUANTAL1, SUBSET_1, SEQM_3, SETFAM_1, WAYBEL11, CLASSES1, CAT_1, PROB_1, YELLOW_9, BOOLE, WAYBEL28; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, CLASSES1, SEQM_3, GRCAT_1, PRE_TOPC, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, WAYBEL_3, YELLOW_6, YELLOW_9, WAYBEL_9, WAYBEL11, WAYBEL17; constructors SEQM_3, GRCAT_1, TOPS_2, CLASSES1, YELLOW_2, WAYBEL_3, YELLOW_9, WAYBEL17, MEMBERED, PARTFUN1; clusters STRUCT_0, SUBSET_1, RELSET_1, LATTICE3, WAYBEL_0, WAYBEL_3, YELLOW_6, YELLOW_9, WAYBEL11, WAYBEL17, CLASSES2, MEMBERED, ZFMISC_1, PARTFUN1; requirements SUBSET, BOOLE; begin theorem :: WAYBEL28:1 for L being complete LATTICE, N being net of L holds inf N <= lim_inf N; theorem :: WAYBEL28:2 ::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); theorem :: WAYBEL28:3 ::3.1 Proposition (1b)=>(2b) 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); definition let N be non empty RelStr; let f be map of N,N; attr f is greater_or_equal_to_id means :: WAYBEL28:def 1 for j being Element of N holds j <= f.j; end; theorem :: WAYBEL28:4 for N being reflexive non empty RelStr holds id N is greater_or_equal_to_id; theorem :: WAYBEL28:5 for N being directed non empty RelStr, x,y being Element of N ex z being Element of N st x <= z & y <= z; theorem :: WAYBEL28:6 for N being directed non empty RelStr holds ex p being map of N,N st p is greater_or_equal_to_id; definition let N be directed non empty RelStr; cluster greater_or_equal_to_id map of N,N; end; definition let N be reflexive non empty RelStr; cluster greater_or_equal_to_id map of N,N; end; definition let L be non empty 1-sorted; let N be non empty NetStr over L; let f be map of N,N; func N * f -> strict non empty NetStr over L means :: WAYBEL28:def 2 the RelStr of it = the RelStr of N & the mapping of it = (the mapping of N) * f; end; theorem :: WAYBEL28:7 for L being non empty 1-sorted, N being non empty NetStr over L, f being map of N, N holds the carrier of N * f = the carrier of N; theorem :: WAYBEL28:8 for L being non empty 1-sorted, N being non empty NetStr over L, f being map of N,N holds N * f = NetStr(#the carrier of N,the InternalRel of N,(the mapping of N)*f#); theorem :: WAYBEL28:9 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; definition 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; end; theorem :: WAYBEL28:10 for L being non empty 1-sorted, N being net of L, p being map of N,N holds N * p is net of L; definition let L be non empty 1-sorted, N be net of L; let p be map of N,N; cluster N * p -> transitive directed; end; theorem :: WAYBEL28:11 for L being non empty 1-sorted, N being net of L, p being map of N,N st N in NetUniv L holds N * p in NetUniv L; theorem :: WAYBEL28:12 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; definition let L be non empty 1-sorted, N be net of L; cluster strict subnet of N; end; theorem :: WAYBEL28:13 for L being non empty 1-sorted, N being net of L, p being greater_or_equal_to_id map of N,N holds N * p is subnet of N; definition ::3.1 Proposition (2)=>(3) let L be non empty 1-sorted; let N be net of L; let p be greater_or_equal_to_id map of N,N; redefine func N * p -> strict subnet of N; end; theorem :: WAYBEL28:14 ::3.1 Proposition (2b)=>(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 map of N,N holds x >= inf (N * p); theorem :: WAYBEL28:15 ::3.1 Proposition (3)=>(1) 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 map of N,N holds x >= inf (N * p) ) implies for M being subnet of N holds x = lim_inf M; definition let L be non empty RelStr; func lim_inf-Convergence L -> Convergence-Class of L means :: WAYBEL28:def 3 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; end; theorem :: WAYBEL28:16 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; theorem :: WAYBEL28:17 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; 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; end; theorem :: WAYBEL28:18 for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS); theorem :: WAYBEL28:19 for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS); theorem :: WAYBEL28:20 for L being continuous complete LATTICE holds lim_inf-Convergence L is (DIVERGENCE); theorem :: WAYBEL28:21 for L being non empty RelStr, N,x being set holds [N,x] in lim_inf-Convergence L implies N in NetUniv L; theorem :: WAYBEL28:22 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; theorem :: WAYBEL28:23 for L being non empty reflexive RelStr holds lim_inf-Convergence L c= Scott-Convergence L; theorem :: WAYBEL28:24 for X,Y being set holds X c= Y implies X in the_universe_of Y; theorem :: WAYBEL28:25 for L being non empty transitive reflexive RelStr, D being directed non empty Subset of L holds Net-Str D in NetUniv L; theorem :: WAYBEL28:26 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; theorem :: WAYBEL28:27 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; theorem :: WAYBEL28:28 for L being complete LATTICE, U1 being Subset of L holds U1 in xi(L) implies U1 is property(S); theorem :: WAYBEL28:29 for L being non empty reflexive RelStr, A being Subset of L holds A in sigma L implies A in xi L; theorem :: WAYBEL28:30 for L being complete LATTICE, A being Subset of L st A is upper holds A in xi L implies A in sigma L; theorem :: WAYBEL28:31 ::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;

Back to top