:: Compactness in Metric Spaces
::  by Kazuhisa Nakasho , Keiko Narita and Yasunari Shidama
:: 
:: Received June 30, 2016
:: Copyright (c) 2016-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 NUMBERS, SUBSET_1, FUNCT_1, NAT_1, RELAT_1, XBOOLE_0, XXREAL_2,
      XXREAL_0, CARD_1, REAL_1, ARYTM_3, ARYTM_1, SEQ_1, SEQ_2, ORDINAL2,
      COMPLEX1, STRUCT_0, TARSKI, TOPMETR, FINSET_1, PRE_TOPC, TOPMETR4,
      MEMBERED, RCOMP_1, BHSP_3, COMPL_SP, NORMSP_1, NORMSP_2, VALUED_0,
      SETFAM_1, METRIC_1, TBSP_1, PCOMPS_1, REWRITE1, ZFMISC_1, TOPGEN_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1,
      PARTFUN1, FUNCT_2, FINSET_1, NUMBERS, XCMPLX_0, MEMBERED, XXREAL_0,
      XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, SEQ_1, SEQ_2, RCOMP_1,
      STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, METRIC_1, NORMSP_1, NFCONT_1,
      NORMSP_2, PCOMPS_1, TBSP_1, TOPMETR, TOPGEN_1, COMPL_SP;
 constructors SEQ_4, NAT_D, INTEGRA2, SEQ_2, TOPGEN_1, TOPMETR, COMSEQ_2,
      C0SP2, TOPS_2, COMPL_SP, TBSP_1, PCOMPS_1, NFCONT_1, NORMSP_2;
 registrations XREAL_0, FUNCT_2, NAT_1, MEMBERED, XXREAL_0, ORDINAL1, VALUED_0,
      RELSET_1, PSCOMP_1, TOPMETR, COMPTS_1, CARD_1, INT_1, PRE_TOPC, PCOMPS_1,
      STRUCT_0, XXREAL_2, FINSET_1, ZFMISC_1, XCMPLX_0, METRIC_1, TBSP_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. Topological properties of metric spaces

theorem :: TOPMETR4:1
  for M be non empty set,
      x be sequence of M st rng x is finite
  ex z be Element of M st x"{z} c= NAT & x"{z} is infinite;

theorem :: TOPMETR4:2
  for X be Subset of NAT st X is infinite
  ex N be increasing sequence of NAT st rng N c= X;

theorem :: TOPMETR4:3
  for M be non empty MetrSpace,
      V be Subset of TopSpaceMetr M st V is open holds
    ex F be Subset-Family of M
      st F = {Ball(x,r) where x is Element of M, r is Real:
              r > 0 & Ball(x,r) c= V}
       & V = union F;

theorem :: TOPMETR4:4
  for M be non empty MetrSpace,
      X be Subset of TopSpaceMetr M,
      p be Element of M holds
    (p in Cl(X) iff for r be Real st 0 < r holds X meets Ball(p,r));

theorem :: TOPMETR4:5
  for M be non empty MetrSpace,
      X be Subset of TopSpaceMetr M holds
    for x be object holds
        x in Cl X
      iff
        ex S be sequence of M
          st (for n be Nat holds S.n in X)
           & S is convergent & lim S = x;

theorem :: TOPMETR4:6
  for M be non empty MetrSpace,
      X be Subset of TopSpaceMetr M holds
      X is closed
    iff
      for S be sequence of M
        st (for n be Nat holds S.n in X)
         & S is convergent
      holds lim S in X;

theorem :: TOPMETR4:7
  for X, Y be non empty MetrSpace
  for f be Function of TopSpaceMetr X, TopSpaceMetr Y holds
      f is continuous
    iff
      for S be sequence of X, T be sequence of Y
        st S is convergent & T = f * S
      holds T is convergent & lim T = f.(lim S);

begin :: 2. Compactness in metric spaces

definition
  let M be non empty MetrSpace;
  let X be Subset of M;
  attr X is sequentially_compact means
:: TOPMETR4:def 1
  for S1 be sequence of M st rng S1 c= X
  ex S2 be sequence of M
    st (ex N be increasing sequence of NAT st S2 = S1 * N)
     & S2 is convergent & lim S2 in X;
end;

registration let M be non empty MetrSpace;
  cluster empty -> sequentially_compact for Subset of M;
end;

definition
  let M be non empty MetrSpace;
  attr M is sequentially_compact means
