ASCOLI: Ascoli-Arzela's Theorem

:: Ascoli-Arzela's Theorem
:: by Hiroshi Yamazaki , Keiichi Miyajima and Yasunari Shidama
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users

definition

let X be non empty MetrSpace;
let Y be Subset of X;

func Cl Y -> Subset of X means :Def1: :: ASCOLI:def 1
ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & it = Cl Z );

correctness

proof end;

end;

:: deftheorem Def1 defines Cl ASCOLI:def 1 :

theorem Th1: :: ASCOLI:1

for X being RealNormSpace
for Y being Subset of X
for Z being Subset of (MetricSpaceNorm X) st Y = Z holds
Cl Y = Cl Z

proof end;

registration

let X be non empty MetrSpace;
let H be non empty Subset of X;

cluster Cl H -> non empty ;

correctness

proof end;

end;

theorem Th2: :: ASCOLI:2

for S being TopSpace
for F being FinSequence of bool the carrier of S st ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) holds
union (rng F) is compact

proof end;

theorem Th3: :: ASCOLI:3

for S being non empty TopSpace
for T being NormedLinearTopSpace
for f being Function of S,T
for x being Point of S holds
( f is_continuous_at x iff for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
||.((f . x) - (f . y)).|| < e ) ) )

proof end;

theorem Th4: :: ASCOLI:4

for S being non empty MetrSpace
for V being non empty compact TopSpace
for T being NormedLinearTopSpace
for f being Function of V,T st V = TopSpaceMetr S holds
( f is continuous iff for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < e ) ) )

proof end;

definition

let S be non empty MetrSpace;
let 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 being Real st
for f being Function of the carrier of S, the carrier of T st f in F holds
for x being Element of S holds ||.(f . x).|| <= K;

end;

:: deftheorem defines equibounded ASCOLI:def 2 :

definition

let S be non empty MetrSpace;
let 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 being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for f being Function of the carrier of S, the carrier of T st f in F holds
for x being Point of S st dist (x,x0) < d holds
||.((f . x) - (f . x0)).|| < e ) );

end;

:: deftheorem defines is_equicontinuous_at ASCOLI:def 3 :

definition

let S be non empty MetrSpace;
let 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 being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for f being Function of the carrier of S, the carrier of T st f in F holds
for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f . x1) - (f . x2)).|| < e ) );

end;

:: deftheorem defines equicontinuous ASCOLI:def 4 :

theorem Th5: :: ASCOLI:5

for S being non empty MetrSpace
for T being RealNormSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T)) st TopSpaceMetr S is compact holds
( F is equicontinuous iff for x being Point of S holds F is_equicontinuous_at x )

proof end;

theorem Th6: :: ASCOLI:6

for Z being RealNormSpace holds
( Z is complete iff MetricSpaceNorm Z is complete )

proof end;

theorem Th7: :: ASCOLI:7

for Z being RealNormSpace
for H being non empty Subset of (MetricSpaceNorm Z) st Z is complete holds
(MetricSpaceNorm Z) | (Cl H) is complete

proof end;

theorem Th8: :: ASCOLI:8

for Z being RealNormSpace
for H being non empty Subset of (MetricSpaceNorm Z) holds
( (MetricSpaceNorm Z) | H is totally_bounded iff (MetricSpaceNorm Z) | (Cl H) is totally_bounded )

proof end;

theorem Th9: :: ASCOLI:9

for Z being RealNormSpace
for F being non empty Subset of Z
for H being 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 )

proof end;

theorem :: ASCOLI:10

proof end;

theorem Th11: :: ASCOLI:11

for S being non empty compact TopSpace
for T being NormedLinearTopSpace st T is complete holds
for H being 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 )

proof end;

theorem Th12: :: ASCOLI:12

for S being non empty compact TopSpace
for T being NormedLinearTopSpace st T is complete holds
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for H being 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 )

proof end;

theorem Th13: :: ASCOLI:13

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace st S = TopSpaceMetr M & T is complete holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being 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 )

proof end;

theorem Th14: :: ASCOLI:14

proof end;

theorem Th15: :: ASCOLI:15

for T being NormedLinearTopSpace
for RNS being RealNormSpace st RNS = NORMSTR(# the carrier of T, the ZeroF of T, the U5 of T, the U7 of T, the normF 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 )

proof end;

theorem Th16: :: ASCOLI:16

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being 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 being Point of S
for Hx being 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 ) ) )

proof end;

theorem :: ASCOLI:17

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being 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 being Point of S
for Hx being 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 ) ) )

proof end;

theorem Th18: :: ASCOLI:18

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being 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 being Point of S
for Fx being 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 ) ) )

proof end;

theorem :: ASCOLI:19

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being 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 being Point of M holds G is_equicontinuous_at x ) & ( for x being Point of S
for Fx being 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 ) ) )

proof end;

theorem Th20: :: ASCOLI:20

for T being NormedLinearTopSpace holds
( T is compact iff TopSpaceNorm T is compact )

proof end;

theorem Th21: :: ASCOLI:21

for T being NormedLinearTopSpace
for X being set holds
( X is compact Subset of T iff X is compact Subset of (TopSpaceNorm T) )

proof end;

theorem ThLast: :: ASCOLI:22

for T being NormedLinearTopSpace st T is compact holds
T is complete

proof end;

registration

cluster non empty V70() V95() V96() V97() V98() V99() V100() V101() discerning V106() RealNormSpace-like TopSpace-like T_2 V213() V214() compact strict norm-generated -> complete for RLNormTopStruct ;

coherence by ThLast;

end;

theorem :: ASCOLI:23

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being NormedLinearTopSpace
for U being compact Subset of T
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for G being Subset of (Funcs ( the carrier of M, the carrier of T)) st S = TopSpaceMetr M & T is complete & G = F & ( for f being 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 ) )

proof end;