:: On the characterizations of compactness :: by Grzegorz Bancerek , Noboru Endou and Yuji Sakai :: :: Received July 29, 2001 :: Copyright (c) 2001-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, CARD_FIL, YELLOW_1, LATTICES, PRE_TOPC, CONNSP_2, STRUCT_0, TARSKI, ZFMISC_1, WAYBEL_0, XXREAL_0, TOPS_1, WAYBEL_7, RCOMP_1, RELAT_1, RELAT_2, FUNCT_1, FINSET_1, SETFAM_1, LATTICE3, ORDERS_2, WELLORD2, ORDINAL1, MCART_1, YELLOW_6, SEQ_2, METRIC_1, CANTOR_1, ARYTM_0, ARYTM_3, CLASSES1, INT_2, YELLOW_0, CAT_1, BHSP_3, YELLOW19; notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, MCART_1, SETFAM_1, FINSET_1, FUNCT_1, RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, CLASSES1, ORDERS_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, CANTOR_1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_7, YELLOW_6, WAYBEL_9, YELLOW_7, WAYBEL32; constructors CLASSES1, TOLER_1, TOPS_1, TOPS_2, CONNSP_2, CANTOR_1, WAYBEL_1, WAYBEL_7, WAYBEL32, COMPTS_1, RELSET_1, XTUPLE_0, XFAMILY; registrations SUBSET_1, RELAT_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_6, WAYBEL_7, WAYBEL_9, WAYBEL32, RELSET_1, XTUPLE_0; requirements BOOLE, SUBSET; begin reserve x,y,X for set; theorem :: YELLOW19:1 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 the set of all A where A is a_neighborhood of x; end; theorem :: YELLOW19:2 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; registration let T be non empty TopSpace; let x be Point of T; cluster NeighborhoodSystem x -> non empty proper upper filtered; end; theorem :: YELLOW19:3 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:4 for T being non empty TopSpace, x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x, T; theorem :: YELLOW19:5 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:6 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; registration let S be non empty 1-sorted; let N be reflexive non empty NetStr over S; cluster -> non empty for Subset of S,N; end; theorem :: YELLOW19:7 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:8 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:9 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:10 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; registration let T be non empty 1-sorted; let N be non empty NetStr over T; cluster a_filter N -> non empty upper; end; registration let T be non empty 1-sorted; let N be net of T; cluster a_filter N -> proper filtered; end; theorem :: YELLOW19:11 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:12 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; registration 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; registration 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:13 for T being non empty 1-sorted for F being Filter of BoolePoset [#]T holds F \ {{}} = a_filter a_net F; theorem :: YELLOW19:14 for T being non empty 1-sorted for F being proper Filter of BoolePoset [#]T holds F = a_filter a_net F; theorem :: YELLOW19:15 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:16 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:17 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; theorem :: YELLOW19:18 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:19 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:20 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:21 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:22 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:23 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:24 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:25 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:26 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:27 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:28 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:29 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:30 for T being non empty TopSpace for F being Subset-Family of T st F is closed holds FinMeetCl F is closed; theorem :: YELLOW19:31 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:32 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:33 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:34 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; registration let L be non empty 1-sorted; let N be transitive NetStr over L; cluster -> transitive for full SubNetStr of N; end; registration let L be non empty 1-sorted; let N be non empty directed NetStr over L; cluster strict non empty directed full for SubNetStr of N; end; theorem :: YELLOW19:35 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; registration let S be non empty 1-sorted; let F be ultra Filter of BoolePoset [#]S; cluster a_net F -> Cauchy; end; theorem :: YELLOW19:36 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;