Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### On the Characterizations of Compactness

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

- [ Mizar article, MML identifier index ]

environ vocabulary YELLOW_1, ORDERS_1, WELLORD2, COLLSP, FILTER_0, LATTICES, BOOLE, PRE_TOPC, SUBSET_1, CONNSP_2, WAYBEL_0, TOPS_1, WAYBEL_7, RELAT_1, RELAT_2, FUNCT_1, FINSET_1, SETFAM_1, QUANTAL1, LATTICE3, ORDINAL2, MCART_1, YELLOW_6, SEQ_2, SUB_METR, CANTOR_1, COMPTS_1, OPPCAT_1, ARYTM_3, CLASSES1, YELLOW_0, CAT_1, BHSP_3, YELLOW19; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MCART_1, SETFAM_1, FINSET_1, FUNCT_1, RELAT_2, RELSET_1, FUNCT_2, CLASSES1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TEX_2, COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, YELLOW_6, WAYBEL_9, YELLOW_7, WAYBEL32; constructors TOLER_1, RELAT_2, WAYBEL_1, CLASSES1, TOPS_1, TOPS_2, CONNSP_2, CANTOR_1, WAYBEL_7, WAYBEL32, TEX_2, REALSET1, MEMBERED; clusters SUBSET_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, PUA2MSS1, RELSET_1, RLVECT_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, WAYBEL_9, YELLOW_6, WAYBEL32, MEMBERED, RELAT_1, ZFMISC_1; requirements BOOLE, SUBSET; begin reserve x,y,X for set; canceled; theorem :: YELLOW19:2 for X being non empty set for F being proper Filter of BoolePoset X for A being set st A in F holds A is not empty; definition let T be non empty TopSpace; let x be Point of T; func NeighborhoodSystem x -> Subset of BoolePoset [#]T equals :: YELLOW19:def 1 {A where A is a_neighborhood of x: not contradiction}; end; theorem :: YELLOW19:3 for T being non empty TopSpace, x being Point of T, A being set holds A in NeighborhoodSystem x iff A is a_neighborhood of x; definition let T be non empty TopSpace; let x be Point of T; cluster NeighborhoodSystem x -> non empty proper upper filtered; end; theorem :: YELLOW19:4 for T being non empty TopSpace, x being Point of T for F being upper Subset of BoolePoset [#]T holds x is_a_convergence_point_of F, T iff NeighborhoodSystem x c= F; theorem :: YELLOW19:5 for T being non empty TopSpace, x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x, T; theorem :: YELLOW19:6 for T being non empty TopSpace for A being Subset of T holds A is open iff for x being Point of T st x in A for F being Filter of BoolePoset [#]T st x is_a_convergence_point_of F, T holds A in F; definition let S be non empty 1-sorted; let N be non empty NetStr over S; mode Subset of S,N -> Subset of S means :: YELLOW19:def 2 ex i being Element of N st it = rng the mapping of N|i; end; theorem :: YELLOW19:7 for S being non empty 1-sorted for N being non empty NetStr over S for i being Element of N holds rng the mapping of N|i is Subset of S, N; definition let S be non empty 1-sorted; let N be reflexive non empty NetStr over S; cluster -> non empty Subset of S,N; end; theorem :: YELLOW19:8 for S being non empty 1-sorted, N being net of S for i being Element of N, x being set holds x in rng the mapping of N|i iff ex j being Element of N st i <= j & x = N.j; theorem :: YELLOW19:9 for S being non empty 1-sorted, N being net of S for A being Subset of S,N holds N is_eventually_in A; theorem :: YELLOW19:10 for S being non empty 1-sorted, N being net of S for F being finite non empty set st for A being Element of F holds A is Subset of S,N ex B being Subset of S,N st B c= meet F; definition let T be non empty 1-sorted; let N be non empty NetStr over T; func a_filter N -> Subset of BoolePoset [#]T equals :: YELLOW19:def 3 {A where A is Subset of T: N is_eventually_in A}; end; theorem :: YELLOW19:11 for T being non empty 1-sorted for N being non empty NetStr over T for A being set holds A in a_filter N iff N is_eventually_in A & A is Subset of T; definition let T be non empty 1-sorted; let N be non empty NetStr over T; cluster a_filter N -> non empty upper; end; definition let T be non empty 1-sorted; let N be net of T; cluster a_filter N -> proper filtered; end; theorem :: YELLOW19:12 for T being non empty TopSpace for N being net of T for x being Point of T holds x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N, T; theorem :: YELLOW19:13 for T being non empty TopSpace for N being net of T for x being Point of T holds x in Lim N iff x is_a_convergence_point_of a_filter N, T; definition let L be non empty 1-sorted; let O be non empty Subset of L; let F be Filter of BoolePoset O; func a_net F -> strict non empty NetStr over L means :: YELLOW19:def 4 the carrier of it = {[a, f] where a is Element of L, f is Element of F: a in f} & (for i,j being Element of it holds i <= j iff j`2 c= i`2) & for i being Element of it holds it.i = i`1; end; definition let L be non empty 1-sorted; let O be non empty Subset of L; let F be Filter of BoolePoset O; cluster a_net F -> reflexive transitive; end; definition let L be non empty 1-sorted; let O be non empty Subset of L; let F be proper Filter of BoolePoset O; cluster a_net F -> directed; end; theorem :: YELLOW19:14 for T being non empty 1-sorted for F being Filter of BoolePoset [#]T holds F \ {{}} = a_filter a_net F; theorem :: YELLOW19:15 for T being non empty 1-sorted for F being proper Filter of BoolePoset [#]T holds F = a_filter a_net F; theorem :: YELLOW19:16 for T being non empty 1-sorted for F being Filter of BoolePoset [#]T for A being non empty Subset of T holds A in F iff a_net F is_eventually_in A; theorem :: YELLOW19:17 for T being non empty TopSpace for F being proper Filter of BoolePoset [#]T for x being Point of T holds x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F, T; theorem :: YELLOW19:18 for T being non empty TopSpace for F being proper Filter of BoolePoset [#]T for x being Point of T holds x in Lim a_net F iff x is_a_convergence_point_of F, T; canceled; theorem :: YELLOW19:20 for T being non empty TopSpace, x being Point of T, A being Subset of T st x in Cl A for F being proper Filter of BoolePoset [#]T st F = NeighborhoodSystem x holds a_net F is_often_in A; theorem :: YELLOW19:21 for T being non empty 1-sorted, A being set for N being net of T st N is_eventually_in A for S being subnet of N holds S is_eventually_in A; theorem :: YELLOW19:22 for T being non empty TopSpace, F,G,x being set st F c= G & x is_a_convergence_point_of F, T holds x is_a_convergence_point_of G, T; theorem :: YELLOW19:23 for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex N being net of T st N is_eventually_in A & x is_a_cluster_point_of N; theorem :: YELLOW19:24 for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex N being convergent net of T st N is_eventually_in A & x in Lim N; theorem :: YELLOW19:25 for T being non empty TopSpace, A being Subset of T holds A is closed iff for N being net of T st N is_eventually_in A for x being Point of T st x is_a_cluster_point_of N holds x in A; theorem :: YELLOW19:26 for T being non empty TopSpace, A being Subset of T holds A is closed iff for N being convergent net of T st N is_eventually_in A for x being Point of T st x in Lim N holds x in A; theorem :: YELLOW19:27 for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex F being proper Filter of BoolePoset [#]T st A in F & x is_a_cluster_point_of F, T; theorem :: YELLOW19:28 for T being non empty TopSpace, A being Subset of T for x being Point of T holds x in Cl A iff ex F being ultra Filter of BoolePoset [#]T st A in F & x is_a_convergence_point_of F, T; theorem :: YELLOW19:29 for T being non empty TopSpace, A being Subset of T holds A is closed iff for F being proper Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_cluster_point_of F,T holds x in A; theorem :: YELLOW19:30 for T being non empty TopSpace, A being Subset of T holds A is closed iff for F being ultra Filter of BoolePoset [#]T st A in F for x being Point of T st x is_a_convergence_point_of F,T holds x in A; theorem :: YELLOW19:31 for T being non empty TopSpace, N being net of T for s being Point of T holds s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A; theorem :: YELLOW19:32 for T being non empty TopSpace for F being Subset-Family of T st F is closed holds FinMeetCl F is closed; theorem :: YELLOW19:33 for T being non empty TopSpace holds T is compact iff for F being ultra Filter of BoolePoset [#]T ex x being Point of T st x is_a_convergence_point_of F, T; theorem :: YELLOW19:34 for T being non empty TopSpace holds T is compact iff for F being proper Filter of BoolePoset [#]T ex x being Point of T st x is_a_cluster_point_of F, T; theorem :: YELLOW19:35 for T being non empty TopSpace holds T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N; theorem :: YELLOW19:36 for T being non empty TopSpace holds T is compact iff for N being net of T st N in NetUniv T ex x being Point of T st x is_a_cluster_point_of N; definition let L be non empty 1-sorted; let N be transitive NetStr over L; cluster -> transitive (full SubNetStr of N); end; definition let L be non empty 1-sorted; let N be non empty directed NetStr over L; cluster strict non empty directed full SubNetStr of N; end; theorem :: YELLOW19:37 for T being non empty TopSpace holds T is compact iff for N being net of T ex S being subnet of N st S is convergent; definition let S be non empty 1-sorted; let N be non empty NetStr over S; attr N is Cauchy means :: YELLOW19:def 5 for A being Subset of S holds N is_eventually_in A or N is_eventually_in A` ; end; definition let S be non empty 1-sorted; let F be ultra Filter of BoolePoset [#]S; cluster a_net F -> Cauchy; end; theorem :: YELLOW19:38 for T being non empty TopSpace holds T is compact iff for N being net of T st N is Cauchy holds N is convergent;

Back to top