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;