:: Ascoli-Arzela's Theorem (Metric Space Version)
:: by Keiichi Miyajima and Hiroshi Yamazaki
::
:: Received November 28, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

theorem Th1: :: ASCOLI2:1

for T being non empty MetrSpace
for A being Subset of T holds A c= Cl A

proof end;

theorem Th2: :: ASCOLI2:2

for S being non empty TopSpace
for T being non empty MetrSpace
for f being Function of S,(TopSpaceMetr 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
dist ((In ((f . x),T)),(In ((f . y),T))) < e ) ) )

proof end;

Lm1: for S, T being non empty MetrSpace
for f being Function of (TopSpaceMetr S),(TopSpaceMetr T) st TopSpaceMetr S is compact 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
dist ((In ((f /. x1),T)),(In ((f /. x2),T))) < e ) ) )

proof end;

definition

let S, T be non empty MetrSpace;
let F be Subset of (Funcs ( the carrier of S, the carrier of T));

attr F is equibounded means :: ASCOLI2:def 1
ex K being Subset of T st
( K is bounded & ( 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 in K ) );

end;

:: deftheorem defines equibounded ASCOLI2:def 1 :
for S, T being non empty MetrSpace
for F being Subset of (Funcs ( the carrier of S, the carrier of T)) holds
( F is equibounded iff ex K being Subset of T st
( K is bounded & ( 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 in K ) ) );

definition

let S, T be non empty MetrSpace;
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 :: ASCOLI2:def 2
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
dist ((f . x),(f . x0)) < e ) );

end;

:: deftheorem defines is_equicontinuous_at ASCOLI2:def 2 :
for S, T being non empty MetrSpace
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
dist ((f . x),(f . x0)) < e ) ) );

definition

let S, T be non empty MetrSpace;
let F be Subset of (Funcs ( the carrier of S, the carrier of T));

attr F is equicontinuous means :: ASCOLI2: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 x1, x2 being Point of S st dist (x1,x2) < d holds
dist ((f . x1),(f . x2)) < e ) );

end;

:: deftheorem defines equicontinuous ASCOLI2:def 3 :
for S, T being non empty MetrSpace
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
dist ((f . x1),(f . x2)) < e ) ) );

Lm2: for S, T being non empty MetrSpace
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 Th3: :: ASCOLI2:3

for Z being non empty MetrSpace
for F being non empty Subset of Z st Z is complete holds
Z | (Cl F) is complete

proof end;

theorem Th4: :: ASCOLI2:4

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

proof end;

theorem Th5: :: ASCOLI2:5

for Z being non empty MetrSpace
for H being non empty Subset of Z st Z is complete & Z | H is totally_bounded holds
( Cl H is sequentially_compact & Z | (Cl H) is compact )

proof end;

theorem :: ASCOLI2:6

for Z being non empty MetrSpace
for H being non empty Subset of Z st Z is complete holds
( ( Z | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies Z | H is totally_bounded ) & ( Z | H is totally_bounded implies Z | (Cl H) is compact ) & ( Z | (Cl H) is compact implies Z | H is totally_bounded ) )

proof end;

definition

let S be non empty TopSpace;
let T be non empty MetrSpace;

func ContinuousFunctions (S,T) -> non empty set equals :: ASCOLI2:def 4
{ f where f is Function of S,(TopSpaceMetr T) : f is continuous } ;

coherence
{ f where f is Function of S,(TopSpaceMetr T) : f is continuous } is non empty set

proof end;

end;

:: deftheorem defines ContinuousFunctions ASCOLI2:def 4 :
for S being non empty TopSpace
for T being non empty MetrSpace holds ContinuousFunctions (S,T) = { f where f is Function of S,(TopSpaceMetr T) : f is continuous } ;

theorem Th7: :: ASCOLI2:7

for X being MetrSpace
for x, y, v, w being Element of X holds |.((dist (x,y)) - (dist (v,w))).| <= (dist (x,v)) + (dist (y,w))

proof end;

theorem Th8: :: ASCOLI2:8

