:: Real Function Uniform Continuity :: by Jaros{\l}aw Kotowicz and Konrad Raczkowski :: :: Received June 18, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3, RELAT_1, COMPLEX1, ARYTM_1, FUNCT_1, TARSKI, XBOOLE_0, XXREAL_0, VALUED_1, XXREAL_2, ORDINAL2, FCONT_1, RCOMP_1, VALUED_0, SEQ_2, FUNCT_2, NAT_1, SEQ_4, XXREAL_1, FUNCOP_1, ORDINAL4, SEQM_3, FCONT_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCOP_1, NUMBERS, XXREAL_0, XREAL_0, XXREAL_2, VALUED_0, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, PARTFUN2, RFUNCT_1, RFUNCT_2, RCOMP_1, FCONT_1, RECDEF_1; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQM_3, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, FCONT_1, RECDEF_1, XXREAL_2, RELSET_1, BINOP_2, COMSEQ_2; registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RFUNCT_2, VALUED_0, VALUED_1, FUNCT_2, ORDINAL1, XXREAL_2, FCONT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve n,m for Element of 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; attr f is uniformly_continuous means :: FCONT_2:def 1 for r st 0 {} & Y c= dom f & Y is compact & f|Y is uniformly_continuous 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:14 X c= dom f & f|X is constant implies f|X is uniformly_continuous; theorem :: FCONT_2:15 p<= g & [.p,g.] c= dom f & f|[.p,g.] is continuous 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:16 p<=g & [.p,g.] c= dom f & f|[.p,g.] is continuous 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:17 f is one-to-one & [.p,g.] c= dom f & p<=g & f|[.p,g.] is continuous implies f|[.p,g.] is increasing or f|[.p,g.] is decreasing; theorem :: FCONT_2:18 f is one-to-one & p<=g & [.p,g.] c= dom f & f|[.p,g.] is continuous 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; ::$N Darboux Theorem theorem :: FCONT_2:19 p<=g & [.p,g.] c= dom f & f|[.p,g.] is continuous implies f.:[.p ,g.]=[.lower_bound (f.:[.p,g.]),upper_bound (f.:[.p,g.]).]; theorem :: FCONT_2:20 for f be one-to-one PartFunc of REAL,REAL st p<=g & [.p,g.] c= dom f & f|[.p,g.] is continuous holds f"|[.lower_bound (f.:[.p,g.]),upper_bound (f.:[.p ,g.]).] is continuous;