:: TOPMETR4:def 2
  [#]M is sequentially_compact;
end;

theorem :: TOPMETR4:8
  for M be non empty MetrSpace,
      X be Subset of M,
      Y be Subset of TopSpaceMetr M,
      x be Element of M,
      y be Element of TopSpaceMetr M
    st X=Y & x=y holds
      y is_an_accumulation_point_of Y
    iff
      for r be Real st 0 < r holds Ball(x,r) meets X \ {x};

theorem :: TOPMETR4:9
  for M be non empty MetrSpace
    st TopSpaceMetr M is countably_compact holds
      M is sequentially_compact;

theorem :: TOPMETR4:10
  for M be non empty MetrSpace st M is sequentially_compact holds
    TopSpaceMetr M is countably_compact;

theorem :: TOPMETR4:11
  for M be non empty MetrSpace holds
    TopSpaceMetr M is compact iff M is sequentially_compact;

theorem :: TOPMETR4:12
  for M be non empty MetrSpace holds
    M is totally_bounded complete iff M is sequentially_compact;

theorem :: TOPMETR4:13
  for M be non empty MetrSpace,
      S be non empty Subset of M holds
      S is sequentially_compact
    iff
      (M|S) is sequentially_compact;

theorem :: TOPMETR4:14
  for M be non empty MetrSpace,
      S be non empty Subset of M holds
      S is sequentially_compact
    iff
      (M|S) is compact;

theorem :: TOPMETR4:15
  for M be non empty MetrSpace,
      S be Subset of M,
      T be Subset of TopSpaceMetr M
    st T = S holds
    T is compact iff S is sequentially_compact;

theorem :: TOPMETR4:16
  for M be non empty MetrSpace,
      S be non empty Subset of M,
      T be non empty Subset of TopSpaceMetr M
    st T = S holds
     (TopSpaceMetr M) | T is countably_compact
     iff S is sequentially_compact;

theorem :: TOPMETR4:17
  for M be non empty MetrSpace,
      S be non empty Subset of M holds
    (M|S is totally_bounded complete)
    iff S is sequentially_compact;

begin :: 3. Compactness in norm spaces

theorem :: TOPMETR4:18
  for NrSp be RealNormSpace,
      S be Subset of NrSp,
      T be Subset of MetricSpaceNorm NrSp
    st S = T
  holds S is compact iff T is sequentially_compact;

theorem :: TOPMETR4:19
  for NrSp be RealNormSpace,
      S be Subset of NrSp,
      T be Subset of TopSpaceNorm NrSp
    st S = T
  holds S is compact iff T is compact;

begin :: 4. Topological properties of the real line

theorem :: TOPMETR4:20
  for S1 be sequence of RealSpace, seq be Real_Sequence,
      g be Real, g1 be Element of RealSpace st S1 = seq & g = g1 holds
      (for p be Real st 0 < p
       ex n be Nat st for m be Nat st n <= m holds |.seq.m - g.| < p)
    iff
      (for p be Real st 0 < p
       ex n be Nat st for m be Nat st n <= m holds dist(S1.m,g1) < p);

theorem :: TOPMETR4:21
  for S1 be sequence of RealSpace, seq be Real_Sequence,
      g be Real, g1 be Element of RealSpace st S1 = seq & g = g1
  holds
      (seq is convergent & lim seq = g)
    iff
      (S1 is convergent & lim S1 = g1);

theorem :: TOPMETR4:22
  for S1 be sequence of RealSpace, seq be Real_Sequence
    st S1 = seq & seq is convergent
  holds S1 is convergent & lim S1 = lim seq;

begin :: 5. Compactness in the real line

:: The equivalence of the notions of compactness in R^1 and REAL was shown
:: in JORDAN5A

theorem :: TOPMETR4:23
  for N be Subset of REAL, M be Subset of R^1 st N = M holds
    (for F be Subset-Family of REAL
       st F is Cover of N
        & (for P be Subset of REAL st P in F holds P is open)
     holds
       ex G be Subset-Family of REAL
         st G c= F & G is Cover of N & G is finite)
  iff
    (for F1 be Subset-Family of R^1 st F1 is Cover of M & F1 is open
     holds
       ex G1 be Subset-Family of R^1
         st G1 c= F1 & G1 is Cover of M & G1 is finite);

theorem :: TOPMETR4:24
  for N be Subset of REAL holds
    N is compact
  iff
    (for F be Subset-Family of REAL
       st F is Cover of N
        & (for P be Subset of REAL st P in F holds P is open) holds
       ex G be Subset-Family of REAL
         st G c= F & G is Cover of N & G is finite);