:: 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
existence
ex b1 being Subset of X ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b1 = Cl Z )
;
uniqueness
for b1, b2 being Subset of X st ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b1 = Cl Z ) & ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b2 = Cl Z ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def1 defines Cl ASCOLI:def 1 :
for X being non empty MetrSpace
for Y, b3 being Subset of X holds
( b3 = Cl Y iff ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b3 = Cl Z ) );

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
coherence
not Cl H is empty
;
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 :
for S being non empty MetrSpace
for T being RealNormSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T)) holds
( F is equibounded iff 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 );

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 :
for S being non empty MetrSpace
for T being RealNormSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T))
for x0 being Point of S holds
( F is_equicontinuous_at x0 iff 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 ) ) );

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 :
for S being non empty MetrSpace
for T being RealNormSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T)) holds
( F is equicontinuous iff 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 ) ) );

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
for Z being RealNormSpace
for F being non empty Subset of Z
for H being non empty Subset of (MetricSpaceNorm Z)
for T being Subset of (TopSpaceNorm Z) st Z is complete & H = F & H = T holds
( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) )
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
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
( ( 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) | Hx is totally_bounded ) & G is equicontinuous )
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
for b1 being NormedLinearTopSpace st b1 is compact holds
b1 is complete
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;