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;