for S being non empty TopSpace
for T being non empty MetrSpace
for f, g being Function of S,(TopSpaceMetr T) st f is continuous & g is continuous holds
for Dist being RealMap of S st ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) holds
Dist is continuous

proof end;

theorem Th9: :: ASCOLI2:9

for S being non empty compact TopSpace
for T being non empty MetrSpace
for f, g being Function of S,(TopSpaceMetr T) st f is continuous & g is continuous holds
for Dist being RealMap of S st ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) holds
( rng Dist <> {} & rng Dist is bounded_above & rng Dist is bounded_below )

proof end;

theorem Th10: :: ASCOLI2:10

for S being non empty TopSpace
for T being non empty MetrSpace ex F being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL st
for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & F . (f,g) = upper_bound (rng Dist) )

proof end;

definition

let S be non empty TopSpace;
let T be non empty MetrSpace;

func dist_Func (S,T) -> Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL means :Def5: :: ASCOLI2:def 5
for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & it . (f,g) = upper_bound (rng Dist) );

existence
ex b₁ being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL st
for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & b₁ . (f,g) = upper_bound (rng Dist) ) by Th10;
uniqueness
for b₁, b₂ being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL st ( for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & b₁ . (f,g) = upper_bound (rng Dist) ) ) & ( for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & b₂ . (f,g) = upper_bound (rng Dist) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines dist_Func ASCOLI2:def 5 :
for S being non empty TopSpace
for T being non empty MetrSpace
for b₃ being Function of [:(ContinuousFunctions (S,T)),(ContinuousFunctions (S,T)):],REAL holds
( b₃ = dist_Func (S,T) iff for f, g being Function of S,(TopSpaceMetr T) st f in ContinuousFunctions (S,T) & g in ContinuousFunctions (S,T) holds
ex Dist being RealMap of S st
( ( for x being Point of S holds Dist . x = dist ((In ((f . x),T)),(In ((g . x),T))) ) & b₃ . (f,g) = upper_bound (rng Dist) ) );

definition

let S be non empty TopSpace;
let T be non empty MetrSpace;

func MetricSpace_of_ContinuousFunctions (S,T) -> MetrStruct equals :: ASCOLI2:def 6
MetrStruct(# (ContinuousFunctions (S,T)),(dist_Func (S,T)) #);

coherence
MetrStruct(# (ContinuousFunctions (S,T)),(dist_Func (S,T)) #) is MetrStruct ;

end;

:: deftheorem defines MetricSpace_of_ContinuousFunctions ASCOLI2:def 6 :
for S being non empty TopSpace
for T being non empty MetrSpace holds MetricSpace_of_ContinuousFunctions (S,T) = MetrStruct(# (ContinuousFunctions (S,T)),(dist_Func (S,T)) #);

Lm3: for S being non empty compact TopSpace
for T being non empty MetrSpace holds
( MetricSpace_of_ContinuousFunctions (S,T) is Reflexive & MetricSpace_of_ContinuousFunctions (S,T) is discerning & MetricSpace_of_ContinuousFunctions (S,T) is symmetric & MetricSpace_of_ContinuousFunctions (S,T) is triangle )

proof end;

registration

let S be non empty compact TopSpace;
let T be non empty MetrSpace;

cluster MetricSpace_of_ContinuousFunctions (S,T) -> Reflexive discerning symmetric triangle ;

coherence
( MetricSpace_of_ContinuousFunctions (S,T) is Reflexive & MetricSpace_of_ContinuousFunctions (S,T) is discerning & MetricSpace_of_ContinuousFunctions (S,T) is symmetric & MetricSpace_of_ContinuousFunctions (S,T) is triangle ) by Lm3;

end;

registration

let S be non empty TopSpace;
let T be non empty MetrSpace;

cluster MetricSpace_of_ContinuousFunctions (S,T) -> non empty strict ;

coherence
( not MetricSpace_of_ContinuousFunctions (S,T) is empty & MetricSpace_of_ContinuousFunctions (S,T) is strict ) ;

end;

registration

let S be non empty TopSpace;
let T be non empty MetrSpace;

cluster ContinuousFunctions (S,T) -> non empty functional ;

coherence
( not ContinuousFunctions (S,T) is empty & ContinuousFunctions (S,T) is functional )

proof end;

end;

registration

let S be non empty compact TopSpace;
let T be non empty MetrSpace;

cluster MetricSpace_of_ContinuousFunctions (S,T) -> constituted-Functions ;

coherence
MetricSpace_of_ContinuousFunctions (S,T) is constituted-Functions by MONOID_0:80;

end;

definition

let S be non empty compact TopSpace;
let T be non empty MetrSpace;
let f be Element of (MetricSpace_of_ContinuousFunctions (S,T));
let v be Point of S;
:: original: .
redefine func f . v -> Point of (TopSpaceMetr T);
coherence
f . v is Point of (TopSpaceMetr T)

proof end;

end;

theorem Th11: :: ASCOLI2:11

for S being non empty compact TopSpace
for T being non empty MetrSpace
for f, g being Point of (MetricSpace_of_ContinuousFunctions (S,T))
for t being Point of S holds dist ((In ((f . t),T)),(In ((g . t),T))) <= dist (f,g)

proof end;

theorem Th12: :: ASCOLI2:12

for S being non empty compact TopSpace
for T being non empty MetrSpace
for f, g being Point of (MetricSpace_of_ContinuousFunctions (S,T))
for f1, g1 being Function of S,T
for e being Real st f = f1 & g = g1 & ( for t being Point of S holds dist ((f1 . t),(g1 . t)) <= e ) holds
dist (f,g) <= e

proof end;

theorem Th13: :: ASCOLI2:13

for S being non empty compact TopSpace
for T being non empty MetrSpace st T is complete holds
MetricSpace_of_ContinuousFunctions (S,T) is complete

proof end;

theorem Th14: :: ASCOLI2:14

for S being non empty compact TopSpace
for T being non empty MetrSpace st T is complete holds
for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) holds
( Cl H is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded )

proof end;

theorem Th15: :: ASCOLI2:15

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace st S = TopSpaceMetr M holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) st G = H & (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded holds
G is equicontinuous

proof end;

theorem Th16: :: ASCOLI2:16

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace st S = TopSpaceMetr M holds
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) st G = H & (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded holds
( ( for x being Point of S
for Hx being non empty Subset of T st Hx = { (f . x) where f is Function of S,T : f in H } holds
T | Hx is totally_bounded ) & G is equicontinuous )

proof end;

theorem Th17: :: ASCOLI2:17

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) st S = TopSpaceMetr M & T is complete & G = H holds
( (MetricSpace_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 T st Hx = { (f . x) where f is Function of S,T : f in H } holds
T | (Cl Hx) is compact ) ) )

proof end;

theorem :: ASCOLI2:18

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace
for G being Subset of (Funcs ( the carrier of M, the carrier of T))
for H being non empty Subset of (MetricSpace_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 T st Hx = { (f . x) where f is Function of S,T : f in H } holds
T | (Cl Hx) is compact ) ) )

proof end;

theorem Th19: :: ASCOLI2:19

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace
for F being non empty Subset of (MetricSpace_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
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff ( G is equicontinuous & ( for x being Point of S
for Fx being non empty Subset of T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) )

proof end;

theorem :: ASCOLI2:20

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace
for F being non empty Subset of (MetricSpace_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
( (MetricSpace_of_ContinuousFunctions (S,T)) | (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 T st Fx = { (f . x) where f is Function of S,T : f in F } holds
T | (Cl Fx) is compact ) ) )

proof end;

theorem :: ASCOLI2:21

for M being non empty MetrSpace
for S being non empty compact TopSpace
for T being non empty MetrSpace
for U being compact Subset of (TopSpaceMetr T)
for F being non empty Subset of (MetricSpace_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
( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl F) is compact iff G is equicontinuous )

proof end;