The abstract of the Mizar article:

Real Function Uniform Continuity

by

Jaroslaw Kotowicz, and

Konrad Raczkowski

Received June 18, 1990

MML identifier: FCONT_2

[ Mizar article, MML identifier index ]

environ

 vocabulary SEQ_1, PARTFUN1, RELAT_1, ABSVALUE, ARYTM_1, FUNCT_1, BOOLE,
      ARYTM_3, SQUARE_1, RFUNCT_1, ARYTM, FCONT_1, COMPTS_1, SEQ_2, ORDINAL2,
      SEQM_3, SEQ_4, PARTFUN2, RCOMP_1, FINSEQ_1, LATTICES, RFUNCT_2, FCONT_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, FUNCT_1, ABSVALUE, RELSET_1, SQUARE_1, PARTFUN1, SEQ_1,
      SEQ_2, SEQM_3, SEQ_4, PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1, FCONT_1;
 constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, SEQ_4, SQUARE_1,
      PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1, FCONT_1, PARTFUN1, MEMBERED,
      XBOOLE_0;
 clusters RELSET_1, RFUNCT_2, PARTFUN2, XREAL_0, SEQ_1, SEQM_3, NAT_1,
      MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve n,m for Nat;
 reserve x, X,X1,Z,Z1 for set;
 reserve s,g,r,t,p,x0,x1,x2 for Real;
 reserve s1,s2,q1 for Real_Sequence;
 reserve Y for Subset of REAL;
 reserve f,f1,f2 for PartFunc of REAL,REAL;

definition let f,X;
 pred f is_uniformly_continuous_on X means
:: FCONT_2:def 1
 X c= dom f & for r st 0<r ex s st 0<s & for x1,x2 st x1 in X & x2 in X &
 abs(x1 - x2) < s holds abs(f.x1 - f.x2) < r;
end;

canceled;

theorem :: FCONT_2:2
f is_uniformly_continuous_on X & X1 c= X implies
f is_uniformly_continuous_on X1;

theorem :: FCONT_2:3
  f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies
f1+f2 is_uniformly_continuous_on X/\X1;

theorem :: FCONT_2:4
  f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies
f1-f2 is_uniformly_continuous_on X/\X1;

theorem :: FCONT_2:5
f is_uniformly_continuous_on X implies p(#)f is_uniformly_continuous_on X;

theorem :: FCONT_2:6
  f is_uniformly_continuous_on X implies -f is_uniformly_continuous_on X;

theorem :: FCONT_2:7
  f is_uniformly_continuous_on X implies abs(f) is_uniformly_continuous_on X;

theorem :: FCONT_2:8
  f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 &
f1 is_bounded_on Z & f2 is_bounded_on Z1 implies
f1(#)f2 is_uniformly_continuous_on X/\Z/\X1/\Z1;

theorem :: FCONT_2:9
f is_uniformly_continuous_on X implies f is_continuous_on X;

theorem :: FCONT_2:10
f is_Lipschitzian_on X implies f is_uniformly_continuous_on X;

theorem :: FCONT_2:11
for f,Y st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y;

canceled;

theorem :: FCONT_2:13
  Y c= dom f & Y is compact & f is_uniformly_continuous_on Y implies
 f.:Y is compact;

theorem :: FCONT_2:14
  for f,Y st Y <> {} & Y c= dom f & Y is compact &
 f is_uniformly_continuous_on Y ex x1,x2 st x1 in Y & x2 in Y &
  f.x1 = upper_bound (f.:Y) & f.x2 = lower_bound (f.:Y);

theorem :: FCONT_2:15
  X c= dom f & f is_constant_on X implies f is_uniformly_continuous_on X;

theorem :: FCONT_2:16
p<=
g & f is_continuous_on [.p,g.] implies for r st r in [.f.p,f.g.] \/ [.f.g,f.p.]
ex s st s in [.p,g.] & r = f.s;

theorem :: FCONT_2:17
p<=g & f is_continuous_on [.p,g.] implies
for r st r in [.(lower_bound (f.:[.p,g.])),(upper_bound (f.:[.p,g.])).]
ex s st s in [.p,g.] & r = f.s;

theorem :: FCONT_2:18
f is one-to-one & p<=g & f is_continuous_on [.p,g.] implies
f is_increasing_on [.p,g.] or f is_decreasing_on [.p,g.];

theorem :: FCONT_2:19
  f is one-to-one & p<=g & f is_continuous_on [.p,g.] implies
(lower_bound (f.:[.p,g.])=f.p & upper_bound (f.:[.p,g.])=f.g) or
(lower_bound (f.:[.p,g.])=f.g & upper_bound (f.:[.p,g.])=f.p);

theorem :: FCONT_2:20
p<=g & f is_continuous_on [.p,g.] implies
f.:[.p,g.]=[.lower_bound (f.:[.p,g.]),upper_bound (f.:[.p,g.]).];

theorem :: FCONT_2:21
  for f be one-to-one PartFunc of REAL,REAL st p<=g & f is_continuous_on [.p,g
.]
 holds f" is_continuous_on [.lower_bound (f.:[.p,g.]),upper_bound (f.:
[.p,g.]).];