:: Real Function Continuity :: by Konrad Raczkowski and Pawe{\l} Sadowski :: :: 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, SEQ_1, PARTFUN1, RELAT_1, TARSKI, SEQ_2, ORDINAL2, FUNCT_2, FUNCT_1, XBOOLE_0, XXREAL_0, NAT_1, ARYTM_3, CARD_1, COMPLEX1, ARYTM_1, REAL_1, RCOMP_1, XXREAL_1, VALUED_1, ORDINAL4, ZFMISC_1, VALUED_0, SEQ_4, XXREAL_2, SQUARE_1, SEQM_3, FCONT_1, JGRAPH_2, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, ZFMISC_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, SQUARE_1, PARTFUN2, RFUNCT_1, RCOMP_1, RECDEF_1, RFUNCT_2; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, SEQ_2, SEQM_3, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, RECDEF_1, RELSET_1, COMSEQ_2, NUMBERS; registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, RFUNCT_2, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, RELAT_1, RFUNCT_1, SEQ_2, FUNCT_1, ZFMISC_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve n,m,k for Element of NAT; reserve x, X,X1,Z,Z1 for set; reserve s,g,r,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,x0; pred f is_continuous_in x0 means :: FCONT_1:def 1 for s1 st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds f/*s1 is convergent & f.x0 = lim (f/*s1); end; theorem :: FCONT_1:1 x0 in X & f is_continuous_in x0 implies f|X is_continuous_in x0; theorem :: FCONT_1:2 f is_continuous_in x0 iff for s1 st rng s1 c= dom f & s1 is convergent & lim s1=x0 & (for n being Nat holds s1.n<>x0) holds f/*s1 is convergent & f.x0=lim(f/*s1); theorem :: FCONT_1:3 f is_continuous_in x0 iff for r st 00 implies f^ is_continuous_in x0; theorem :: FCONT_1:11 x0 in dom f2 & f1 is_continuous_in x0 & f1.x0<>0 & f2 is_continuous_in x0 implies f2/f1 is_continuous_in x0; theorem :: FCONT_1:12 x0 in dom (f2*f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1.x0 implies f2*f1 is_continuous_in x0; definition let f; attr f is continuous means :: FCONT_1:def 2 for x0 st x0 in dom f holds f is_continuous_in x0; end; theorem :: FCONT_1:13 for X,f st X c= dom f holds f|X is continuous iff for s1 st rng s1 c= X & s1 is convergent & lim s1 in X holds f/*s1 is convergent & f.(lim s1) = lim (f/*s1); theorem :: FCONT_1:14 X c= dom f implies (f|X is continuous iff for x0,r st x0 in X & 0 continuous for PartFunc of REAL,REAL; end; registration cluster continuous for PartFunc of REAL,REAL; end; registration let f be continuous PartFunc of REAL,REAL, X be set; cluster f|X -> continuous for PartFunc of REAL,REAL; end; theorem :: FCONT_1:15 f|X is continuous iff f|X|X is continuous; theorem :: FCONT_1:16 f|X is continuous & X1 c= X implies f|X1 is continuous; registration cluster empty -> continuous for PartFunc of REAL,REAL; end; registration let f; let X be trivial set; cluster f|X -> continuous for PartFunc of REAL,REAL; end; theorem :: FCONT_1:17 f|{x0} is continuous; registration let f1,f2 be continuous PartFunc of REAL,REAL; cluster f1+f2 -> continuous for PartFunc of REAL,REAL; cluster f1-f2 -> continuous for PartFunc of REAL,REAL; cluster f1(#)f2 -> continuous for PartFunc of REAL,REAL; end; theorem :: FCONT_1:18 for X,f1,f2 st X c= dom f1 /\ dom f2 & f1|X is continuous & f2|X is continuous holds (f1+f2)|X is continuous & (f1-f2)|X is continuous & (f1(#) f2)|X is continuous; theorem :: FCONT_1:19 for X,X1,f1,f2 st X c= dom f1 & X1 c= dom f2 & f1|X is continuous & f2 |X1 is continuous holds (f1+f2)|(X /\ X1) is continuous & (f1-f2)|(X /\ X1) is continuous & (f1(#)f2)|(X /\ X1) is continuous; registration let f be continuous PartFunc of REAL,REAL; let r; cluster r(#)f -> continuous for PartFunc of REAL,REAL; end; theorem :: FCONT_1:20 for r,X,f st X c= dom f & f|X is continuous holds (r(#)f)|X is continuous; theorem :: FCONT_1:21 X c= dom f & f|X is continuous implies (abs f)|X is continuous & (-f)| X is continuous; theorem :: FCONT_1:22 f|X is continuous & f"{0} = {} implies f^|X is continuous; theorem :: FCONT_1:23 f|X is continuous & (f|X)"{0} = {} implies f^|X is continuous; theorem :: FCONT_1:24 X c= dom f1 /\ dom f2 & f1|X is continuous & f1"{0} = {} & f2|X is continuous implies (f2/f1)|X is continuous; registration let f1,f2 be continuous PartFunc of REAL,REAL; cluster f2*f1 -> continuous for PartFunc of REAL,REAL; end; theorem :: FCONT_1:25 f1|X is continuous & f2|(f1.:X) is continuous implies (f2*f1)|X is continuous ; theorem :: FCONT_1:26 f1|X is continuous & f2|X1 is continuous implies (f2*f1)|(X /\ (f1"X1) ) is continuous; theorem :: FCONT_1:27 f is total & (for x1,x2 holds f.(x1+x2) = f.x1 + f.x2) & (ex x0 st f is_continuous_in x0) implies f|REAL is continuous; theorem :: FCONT_1:28 for f st dom f is compact & f|dom f is continuous holds rng f is compact; theorem :: FCONT_1:29 Y c= dom f & Y is compact & f|Y is continuous implies (f.:Y) is compact; theorem :: FCONT_1:30 for f st dom f<>{} & (dom f) is compact & f|dom f is continuous ex x1,x2 st x1 in dom f & x2 in dom f & f.x1 = upper_bound (rng f) & f.x2 = lower_bound (rng f); ::$N Extreme value theorem theorem :: FCONT_1:31 for f,Y st Y<>{} & Y c= dom f & Y is compact & f|Y is continuous ex x1 ,x2 st x1 in Y & x2 in Y & f.x1 = upper_bound (f.:Y) & f.x2 = lower_bound (f.:Y ); definition let f; attr f is Lipschitzian means :: FCONT_1:def 3 ex r st 0 Lipschitzian for PartFunc of REAL,REAL; end; registration cluster empty for PartFunc of REAL,REAL; end; registration let f be Lipschitzian PartFunc of REAL,REAL, X be set; cluster f|X -> Lipschitzian for PartFunc of REAL,REAL; end; theorem :: FCONT_1:33 f|X is Lipschitzian & X1 c= X implies f|X1 is Lipschitzian; registration let f1,f2 be Lipschitzian PartFunc of REAL,REAL; cluster f1+f2 -> Lipschitzian for PartFunc of REAL,REAL; cluster f1-f2 -> Lipschitzian for PartFunc of REAL,REAL; end; theorem :: FCONT_1:34 f1|X is Lipschitzian & f2|X1 is Lipschitzian implies (f1+f2)|(X /\ X1) is Lipschitzian; theorem :: FCONT_1:35 f1|X is Lipschitzian & f2|X1 is Lipschitzian implies (f1-f2)|(X /\ X1) is Lipschitzian; registration let f1,f2 be bounded Lipschitzian PartFunc of REAL,REAL; cluster f1 (#) f2 -> Lipschitzian for PartFunc of REAL,REAL; end; theorem :: FCONT_1:36 f1|X is Lipschitzian & f2|X1 is Lipschitzian & f1|Z is bounded & f2|Z1 is bounded implies (f1(#)f2)|(X /\ Z /\ X1 /\ Z1) is Lipschitzian; registration let f be Lipschitzian PartFunc of REAL, REAL; let p; cluster p(#)f -> Lipschitzian for PartFunc of REAL, REAL; end; theorem :: FCONT_1:37 f|X is Lipschitzian & X c= dom f implies (p(#)f)|X is Lipschitzian; registration let f be Lipschitzian PartFunc of REAL, REAL; cluster abs f -> Lipschitzian for PartFunc of REAL, REAL; end; theorem :: FCONT_1:38 f|X is Lipschitzian implies -f|X is Lipschitzian & (abs f)|X is Lipschitzian; registration cluster constant -> Lipschitzian for PartFunc of REAL, REAL; end; registration let Y; cluster id Y -> Lipschitzian for PartFunc of REAL,REAL; end; registration ::$N Lipschitz continuity cluster Lipschitzian -> continuous for PartFunc of REAL, REAL; end; theorem :: FCONT_1:39 for f st (ex r st rng f = {r}) holds f is continuous; theorem :: FCONT_1:40 for f st (for x0 st x0 in dom f holds f.x0 = x0) holds f is continuous; theorem :: FCONT_1:41 (for x0 st x0 in X holds f.x0 = r*x0+p) implies f|X is continuous; theorem :: FCONT_1:42 (for x0 st x0 in dom f holds f.x0 = x0^2) implies f|dom f is continuous; theorem :: FCONT_1:43 X c= dom f & (for x0 st x0 in X holds f.x0 = x0^2) implies f|X is continuous; theorem :: FCONT_1:44 (for x0 st x0 in dom f holds f.x0 = |.x0.|) implies f is continuous; theorem :: FCONT_1:45 (for x0 st x0 in X holds f.x0 = |.x0.|) implies f|X is continuous; theorem :: FCONT_1:46 f|X is monotone & (ex p,g st p<=g & f.:X=[.p,g.]) implies f|X is continuous; theorem :: FCONT_1:47 for f being one-to-one PartFunc of REAL,REAL st p<=g & [.p,g.] c= dom f & (f|[.p,g.] is increasing or f|[.p,g.] is decreasing) holds (f|[.p,g.])"|(f .:[.p,g.]) is continuous; :: from definition let a,b be Real; func AffineMap(a,b) -> Function of REAL, REAL means :: FCONT_1:def 4 for x being Real holds it.x = a*x + b; end; registration let a,b be Real; cluster AffineMap(a,b) -> continuous; end; registration cluster continuous for Function of REAL, REAL; end; theorem :: FCONT_1:48 for a,b being Real holds AffineMap(a,b).0 = b; theorem :: FCONT_1:49 for a,b being Real holds AffineMap(a,b).1 = a+b; theorem :: FCONT_1:50 for a,b being Real st a<> 0 holds AffineMap(a,b) is one-to-one; theorem :: FCONT_1:51 for a,b,x,y being Real st a > 0 & x < y holds AffineMap(a,b).x < AffineMap(a,b).y; theorem :: FCONT_1:52 for a,b,x,y being Real st a < 0 & x < y holds AffineMap(a,b).x > AffineMap(a,b).y; theorem :: FCONT_1:53 for a,b,x,y being Real st a >= 0 & x <= y holds AffineMap (a,b).x <= AffineMap(a,b).y; theorem :: FCONT_1:54 for a,b,x,y being Real st a <= 0 & x <= y holds AffineMap(a,b). x >= AffineMap(a,b).y; theorem :: FCONT_1:55 for a,b being Real st a <> 0 holds rng AffineMap(a,b) = REAL; theorem :: FCONT_1:56 for a,b being Real st a <> 0 holds (AffineMap(a,b) qua Function)" = AffineMap(a",-b/a); theorem :: FCONT_1:57 for a,b being Real st a > 0 holds AffineMap(a,b).:[.0,1.] = [.b,a+b.];