let CNS be ComplexNormSpace; for RNS being RealNormSpace
for f being PartFunc of CNS,RNS st dom f is compact & f is_continuous_on dom f holds
rng f is compact
let RNS be RealNormSpace; for f being PartFunc of CNS,RNS st dom f is compact & f is_continuous_on dom f holds
rng f is compact
let f be PartFunc of CNS,RNS; ( dom f is compact & f is_continuous_on dom f implies rng f is compact )
assume that
A1:
dom f is compact
and
A2:
f is_continuous_on dom f
; rng f is compact
now for s1 being sequence of RNS st rng s1 c= rng f holds
ex q2 being Element of K16(K17(NAT, the carrier of RNS)) st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )let s1 be
sequence of
RNS;
( rng s1 c= rng f implies ex q2 being Element of K16(K17(NAT, the carrier of RNS)) st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) )assume A3:
rng s1 c= rng f
;
ex q2 being Element of K16(K17(NAT, the carrier of RNS)) st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )defpred S1[
set ,
set ]
means ( $2
in dom f &
f /. $2
= s1 . $1 );
A4:
for
n being
Element of
NAT ex
p being
Point of
CNS st
S1[
n,
p]
consider q1 being
sequence of
CNS such that A6:
for
n being
Element of
NAT holds
S1[
n,
q1 . n]
from FUNCT_2:sch 3(A4);
then A8:
rng q1 c= dom f
;
then consider s2 being
sequence of
CNS such that A9:
s2 is
subsequence of
q1
and A10:
s2 is
convergent
and A11:
lim s2 in dom f
by A1;
take q2 =
f /* s2;
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
rng s2 c= rng q1
by A9, VALUED_0:21;
then A12:
rng s2 c= dom f
by A8;
then A13:
f /* q1 = s1
by FUNCT_2:63;
f | (dom f) is_continuous_in lim s2
by A2, A11;
then A14:
f is_continuous_in lim s2
by RELAT_1:68;
then
f /. (lim s2) = lim (f /* s2)
by A10, A12;
hence
(
q2 is
subsequence of
s1 &
q2 is
convergent &
lim q2 in rng f )
by A8, A13, A9, A10, A14, A12, PARTFUN2:2, VALUED_0:22;
verum end;
hence
rng f is compact
; verum