NFCONT_2: The Uniform Continuity of Functions on Normed Linear Spaces

:: The Uniform Continuity of Functions on Normed Linear Spaces
:: by Takaya Nishiyama , Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received April 6, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, NORMSP_1, PARTFUN1, NAT_1, PRE_TOPC, TARSKI, RELAT_1, CARD_1, ARYTM_3, ARYTM_1, STRUCT_0, COMPLEX1, XBOOLE_0, XXREAL_0, VALUED_1, SUPINF_2, FUNCT_1, CFCONT_1, NFCONT_1, RCOMP_1, VALUED_0, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, SEQ_4, LOPBAN_1, ALI2, FUNCOP_1, POWER, SEQ_1, RSSPACE3, FUNCT_7, NFCONT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NUMBERS, COMPLEX1, REAL_1, NAT_1, RLVECT_1, STRUCT_0, PRE_TOPC, VALUED_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, ABIAN, POWER, VFUNCT_1, NORMSP_0, NORMSP_1, LOPBAN_1, RSSPACE3, NFCONT_1, RECDEF_1;
definitions ;
theorems TARSKI, ABSVALUE, XBOOLE_1, RLVECT_1, XCMPLX_1, FUNCOP_1, SEQ_1, SEQ_2, SERIES_1, NAT_1, POWER, RELAT_1, VFUNCT_1, LOPBAN_1, NORMSP_1, SEQ_4, FUNCT_2, RSSPACE3, FUNCT_7, LOPBAN_3, PARTFUN2, NFCONT_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, PARTFUN1, VALUED_0, NORMSP_0;
schemes SEQ_1, NAT_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, NORMSP_1, NAT_1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, SEQ_2, SEQ_4, POWER, ABIAN, VFUNCT_1, RSSPACE3, LOPBAN_3, NFCONT_1, RECDEF_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1;
expansions ;

definition

let X be set ;
let S, T be RealNormSpace;
let f be PartFunc of S,T;

pred f is_uniformly_continuous_on X means :: NFCONT_2:def 1
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) );

end;

:: deftheorem defines is_uniformly_continuous_on NFCONT_2:def 1 :

definition

let X be set ;
let S be RealNormSpace;
let f be PartFunc of the carrier of S,REAL;

pred f is_uniformly_continuous_on X means :: NFCONT_2:def 2
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) );

end;

:: deftheorem defines is_uniformly_continuous_on NFCONT_2:def 2 :

theorem Th1: :: NFCONT_2:1

for X, X1 being set
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1

proof end;

theorem :: NFCONT_2:2

for X, X1 being set
for S, T being RealNormSpace
for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem :: NFCONT_2:3

for X, X1 being set
for S, T being RealNormSpace
for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem Th4: :: NFCONT_2:4

for X being set
for p being Real
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
p (#) f is_uniformly_continuous_on X

proof end;

theorem :: NFCONT_2:5

for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X

proof end;

theorem :: NFCONT_2:6

for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X

proof end;

theorem Th7: :: NFCONT_2:7

for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_uniformly_continuous_on X holds
f is_continuous_on X

proof end;

theorem Th8: :: NFCONT_2:8

for X being set
for S being RealNormSpace
for f being PartFunc of the carrier of S,REAL st f is_uniformly_continuous_on X holds
f is_continuous_on X

proof end;

theorem Th9: :: NFCONT_2:9

for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X

proof end;

theorem :: NFCONT_2:10

for S, T being RealNormSpace
for f being PartFunc of S,T
for Y being Subset of S st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y

proof end;

theorem :: NFCONT_2:11

for S, T being RealNormSpace
for f being PartFunc of S,T
for Y being Subset of S st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact by Th7, NFCONT_1:32;

theorem :: NFCONT_2:12

for S being RealNormSpace
for f being PartFunc of the carrier of S,REAL
for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
ex x1, x2 being Point of S st
( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) by Th8, NFCONT_1:37;

theorem :: NFCONT_2:13

for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st X c= dom f & f | X is constant holds
f is_uniformly_continuous_on X by Th9, NFCONT_1:43;

definition

let M be non empty NORMSTR ;
let f be Function of M,M;

attr f is contraction means :Def3: :: NFCONT_2:def 3
ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) );

end;

:: deftheorem Def3 defines contraction NFCONT_2:def 3 :

registration

let M be RealNormSpace;

cluster Relation-like the carrier of M -defined the carrier of M -valued non empty Function-like total quasi_total contraction for Element of K16(K17( the carrier of M, the carrier of M));

existence

proof end;

end;

definition

let M be RealNormSpace;
mode Contraction of M is contraction Function of M,M;

end;

Lm1: ( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )

proof end;

Lm2: for K, L, e being Real st 0 < K & K < 1 & 0 < e holds
ex n being Nat st |.(L * (K to_power n)).| < e

proof end;

theorem Th14: :: NFCONT_2:14

for X being RealBanachSpace
for f being Function of X,X st f is Contraction of X holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )

proof end;

theorem :: NFCONT_2:15

for X being RealBanachSpace
for f being Function of X,X st ex n0 being Nat st iter (f,n0) is Contraction of X holds
ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )

proof end;

theorem :: NFCONT_2:16

for K, L, e being Real st 0 < K & K < 1 & 0 < e holds
ex n being Nat st |.(L * (K to_power n)).| < e by Lm2;