let X be set ; for f being PartFunc of REAL,REAL holds
( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) ) )
let f be PartFunc of REAL,REAL; ( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) ) )
thus
( f | X is uniformly_continuous implies for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) ) )
( ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) ) ) implies f | X is uniformly_continuous )proof
assume A1:
f | X is
uniformly_continuous
;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) )
let r be
Real;
( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) ) )
assume
0 < r
;
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) )
then consider s being
Real such that A2:
0 < s
and A3:
for
x1,
x2 being
Real st
x1 in dom (f | X) &
x2 in dom (f | X) &
|.(x1 - x2).| < s holds
|.(((f | X) . x1) - ((f | X) . x2)).| < r
by A1;
take
s
;
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) )
thus
0 < s
by A2;
for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r
let x1,
x2 be
Real;
( x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s implies |.((f . x1) - (f . x2)).| < r )
assume that A4:
x1 in dom (f | X)
and A5:
x2 in dom (f | X)
;
( not |.(x1 - x2).| < s or |.((f . x1) - (f . x2)).| < r )
A6:
(f | X) . x2 = f . x2
by A5, FUNCT_1:47;
(f | X) . x1 = f . x1
by A4, FUNCT_1:47;
hence
( not
|.(x1 - x2).| < s or
|.((f . x1) - (f . x2)).| < r )
by A3, A4, A5, A6;
verum
end;
assume A7:
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) )
; f | X is uniformly_continuous
let r be Real; FCONT_2:def 1 ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.(((f | X) . x1) - ((f | X) . x2)).| < r ) ) )
assume
0 < r
; ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.(((f | X) . x1) - ((f | X) . x2)).| < r ) )
then consider s being Real such that
A8:
0 < s
and
A9:
for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r
by A7;
take
s
; ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.(((f | X) . x1) - ((f | X) . x2)).| < r ) )
thus
0 < s
by A8; for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.(((f | X) . x1) - ((f | X) . x2)).| < r
let x1, x2 be Real; ( x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s implies |.(((f | X) . x1) - ((f | X) . x2)).| < r )
assume that
A10:
x1 in dom (f | X)
and
A11:
x2 in dom (f | X)
; ( not |.(x1 - x2).| < s or |.(((f | X) . x1) - ((f | X) . x2)).| < r )
A12:
(f | X) . x2 = f . x2
by A11, FUNCT_1:47;
(f | X) . x1 = f . x1
by A10, FUNCT_1:47;
hence
( not |.(x1 - x2).| < s or |.(((f | X) . x1) - ((f | X) . x2)).| < r )
by A9, A10, A11, A12; verum