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

existence

ex b_{1} being Subset of X ex Z being Subset of (TopSpaceMetr X) st

( Z = Y & b_{1} = Cl Z );

uniqueness

for b_{1}, b_{2} being Subset of X st ex Z being Subset of (TopSpaceMetr X) st

( Z = Y & b_{1} = Cl Z ) & ex Z being Subset of (TopSpaceMetr X) st

( Z = Y & b_{2} = Cl Z ) holds

b_{1} = b_{2};

end;
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 ex Z being Subset of (TopSpaceMetr X) st

( Z = Y & it = Cl Z );

existence

ex b

( Z = Y & b

uniqueness

for b

( Z = Y & b

( Z = Y & b

b

proof end;

:: deftheorem Def1 defines Cl ASCOLI:def 1 :

for X being non empty MetrSpace

for Y, b_{3} being Subset of X holds

( b_{3} = Cl Y iff ex Z being Subset of (TopSpaceMetr X) st

( Z = Y & b_{3} = Cl Z ) );

for X being non empty MetrSpace

for Y, b

( b

( Z = Y & b

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

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;

correctness

coherence

not Cl H is empty ;

end;
let H be non empty Subset of X;

correctness

coherence

not Cl H is empty ;

proof 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

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

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

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

end;
let T be RealNormSpace;

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

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

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;

end;
let T be RealNormSpace;

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

let x0 be Point of S;

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

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

end;
let T be RealNormSpace;

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

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

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 )

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 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

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 )

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 )

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

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 )

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 )

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 )

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 )

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 )

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

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

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

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

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

for X being set holds

( X is compact Subset of T iff X is compact Subset of (TopSpaceNorm T) )

proof end;

registration

for b_{1} being NormedLinearTopSpace st b_{1} is compact holds

b_{1} is complete
by ThLast;

end;

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 b

b

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

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;