:: 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);