:: Monotonic and Continuous Real Function
:: by Jaros{\l}aw Kotowicz
::
:: Received January 10, 1991
:: Copyright (c) 1991-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, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, RCOMP_1, XBOOLE_0,
RELAT_1, TARSKI, SEQ_2, LIMFUNC1, FUNCT_1, XXREAL_0, ORDINAL2, CARD_1,
PROB_1, XXREAL_1, ARYTM_1, ARYTM_3, COMPLEX1, FCONT_1, FUNCT_2, VALUED_0,
SEQM_3, NAT_1, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, PROB_1, REAL_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1,
RELSET_1, COMSEQ_2, SEQ_2, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1,
LIMFUNC1, XXREAL_0, RFUNCT_2;
constructors PARTFUN1, REAL_1, COMPLEX1, NAT_1, SEQ_2, PROB_1, RCOMP_1,
PARTFUN2, RFUNCT_2, FCONT_1, LIMFUNC1, VALUED_1, XXREAL_2, RELSET_1,
BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
RCOMP_1, RFUNCT_2, VALUED_1, FUNCT_2, VALUED_0, XXREAL_2, RELAT_1, SEQ_1,
SEQ_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve x,X for set;
reserve x0,r1,r2,g,g1,g2,p,s for Real;
reserve r for Real;
reserve n,m for Nat;
reserve a,b,d for Real_Sequence;
reserve f for PartFunc of REAL,REAL;
registration
cluster [#] REAL -> closed;
cluster empty -> closed for Subset of REAL;
end;
registration
cluster [#] REAL -> open;
cluster empty -> open for Subset of REAL;
end;
registration
let r;
cluster right_closed_halfline(r) -> closed;
cluster left_closed_halfline(r) -> closed;
cluster right_open_halfline(r) -> open;
cluster halfline(r) -> open;
end;
theorem :: FCONT_3:1
g in ].x0 - r,x0 + r.[ implies |.g-x0.| < r;
theorem :: FCONT_3:2
g in ].x0 - r,x0 + r.[ implies g - x0 in ].-r,r.[;
theorem :: FCONT_3:3
g = x0 + r1 & |.r1.| < r implies 0 < r & g in ].x0 - r,x0 + r.[;
theorem :: FCONT_3:4
g - x0 in ].-r,r.[ implies 0 < r & g in ].x0 - r,x0 + r.[;
theorem :: FCONT_3:5
for x0 be Real holds (for n holds a.n = x0 - p/(n+1))
implies a is convergent & lim a = x0;
theorem :: FCONT_3:6
for x0 be Real holds (for n holds a.n = x0 + p/(n+1))
implies a is convergent & lim a = x0;
theorem :: FCONT_3:7
f is_continuous_in x0 & f.x0 <> r & (ex N be Neighbourhood of x0 st N
c= dom f) implies ex N be Neighbourhood of x0 st N c= dom f & for g st g in N
holds f.g <> r;
theorem :: FCONT_3:8
f|X is increasing or f|X is decreasing implies f|X is one-to-one;
theorem :: FCONT_3:9
for f be one-to-one PartFunc of REAL,REAL st f|X is increasing
holds (f|X)"|(f.:X) is increasing;
theorem :: FCONT_3:10
for f be one-to-one PartFunc of REAL,REAL st f|X is decreasing
holds (f|X)"|(f.:X) is decreasing;
theorem :: FCONT_3:11
X c= dom f & f|X is monotone & (ex p st f.:X =
left_open_halfline(p)) implies f|X is continuous;
theorem :: FCONT_3:12
X c= dom f & f|X is monotone & (ex p st f.:X =
right_open_halfline(p)) implies f|X is continuous;
theorem :: FCONT_3:13
X c= dom f & f|X is monotone & (ex p st f.:X =
left_closed_halfline(p)) implies f|X is continuous;
theorem :: FCONT_3:14
X c= dom f & f|X is monotone & (ex p st f.:X =
right_closed_halfline(p)) implies f|X is continuous;
theorem :: FCONT_3:15
X c= dom f & f|X is monotone & (ex p,g st f.:X = ].p,g.[)
implies f|X is continuous;
theorem :: FCONT_3:16
X c= dom f & f|X is monotone & f.:X = REAL implies f|X is continuous;
theorem :: FCONT_3:17
for f be one-to-one PartFunc of REAL,REAL st (f|].p,g.[ is increasing
or f|].p,g.[ is decreasing) & ].p,g.[ c= dom f holds (f|].p,g.[)"|(f.:].p,g.[)
is continuous;
theorem :: FCONT_3:18
for f be one-to-one PartFunc of REAL,REAL st (f|left_open_halfline p
is increasing or f|left_open_halfline p is decreasing) & left_open_halfline(p)
c= dom f holds (f|left_open_halfline(p))"|(f.:left_open_halfline(p)) is
continuous;
theorem :: FCONT_3:19
for f be one-to-one PartFunc of REAL,REAL st (f|right_open_halfline p
is increasing or f|right_open_halfline p is decreasing) & right_open_halfline(p
) c= dom f holds (f|right_open_halfline(p))"|(f.:right_open_halfline(p)) is
continuous;
theorem :: FCONT_3:20
for f be one-to-one PartFunc of REAL,REAL st (f|left_closed_halfline p
is increasing or f|left_closed_halfline p is decreasing) & left_closed_halfline
(p) c= dom f holds (f|left_closed_halfline(p))"|(f.:left_closed_halfline(p)) is
continuous;
theorem :: FCONT_3:21
for f be one-to-one PartFunc of REAL,REAL st (f|right_closed_halfline
p is increasing or f|right_closed_halfline p is decreasing) &
right_closed_halfline(p) c= dom f holds (f|right_closed_halfline(p))"|(f.:
right_closed_halfline(p)) is continuous;
theorem :: FCONT_3:22
for f be one-to-one PartFunc of REAL,REAL st (f|[#]REAL is increasing
or f|[#]REAL is decreasing) & f is total holds f"|rng f is continuous;
theorem :: FCONT_3:23
].p,g.[ c= dom f & f|].p,g.[ is continuous & (f|].p,g.[ is increasing
or f|].p,g.[ is decreasing) implies rng (f|].p,g.[) is open;
theorem :: FCONT_3:24
left_open_halfline(p) c= dom f & f|left_open_halfline p is continuous
& (f|left_open_halfline p is increasing or f|left_open_halfline p is decreasing
) implies rng (f|left_open_halfline(p)) is open;
theorem :: FCONT_3:25
right_open_halfline(p) c= dom f & f|right_open_halfline p is
continuous & (f|right_open_halfline p is increasing or f|right_open_halfline p
is decreasing) implies rng (f|right_open_halfline(p)) is open;
theorem :: FCONT_3:26
[#](REAL) c= dom f & f|[#]REAL is continuous & (f|[#]REAL is
increasing or f|[#]REAL is decreasing) implies rng f is open;