:: Real Function Continuity
:: by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2016 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.];