let S be 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 ) ) )
let V be 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 ) ) )
let T be 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 ) ) )
let f be Function of V,T; ( V = TopSpaceMetr S implies ( 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 ) ) ) )
assume A1:
V = TopSpaceMetr S
; ( 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 ) ) )
hereby ( ( 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 ) ) ) implies f is continuous )
assume A2:
f is
continuous
;
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 ) )let e be
Real;
( 0 < e implies 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 ) ) )assume A3:
0 < e
;
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 ) )A4:
[#] (TopSpaceMetr S) is
compact
by A1, COMPTS_1:1;
defpred S1[
Element of
S,
Real]
means (
0 < $2 & ( for
x being
Point of
S st
dist (
x,$1)
< $2 holds
||.((f /. x) - (f /. $1)).|| < e / 2 ) );
A5:
for
x0 being
Element of the
carrier of
S ex
d being
Element of
REAL st
S1[
x0,
d]
proof
let x0 be
Element of the
carrier of
S;
ex d being Element of REAL st S1[x0,d]
reconsider xx0 =
x0 as
Point of
V by A1;
consider H being
Subset of
V such that A6:
(
H is
open &
xx0 in H & ( for
y being
Point of
V st
y in H holds
||.((f . xx0) - (f . y)).|| < e / 2 ) )
by A3, Th3, A2, TMAP_1:50;
consider d being
Real such that A7:
(
d > 0 &
Ball (
x0,
d)
c= H )
by A1, PCOMPS_1:def 4, A6;
reconsider d =
d as
Element of
REAL by XREAL_0:def 1;
take
d
;
S1[x0,d]
for
x being
Point of
S st
dist (
x,
x0)
< d holds
||.((f /. x) - (f /. x0)).|| < e / 2
hence
S1[
x0,
d]
by A7;
verum
end; consider D being
Function of the
carrier of
S,
REAL such that A10:
for
x0 being
Element of the
carrier of
S holds
S1[
x0,
D . x0]
from FUNCT_2:sch 3(A5);
set CV =
{ (Ball (x0,((D . x0) / 2))) where x0 is Element of S : verum } ;
{ (Ball (x0,((D . x0) / 2))) where x0 is Element of S : verum } c= bool the
carrier of
(TopSpaceMetr S)
then reconsider CV =
{ (Ball (x0,((D . x0) / 2))) where x0 is Element of S : verum } as
Subset-Family of
(TopSpaceMetr S) ;
for
P being
Subset of
(TopSpaceMetr S) st
P in CV holds
P is
open
then A13:
CV is
open
by TOPS_2:def 1;
the
carrier of
(TopSpaceMetr S) c= union CV
then consider G being
Subset-Family of
(TopSpaceMetr S) such that A17:
(
G c= CV &
G is
Cover of
[#] (TopSpaceMetr S) &
G is
finite )
by COMPTS_1:def 4, A4, A13, SETFAM_1:def 11;
defpred S2[
object ,
object ]
means ex
x0 being
Point of
S st
( $2
= x0 & $1
= Ball (
x0,
((D . x0) / 2)) );
A18:
for
Z being
object st
Z in G holds
ex
x0 being
object st
(
x0 in the
carrier of
S &
S2[
Z,
x0] )
consider H being
Function of
G, the
carrier of
S such that A20:
for
Z being
object st
Z in G holds
S2[
Z,
H . Z]
from FUNCT_2:sch 1(A18);
A21:
for
Z being
object st
Z in G holds
Z = Ball (
(H /. Z),
((D . (H . Z)) / 2))
A24:
dom H = G
by FUNCT_2:def 1;
reconsider D0 =
D .: (rng H) as
finite Subset of
REAL by A17;
A25:
dom D = the
carrier of
S
by FUNCT_2:def 1;
G <> {}
then consider xx being
object such that A26:
xx in G
by XBOOLE_0:def 1;
rng H <> {}
by A24, A26, FUNCT_1:3;
then consider xx being
object such that A27:
xx in rng H
by XBOOLE_0:def 1;
reconsider xx =
xx as
Point of
S by A27;
set d0 =
lower_bound D0;
A28:
for
r being
Real st
r in D0 holds
lower_bound D0 <= r
by SEQ_4:def 2;
lower_bound D0 in D0
by SEQ_4:133, A27;
then consider xx being
object such that A29:
(
xx in dom D &
xx in rng H &
lower_bound D0 = D . xx )
by FUNCT_1:def 6;
reconsider xx =
xx as
Point of
S by A29;
A30:
0 < lower_bound D0
by A29, A10;
reconsider d =
(lower_bound D0) / 2 as
Real ;
take d =
d;
( 0 < d & ( for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < e ) )thus
0 < d
by A30;
for x1, x2 being Point of S st dist (x1,x2) < d holds
||.((f /. x1) - (f /. x2)).|| < ethus
for
x1,
x2 being
Point of
S st
dist (
x1,
x2)
< d holds
||.((f /. x1) - (f /. x2)).|| < e
verumproof
let x1,
x2 be
Point of
S;
( dist (x1,x2) < d implies ||.((f /. x1) - (f /. x2)).|| < e )
assume A31:
dist (
x1,
x2)
< d
;
||.((f /. x1) - (f /. x2)).|| < e
x1 in union G
by A17, SETFAM_1:def 11, TARSKI:def 3;
then consider X1 being
set such that A32:
(
x1 in X1 &
X1 in G )
by TARSKI:def 4;
A33:
X1 = Ball (
(H /. X1),
((D . (H . X1)) / 2))
by A21, A32;
A34:
(D . (H /. X1)) / 2
< D . (H /. X1)
by A10, XREAL_1:216;
x1 in { y where y is Point of S : dist ((H /. X1),y) < (D . (H . X1)) / 2 }
by A33, A32, METRIC_1:def 14;
then A35:
ex
y being
Point of
S st
(
y = x1 &
dist (
(H /. X1),
y)
< (D . (H . X1)) / 2 )
;
then
dist (
x1,
(H /. X1))
< (D . (H /. X1)) / 2
by A24, PARTFUN1:def 6, A32;
then
dist (
x1,
(H /. X1))
< D . (H /. X1)
by A34, XXREAL_0:2;
then A36:
||.((f /. x1) - (f /. (H /. X1))).|| < e / 2
by A10;
A37:
H . X1 in rng H
by A24, A32, FUNCT_1:3;
H /. X1 in dom D
by A25;
then
H . X1 in dom D
by A24, A32, PARTFUN1:def 6;
then
D . (H . X1) in D0
by FUNCT_1:def 6, A37;
then
(lower_bound D0) / 2
<= (D . (H . X1)) / 2
by A28, XREAL_1:72;
then A38:
dist (
x1,
x2)
< (D . (H . X1)) / 2
by A31, XXREAL_0:2;
A39:
dist (
x2,
(H /. X1))
<= (dist (x1,x2)) + (dist ((H /. X1),x1))
by METRIC_1:4;
(dist (x1,x2)) + (dist ((H /. X1),x1)) < ((D . (H . X1)) / 2) + ((D . (H . X1)) / 2)
by A38, A35, XREAL_1:8;
then A40:
dist (
x2,
(H /. X1))
< D . (H . X1)
by A39, XXREAL_0:2;
dist (
x2,
(H /. X1))
< D . (H /. X1)
by PARTFUN1:def 6, A24, A40, A32;
then A41:
||.((f /. x2) - (f /. (H /. X1))).|| < e / 2
by A10;
(f /. x1) - (f /. x2) =
(((f /. x1) - (f /. (H /. X1))) + (f /. (H /. X1))) - (f /. x2)
by RLVECT_4:1
.=
((f /. x1) - (f /. (H /. X1))) + ((f /. (H /. X1)) - (f /. x2))
by RLVECT_1:28
;
then
||.((f /. x1) - (f /. x2)).|| <= ||.((f /. x1) - (f /. (H /. X1))).|| + ||.((f /. (H /. X1)) - (f /. x2)).||
by NORMSP_1:def 1;
then A42:
||.((f /. x1) - (f /. x2)).|| <= ||.((f /. x1) - (f /. (H /. X1))).|| + ||.((f /. x2) - (f /. (H /. X1))).||
by NORMSP_1:7;
||.((f /. x1) - (f /. (H /. X1))).|| + ||.((f /. x2) - (f /. (H /. X1))).|| < (e / 2) + (e / 2)
by A41, A36, XREAL_1:8;
hence
||.((f /. x1) - (f /. x2)).|| < e
by A42, XXREAL_0:2;
verum
end;
end;
assume A43:
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 ) )
; f is continuous
for x being Point of V holds f is_continuous_at x
hence
f is continuous
by TMAP_1:50; verum