:: Monotonic and Continuous Real Function
:: by Jaros{\l}aw Kotowicz
::
:: Received January 10, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

registration
cluster [#] REAL ->  closed ;
coherence
 [#] REAL is closed
proofend;
cluster empty  ->  closed for Element of K19(REAL);
coherence
 for b1 being Subset of REAL st b1 is empty holds
b1 is closed
proofend;
end;

registration
cluster [#] REAL ->  open ;
coherence
 [#] REAL is open
proofend;
cluster empty  ->  open for Element of K19(REAL);
coherence
 for b1 being Subset of REAL st b1 is empty holds
b1 is open
proofend;
end;

registration
let r be real number ;
cluster right_closed_halfline r ->  closed ;
coherence
 right_closed_halfline r is closed
proofend;
cluster left_closed_halfline r ->  closed ;
coherence
 left_closed_halfline r is closed
proofend;
cluster right_open_halfline r ->  open ;
coherence
 right_open_halfline r is open
proofend;
cluster halfline r ->  open ;
coherence
 halfline r is open
proofend;
end;

theorem Th1: :: FCONT_3:1
for g, x0 being Real
for r being real number st g in ].(x0 - r),(x0 + r).[ holds
abs (g - x0) < r
proofend;

theorem :: FCONT_3:2
for g, x0 being Real
for r being real number st g in ].(x0 - r),(x0 + r).[ holds
g - x0 in ].(- r),r.[
proofend;

theorem Th3: :: FCONT_3:3
for g, x0, r1 being Real
for r being real number st g = x0 + r1 &amp; abs r1 < r holds
( 0 < r &amp; g in ].(x0 - r),(x0 + r).[ )
proofend;

theorem :: FCONT_3:4
for g, x0 being Real
for r being real number st g - x0 in ].(- r),r.[ holds
( 0 < r &amp; g in ].(x0 - r),(x0 + r).[ )
proofend;

theorem Th5: :: FCONT_3:5
for p being Real
for a being Real_Sequence
for x0 being real number st ( for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ) holds
( a is convergent &amp; lim a = x0 )
proofend;

theorem Th6: :: FCONT_3:6
for p being Real
for a being Real_Sequence
for x0 being real number st ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) holds
( a is convergent &amp; lim a = x0 )
proofend;

theorem :: FCONT_3:7
for x0 being Real
for r being real number
for f being PartFunc of REAL,REAL st f is_continuous_in x0 &amp; f . x0 <> r &amp; ex N being Neighbourhood of x0 st N c= dom f holds
ex N being Neighbourhood of x0 st
( N c= dom f &amp; ( for g being Real st g in N holds
f . g <> r ) )
proofend;

theorem :: FCONT_3:8
for X being set
for f being PartFunc of REAL,REAL st ( f | X is increasing or f | X is decreasing ) holds
f | X is one-to-one
proofend;

theorem Th9: :: FCONT_3:9
for X being set
for f being one-to-one PartFunc of REAL,REAL st f | X is increasing holds
((f | X) ") | (f .: X) is increasing
proofend;

theorem Th10: :: FCONT_3:10
for X being set
for f being one-to-one PartFunc of REAL,REAL st f | X is decreasing holds
((f | X) ") | (f .: X) is decreasing
proofend;

theorem Th11: :: FCONT_3:11
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is monotone &amp; ex p being Real st f .: X = left_open_halfline p holds
f | X is continuous
proofend;

theorem Th12: :: FCONT_3:12
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is monotone &amp; ex p being Real st f .: X = right_open_halfline p holds
f | X is continuous
proofend;

theorem Th13: :: FCONT_3:13
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is monotone &amp; ex p being Real st f .: X = left_closed_halfline p holds
f | X is continuous
proofend;

theorem Th14: :: FCONT_3:14
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is monotone &amp; ex p being Real st f .: X = right_closed_halfline p holds
f | X is continuous
proofend;

theorem Th15: :: FCONT_3:15
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is monotone &amp; ex p, g being Real st f .: X = ].p,g.[ holds
f | X is continuous
proofend;

theorem Th16: :: FCONT_3:16
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is monotone &amp; f .: X = REAL holds
f | X is continuous
proofend;

theorem :: FCONT_3:17
for p, g being Real
for f being one-to-one PartFunc of REAL,REAL st ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) &amp; ].p,g.[ c= dom f holds
((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous
proofend;

theorem :: FCONT_3:18
for p being Real
for f being one-to-one PartFunc of REAL,REAL st ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) &amp; left_open_halfline p c= dom f holds
((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous
proofend;

theorem :: FCONT_3:19
for p being Real
for f being one-to-one PartFunc of REAL,REAL st ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) &amp; right_open_halfline p c= dom f holds
((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous
proofend;

theorem :: FCONT_3:20
for p being Real
for f being one-to-one PartFunc of REAL,REAL st ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) &amp; left_closed_halfline p c= dom f holds
((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous
proofend;

theorem :: FCONT_3:21
for p being Real
for f being one-to-one PartFunc of REAL,REAL st ( f | (right_closed_halfline p) is increasing or f | (right_closed_halfline p) is decreasing ) &amp; right_closed_halfline p c= dom f holds
((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous
proofend;

theorem :: FCONT_3:22
for f being one-to-one PartFunc of REAL,REAL st ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) &amp; f is total holds
(f ") | (rng f) is continuous
proofend;

theorem :: FCONT_3:23
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f &amp; f | ].p,g.[ is continuous &amp; ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) holds
rng (f | ].p,g.[) is open
proofend;

theorem :: FCONT_3:24
for p being Real
for f being PartFunc of REAL,REAL st left_open_halfline p c= dom f &amp; f | (left_open_halfline p) is continuous &amp; ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) holds
rng (f | (left_open_halfline p)) is open
proofend;

theorem :: FCONT_3:25
for p being Real
for f being PartFunc of REAL,REAL st right_open_halfline p c= dom f &amp; f | (right_open_halfline p) is continuous &amp; ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) holds
rng (f | (right_open_halfline p)) is open
proofend;

theorem :: FCONT_3:26
for f being PartFunc of REAL,REAL st [#] REAL c= dom f &amp; f | ([#] REAL) is continuous &amp; ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) holds
rng f is open
proofend;