:: Ascoli-Arzela's Theorem
:: by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
::
:: Received June 30, 2021
:: Copyright (c) 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 ASCOLI, STRUCT_0, NUMBERS, PRE_TOPC, ORDINAL2, PCOMPS_1,
NORMSP_0, SUBSET_1, RCOMP_1, RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, CARD_1,
ARYTM_3, ARYTM_1, REAL_1, FUNCT_2, ZFMISC_1, RSSPACE4, XXREAL_2,
XXREAL_0, NORMSP_1, NORMSP_2, REWRITE1, NAT_1, ORDINAL4, RSSPACE3, SEQ_2,
TMAP_1, ORDEQ_01, PARTFUN1, C0SP2, LOPBAN_1, METRIC_1, SETFAM_1,
FINSET_1, METRIC_6, SEQ_4, TBSP_1, TOPMETR4, BHSP_3, C0SP3, UPROOTS,
FINSEQ_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, CARD_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_2, SEQ_4, STRUCT_0, PCOMPS_1, TBSP_1,
RLVECT_1, NORMSP_0, NORMSP_1, NFCONT_1, PRE_TOPC, COMPTS_1, TOPS_2,
METRIC_1, TMAP_1, TOPMETR, RSSPACE3, LOPBAN_1, NORMSP_2, RSSPACE4,
NORMSP_3, TOPMETR4, C0SP3, METRIC_6, FINSEQ_1;
constructors RSSPACE3, COMPLEX1, PCOMPS_1, TBSP_1, NFCONT_1, TOPMETR, SEQ_4,
NORMSP_2, TMAP_1, TOPS_2, RSSPACE4, NORMSP_3, TOPMETR4, C0SP3, METRIC_6;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, XREAL_0, NUMBERS,
ORDINAL1, MEMBERED, VALUED_0, COMPTS_1, XXREAL_0, FUNCT_2, XXREAL_2,
TOPMETR, RELSET_1, WAYBEL_2, XCMPLX_0, TOPS_1, RSSPACE4, NORMSP_3, C0SP3,
TBSP_1, PCOMPS_1, CARD_1, NAT_1, FINSEQ_1, FINSET_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Equicontinuousness and Equiboundedness of Continuous Functions
reserve S, T for RealNormSpace;
reserve F for Subset of Funcs(the carrier of S,the carrier of T);
definition
let X be non empty MetrSpace, Y be Subset of X;
func Cl Y -> Subset of X means
:: ASCOLI:def 1
ex Z be Subset of TopSpaceMetr X st Z = Y & it = Cl Z;
end;
theorem :: ASCOLI:1
for X be RealNormSpace,
Y be Subset of X,
Z be Subset of MetricSpaceNorm X
st Y = Z
holds Cl(Y) = Cl(Z);
registration
let X be non empty MetrSpace;
let H be non empty Subset of X;
cluster Cl(H) -> non empty;
end;
theorem :: ASCOLI:2
for S be TopSpace,
F be FinSequence of bool the carrier of S
st for i be Nat st i in Seg len F
holds F/.i is compact
holds
union rng F is compact;
theorem :: ASCOLI:3
for S be non empty TopSpace,T be NormedLinearTopSpace,
f be Function of S,T,
x be Point of S holds
( f is_continuous_at x
iff
for e be Real
st 0 < e
holds ex H being Subset of S st
( H is open & x in H
&
for y be Point of S
st y in H holds ||.f.x-f.y.|| < e ) );
theorem :: ASCOLI:4
for S be non empty MetrSpace,
V be non empty compact TopSpace,
T be NormedLinearTopSpace,
f be Function of V,T
st V = TopSpaceMetr(S)
holds
f is continuous
iff
for e be Real
st 0 < e
holds ex d be Real
st 0 < d
& for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f/.x1-f/.x2.|| < e;
definition
let S be non empty MetrSpace,T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
attr F is equibounded means
:: ASCOLI:def 2
ex K be Real
st for f be Function of the carrier of S,the carrier of T
st f in F
holds
for x be Element of S
holds
||.f.x.|| <= K;
end;
definition
let S be non empty MetrSpace, T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
let x0 be Point of S;
pred F is_equicontinuous_at x0 means
:: ASCOLI:def 3
for e be Real st 0 < e
ex d be Real st 0 < d &
for f be Function of the carrier of S,the carrier of T
st f in F
holds
for x be Point of S
st dist(x,x0) < d holds ||.f.x-f.x0.|| < e;
end;
definition
let S be non empty MetrSpace, T be RealNormSpace;
let F be Subset of Funcs(the carrier of S,the carrier of T);
attr F is equicontinuous means
:: ASCOLI:def 4
for e be Real st 0 < e
ex d be Real st 0 < d &
for f be Function of the carrier of S,the carrier of T
st f in F
holds
for x1,x2 be Point of S
st dist(x1,x2) < d holds ||.f.x1-f.x2.|| < e;
end;
theorem :: ASCOLI:5
for S be non empty MetrSpace,
T be RealNormSpace,
F be Subset of Funcs(the carrier of S,the carrier of T)
st TopSpaceMetr(S) is compact
holds
F is equicontinuous
iff
for x be Point of S holds F is_equicontinuous_at x;
begin :: Ascoli-Arzela's Theorem
reserve S,Z for RealNormSpace;
reserve T for RealBanachSpace;
reserve F for Subset of Funcs(the carrier of S,the carrier of T);
theorem :: ASCOLI:6
for Z be RealNormSpace
holds
Z is complete iff MetricSpaceNorm Z is complete;
theorem :: ASCOLI:7
for Z be RealNormSpace,
H be non empty Subset of MetricSpaceNorm Z
st Z is complete
holds
(MetricSpaceNorm Z) | Cl(H) is complete;
theorem :: ASCOLI:8
for Z be RealNormSpace,
H be non empty Subset of MetricSpaceNorm Z
holds
(MetricSpaceNorm Z) | H is totally_bounded
iff (MetricSpaceNorm Z) | Cl(H) is totally_bounded;
theorem :: ASCOLI:9
for Z be RealNormSpace,
F be non empty Subset of Z,
H be non empty Subset of MetricSpaceNorm Z
st Z is complete & H = F
& (MetricSpaceNorm Z) | H is totally_bounded
holds
Cl(H) is sequentially_compact
&
(MetricSpaceNorm Z) | Cl(H) is compact
&
Cl(F) is compact;
theorem :: ASCOLI:10
for Z be RealNormSpace,
F be non empty Subset of Z,
H be non empty Subset of MetricSpaceNorm Z,
T being Subset of TopSpaceNorm Z
st Z is complete & H = F & H = T
holds
( (MetricSpaceNorm Z) | H is totally_bounded
iff Cl(H) is sequentially_compact) &
( (MetricSpaceNorm Z) | H is totally_bounded
iff
(MetricSpaceNorm Z) | Cl(H) is compact) &
( (MetricSpaceNorm Z) | H is totally_bounded
iff
Cl(F) is compact) &
( (MetricSpaceNorm Z) | H is totally_bounded
iff
Cl(T) is compact);
theorem :: ASCOLI:11
for S be non empty compact TopSpace,T be NormedLinearTopSpace
st T is complete holds
for H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
holds
Cl(H) is sequentially_compact iff
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) )
| H is totally_bounded;
theorem :: ASCOLI:12
for S be non empty compact TopSpace,T be NormedLinearTopSpace
st T is complete holds
for F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) st
H = F holds
Cl(F) is compact iff
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) )
| H is totally_bounded;
theorem :: ASCOLI:13
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T) st
G = H & (MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded holds
G is equibounded & G is equicontinuous;
theorem :: ASCOLI:14
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace
st S = TopSpaceMetr(M) & T is complete holds
for G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T)
st G = H &
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded holds
( for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Hx is totally_bounded )
& G is equicontinuous;
theorem :: ASCOLI:15
for T be NormedLinearTopSpace,
RNS be RealNormSpace st
RNS = the NORMSTR of T &
the topology of T = the topology of TopSpaceNorm RNS holds
distance_by_norm_of RNS = distance_by_norm_of T &
MetricSpaceNorm RNS = MetricSpaceNorm T &
TopSpaceNorm T = TopSpaceNorm RNS;
theorem :: ASCOLI:16
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T)
st S = TopSpaceMetr(M) & T is complete & G = H holds
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
| H is totally_bounded
iff
G is equicontinuous &
for x be Point of S,
Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Cl(Hx) is compact;
theorem :: ASCOLI:17
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
G be Subset of Funcs(the carrier of M, the carrier of T),
H be non empty Subset of
(MetricSpaceNorm R_NormSpace_of_ContinuousFunctions(S,T))
st S = TopSpaceMetr(M) & T is complete & G = H
holds
Cl(H) is sequentially_compact
iff
G is equicontinuous
&
for x be Point of S, Hx be non empty Subset of MetricSpaceNorm T
st Hx = {f.x where f is Function of S,T :f in H }
holds (MetricSpaceNorm T) | Cl(Hx) is compact;
theorem :: ASCOLI:18
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete & G = F holds
Cl(F) is compact
iff
G is equicontinuous
&
for x be Point of S,
Fx be non empty Subset of MetricSpaceNorm T
st Fx = {f.x where f is Function of S,T :f in F }
holds
(MetricSpaceNorm T) | Cl(Fx) is compact;
theorem :: ASCOLI:19
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete & G = F
holds
Cl(F) is compact
iff
( for x be Point of M holds G is_equicontinuous_at x ) &
for x be Point of S,
Fx be non empty Subset of MetricSpaceNorm T
st Fx = {f.x where f is Function of S,T :f in F }
holds (MetricSpaceNorm T) | Cl(Fx) is compact;
theorem :: ASCOLI:20
for T be NormedLinearTopSpace holds
T is compact iff TopSpaceNorm T is compact;
theorem :: ASCOLI:21
for T be NormedLinearTopSpace,
X be set holds
X is compact Subset of T
iff
X is compact Subset of TopSpaceNorm T;
theorem :: ASCOLI:22
for T be NormedLinearTopSpace
st T is compact holds
T is complete;
registration
cluster compact -> complete for NormedLinearTopSpace;
end;
theorem :: ASCOLI:23
for M be non empty MetrSpace,S be non empty compact TopSpace,
T be NormedLinearTopSpace,
U be compact Subset of T,
F be non empty Subset of
R_NormSpace_of_ContinuousFunctions(S,T),
G be Subset of Funcs(the carrier of M, the carrier of T)
st S = TopSpaceMetr(M) & T is complete
& G = F & for f be Function st f in F holds rng f c= U
holds
( Cl(F) is compact implies G is equibounded & G is equicontinuous )
&
( G is equicontinuous implies Cl(F) is compact );