:: Compactness of Lim-inf Topology
::  by Grzegorz Bancerek and Noboru Endou
::
:: 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, ORDERS_2, SUBSET_1, CARD_FIL, YELLOW_1, ORDINAL2,
      EQREL_1, REWRITE1, WAYBEL_0, TARSKI, STRUCT_0, ZFMISC_1, WAYBEL_9,
      PRE_TOPC, WAYBEL28, YELLOW_6, SETFAM_1, FUNCT_1, XXREAL_0, LATTICES,
      YELLOW_0, RELAT_1, RELAT_2, YELLOW_9, LATTICE3, YELLOW_2, YELLOW19,
      MCART_1, CLASSES2, CLASSES1, METRIC_1, INT_2, RCOMP_1, FINSET_1, PROB_1,
      CANTOR_1, RLVECT_3, ORDINAL1, PRELAMB, DIRAF, WAYBEL19, WAYBEL11,
      WAYBEL_7, WAYBEL33, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1,
      ORDERS_2, CARD_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, LATTICE3, YELLOW_0,
      CLASSES1, CLASSES2, CANTOR_1, WAYBEL_0, YELLOW_1, YELLOW_6, YELLOW_2,
      WAYBEL_3, WAYBEL_7, WAYBEL_9, WAYBEL11, COMPTS_1, YELLOW_9, WAYBEL19,
      WAYBEL28, YELLOW19;
 constructors CLASSES1, TOLER_1, CLASSES2, REALSET2, CANTOR_1, WAYBEL_1,
      WAYBEL_3, WAYBEL_7, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL28, YELLOW19,
      COMPTS_1, RELSET_1, TOPS_2, WAYBEL_2, XTUPLE_0, XFAMILY;
 registrations SUBSET_1, RELAT_1, FINSET_1, CLASSES2, STRUCT_0, TOPS_1,
      LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_7,
      WAYBEL_9, YELLOW_9, WAYBEL19, YELLOW13, WAYBEL28, WAYBEL29, YELLOW19,
      CARD_1, TEX_1, RELSET_1, XTUPLE_0;
 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;

registration
  cluster lim-inf -> TopSpace-like for non empty TopRelStr;
end;

registration
  cluster trivial -> lim-inf for TopLattice;
end;

registration
  cluster lim-inf continuous complete for 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;

registration
  let R be /\-complete non empty reflexive RelStr;
  cluster -> /\-complete for TopAugmentation of R;
end;

registration
  let R be Semilattice;
  cluster -> with_infima for TopAugmentation of R;
end;

registration
  let L be /\-complete up-complete Semilattice;
  cluster strict lim-inf for 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;

registration
  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 =
  "\/"((the set of all inf (N|i) where i is Element of N), 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 Function 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 N9 being strict subnet of N st rng the mapping of N9
  c= A & N9 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;

::$N Compactness of Lim-inf Topology
theorem :: WAYBEL33:27 :: 3.6. PROPOSITION (A), p. 169(?)
  for L being complete lim-inf TopLattice holds L is compact T_1;