Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### Compactness of Lim-inf Topology

**by****Grzegorz Bancerek, and****Noboru Endou**- Received July 29, 2001
- MML identifier: WAYBEL33

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, FILTER_0, YELLOW_1, ORDINAL2, LATTICES, BHSP_3, WAYBEL_0, YELLOW_0, WAYBEL_9, PRE_TOPC, WAYBEL28, YELLOW_6, SETFAM_1, TARSKI, BOOLE, REALSET1, FUNCT_1, SUBSET_1, QUANTAL1, RELAT_2, YELLOW_9, LATTICE3, RELAT_1, YELLOW_2, COLLSP, YELLOW19, MCART_1, CLASSES1, ZF_LANG, SUB_METR, FINSET_1, PROB_1, CANTOR_1, PRELAMB, DIRAF, WAYBEL19, WAYBEL11, WAYBEL_7, COMPTS_1, URYSOHN1, WAYBEL33, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, ORDERS_1, FINSET_1, RELAT_1, RELSET_1, REALSET1, FUNCT_1, FUNCT_2, SETFAM_1, STRUCT_0, PRE_TOPC, TEX_2, LATTICE3, YELLOW_0, CARD_FIL, CLASSES1, CLASSES2, CANTOR_1, WAYBEL_0, YELLOW_1, YELLOW_6, YELLOW_2, WAYBEL_3, WAYBEL_7, WAYBEL_9, WAYBEL11, COMPTS_1, URYSOHN1, YELLOW_9, WAYBEL19, WAYBEL28, YELLOW19; constructors WAYBEL_3, TOLER_1, WAYBEL_1, CANTOR_1, WAYBEL_7, TEX_2, REALSET1, URYSOHN1, YELLOW_9, WAYBEL19, WAYBEL17, CARD_FIL, CLASSES1, WAYBEL28, YELLOW19, GROUP_1, TDLAT_3, CLASSES2, MEMBERED, TOPS_2; clusters SUBSET_1, STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, TOPS_1, FUNCT_1, LATTICE3, WAYBEL_7, FINSET_1, YELLOW11, YELLOW13, PUA2MSS1, YELLOW_6, YELLOW_9, WAYBEL19, CLASSES2, WAYBEL28, WAYBEL29, YELLOW19, MEMBERED, RELAT_1, ZFMISC_1; requirements BOOLE, SUBSET; begin reserve x for set; 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); end; theorem :: WAYBEL33:1 for L1, L2 being complete LATTICE st the RelStr of L1 = the RelStr of L2 for X1 being non empty Subset of L1 for X2 being non empty Subset of L2 for F1 being Filter of BoolePoset X1, F2 being Filter of BoolePoset X2 st F1 = F2 holds lim_inf F1 = lim_inf F2; definition let L be non empty TopRelStr; attr L is lim-inf means :: WAYBEL33:def 2 the topology of L = xi L; end; definition cluster lim-inf -> TopSpace-like (non empty TopRelStr); end; definition cluster trivial -> lim-inf TopLattice; end; definition cluster lim-inf continuous complete TopLattice; end; theorem :: WAYBEL33:2 for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 for N1 being NetStr over L1 ex N2 being strict NetStr over L2 st the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2; theorem :: WAYBEL33:3 for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 for N1 being NetStr over L1 st N1 in NetUniv L1 ex N2 being strict net of L2 st N2 in NetUniv L2 & the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2; theorem :: WAYBEL33:4 for L1, L2 being /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 for N1 being net of L1, N2 being net of L2 st the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2 holds lim_inf N1 = lim_inf N2; theorem :: WAYBEL33:5 for L1, L2 being non empty 1-sorted st the carrier of L1 = the carrier of L2 for N1 being net of L1, N2 being net of L2 st the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2 for S1 being subnet of N1 ex S2 being strict subnet of N2 st the RelStr of S1 = the RelStr of S2 & the mapping of S1 = the mapping of S2; theorem :: WAYBEL33:6 for L1, L2 being /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 for N1 being NetStr over L1, a being set st [N1,a] in lim_inf-Convergence L1 ex N2 being strict net of L2 st [N2,a] in lim_inf-Convergence L2 & the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2; theorem :: 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 the RelStr of N1 = the RelStr of N2 & the mapping of N1 = the mapping of N2 for X being set st N1 is_eventually_in X holds N2 is_eventually_in X; theorem :: WAYBEL33:8 for L1, L2 being /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 holds ConvergenceSpace lim_inf-Convergence L1 = ConvergenceSpace lim_inf-Convergence L2; theorem :: WAYBEL33:9 for L1, L2 being /\-complete up-complete Semilattice st the RelStr of L1 = the RelStr of L2 holds xi L1 = xi L2; definition let R be /\-complete (non empty reflexive RelStr); cluster -> /\-complete TopAugmentation of R; end; definition let R be Semilattice; cluster -> with_infima TopAugmentation of R; end; definition let L be /\-complete up-complete Semilattice; cluster strict lim-inf TopAugmentation of L; end; theorem :: WAYBEL33:10 for L being /\-complete up-complete Semilattice for X being lim-inf TopAugmentation of L holds xi L = the topology of X; definition let L be /\-complete up-complete Semilattice; func Xi L -> strict TopAugmentation of L means :: WAYBEL33:def 3 it is lim-inf; end; definition let L be /\-complete up-complete Semilattice; cluster Xi L -> lim-inf; end; theorem :: WAYBEL33:11 for L being complete LATTICE, N being net of L holds lim_inf N = "\/"({inf (N|i) where i is Element of N: not contradiction}, L); theorem :: WAYBEL33:12 for L being complete LATTICE, F being proper Filter of BoolePoset [#]L, f being Subset of L st f in F for i being Element of a_net F st i`2 = f holds inf f = inf ((a_net F)|i); theorem :: WAYBEL33:13 for L being complete LATTICE, F being proper Filter of BoolePoset [#]L holds lim_inf F = lim_inf a_net F; theorem :: WAYBEL33:14 for L being complete LATTICE, F being proper Filter of BoolePoset [#]L holds a_net F in NetUniv L; theorem :: WAYBEL33:15 for L being complete LATTICE, F being ultra Filter of BoolePoset [#]L for p being greater_or_equal_to_id map of a_net F, a_net F holds lim_inf F >= inf ((a_net F) * p); theorem :: WAYBEL33:16 for L being complete LATTICE, F being ultra Filter of BoolePoset [#]L holds for M being subnet of a_net F holds lim_inf F = lim_inf M; theorem :: 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 ex N' being strict subnet of N st rng the mapping of N' c= A & N' is SubNetStr of N; theorem :: WAYBEL33:18 :: III. 3.4. LEMMA, p. 168(?) for L being complete lim-inf TopLattice, 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; theorem :: WAYBEL33:19 for L being non empty reflexive RelStr holds sigma L c= xi L; theorem :: WAYBEL33:20 for T1, T2 being non empty TopSpace, 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; theorem :: WAYBEL33:21 for L being complete LATTICE holds omega L c= xi L; theorem :: WAYBEL33:22 for T1,T2 being TopSpace, T being non empty TopSpace st T is TopExtension of T1 & T is TopExtension of T2 for R being Refinement of T1,T2 holds T is TopExtension of R; theorem :: WAYBEL33:23 for T1 being TopSpace, 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); theorem :: WAYBEL33:24 :: III. 3.5. LEMMA, p. 168(?) for L being complete LATTICE holds lambda L c= xi L; theorem :: WAYBEL33:25 :: 3.6. PROPOSITION (B), p. 169(?) for L being complete LATTICE for T being lim-inf TopAugmentation of L for S being Lawson correct TopAugmentation of L holds T is TopExtension of S; theorem :: 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; theorem :: WAYBEL33:27 :: 3.6. PROPOSITION (A), p. 169(?) for L being complete lim-inf TopLattice holds L is compact being_T1;

Back to top