:: 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;