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
( ( 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 )
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
( ( 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 )
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
( ( 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 ) )
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
( ( 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 )
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
( ( 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 )
let H be non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)); ( G = H & (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded implies ( ( 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 ) )
assume A2:
G = H
; ( not (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded or ( ( 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 ) )
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
; ( ( 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 )
thus
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
let x be
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 let Hx be non
empty Subset of
T;
( Hx = { (f . x) where f is Function of S,T : f in H } implies T | Hx is totally_bounded )
assume A5:
Hx = { (f . x) where f is Function of S,T : f in H }
;
T | Hx is totally_bounded
set MTHx =
T | Hx;
let e be
Real;
TBSP_1:def 1 ( e <= 0 or ex b1 being Element of bool (bool the carrier of (T | Hx)) st
( b1 is finite & the carrier of (T | Hx) = union b1 & ( for b2 being Element of bool the carrier of (T | Hx) holds
( not b2 in b1 or ex b3 being Element of the carrier of (T | Hx) st b2 = Ball (b3,e) ) ) ) )
assume
0 < e
;
ex b1 being Element of bool (bool the carrier of (T | Hx)) st
( b1 is finite & the carrier of (T | Hx) = union b1 & ( for b2 being Element of bool the carrier of (T | Hx) holds
( not b2 in b1 or ex b3 being Element of the carrier of (T | Hx) st b2 = Ball (b3,e) ) ) )
then consider L being
Subset-Family of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) such that A6:
(
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) ) )
by A4;
defpred S1[
object ,
object ]
means ex
w being
Point of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) st
( $2
= w & $1
= Ball (
w,
e) );
A7:
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) &
S1[
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) & S1[D,w] ) )
assume A8:
D in L
;
ex w being object st
( w in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S1[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 A9:
D0 = Ball (
w,
e)
by A6, A8;
take
w
;
( w in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) & S1[D,w] )
thus
(
w in the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) &
S1[
D,
w] )
by A9;
verum
end;
consider U being
Function of
L, the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) such that A10:
for
D being
object st
D in L holds
S1[
D,
U . D]
from FUNCT_2:sch 1(A7);
A11:
for
D being
object st
D in L holds
D = Ball (
(U /. D),
e)
defpred S2[
object ,
object ]
means ex
w being
Function of
S,
T ex
p being
Point of
(T | Hx) st
( $1
= w &
p = w . x & $2
= Ball (
p,
e) );
A14:
for
f being
object st
f in the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) holds
ex
B being
object st
(
B in bool the
carrier of
(T | Hx) &
S2[
f,
B] )
proof
let f be
object ;
( f in the carrier of ((MetricSpace_of_ContinuousFunctions (S,T)) | H) implies ex B being object st
( B in bool the carrier of (T | Hx) & S2[f,B] ) )
assume A15:
f in the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H)
;
ex B being object st
( B in bool the carrier of (T | Hx) & S2[f,B] )
then
f in MetricSpace_of_ContinuousFunctions (
S,
T)
by A3;
then
ex
g being
Function of
S,
(TopSpaceMetr T) st
(
f = g &
g is
continuous )
;
then reconsider g =
f as
Function of
S,
T ;
g . x in Hx
by A15, A5, A3;
then reconsider p =
g . x as
Point of
(T | Hx) by TOPMETR:def 2;
take B =
Ball (
p,
e);
( B in bool the carrier of (T | Hx) & S2[f,B] )
thus
(
B in bool the
carrier of
(T | Hx) &
S2[
f,
B] )
;
verum
end;
consider NF being
Function of the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H),
(bool the carrier of (T | Hx)) such that A16:
for
D being
object st
D in the
carrier of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) holds
S2[
D,
NF . D]
from FUNCT_2:sch 1(A14);
A17:
dom U = L
by FUNCT_2:def 1;
set Le =
NF .: (rng U);
reconsider Le =
NF .: (rng U) as
Subset-Family of
(T | Hx) ;
take
Le
;
( Le is finite & the carrier of (T | Hx) = union Le & ( for b1 being Element of bool the carrier of (T | Hx) holds
( not b1 in Le or ex b2 being Element of the carrier of (T | Hx) st b1 = Ball (b2,e) ) ) )
thus
Le is
finite
by A6;
( the carrier of (T | Hx) = union Le & ( for b1 being Element of bool the carrier of (T | Hx) holds
( not b1 in Le or ex b2 being Element of the carrier of (T | Hx) st b1 = Ball (b2,e) ) ) )
for
t being
object holds
(
t in the
carrier of
(T | Hx) iff
t in union Le )
proof
let t0 be
object ;
( t0 in the carrier of (T | Hx) iff t0 in union Le )
hereby ( t0 in union Le implies t0 in the carrier of (T | Hx) )
assume A18:
t0 in the
carrier of
(T | Hx)
;
t0 in union Lethen A19:
t0 in Hx
by TOPMETR:def 2;
reconsider t =
t0 as
Point of
(T | Hx) by A18;
consider f being
Function of
S,
T such that A20:
(
t = f . x &
f in H )
by A5, A19;
consider K being
set such that A21:
(
f in K &
K in L )
by TARSKI:def 4, A6, A3, A20;
U /. K = U . K
by PARTFUN1:def 6, A21, A17;
then A22:
U /. K in rng U
by FUNCT_1:def 3, A17, A21;
consider g being
Function of
S,
T,
p being
Point of
(T | Hx) such that A23:
(
U /. K = g &
p = g . x &
NF . (U /. K) = Ball (
p,
e) )
by A16;
A24:
f in Ball (
(U /. K),
e)
by A21, A11;
reconsider f0 =
f as
Point of
((MetricSpace_of_ContinuousFunctions (S,T)) | H) by A21;
A25:
dist (
f0,
(U /. K))
< e
by A24, METRIC_1:11;
reconsider f1 =
f0 as
Point of
(MetricSpace_of_ContinuousFunctions (S,T)) by TOPMETR:def 1, TARSKI:def 3;
reconsider g1 =
U /. K as
Point of
(MetricSpace_of_ContinuousFunctions (S,T)) by TOPMETR:def 1, TARSKI:def 3;
A26:
dist (
f1,
g1)
< e
by A25, TOPMETR:def 1;
dist (
(In ((f1 . x),T)),
(In ((g1 . x),T)))
<= dist (
f1,
g1)
by Th11;
then A27:
dist (
(g /. x),
(f /. x))
< e
by A23, A26, XXREAL_0:2;
A28:
NF . (U /. K) in Le
by A22, FUNCT_2:35;
reconsider tt =
t as
Point of
T by A20;
reconsider pp =
p as
Point of
T by TOPMETR:def 1, TARSKI:def 3;
reconsider p1 =
pp as
Point of
T ;
dist (
p,
t)
< e
by A20, A23, A27, TOPMETR:def 1;
then
f . x in { y where y is Point of (T | Hx) : dist (p,y) < e }
by A20;
then
f . x in NF . (U /. K)
by A23, METRIC_1:def 14;
hence
t0 in union Le
by TARSKI:def 4, A28, A20;
verum
end;
assume
t0 in union Le
;
t0 in the carrier of (T | Hx)
hence
t0 in the
carrier of
(T | Hx)
;
verum
end;
hence
the
carrier of
(T | Hx) = union Le
by TARSKI:2;
for b1 being Element of bool the carrier of (T | Hx) holds
( not b1 in Le or ex b2 being Element of the carrier of (T | Hx) st b1 = Ball (b2,e) )
let C be
Subset of
(T | Hx);
( not C in Le or ex b1 being Element of the carrier of (T | Hx) st C = Ball (b1,e) )
assume
C in Le
;
ex b1 being Element of the carrier of (T | Hx) st C = Ball (b1,e)
then consider t being
object such that A29:
(
t in dom NF &
t in rng U &
C = NF . t )
by FUNCT_1:def 6;
consider w being
Function of
S,
T,
p being
Point of
(T | Hx) such that A30:
(
t = w &
p = w . x &
NF . t = Ball (
p,
e) )
by A29, A16;
take
p
;
C = Ball (p,e)
thus
C = Ball (
p,
e)
by A30, A29;
verum
end;
thus
G is equicontinuous
by Th15, A1, A2, A4; verum