let M be 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
let S be 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
let T be non empty MetrSpace; ( S = TopSpaceMetr M implies 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 )
assume A1:
S = TopSpaceMetr M
; 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
let G be 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
let H be non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)); ( G = H & (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded implies G is equicontinuous )
assume A2:
G = H
; ( not (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded or G is equicontinuous )
set Z = MetricSpace_of_ContinuousFunctions (S,T);
set MZH = (MetricSpace_of_ContinuousFunctions (S,T)) | H;
A3:
the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) = H
by TOPMETR:def 2;
assume A4:
(MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded
; G is equicontinuous
defpred S1[ object , object ] means ex w being Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
( $2 = w & $1 = Ball (w,1) );
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
dist ((f . x1),(f . x2)) < e ) )
proof
let e be
Real;
( 0 < e implies ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
dist ((f . x1),(f . x2)) < e ) ) )
assume A10:
0 < e
;
ex d being Real st
( 0 < d & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < d holds
dist ((f . x1),(f . x2)) < e ) )
then consider L being
Subset-Family of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) such that A11:
(
L is
finite & the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) = union L & ( for
C being
Subset of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
C in L holds
ex
w being
Element of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
C = Ball (
w,
(e / 3)) ) )
by A4;
defpred S2[
object ,
object ]
means ex
w being
Point of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
( $2
= w & $1
= Ball (
w,
(e / 3)) );
A12:
for
D being
object st
D in L holds
ex
w being
object st
(
w in the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) &
S2[
D,
w] )
proof
let D be
object ;
( D in L implies ex w being object st
( w in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S2[D,w] ) )
assume A13:
D in L
;
ex w being object st
( w in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S2[D,w] )
then reconsider D0 =
D as
Subset of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) ;
consider w being
Element of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) such that A14:
D0 = Ball (
w,
(e / 3))
by A11, A13;
take
w
;
( w in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S2[D,w] )
thus
(
w in the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) &
S2[
D,
w] )
by A14;
verum
end;
consider U being
Function of
L, the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) such that A15:
for
D being
object st
D in L holds
S2[
D,
U . D]
from FUNCT_2:sch 1(A12);
A16:
for
D being
object st
D in L holds
D = Ball (
(U /. D),
(e / 3))
defpred S3[
Element of
((MetricSpace_of_ContinuousFunctions (S,T)) | H),
Real]
means ex
f being
Function of the
carrier of
S, the
carrier of
T st
( $1
= f &
0 < $2 & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< $2 holds
dist (
(f /. x1),
(f /. x2))
< e / 3 ) );
A19:
for
x0 being
Element of the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) ex
d being
Element of
REAL st
S3[
x0,
d]
proof
let x0 be
Element of the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H);
ex d being Element of REAL st S3[x0,d]
x0 in H
by A3;
then
x0 in MetricSpace_of_ContinuousFunctions (
S,
T)
;
then A20:
ex
f being
Function of
S,
(TopSpaceMetr T) st
(
x0 = f &
f is
continuous )
;
then reconsider f =
x0 as
Function of the
carrier of
S, the
carrier of
T ;
consider d being
Real such that A21:
(
0 < d & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< d holds
dist (
(In ((f /. x1),T)),
(In ((f /. x2),T)))
< e / 3 ) )
by A10, Lm1, A1, A20;
reconsider d0 =
d as
Element of
REAL by XREAL_0:def 1;
take
d0
;
S3[x0,d0]
hence
S3[
x0,
d0]
by A21;
verum
end;
consider NF being
Function of the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H),
REAL such that A22:
for
f being
Element of the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) holds
S3[
f,
NF . f]
from FUNCT_2:sch 3(A19);
A23:
dom U = L
by FUNCT_2:def 1;
reconsider NFU =
NF .: (rng U) as
finite Subset of
REAL by A11;
consider xx being
object such that A24:
xx in L
by XBOOLE_0:def 1, A11, ZFMISC_1:2;
rng U <> {}
by A23, A24, FUNCT_1:3;
then consider xx being
object such that A25:
xx in rng U
by XBOOLE_0:def 1;
reconsider xx =
xx as
Point of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) by A25;
A26:
(
NFU is
bounded_below &
lower_bound NFU in NFU )
by SEQ_4:133, A25;
set d =
lower_bound NFU;
consider xx being
object such that A27:
(
xx in dom NF &
xx in rng U &
lower_bound NFU = NF . xx )
by FUNCT_1:def 6, A26;
reconsider xx =
xx as
Point of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) by A27;
A28:
ex
f being
Function of
S,
T st
(
xx = f &
0 < NF . xx & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< NF . xx holds
dist (
(f /. x1),
(f /. x2))
< e / 3 ) )
by A22;
take
lower_bound NFU
;
( 0 < lower_bound NFU & ( for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
dist ((f . x1),(f . x2)) < e ) )
thus
0 < lower_bound NFU
by A28, A27;
for f being Function of the carrier of M, the carrier of T st f in G holds
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
dist ((f . x1),(f . x2)) < e
thus
for
f being
Function of
M,
T st
f in G holds
for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< lower_bound NFU holds
dist (
(f . x1),
(f . x2))
< e
verumproof
let f0 be
Function of
M,
T;
( f0 in G implies for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
dist ((f0 . x1),(f0 . x2)) < e )
assume
f0 in G
;
for x1, x2 being Point of M st dist (x1,x2) < lower_bound NFU holds
dist ((f0 . x1),(f0 . x2)) < e
then consider C being
set such that A29:
(
f0 in C &
C in L )
by A11, TARSKI:def 4, A3, A2;
reconsider f =
f0 as
Function of the
carrier of
S, the
carrier of
T by A1;
reconsider pf =
f0 as
Element of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) by A29;
A30:
pf in H
by A3;
reconsider pg =
U /. C as
Element of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) ;
A31:
C = Ball (
pg,
(e / 3))
by A16, A29;
A32:
pg in H
by A3;
then
pg in ContinuousFunctions (
S,
T)
;
then
ex
f being
Function of the
carrier of
S,
(TopSpaceMetr T) st
(
pg = f &
f is
continuous )
;
then reconsider g =
pg as
Function of
S,
(TopSpaceMetr T) ;
pf in { y where y is Point of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) : dist (pg,y) < e / 3 }
by METRIC_1:def 14, A29, A31;
then A33:
ex
y being
Point of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
(
pf = y &
dist (
pg,
y)
< e / 3 )
;
reconsider ppf =
pf,
ppg =
pg as
Element of
(MetricSpace_of_ContinuousFunctions (S,T)) by A30, A32;
reconsider pppf =
ppf,
pppg =
ppg as
Point of
(MetricSpace_of_ContinuousFunctions (S,T)) ;
A35:
dist (
pppg,
pppf)
< e / 3
by A33, TOPMETR:def 1;
A36:
C in dom U
by FUNCT_2:def 1, A29;
U . C in rng U
by FUNCT_1:3, A23, A29;
then
pg in rng U
by A36, PARTFUN1:def 6;
then A37:
NF . pppg in NF .: (rng U)
by FUNCT_2:35;
let x1,
x2 be
Element of
M;
( dist (x1,x2) < lower_bound NFU implies dist ((f0 . x1),(f0 . x2)) < e )
reconsider x10 =
x1,
x20 =
x2 as
Point of
S by A1;
assume A38:
dist (
x1,
x2)
< lower_bound NFU
;
dist ((f0 . x1),(f0 . x2)) < e
lower_bound NFU <= NF . pg
by A37, SEQ_4:def 2;
then A39:
dist (
x1,
x2)
< NF . pg
by A38, XXREAL_0:2;
ex
f being
Function of
S,
T st
(
pg = f &
0 < NF . pg & ( for
x1,
x2 being
Point of
M st
dist (
x1,
x2)
< NF . pg holds
dist (
(f /. x1),
(f /. x2))
< e / 3 ) )
by A22;
then A40:
dist (
(In ((g /. x1),T)),
(In ((g /. x2),T)))
< e / 3
by A39;
A41:
dist (
(In ((g . x20),T)),
(In ((f . x20),T)))
<= dist (
pppg,
pppf)
by Th11;
(
f /. x20 = f . x20 &
g /. x20 = g . x20 )
;
then A42:
dist (
(In ((g /. x2),T)),
(In ((f /. x2),T)))
< e / 3
by A41, XXREAL_0:2, A35;
A43:
dist (
(In ((f . x10),T)),
(In ((g . x10),T)))
<= dist (
pppf,
pppg)
by Th11;
(
f /. x10 = f . x10 &
g /. x10 = g . x10 )
;
then A44:
dist (
(In ((f /. x1),T)),
(In ((g /. x1),T)))
< e / 3
by A43, XXREAL_0:2, A35;
A45:
dist (
(f /. x1),
(f /. x2))
<= (dist ((f /. x1),(In ((g /. x1),T)))) + (dist ((In ((g /. x1),T)),(f /. x2)))
by METRIC_1:4;
dist (
(In ((g /. x1),T)),
(f /. x2))
<= (dist ((In ((g /. x1),T)),(In ((g /. x2),T)))) + (dist ((In ((g /. x2),T)),(f /. x2)))
by METRIC_1:4;
then
(dist ((f /. x1),(In ((g /. x1),T)))) + (dist ((In ((g /. x1),T)),(f /. x2))) <= (dist ((f /. x1),(In ((g /. x1),T)))) + ((dist ((In ((g /. x1),T)),(In ((g /. x2),T)))) + (dist ((In ((g /. x2),T)),(f /. x2))))
by XREAL_1:7;
then A46:
dist (
(f /. x1),
(f /. x2))
<= ((dist ((In ((f /. x1),T)),(In ((g /. x1),T)))) + (dist ((In ((g /. x1),T)),(In ((g /. x2),T))))) + (dist ((In ((g /. x2),T)),(In ((f /. x2),T))))
by A45, XXREAL_0:2;
(dist ((In ((g /. x1),T)),(In ((g /. x2),T)))) + (dist ((In ((g /. x2),T)),(In ((f /. x2),T)))) < (e / 3) + (e / 3)
by A40, A42, XREAL_1:8;
then A47:
(dist ((In ((f /. x1),T)),(In ((g /. x1),T)))) + ((dist ((In ((g /. x1),T)),(In ((g /. x2),T)))) + (dist ((In ((g /. x2),T)),(In ((f /. x2),T))))) < (e / 3) + ((e / 3) + (e / 3))
by A44, XREAL_1:8;
(
f /. x10 = f . x10 &
f /. x20 = f . x20 )
;
hence
dist (
(f0 . x1),
(f0 . x2))
< e
by A47, A46, XXREAL_0:2;
verum
end;
end;
hence
G is equicontinuous
; verum