:: FCONT_3 semantic presentation
begin
registration
cluster [#] REAL -> closed ;
coherence
[#] REAL is closed
proof
let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= [#] REAL or not a is convergent or lim a in [#] REAL )
thus ( not rng a c= [#] REAL or not a is convergent or lim a in [#] REAL ) ; ::_thesis: verum
end;
cluster empty -> closed for Element of K19(REAL);
coherence
for b1 being Subset of REAL st b1 is empty holds
b1 is closed
proof
let S be Subset of REAL; ::_thesis: ( S is empty implies S is closed )
assume A1: S is empty ; ::_thesis: S is closed
let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= S or not a is convergent or lim a in S )
assume that
A2: rng a c= S and
a is convergent ; ::_thesis: lim a in S
thus lim a in S by A1, A2, XBOOLE_1:3; ::_thesis: verum
end;
end;
registration
cluster [#] REAL -> open ;
coherence
[#] REAL is open
proof
([#] REAL) ` = {} REAL by XBOOLE_1:37;
hence [#] REAL is open by RCOMP_1:def_5; ::_thesis: verum
end;
cluster empty -> open for Element of K19(REAL);
coherence
for b1 being Subset of REAL st b1 is empty holds
b1 is open
proof
let S be Subset of REAL; ::_thesis: ( S is empty implies S is open )
assume S is empty ; ::_thesis: S is open
then S ` = [#] REAL ;
hence S is open by RCOMP_1:def_5; ::_thesis: verum
end;
end;
registration
let r be real number ;
cluster right_closed_halfline r -> closed ;
coherence
right_closed_halfline r is closed
proof
r in REAL by XREAL_0:def_1;
then reconsider b = NAT --> r as Real_Sequence by FUNCOP_1:45;
let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= right_closed_halfline r or not a is convergent or lim a in right_closed_halfline r )
assume that
A1: rng a c= right_closed_halfline r and
A2: a is convergent ; ::_thesis: lim a in right_closed_halfline r
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_b_._n_<=_a_._n
let n be Element of NAT ; ::_thesis: b . n <= a . n
a . n in rng a by VALUED_0:28;
then a . n in right_closed_halfline r by A1;
then a . n in { g1 where g1 is Real : r <= g1 } by XXREAL_1:232;
then ex r1 being Real st
( a . n = r1 & r <= r1 ) ;
hence b . n <= a . n by FUNCOP_1:7; ::_thesis: verum
end;
lim b = b . 0 by SEQ_4:26
.= r by FUNCOP_1:7 ;
then r <= lim a by A2, A3, SEQ_2:18;
then lim a in { g1 where g1 is Real : r <= g1 } ;
hence lim a in right_closed_halfline r by XXREAL_1:232; ::_thesis: verum
end;
cluster left_closed_halfline r -> closed ;
coherence
left_closed_halfline r is closed
proof
r in REAL by XREAL_0:def_1;
then reconsider b = NAT --> r as Real_Sequence by FUNCOP_1:45;
let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= left_closed_halfline r or not a is convergent or lim a in left_closed_halfline r )
assume that
A4: rng a c= left_closed_halfline r and
A5: a is convergent ; ::_thesis: lim a in left_closed_halfline r
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_a_._n_<=_b_._n
let n be Element of NAT ; ::_thesis: a . n <= b . n
a . n in rng a by VALUED_0:28;
then a . n in left_closed_halfline r by A4;
then a . n in { g where g is Real : g <= r } by XXREAL_1:231;
then ex r1 being Real st
( a . n = r1 & r1 <= r ) ;
hence a . n <= b . n by FUNCOP_1:7; ::_thesis: verum
end;
lim b = b . 0 by SEQ_4:26
.= r by FUNCOP_1:7 ;
then lim a <= r by A5, A6, SEQ_2:18;
then lim a in { g1 where g1 is Real : g1 <= r } ;
hence lim a in left_closed_halfline r by XXREAL_1:231; ::_thesis: verum
end;
cluster right_open_halfline r -> open ;
coherence
right_open_halfline r is open
proof
(right_open_halfline r) ` = left_closed_halfline r by XXREAL_1:224, XXREAL_1:296;
hence right_open_halfline r is open by RCOMP_1:def_5; ::_thesis: verum
end;
cluster halfline r -> open ;
coherence
halfline r is open
proof
(left_open_halfline r) ` = right_closed_halfline r by XXREAL_1:224, XXREAL_1:290;
hence halfline r is open by RCOMP_1:def_5; ::_thesis: verum
end;
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
proof
let g, x0 be Real; ::_thesis: for r being real number st g in ].(x0 - r),(x0 + r).[ holds
abs (g - x0) < r
let r be real number ; ::_thesis: ( g in ].(x0 - r),(x0 + r).[ implies abs (g - x0) < r )
assume g in ].(x0 - r),(x0 + r).[ ; ::_thesis: abs (g - x0) < r
then A1: ex g1 being Real st
( g1 = g & x0 - r < g1 & g1 < x0 + r ) ;
percases ( x0 <= g or g <= x0 ) ;
supposeA2: x0 <= g ; ::_thesis: abs (g - x0) < r
A3: g - x0 < (x0 + r) - x0 by A1, XREAL_1:14;
0 <= g - x0 by A2, XREAL_1:48;
hence abs (g - x0) < r by A3, ABSVALUE:def_1; ::_thesis: verum
end;
suppose g <= x0 ; ::_thesis: abs (g - x0) < r
then 0 <= x0 - g by XREAL_1:48;
then A4: x0 - g = abs (- (g - x0)) by ABSVALUE:def_1
.= abs (g - x0) by COMPLEX1:52 ;
x0 - g < x0 - (x0 - r) by A1, XREAL_1:15;
hence abs (g - x0) < r by A4; ::_thesis: verum
end;
end;
end;
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.[
proof
let g, x0 be Real; ::_thesis: for r being real number st g in ].(x0 - r),(x0 + r).[ holds
g - x0 in ].(- r),r.[
let r be real number ; ::_thesis: ( g in ].(x0 - r),(x0 + r).[ implies g - x0 in ].(- r),r.[ )
set r1 = g - x0;
assume g in ].(x0 - r),(x0 + r).[ ; ::_thesis: g - x0 in ].(- r),r.[
then abs (g - x0) < r by Th1;
then abs ((g - x0) - 0) < r ;
then g - x0 in ].(0 - r),(0 + r).[ by RCOMP_1:1;
hence g - x0 in ].(- r),r.[ ; ::_thesis: verum
end;
theorem Th3: :: FCONT_3:3
for g, x0, r1 being Real
for r being real number st g = x0 + r1 & abs r1 < r holds
( 0 < r & g in ].(x0 - r),(x0 + r).[ )
proof
let g, x0, r1 be Real; ::_thesis: for r being real number st g = x0 + r1 & abs r1 < r holds
( 0 < r & g in ].(x0 - r),(x0 + r).[ )
let r be real number ; ::_thesis: ( g = x0 + r1 & abs r1 < r implies ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) )
assume that
A1: g = x0 + r1 and
A2: abs r1 < r ; ::_thesis: ( 0 < r & g in ].(x0 - r),(x0 + r).[ )
thus 0 < r by A2, COMPLEX1:46; ::_thesis: g in ].(x0 - r),(x0 + r).[
abs (g - x0) < r by A1, A2;
hence g in ].(x0 - r),(x0 + r).[ by RCOMP_1:1; ::_thesis: verum
end;
theorem :: FCONT_3:4
for g, x0 being Real
for r being real number st g - x0 in ].(- r),r.[ holds
( 0 < r & g in ].(x0 - r),(x0 + r).[ )
proof
let g, x0 be Real; ::_thesis: for r being real number st g - x0 in ].(- r),r.[ holds
( 0 < r & g in ].(x0 - r),(x0 + r).[ )
let r be real number ; ::_thesis: ( g - x0 in ].(- r),r.[ implies ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) )
set r1 = g - x0;
assume g - x0 in ].(- r),r.[ ; ::_thesis: ( 0 < r & g in ].(x0 - r),(x0 + r).[ )
then ex g1 being Real st
( g1 = g - x0 & - r < g1 & g1 < r ) ;
then A1: abs (g - x0) < r by SEQ_2:1;
x0 + (g - x0) = g ;
hence ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) by A1, Th3; ::_thesis: verum
end;
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 & lim a = x0 )
proof
let p be Real; ::_thesis: 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 & lim a = x0 )
let a be Real_Sequence; ::_thesis: for x0 being real number st ( for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )
let x0 be real number ; ::_thesis: ( ( for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ) implies ( a is convergent & lim a = x0 ) )
deffunc H1( Element of NAT ) -> Element of REAL = p / ($1 + 1);
consider d being Real_Sequence such that
A1: for n being Element of NAT holds d . n = H1(n) from SEQ_1:sch_1();
x0 in REAL by XREAL_0:def_1;
then reconsider b = NAT --> x0 as Real_Sequence by FUNCOP_1:45;
assume A2: for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ; ::_thesis: ( a is convergent & lim a = x0 )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(b_-_d)_._n_=_a_._n
let n be Element of NAT ; ::_thesis: (b - d) . n = a . n
thus (b - d) . n = (b . n) - (d . n) by VALUED_1:15
.= x0 - (d . n) by FUNCOP_1:7
.= x0 - (p / (n + 1)) by A1
.= a . n by A2 ; ::_thesis: verum
end;
then A3: a = b - d by FUNCT_2:63;
A4: d is convergent by A1, SEQ_4:31;
hence a is convergent by A3, SEQ_2:11; ::_thesis: lim a = x0
A5: lim b = b . 0 by SEQ_4:26
.= x0 by FUNCOP_1:7 ;
lim d = 0 by A1, SEQ_4:31;
hence lim a = x0 - 0 by A4, A5, A3, SEQ_2:12
.= x0 ;
::_thesis: verum
end;
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 & lim a = x0 )
proof
let p be Real; ::_thesis: 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 & lim a = x0 )
let a be Real_Sequence; ::_thesis: for x0 being real number st ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )
let x0 be real number ; ::_thesis: ( ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) implies ( a is convergent & lim a = x0 ) )
deffunc H1( Element of NAT ) -> Element of REAL = p / ($1 + 1);
consider d being Real_Sequence such that
A1: for n being Element of NAT holds d . n = H1(n) from SEQ_1:sch_1();
x0 in REAL by XREAL_0:def_1;
then reconsider b = NAT --> x0 as Real_Sequence by FUNCOP_1:45;
assume A2: for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ; ::_thesis: ( a is convergent & lim a = x0 )
now__::_thesis:_for_n_being_Element_of_NAT_holds_(b_+_d)_._n_=_a_._n
let n be Element of NAT ; ::_thesis: (b + d) . n = a . n
thus (b + d) . n = (b . n) + (d . n) by VALUED_1:1
.= x0 + (d . n) by FUNCOP_1:7
.= x0 + (p / (n + 1)) by A1
.= a . n by A2 ; ::_thesis: verum
end;
then A3: a = b + d by FUNCT_2:63;
A4: d is convergent by A1, SEQ_4:31;
hence a is convergent by A3, SEQ_2:5; ::_thesis: lim a = x0
A5: lim b = b . 0 by SEQ_4:26
.= x0 by FUNCOP_1:7 ;
lim d = 0 by A1, SEQ_4:31;
hence lim a = x0 + 0 by A4, A5, A3, SEQ_2:6
.= x0 ;
::_thesis: verum
end;
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 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )
proof
let x0 be Real; ::_thesis: for r being real number
for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )
let r be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f implies ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) ) )
assume that
A1: f is_continuous_in x0 and
A2: f . x0 <> r ; ::_thesis: ( for N being Neighbourhood of x0 holds not N c= dom f or ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) ) )
given N being Neighbourhood of x0 such that A3: N c= dom f ; ::_thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )
consider p being real number such that
A4: 0 < p and
A5: N = ].(x0 - p),(x0 + p).[ by RCOMP_1:def_6;
defpred S1[ Element of NAT , real number ] means ( x0 - (p / ($1 + 1)) < $2 & $2 < x0 + (p / ($1 + 1)) & f . $2 = r & $2 in dom f );
assume A6: for N being Neighbourhood of x0 holds
( not N c= dom f or ex g being Real st
( g in N & f . g = r ) ) ; ::_thesis: contradiction
A7: for n being Element of NAT ex g being Real st S1[n,g]
proof
let n be Element of NAT ; ::_thesis: ex g being Real st S1[n,g]
A8: 0 <= n by NAT_1:2;
then reconsider Nn = ].(x0 - (p / (n + 1))),(x0 + (p / (n + 1))).[ as Neighbourhood of x0 by A4, RCOMP_1:def_6, XREAL_1:139;
A9: Nn c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Nn or x in dom f )
assume x in Nn ; ::_thesis: x in dom f
then consider g2 being Real such that
A10: g2 = x and
A11: x0 - (p / (n + 1)) < g2 and
A12: g2 < x0 + (p / (n + 1)) ;
0 + 1 <= n + 1 by A8, XREAL_1:7;
then A13: p / (n + 1) <= p / 1 by A4, XREAL_1:118;
then x0 + (p / (n + 1)) <= x0 + p by XREAL_1:7;
then A14: g2 < x0 + p by A12, XXREAL_0:2;
x0 - p <= x0 - (p / (n + 1)) by A13, XREAL_1:13;
then x0 - p < g2 by A11, XXREAL_0:2;
then x in N by A5, A10, A14;
hence x in dom f by A3; ::_thesis: verum
end;
then consider g being Real such that
A15: g in Nn and
A16: f . g = r by A6;
take g ; ::_thesis: S1[n,g]
ex g1 being Real st
( g1 = g & x0 - (p / (n + 1)) < g1 & g1 < x0 + (p / (n + 1)) ) by A15;
hence ( x0 - (p / (n + 1)) < g & g < x0 + (p / (n + 1)) ) ; ::_thesis: ( f . g = r & g in dom f )
thus f . g = r by A16; ::_thesis: g in dom f
thus g in dom f by A9, A15; ::_thesis: verum
end;
consider d being Real_Sequence such that
A17: for n being Element of NAT holds S1[n,d . n] from FUNCT_2:sch_3(A7);
A18: rng d c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng d or x in dom f )
assume x in rng d ; ::_thesis: x in dom f
then ex n being Element of NAT st x = d . n by FUNCT_2:113;
hence x in dom f by A17; ::_thesis: verum
end;
A19: now__::_thesis:_for_r2_being_real_number_st_0_<_r2_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((f_/*_d)_._m)_-_r)_<_r2
let r2 be real number ; ::_thesis: ( 0 < r2 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* d) . m) - r) < r2 )
assume A20: 0 < r2 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* d) . m) - r) < r2
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
abs (((f /* d) . m) - r) < r2
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((f /* d) . m) - r) < r2 )
assume n <= m ; ::_thesis: abs (((f /* d) . m) - r) < r2
abs (((f /* d) . m) - r) = abs ((f . (d . m)) - r) by A18, FUNCT_2:108
.= abs (r - r) by A17
.= 0 by ABSVALUE:2 ;
hence abs (((f /* d) . m) - r) < r2 by A20; ::_thesis: verum
end;
deffunc H1( Element of NAT ) -> Element of REAL = x0 - (p / ($1 + 1));
consider a being Real_Sequence such that
A21: for n being Element of NAT holds a . n = H1(n) from SEQ_1:sch_1();
deffunc H2( Element of NAT ) -> Element of REAL = x0 + (p / ($1 + 1));
consider b being Real_Sequence such that
A22: for n being Element of NAT holds b . n = H2(n) from SEQ_1:sch_1();
A23: now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_a_._n_<=_d_._n_&_d_._n_<=_b_._n_)
let n be Element of NAT ; ::_thesis: ( a . n <= d . n & d . n <= b . n )
( x0 - (p / (n + 1)) < d . n & d . n < x0 + (p / (n + 1)) ) by A17;
hence ( a . n <= d . n & d . n <= b . n ) by A21, A22; ::_thesis: verum
end;
A24: p is Real by XREAL_0:def_1;
then A25: ( b is convergent & lim b = x0 ) by A22, Th6;
( a is convergent & lim a = x0 ) by A24, A21, Th5;
then ( d is convergent & lim d = x0 ) by A25, A23, SEQ_2:19, SEQ_2:20;
then ( f /* d is convergent & f . x0 = lim (f /* d) ) by A1, A18, FCONT_1:def_1;
hence contradiction by A2, A19, SEQ_2:def_7; ::_thesis: verum
end;
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
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st ( f | X is increasing or f | X is decreasing ) holds
f | X is one-to-one
let f be PartFunc of REAL,REAL; ::_thesis: ( ( f | X is increasing or f | X is decreasing ) implies f | X is one-to-one )
assume A1: ( f | X is increasing or f | X is decreasing ) ; ::_thesis: f | X is one-to-one
now__::_thesis:_f_|_X_is_one-to-one
percases ( f | X is increasing or f | X is decreasing ) by A1;
supposeA2: f | X is increasing ; ::_thesis: f | X is one-to-one
now__::_thesis:_for_r1,_r2_being_Real_holds_
(_not_r1_in_dom_(f_|_X)_or_not_r2_in_dom_(f_|_X)_or_not_(f_|_X)_._r1_=_(f_|_X)_._r2_or_not_r1_<>_r2_)
given r1, r2 being Real such that A3: r1 in dom (f | X) and
A4: r2 in dom (f | X) and
A5: (f | X) . r1 = (f | X) . r2 and
A6: r1 <> r2 ; ::_thesis: contradiction
A7: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A3, A4, RELAT_1:61;
now__::_thesis:_contradiction
percases ( r1 < r2 or r2 < r1 ) by A6, XXREAL_0:1;
suppose r1 < r2 ; ::_thesis: contradiction
then f . r1 < f . r2 by A2, A7, RFUNCT_2:20;
then (f | X) . r1 < f . r2 by A3, FUNCT_1:47;
hence contradiction by A4, A5, FUNCT_1:47; ::_thesis: verum
end;
suppose r2 < r1 ; ::_thesis: contradiction
then f . r2 < f . r1 by A2, A7, RFUNCT_2:20;
then (f | X) . r2 < f . r1 by A4, FUNCT_1:47;
hence contradiction by A3, A5, FUNCT_1:47; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence f | X is one-to-one by PARTFUN1:8; ::_thesis: verum
end;
supposeA8: f | X is decreasing ; ::_thesis: f | X is one-to-one
now__::_thesis:_for_r1,_r2_being_Real_holds_
(_not_r1_in_dom_(f_|_X)_or_not_r2_in_dom_(f_|_X)_or_not_(f_|_X)_._r1_=_(f_|_X)_._r2_or_not_r1_<>_r2_)
given r1, r2 being Real such that A9: r1 in dom (f | X) and
A10: r2 in dom (f | X) and
A11: (f | X) . r1 = (f | X) . r2 and
A12: r1 <> r2 ; ::_thesis: contradiction
A13: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A9, A10, RELAT_1:61;
now__::_thesis:_contradiction
percases ( r1 < r2 or r2 < r1 ) by A12, XXREAL_0:1;
suppose r1 < r2 ; ::_thesis: contradiction
then f . r2 < f . r1 by A8, A13, RFUNCT_2:21;
then (f | X) . r2 < f . r1 by A10, FUNCT_1:47;
hence contradiction by A9, A11, FUNCT_1:47; ::_thesis: verum
end;
suppose r2 < r1 ; ::_thesis: contradiction
then f . r1 < f . r2 by A8, A13, RFUNCT_2:21;
then (f | X) . r1 < f . r2 by A9, FUNCT_1:47;
hence contradiction by A10, A11, FUNCT_1:47; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence f | X is one-to-one by PARTFUN1:8; ::_thesis: verum
end;
end;
end;
hence f | X is one-to-one ; ::_thesis: verum
end;
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
proof
let X be set ; ::_thesis: for f being one-to-one PartFunc of REAL,REAL st f | X is increasing holds
((f | X) ") | (f .: X) is increasing
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( f | X is increasing implies ((f | X) ") | (f .: X) is increasing )
assume that
A1: f | X is increasing and
A2: not ((f | X) ") | (f .: X) is increasing ; ::_thesis: contradiction
consider r1, r2 being Real such that
A3: r1 in (f .: X) /\ (dom ((f | X) ")) and
A4: r2 in (f .: X) /\ (dom ((f | X) ")) and
A5: r1 < r2 and
A6: ((f | X) ") . r1 >= ((f | X) ") . r2 by A2, RFUNCT_2:20;
A7: f .: X = rng (f | X) by RELAT_1:115;
then A8: r1 in rng (f | X) by A3, XBOOLE_0:def_4;
A9: r2 in rng (f | X) by A4, A7, XBOOLE_0:def_4;
A10: (f | X) | X is increasing by A1;
now__::_thesis:_contradiction
percases ( ((f | X) ") . r1 = ((f | X) ") . r2 or ((f | X) ") . r1 <> ((f | X) ") . r2 ) ;
suppose ((f | X) ") . r1 = ((f | X) ") . r2 ; ::_thesis: contradiction
then r1 = (f | X) . (((f | X) ") . r2) by A8, FUNCT_1:35
.= r2 by A9, FUNCT_1:35 ;
hence contradiction by A5; ::_thesis: verum
end;
supposeA11: ((f | X) ") . r1 <> ((f | X) ") . r2 ; ::_thesis: contradiction
A12: dom (f | X) = dom ((f | X) | X)
.= X /\ (dom (f | X)) by RELAT_1:61 ;
A13: ( ((f | X) ") . r2 in dom (f | X) & ((f | X) ") . r1 in dom (f | X) ) by A8, A9, PARTFUN2:60;
((f | X) ") . r2 < ((f | X) ") . r1 by A6, A11, XXREAL_0:1;
then (f | X) . (((f | X) ") . r2) < (f | X) . (((f | X) ") . r1) by A10, A13, A12, RFUNCT_2:20;
then r2 < (f | X) . (((f | X) ") . r1) by A9, FUNCT_1:35;
hence contradiction by A5, A8, FUNCT_1:35; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
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
proof
let X be set ; ::_thesis: for f being one-to-one PartFunc of REAL,REAL st f | X is decreasing holds
((f | X) ") | (f .: X) is decreasing
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( f | X is decreasing implies ((f | X) ") | (f .: X) is decreasing )
assume that
A1: f | X is decreasing and
A2: not ((f | X) ") | (f .: X) is decreasing ; ::_thesis: contradiction
consider r1, r2 being Real such that
A3: r1 in (f .: X) /\ (dom ((f | X) ")) and
A4: r2 in (f .: X) /\ (dom ((f | X) ")) and
A5: r1 < r2 and
A6: ((f | X) ") . r1 <= ((f | X) ") . r2 by A2, RFUNCT_2:21;
A7: f .: X = rng (f | X) by RELAT_1:115;
then A8: r1 in rng (f | X) by A3, XBOOLE_0:def_4;
A9: r2 in rng (f | X) by A4, A7, XBOOLE_0:def_4;
A10: (f | X) | X is decreasing by A1;
now__::_thesis:_contradiction
percases ( ((f | X) ") . r1 = ((f | X) ") . r2 or ((f | X) ") . r1 <> ((f | X) ") . r2 ) ;
suppose ((f | X) ") . r1 = ((f | X) ") . r2 ; ::_thesis: contradiction
then r1 = (f | X) . (((f | X) ") . r2) by A8, FUNCT_1:35
.= r2 by A9, FUNCT_1:35 ;
hence contradiction by A5; ::_thesis: verum
end;
supposeA11: ((f | X) ") . r1 <> ((f | X) ") . r2 ; ::_thesis: contradiction
A12: dom (f | X) = dom ((f | X) | X)
.= X /\ (dom (f | X)) by RELAT_1:61 ;
A13: ( ((f | X) ") . r2 in dom (f | X) & ((f | X) ") . r1 in dom (f | X) ) by A8, A9, PARTFUN2:60;
((f | X) ") . r2 > ((f | X) ") . r1 by A6, A11, XXREAL_0:1;
then (f | X) . (((f | X) ") . r2) < (f | X) . (((f | X) ") . r1) by A10, A13, A12, RFUNCT_2:21;
then r2 < (f | X) . (((f | X) ") . r1) by A9, FUNCT_1:35;
hence contradiction by A5, A8, FUNCT_1:35; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem Th11: :: FCONT_3:11
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_open_halfline p holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_open_halfline p holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_open_halfline p implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = left_open_halfline p or f | X is continuous )
given p being Real such that A3: f .: X = left_open_halfline p ; ::_thesis: f | X is continuous
set L = left_open_halfline p;
now__::_thesis:_f_|_X_is_continuous
percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5;
suppose f | X is non-decreasing ; ::_thesis: f | X is continuous
then A4: (f | X) | X is non-decreasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A5: x0 in REAL by XREAL_0:def_1;
A6: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A7: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then A8: (f | X) . x0 in left_open_halfline p by A3, RELAT_1:129;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A9: N2 c= left_open_halfline p by A8, RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A10: N3 c= N1 and
A11: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A12: r > 0 and
A13: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A14: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A15: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
A16: (f | X) . x0 < ((f | X) . x0) + r by A12, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A15, XXREAL_0:2;
then A17: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A14;
then ((f | X) . x0) + (r / 2) in N2 by A11, A13;
then consider r2 being Real such that
A18: ( r2 in dom (f | X) & r2 in X ) and
A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, A9, PARTFUN2:59;
A20: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A12, XREAL_1:29, XREAL_1:215;
A21: now__::_thesis:_not_r2_<_x0
assume A22: r2 < x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A18, XBOOLE_0:def_4;
hence contradiction by A4, A19, A20, A22, RFUNCT_2:22, A5; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A23: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A15, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A16, XXREAL_0:2;
then A24: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A23;
then ((f | X) . x0) - (r / 2) in N2 by A11, A13;
then consider r1 being Real such that
A25: ( r1 in dom (f | X) & r1 in X ) and
A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, A9, PARTFUN2:59;
A27: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
then A28: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A29: now__::_thesis:_not_x0_<_r1
assume A30: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A25, XBOOLE_0:def_4;
hence contradiction by A4, A26, A28, A30, RFUNCT_2:22, A5; ::_thesis: verum
end;
x0 <> r2 by A12, A19, XREAL_1:29, XREAL_1:215;
then x0 < r2 by A21, XXREAL_0:1;
then A31: r2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - r1),(r2 - x0));
A32: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A26, A27, XREAL_1:19;
then r1 < x0 by A29, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by A31, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A33: x in REAL by XREAL_0:def_1;
assume that
A34: x in dom (f | X) and
A35: x in N ; ::_thesis: (f | X) . x in N1
A36: x in X /\ (dom (f | X)) by A34, XBOOLE_1:28;
A37: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A35;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A38: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A38, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:24;
then A39: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A25, XBOOLE_0:def_4;
then A40: (f | X) . r1 <= (f | X) . x by A4, A39, A36, RFUNCT_2:22, A33;
x - x0 < min ((x0 - r1),(r2 - x0)) by A37, XREAL_1:19;
then x - x0 < r2 - x0 by A32, XXREAL_0:2;
then A41: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A18, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A4, A41, A36, RFUNCT_2:22, A33;
then A42: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A40;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24, A17, XXREAL_2:def_12;
then (f | X) . x in N3 by A13, A42;
hence (f | X) . x in N1 by A10; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
suppose f | X is non-increasing ; ::_thesis: f | X is continuous
then A43: (f | X) | X is non-increasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A44: x0 in REAL by XREAL_0:def_1;
A45: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A46: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then A47: (f | X) . x0 in left_open_halfline p by A3, RELAT_1:129;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A48: N2 c= left_open_halfline p by A47, RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A49: N3 c= N1 and
A50: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A51: r > 0 and
A52: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A53: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A54: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
A55: (f | X) . x0 < ((f | X) . x0) + r by A51, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A54, XXREAL_0:2;
then A56: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A53;
then ((f | X) . x0) + (r / 2) in N2 by A50, A52;
then consider r2 being Real such that
A57: ( r2 in dom (f | X) & r2 in X ) and
A58: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A45, A48, PARTFUN2:59;
A59: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A51, XREAL_1:29, XREAL_1:215;
A60: now__::_thesis:_not_r2_>_x0
assume A61: r2 > x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A46, A57, XBOOLE_0:def_4;
hence contradiction by A43, A58, A59, A61, RFUNCT_2:23, A44; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A62: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A54, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A55, XXREAL_0:2;
then A63: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62;
then ((f | X) . x0) - (r / 2) in N2 by A50, A52;
then consider r1 being Real such that
A64: ( r1 in dom (f | X) & r1 in X ) and
A65: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A45, A48, PARTFUN2:59;
A66: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
then A67: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A68: now__::_thesis:_not_x0_>_r1
assume A69: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A46, A64, XBOOLE_0:def_4;
hence contradiction by A43, A65, A67, A69, RFUNCT_2:23, A44; ::_thesis: verum
end;
x0 <> r2 by A51, A58, XREAL_1:29, XREAL_1:215;
then x0 > r2 by A60, XXREAL_0:1;
then A70: x0 - r2 > 0 by XREAL_1:50;
set R = min ((r1 - x0),(x0 - r2));
A71: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A65, A66, XREAL_1:19;
then r1 > x0 by A68, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by A70, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A72: x in REAL by XREAL_0:def_1;
assume that
A73: x in dom (f | X) and
A74: x in N ; ::_thesis: (f | X) . x in N1
A75: x in X /\ (dom (f | X)) by A73, XBOOLE_1:28;
A76: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A74;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A77: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) by A76, XREAL_1:19;
then x - x0 < r1 - x0 by A71, XXREAL_0:2;
then A78: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A64, XBOOLE_0:def_4;
then A79: (f | X) . r1 <= (f | X) . x by A43, A78, A75, RFUNCT_2:23, A72;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A77, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:24;
then A80: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A57, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A43, A80, A75, RFUNCT_2:23, A72;
then A81: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A65, A58, A79;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A63, A56, XXREAL_2:def_12;
then (f | X) . x in N3 by A52, A81;
hence (f | X) . x in N1 by A49; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
end;
end;
hence f | X is continuous ; ::_thesis: verum
end;
theorem Th12: :: FCONT_3:12
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_open_halfline p holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_open_halfline p holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = right_open_halfline p implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = right_open_halfline p or f | X is continuous )
given p being Real such that A3: f .: X = right_open_halfline p ; ::_thesis: f | X is continuous
set L = right_open_halfline p;
now__::_thesis:_f_|_X_is_continuous
percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5;
suppose f | X is non-decreasing ; ::_thesis: f | X is continuous
then A4: (f | X) | X is non-decreasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A5: x0 in REAL by XREAL_0:def_1;
A6: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A7: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then A8: (f | X) . x0 in right_open_halfline p by A3, RELAT_1:129;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A9: N2 c= right_open_halfline p by A8, RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A10: N3 c= N1 and
A11: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A12: r > 0 and
A13: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A14: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A15: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
A16: (f | X) . x0 < ((f | X) . x0) + r by A12, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A15, XXREAL_0:2;
then A17: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A14;
then ((f | X) . x0) + (r / 2) in N2 by A11, A13;
then consider r2 being Real such that
A18: ( r2 in dom (f | X) & r2 in X ) and
A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, A9, PARTFUN2:59;
A20: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A12, XREAL_1:29, XREAL_1:215;
A21: now__::_thesis:_not_r2_<_x0
assume A22: r2 < x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A18, XBOOLE_0:def_4;
hence contradiction by A4, A19, A20, A22, RFUNCT_2:22, A5; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A23: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A15, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A16, XXREAL_0:2;
then A24: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A23;
then ((f | X) . x0) - (r / 2) in N2 by A11, A13;
then consider r1 being Real such that
A25: ( r1 in dom (f | X) & r1 in X ) and
A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, A9, PARTFUN2:59;
A27: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
then A28: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A29: now__::_thesis:_not_x0_<_r1
assume A30: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A25, XBOOLE_0:def_4;
hence contradiction by A4, A26, A28, A30, RFUNCT_2:22, A5; ::_thesis: verum
end;
x0 <> r2 by A12, A19, XREAL_1:29, XREAL_1:215;
then x0 < r2 by A21, XXREAL_0:1;
then A31: r2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - r1),(r2 - x0));
A32: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A26, A27, XREAL_1:19;
then r1 < x0 by A29, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by A31, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A33: x in REAL by XREAL_0:def_1;
assume that
A34: x in dom (f | X) and
A35: x in N ; ::_thesis: (f | X) . x in N1
A36: x in X /\ (dom (f | X)) by A34, XBOOLE_1:28;
A37: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A35;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A38: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A38, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:24;
then A39: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A25, XBOOLE_0:def_4;
then A40: (f | X) . r1 <= (f | X) . x by A4, A39, A36, RFUNCT_2:22, A33;
x - x0 < min ((x0 - r1),(r2 - x0)) by A37, XREAL_1:19;
then x - x0 < r2 - x0 by A32, XXREAL_0:2;
then A41: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A18, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A4, A41, A36, RFUNCT_2:22, A33;
then A42: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A40;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24, A17, XXREAL_2:def_12;
then (f | X) . x in N3 by A13, A42;
hence (f | X) . x in N1 by A10; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
suppose f | X is non-increasing ; ::_thesis: f | X is continuous
then A43: (f | X) | X is non-increasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A44: x0 in REAL by XREAL_0:def_1;
A45: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A46: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then A47: (f | X) . x0 in right_open_halfline p by A3, RELAT_1:129;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A48: N2 c= right_open_halfline p by A47, RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A49: N3 c= N1 and
A50: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A51: r > 0 and
A52: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A53: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A54: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
A55: (f | X) . x0 < ((f | X) . x0) + r by A51, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A54, XXREAL_0:2;
then A56: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A53;
then ((f | X) . x0) + (r / 2) in N2 by A50, A52;
then consider r2 being Real such that
A57: ( r2 in dom (f | X) & r2 in X ) and
A58: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A45, A48, PARTFUN2:59;
A59: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A51, XREAL_1:29, XREAL_1:215;
A60: now__::_thesis:_not_r2_>_x0
assume A61: r2 > x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A46, A57, XBOOLE_0:def_4;
hence contradiction by A43, A58, A59, A61, RFUNCT_2:23, A44; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A62: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A54, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A55, XXREAL_0:2;
then A63: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62;
then ((f | X) . x0) - (r / 2) in N2 by A50, A52;
then consider r1 being Real such that
A64: ( r1 in dom (f | X) & r1 in X ) and
A65: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A45, A48, PARTFUN2:59;
A66: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
then A67: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A68: now__::_thesis:_not_x0_>_r1
assume A69: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A46, A64, XBOOLE_0:def_4;
hence contradiction by A43, A65, A67, A69, RFUNCT_2:23, A44; ::_thesis: verum
end;
x0 <> r2 by A51, A58, XREAL_1:29, XREAL_1:215;
then x0 > r2 by A60, XXREAL_0:1;
then A70: x0 - r2 > 0 by XREAL_1:50;
set R = min ((r1 - x0),(x0 - r2));
A71: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A65, A66, XREAL_1:19;
then r1 > x0 by A68, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by A70, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A72: x in REAL by XREAL_0:def_1;
assume that
A73: x in dom (f | X) and
A74: x in N ; ::_thesis: (f | X) . x in N1
A75: x in X /\ (dom (f | X)) by A73, XBOOLE_1:28;
A76: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A74;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A77: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) by A76, XREAL_1:19;
then x - x0 < r1 - x0 by A71, XXREAL_0:2;
then A78: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A64, XBOOLE_0:def_4;
then A79: (f | X) . r1 <= (f | X) . x by A43, A78, A75, RFUNCT_2:23, A72;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A77, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:24;
then A80: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A57, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A43, A80, A75, RFUNCT_2:23, A72;
then A81: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A65, A58, A79;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A63, A56, XXREAL_2:def_12;
then (f | X) . x in N3 by A52, A81;
hence (f | X) . x in N1 by A49; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
end;
end;
hence f | X is continuous ; ::_thesis: verum
end;
theorem Th13: :: FCONT_3:13
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = left_closed_halfline p or f | X is continuous )
given p being Real such that A3: f .: X = left_closed_halfline p ; ::_thesis: f | X is continuous
set L = left_open_halfline p;
set l = left_closed_halfline p;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A4: x0 in REAL by XREAL_0:def_1;
A5: (f | X) .: X = f .: X by RELAT_1:129;
A6: left_open_halfline p c= left_closed_halfline p by XXREAL_1:21;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A7: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then (f | X) . x0 in {p} \/ (left_open_halfline p) by A3, A5, XXREAL_1:423;
then A8: ( (f | X) . x0 in {p} or (f | X) . x0 in left_open_halfline p ) by XBOOLE_0:def_3;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_
(f_|_X)_._r1_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_
(f_|_X)_._r1_in_N1
percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5;
suppose f | X is non-decreasing ; ::_thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1
then A9: (f | X) | X is non-decreasing ;
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
percases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1;
suppose (f | X) . x0 in left_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider N2 being Neighbourhood of (f | X) . x0 such that
A10: N2 c= left_open_halfline p by RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A11: N3 c= N1 and
A12: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A13: r > 0 and
A14: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A15: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A16: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
A17: (f | X) . x0 < ((f | X) . x0) + r by A13, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A16, XXREAL_0:2;
then A18: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A15;
then ((f | X) . x0) + (r / 2) in N2 by A12, A14;
then ((f | X) . x0) + (r / 2) in left_open_halfline p by A10;
then consider r2 being Real such that
A19: ( r2 in dom (f | X) & r2 in X ) and
A20: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59;
A21: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A13, XREAL_1:29, XREAL_1:215;
A22: now__::_thesis:_not_r2_<_x0
assume A23: r2 < x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A19, XBOOLE_0:def_4;
hence contradiction by A9, A20, A21, A23, RFUNCT_2:22, A4; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A16, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A17, XXREAL_0:2;
then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24;
then ((f | X) . x0) - (r / 2) in N2 by A12, A14;
then ((f | X) . x0) - (r / 2) in left_open_halfline p by A10;
then consider r1 being Real such that
A26: ( r1 in dom (f | X) & r1 in X ) and
A27: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A30: now__::_thesis:_not_x0_<_r1
assume A31: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A26, XBOOLE_0:def_4;
hence contradiction by A9, A27, A29, A31, RFUNCT_2:22, A4; ::_thesis: verum
end;
x0 <> r2 by A13, A20, XREAL_1:29, XREAL_1:215;
then x0 < r2 by A22, XXREAL_0:1;
then A32: r2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - r1),(r2 - x0));
A33: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A27, A28, XREAL_1:19;
then r1 < x0 by A30, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by A32, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A34: x in REAL by XREAL_0:def_1;
assume that
A35: x in dom (f | X) and
A36: x in N ; ::_thesis: (f | X) . x in N1
A37: x in X /\ (dom (f | X)) by A35, XBOOLE_1:28;
A38: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A36;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A39: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A39, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:24;
then A40: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def_4;
then A41: (f | X) . r1 <= (f | X) . x by A9, A40, A37, RFUNCT_2:22, A34;
x - x0 < min ((x0 - r1),(r2 - x0)) by A38, XREAL_1:19;
then x - x0 < r2 - x0 by A33, XXREAL_0:2;
then A42: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A19, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A9, A42, A37, RFUNCT_2:22, A34;
then A43: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A27, A20, A41;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A18, XXREAL_2:def_12;
then (f | X) . x in N3 by A14, A43;
hence (f | X) . x in N1 by A11; ::_thesis: verum
end;
supposeA44: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider r being real number such that
A45: r > 0 and
A46: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = r / 2;
A47: p < p + (r / 2) by A45, XREAL_1:29, XREAL_1:215;
A48: p - (r / 2) < p by A45, XREAL_1:44, XREAL_1:215;
then p - (r / 2) in { s where s is Real : s < p } ;
then p - (r / 2) in left_open_halfline p by XXREAL_1:229;
then consider r1 being Real such that
A49: ( r1 in dom (f | X) & r1 in X ) and
A50: p - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A51: r1 in X /\ (dom (f | X)) by A49, XBOOLE_0:def_4;
A52: now__::_thesis:_not_x0_<_r1
assume A53: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A49, XBOOLE_0:def_4;
hence contradiction by A9, A44, A48, A50, A53, RFUNCT_2:22, A4; ::_thesis: verum
end;
r1 <> x0 by A44, A45, A50, XREAL_1:44, XREAL_1:215;
then r1 < x0 by A52, XXREAL_0:1;
then reconsider N = ].(x0 - (x0 - r1)),(x0 + (x0 - r1)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A54: x in dom (f | X) and
A55: x in N ; ::_thesis: (f | X) . x in N1
A56: ex s being Real st
( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A55;
A57: r / 2 < r by A45, XREAL_1:216;
then A58: p - r < p - (r / 2) by XREAL_1:15;
(f | X) . x in left_closed_halfline p by A3, A5, A54, FUNCT_1:def_6;
then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;
then ex s being Real st
( s = (f | X) . x & s <= p ) ;
then A59: (f | X) . x <= p + (r / 2) by A47, XXREAL_0:2;
x in X /\ (dom (f | X)) by A54, XBOOLE_0:def_4;
then p - (r / 2) <= (f | X) . x by A9, A50, A51, A56, RFUNCT_2:22;
then A60: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A59;
p < p + r by A45, XREAL_1:29;
then p - (r / 2) < p + r by A48, XXREAL_0:2;
then A61: p - (r / 2) in ].(p - r),(p + r).[ by A58;
A62: p + (r / 2) < p + r by A57, XREAL_1:6;
p - r < p by A45, XREAL_1:44;
then p - r < p + (r / 2) by A47, XXREAL_0:2;
then p + (r / 2) in ].(p - r),(p + r).[ by A62;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A46, A61, XXREAL_2:def_12;
hence (f | X) . x in N1 by A60; ::_thesis: verum
end;
end;
end;
hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; ::_thesis: verum
end;
suppose f | X is non-increasing ; ::_thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1
then A63: (f | X) | X is non-increasing ;
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
percases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1;
suppose (f | X) . x0 in left_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider N2 being Neighbourhood of (f | X) . x0 such that
A64: N2 c= left_open_halfline p by RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A65: N3 c= N1 and
A66: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A67: r > 0 and
A68: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A69: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A70: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
A71: (f | X) . x0 < ((f | X) . x0) + r by A67, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A70, XXREAL_0:2;
then A72: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A69;
then ((f | X) . x0) + (r / 2) in N2 by A66, A68;
then ((f | X) . x0) + (r / 2) in left_open_halfline p by A64;
then consider r2 being Real such that
A73: ( r2 in dom (f | X) & r2 in X ) and
A74: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59;
A75: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A67, XREAL_1:29, XREAL_1:215;
A76: now__::_thesis:_not_r2_>_x0
assume A77: r2 > x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A73, XBOOLE_0:def_4;
hence contradiction by A63, A74, A75, A77, RFUNCT_2:23, A4; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A78: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A70, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A71, XXREAL_0:2;
then A79: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A78;
then ((f | X) . x0) - (r / 2) in N2 by A66, A68;
then ((f | X) . x0) - (r / 2) in left_open_halfline p by A64;
then consider r1 being Real such that
A80: ( r1 in dom (f | X) & r1 in X ) and
A81: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A82: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
then A83: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A84: now__::_thesis:_not_x0_>_r1
assume A85: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A80, XBOOLE_0:def_4;
hence contradiction by A63, A81, A83, A85, RFUNCT_2:23, A4; ::_thesis: verum
end;
x0 <> r2 by A67, A74, XREAL_1:29, XREAL_1:215;
then x0 > r2 by A76, XXREAL_0:1;
then A86: x0 - r2 > 0 by XREAL_1:50;
set R = min ((r1 - x0),(x0 - r2));
A87: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A81, A82, XREAL_1:19;
then r1 > x0 by A84, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by A86, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A88: x in REAL by XREAL_0:def_1;
assume that
A89: x in dom (f | X) and
A90: x in N ; ::_thesis: (f | X) . x in N1
A91: x in X /\ (dom (f | X)) by A89, XBOOLE_1:28;
A92: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A90;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A93: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) by A92, XREAL_1:19;
then x - x0 < r1 - x0 by A87, XXREAL_0:2;
then A94: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A80, XBOOLE_0:def_4;
then A95: (f | X) . r1 <= (f | X) . x by A63, A94, A91, RFUNCT_2:23, A88;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A93, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:24;
then A96: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A73, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A63, A96, A91, RFUNCT_2:23, A88;
then A97: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A81, A74, A95;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A79, A72, XXREAL_2:def_12;
then (f | X) . x in N3 by A68, A97;
hence (f | X) . x in N1 by A65; ::_thesis: verum
end;
supposeA98: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider r being real number such that
A99: r > 0 and
A100: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = r / 2;
A101: p < p + (r / 2) by A99, XREAL_1:29, XREAL_1:215;
A102: p - (r / 2) < p by A99, XREAL_1:44, XREAL_1:215;
then p - (r / 2) in { s where s is Real : s < p } ;
then p - (r / 2) in left_open_halfline p by XXREAL_1:229;
then consider r1 being Real such that
A103: ( r1 in dom (f | X) & r1 in X ) and
A104: p - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A105: r1 in X /\ (dom (f | X)) by A103, XBOOLE_0:def_4;
A106: now__::_thesis:_not_x0_>_r1
assume A107: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A103, XBOOLE_0:def_4;
hence contradiction by A63, A98, A102, A104, A107, RFUNCT_2:23, A4; ::_thesis: verum
end;
r1 <> x0 by A98, A99, A104, XREAL_1:44, XREAL_1:215;
then r1 > x0 by A106, XXREAL_0:1;
then reconsider N = ].(x0 - (r1 - x0)),(x0 + (r1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A108: x in dom (f | X) and
A109: x in N ; ::_thesis: (f | X) . x in N1
A110: ex s being Real st
( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A109;
A111: r / 2 < r by A99, XREAL_1:216;
then A112: p - r < p - (r / 2) by XREAL_1:15;
(f | X) . x in left_closed_halfline p by A3, A5, A108, FUNCT_1:def_6;
then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231;
then ex s being Real st
( s = (f | X) . x & s <= p ) ;
then A113: (f | X) . x <= p + (r / 2) by A101, XXREAL_0:2;
x in X /\ (dom (f | X)) by A108, XBOOLE_0:def_4;
then p - (r / 2) <= (f | X) . x by A63, A104, A105, A110, RFUNCT_2:23;
then A114: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A113;
p < p + r by A99, XREAL_1:29;
then p - (r / 2) < p + r by A102, XXREAL_0:2;
then A115: p - (r / 2) in ].(p - r),(p + r).[ by A112;
A116: p + (r / 2) < p + r by A111, XREAL_1:6;
p - r < p by A99, XREAL_1:44;
then p - r < p + (r / 2) by A101, XXREAL_0:2;
then p + (r / 2) in ].(p - r),(p + r).[ by A116;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A100, A115, XXREAL_2:def_12;
hence (f | X) . x in N1 by A114; ::_thesis: verum
end;
end;
end;
hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; ::_thesis: verum
end;
end;
end;
hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
theorem Th14: :: FCONT_3:14
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_closed_halfline p holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_closed_halfline p holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = right_closed_halfline p implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = right_closed_halfline p or f | X is continuous )
given p being Real such that A3: f .: X = right_closed_halfline p ; ::_thesis: f | X is continuous
set L = right_open_halfline p;
set l = right_closed_halfline p;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A4: x0 in REAL by XREAL_0:def_1;
A5: (f | X) .: X = f .: X by RELAT_1:129;
A6: right_open_halfline p c= right_closed_halfline p by XXREAL_1:22;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A7: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then (f | X) . x0 in {p} \/ (right_open_halfline p) by A3, A5, XXREAL_1:427;
then A8: ( (f | X) . x0 in {p} or (f | X) . x0 in right_open_halfline p ) by XBOOLE_0:def_3;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_
(f_|_X)_._r1_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_
(f_|_X)_._r1_in_N1
percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5;
suppose f | X is non-decreasing ; ::_thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1
then A9: (f | X) | X is non-decreasing ;
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
percases ( (f | X) . x0 in right_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1;
suppose (f | X) . x0 in right_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider N2 being Neighbourhood of (f | X) . x0 such that
A10: N2 c= right_open_halfline p by RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A11: N3 c= N1 and
A12: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A13: r > 0 and
A14: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A15: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A16: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
A17: (f | X) . x0 < ((f | X) . x0) + r by A13, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A16, XXREAL_0:2;
then A18: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A15;
then ((f | X) . x0) + (r / 2) in N2 by A12, A14;
then ((f | X) . x0) + (r / 2) in right_open_halfline p by A10;
then consider r2 being Real such that
A19: ( r2 in dom (f | X) & r2 in X ) and
A20: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59;
A21: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A13, XREAL_1:29, XREAL_1:215;
A22: now__::_thesis:_not_r2_<_x0
assume A23: r2 < x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A19, XBOOLE_0:def_4;
hence contradiction by A9, A20, A21, A23, RFUNCT_2:22, A4; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A16, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A17, XXREAL_0:2;
then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24;
then ((f | X) . x0) - (r / 2) in N2 by A12, A14;
then ((f | X) . x0) - (r / 2) in right_open_halfline p by A10;
then consider r1 being Real such that
A26: ( r1 in dom (f | X) & r1 in X ) and
A27: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215;
then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A30: now__::_thesis:_not_x0_<_r1
assume A31: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A26, XBOOLE_0:def_4;
hence contradiction by A9, A27, A29, A31, RFUNCT_2:22, A4; ::_thesis: verum
end;
x0 <> r2 by A13, A20, XREAL_1:29, XREAL_1:215;
then x0 < r2 by A22, XXREAL_0:1;
then A32: r2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - r1),(r2 - x0));
A33: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A27, A28, XREAL_1:19;
then r1 < x0 by A30, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by A32, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A34: x in REAL by XREAL_0:def_1;
assume that
A35: x in dom (f | X) and
A36: x in N ; ::_thesis: (f | X) . x in N1
A37: x in X /\ (dom (f | X)) by A35, XBOOLE_1:28;
A38: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A36;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A39: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A39, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:24;
then A40: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def_4;
then A41: (f | X) . r1 <= (f | X) . x by A9, A40, A37, RFUNCT_2:22, A34;
x - x0 < min ((x0 - r1),(r2 - x0)) by A38, XREAL_1:19;
then x - x0 < r2 - x0 by A33, XXREAL_0:2;
then A42: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A19, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A9, A42, A37, RFUNCT_2:22, A34;
then A43: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A27, A20, A41;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A18, XXREAL_2:def_12;
then (f | X) . x in N3 by A14, A43;
hence (f | X) . x in N1 by A11; ::_thesis: verum
end;
supposeA44: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider r being real number such that
A45: r > 0 and
A46: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = r / 2;
A47: p - (r / 2) < p by A45, XREAL_1:44, XREAL_1:215;
A48: p < p + (r / 2) by A45, XREAL_1:29, XREAL_1:215;
then p + (r / 2) in { s where s is Real : p < s } ;
then p + (r / 2) in right_open_halfline p by XXREAL_1:230;
then consider r1 being Real such that
A49: ( r1 in dom (f | X) & r1 in X ) and
A50: p + (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A51: now__::_thesis:_not_x0_>_r1
assume A52: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A49, XBOOLE_0:def_4;
hence contradiction by A9, A44, A48, A50, A52, RFUNCT_2:22, A4; ::_thesis: verum
end;
r1 <> x0 by A44, A45, A50, XREAL_1:29, XREAL_1:215;
then r1 > x0 by A51, XXREAL_0:1;
then reconsider N = ].(x0 - (r1 - x0)),(x0 + (r1 - x0)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A53: x in dom (f | X) and
A54: x in N ; ::_thesis: (f | X) . x in N1
A55: ex s being Real st
( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A54;
(f | X) . x in right_closed_halfline p by A3, A5, A53, FUNCT_1:def_6;
then (f | X) . x in { s where s is Real : p <= s } by XXREAL_1:232;
then ex s being Real st
( s = (f | X) . x & p <= s ) ;
then A56: p - (r / 2) <= (f | X) . x by A47, XXREAL_0:2;
A57: r1 in X /\ (dom (f | X)) by A49, XBOOLE_0:def_4;
x in X /\ (dom (f | X)) by A53, XBOOLE_0:def_4;
then p + (r / 2) >= (f | X) . x by A9, A50, A57, A55, RFUNCT_2:22;
then A58: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A56;
A59: r / 2 < r by A45, XREAL_1:216;
then A60: p - r < p - (r / 2) by XREAL_1:15;
p < p + r by A45, XREAL_1:29;
then p - (r / 2) < p + r by A47, XXREAL_0:2;
then A61: p - (r / 2) in ].(p - r),(p + r).[ by A60;
A62: p + (r / 2) < p + r by A59, XREAL_1:6;
p - r < p by A45, XREAL_1:44;
then p - r < p + (r / 2) by A48, XXREAL_0:2;
then p + (r / 2) in ].(p - r),(p + r).[ by A62;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A46, A61, XXREAL_2:def_12;
hence (f | X) . x in N1 by A58; ::_thesis: verum
end;
end;
end;
hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; ::_thesis: verum
end;
suppose f | X is non-increasing ; ::_thesis: ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1
then A63: (f | X) | X is non-increasing ;
now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
percases ( (f | X) . x0 in right_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1;
suppose (f | X) . x0 in right_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider N2 being Neighbourhood of (f | X) . x0 such that
A64: N2 c= right_open_halfline p by RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A65: N3 c= N1 and
A66: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A67: r > 0 and
A68: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A69: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A70: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
A71: (f | X) . x0 < ((f | X) . x0) + r by A67, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A70, XXREAL_0:2;
then A72: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A69;
then ((f | X) . x0) + (r / 2) in N2 by A66, A68;
then ((f | X) . x0) + (r / 2) in right_open_halfline p by A64;
then consider r2 being Real such that
A73: ( r2 in dom (f | X) & r2 in X ) and
A74: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59;
A75: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A67, XREAL_1:29, XREAL_1:215;
A76: now__::_thesis:_not_r2_>_x0
assume A77: r2 > x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A73, XBOOLE_0:def_4;
hence contradiction by A63, A74, A75, A77, RFUNCT_2:23, A4; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A78: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A70, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A71, XXREAL_0:2;
then A79: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A78;
then ((f | X) . x0) - (r / 2) in N2 by A66, A68;
then ((f | X) . x0) - (r / 2) in right_open_halfline p by A64;
then consider r1 being Real such that
A80: ( r1 in dom (f | X) & r1 in X ) and
A81: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A82: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215;
then A83: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A84: now__::_thesis:_not_x0_>_r1
assume A85: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A80, XBOOLE_0:def_4;
hence contradiction by A63, A81, A83, A85, RFUNCT_2:23, A4; ::_thesis: verum
end;
x0 <> r2 by A67, A74, XREAL_1:29, XREAL_1:215;
then x0 > r2 by A76, XXREAL_0:1;
then A86: x0 - r2 > 0 by XREAL_1:50;
set R = min ((r1 - x0),(x0 - r2));
A87: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A81, A82, XREAL_1:19;
then r1 > x0 by A84, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by A86, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A88: x in REAL by XREAL_0:def_1;
assume that
A89: x in dom (f | X) and
A90: x in N ; ::_thesis: (f | X) . x in N1
A91: x in X /\ (dom (f | X)) by A89, XBOOLE_1:28;
A92: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A90;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A93: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) by A92, XREAL_1:19;
then x - x0 < r1 - x0 by A87, XXREAL_0:2;
then A94: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A80, XBOOLE_0:def_4;
then A95: (f | X) . r1 <= (f | X) . x by A63, A94, A91, RFUNCT_2:23, A88;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A93, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:24;
then A96: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A73, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A63, A96, A91, RFUNCT_2:23, A88;
then A97: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A81, A74, A95;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A79, A72, XXREAL_2:def_12;
then (f | X) . x in N3 by A68, A97;
hence (f | X) . x in N1 by A65; ::_thesis: verum
end;
supposeA98: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
then consider r being real number such that
A99: r > 0 and
A100: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
set R = r / 2;
A101: p - (r / 2) < p by A99, XREAL_1:44, XREAL_1:215;
A102: p < p + (r / 2) by A99, XREAL_1:29, XREAL_1:215;
then p + (r / 2) in { s where s is Real : p < s } ;
then p + (r / 2) in right_open_halfline p by XXREAL_1:230;
then consider r1 being Real such that
A103: ( r1 in dom (f | X) & r1 in X ) and
A104: p + (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59;
A105: now__::_thesis:_not_x0_<_r1
assume A106: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A103, XBOOLE_0:def_4;
hence contradiction by A63, A98, A102, A104, A106, RFUNCT_2:23, A4; ::_thesis: verum
end;
r1 <> x0 by A98, A99, A104, XREAL_1:29, XREAL_1:215;
then r1 < x0 by A105, XXREAL_0:1;
then reconsider N = ].(x0 - (x0 - r1)),(x0 + (x0 - r1)).[ as Neighbourhood of x0 by RCOMP_1:def_6, XREAL_1:50;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
assume that
A107: x in dom (f | X) and
A108: x in N ; ::_thesis: (f | X) . x in N1
A109: ex s being Real st
( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A108;
(f | X) . x in right_closed_halfline p by A3, A5, A107, FUNCT_1:def_6;
then (f | X) . x in { s where s is Real : p <= s } by XXREAL_1:232;
then ex s being Real st
( s = (f | X) . x & p <= s ) ;
then A110: p - (r / 2) <= (f | X) . x by A101, XXREAL_0:2;
A111: r1 in X /\ (dom (f | X)) by A103, XBOOLE_0:def_4;
x in X /\ (dom (f | X)) by A107, XBOOLE_0:def_4;
then p + (r / 2) >= (f | X) . x by A63, A104, A111, A109, RFUNCT_2:23;
then A112: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A110;
A113: r / 2 < r by A99, XREAL_1:216;
then A114: p - r < p - (r / 2) by XREAL_1:15;
p < p + r by A99, XREAL_1:29;
then p - (r / 2) < p + r by A101, XXREAL_0:2;
then A115: p - (r / 2) in ].(p - r),(p + r).[ by A114;
A116: p + (r / 2) < p + r by A113, XREAL_1:6;
p - r < p by A99, XREAL_1:44;
then p - r < p + (r / 2) by A102, XXREAL_0:2;
then p + (r / 2) in ].(p - r),(p + r).[ by A116;
then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A100, A115, XXREAL_2:def_12;
hence (f | X) . x in N1 by A112; ::_thesis: verum
end;
end;
end;
hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; ::_thesis: verum
end;
end;
end;
hence ex N being Neighbourhood of x0 st
for r1 being real number st r1 in dom (f | X) & r1 in N holds
(f | X) . r1 in N1 ; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
theorem Th15: :: FCONT_3:15
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone ; ::_thesis: ( for p, g being Real holds not f .: X = ].p,g.[ or f | X is continuous )
given p, g being Real such that A3: f .: X = ].p,g.[ ; ::_thesis: f | X is continuous
set L = ].p,g.[;
now__::_thesis:_f_|_X_is_continuous
percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5;
suppose f | X is non-decreasing ; ::_thesis: f | X is continuous
then A4: (f | X) | X is non-decreasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A5: x0 in REAL by XREAL_0:def_1;
A6: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A7: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then A8: (f | X) . x0 in ].p,g.[ by A3, RELAT_1:129;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A9: N2 c= ].p,g.[ by A8, RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A10: N3 c= N1 and
A11: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A12: r > 0 and
A13: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A14: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A15: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
A16: (f | X) . x0 < ((f | X) . x0) + r by A12, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A15, XXREAL_0:2;
then A17: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A14;
then ((f | X) . x0) + (r / 2) in N2 by A11, A13;
then consider r2 being Real such that
A18: ( r2 in dom (f | X) & r2 in X ) and
A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, A9, PARTFUN2:59;
A20: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A12, XREAL_1:29, XREAL_1:215;
A21: now__::_thesis:_not_r2_<_x0
assume A22: r2 < x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A18, XBOOLE_0:def_4;
hence contradiction by A4, A19, A20, A22, RFUNCT_2:22, A5; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A23: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A15, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A16, XXREAL_0:2;
then A24: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A23;
then ((f | X) . x0) - (r / 2) in N2 by A11, A13;
then consider r1 being Real such that
A25: ( r1 in dom (f | X) & r1 in X ) and
A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, A9, PARTFUN2:59;
A27: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215;
then A28: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A29: now__::_thesis:_not_x0_<_r1
assume A30: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A25, XBOOLE_0:def_4;
hence contradiction by A4, A26, A28, A30, RFUNCT_2:22, A5; ::_thesis: verum
end;
x0 <> r2 by A12, A19, XREAL_1:29, XREAL_1:215;
then x0 < r2 by A21, XXREAL_0:1;
then A31: r2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - r1),(r2 - x0));
A32: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A26, A27, XREAL_1:19;
then r1 < x0 by A29, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by A31, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A33: x in REAL by XREAL_0:def_1;
assume that
A34: x in dom (f | X) and
A35: x in N ; ::_thesis: (f | X) . x in N1
A36: x in X /\ (dom (f | X)) by A34, XBOOLE_1:28;
A37: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A35;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A38: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A38, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:24;
then A39: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A25, XBOOLE_0:def_4;
then A40: (f | X) . r1 <= (f | X) . x by A4, A39, A36, RFUNCT_2:22, A33;
x - x0 < min ((x0 - r1),(r2 - x0)) by A37, XREAL_1:19;
then x - x0 < r2 - x0 by A32, XXREAL_0:2;
then A41: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A18, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A4, A41, A36, RFUNCT_2:22, A33;
then A42: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A40;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24, A17, XXREAL_2:def_12;
then (f | X) . x in N3 by A13, A42;
hence (f | X) . x in N1 by A10; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
suppose f | X is non-increasing ; ::_thesis: f | X is continuous
then A43: (f | X) | X is non-increasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A44: x0 in REAL by XREAL_0:def_1;
A45: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A46: x0 in dom (f | X) by RELAT_1:61;
then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6;
then A47: (f | X) . x0 in ].p,g.[ by A3, RELAT_1:129;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider N2 being Neighbourhood of (f | X) . x0 such that
A48: N2 c= ].p,g.[ by A47, RCOMP_1:18;
consider N3 being Neighbourhood of (f | X) . x0 such that
A49: N3 c= N1 and
A50: N3 c= N2 by RCOMP_1:17;
consider r being real number such that
A51: r > 0 and
A52: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A53: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
set M2 = ((f | X) . x0) + (r / 2);
A54: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
A55: (f | X) . x0 < ((f | X) . x0) + r by A51, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A54, XXREAL_0:2;
then A56: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A53;
then ((f | X) . x0) + (r / 2) in N2 by A50, A52;
then consider r2 being Real such that
A57: ( r2 in dom (f | X) & r2 in X ) and
A58: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A45, A48, PARTFUN2:59;
A59: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A51, XREAL_1:29, XREAL_1:215;
A60: now__::_thesis:_not_r2_>_x0
assume A61: r2 > x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A46, A57, XBOOLE_0:def_4;
hence contradiction by A43, A58, A59, A61, RFUNCT_2:23, A44; ::_thesis: verum
end;
set M1 = ((f | X) . x0) - (r / 2);
A62: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A54, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A55, XXREAL_0:2;
then A63: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62;
then ((f | X) . x0) - (r / 2) in N2 by A50, A52;
then consider r1 being Real such that
A64: ( r1 in dom (f | X) & r1 in X ) and
A65: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A45, A48, PARTFUN2:59;
A66: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215;
then A67: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A68: now__::_thesis:_not_x0_>_r1
assume A69: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A46, A64, XBOOLE_0:def_4;
hence contradiction by A43, A65, A67, A69, RFUNCT_2:23, A44; ::_thesis: verum
end;
x0 <> r2 by A51, A58, XREAL_1:29, XREAL_1:215;
then x0 > r2 by A60, XXREAL_0:1;
then A70: x0 - r2 > 0 by XREAL_1:50;
set R = min ((r1 - x0),(x0 - r2));
A71: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A65, A66, XREAL_1:19;
then r1 > x0 by A68, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by A70, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A72: x in REAL by XREAL_0:def_1;
assume that
A73: x in dom (f | X) and
A74: x in N ; ::_thesis: (f | X) . x in N1
A75: x in X /\ (dom (f | X)) by A73, XBOOLE_1:28;
A76: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A74;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A77: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) by A76, XREAL_1:19;
then x - x0 < r1 - x0 by A71, XXREAL_0:2;
then A78: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A64, XBOOLE_0:def_4;
then A79: (f | X) . r1 <= (f | X) . x by A43, A78, A75, RFUNCT_2:23, A72;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A77, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:24;
then A80: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A57, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A43, A80, A75, RFUNCT_2:23, A72;
then A81: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A65, A58, A79;
[.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A63, A56, XXREAL_2:def_12;
then (f | X) . x in N3 by A52, A81;
hence (f | X) . x in N1 by A49; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
end;
end;
hence f | X is continuous ; ::_thesis: verum
end;
theorem Th16: :: FCONT_3:16
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & f .: X = REAL holds
f | X is continuous
proof
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & f .: X = REAL holds
f | X is continuous
let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & f .: X = REAL implies f | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is monotone and
A3: f .: X = REAL ; ::_thesis: f | X is continuous
now__::_thesis:_f_|_X_is_continuous
percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5;
suppose f | X is non-decreasing ; ::_thesis: f | X is continuous
then A4: (f | X) | X is non-decreasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A5: x0 in REAL by XREAL_0:def_1;
A6: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A7: x0 in dom (f | X) by RELAT_1:61;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider r being real number such that
A8: r > 0 and
A9: N1 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A10: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A8, XREAL_1:29, XREAL_1:215;
set M1 = ((f | X) . x0) - (r / 2);
consider r1 being Real such that
A11: ( r1 in dom (f | X) & r1 in X ) and
A12: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, PARTFUN2:59;
A13: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A8, XREAL_1:29, XREAL_1:215;
then A14: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A15: now__::_thesis:_not_x0_<_r1
assume A16: x0 < r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A11, XBOOLE_0:def_4;
hence contradiction by A4, A12, A14, A16, RFUNCT_2:22, A5; ::_thesis: verum
end;
set M2 = ((f | X) . x0) + (r / 2);
consider r2 being Real such that
A17: ( r2 in dom (f | X) & r2 in X ) and
A18: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, PARTFUN2:59;
A19: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A8, XREAL_1:29, XREAL_1:215;
A20: now__::_thesis:_not_r2_<_x0
assume A21: r2 < x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A17, XBOOLE_0:def_4;
hence contradiction by A4, A18, A19, A21, RFUNCT_2:22, A5; ::_thesis: verum
end;
x0 <> r2 by A8, A18, XREAL_1:29, XREAL_1:215;
then x0 < r2 by A20, XXREAL_0:1;
then A22: r2 - x0 > 0 by XREAL_1:50;
set R = min ((x0 - r1),(r2 - x0));
A23: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17;
r1 <> x0 by A12, A13, XREAL_1:19;
then r1 < x0 by A15, XXREAL_0:1;
then x0 - r1 > 0 by XREAL_1:50;
then min ((x0 - r1),(r2 - x0)) > 0 by A22, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A24: x in REAL by XREAL_0:def_1;
assume that
A25: x in dom (f | X) and
A26: x in N ; ::_thesis: (f | X) . x in N1
A27: x in X /\ (dom (f | X)) by A25, XBOOLE_1:28;
A28: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A8, XREAL_1:29, XREAL_1:215;
A29: (f | X) . x0 < ((f | X) . x0) + r by A8, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A10, XXREAL_0:2;
then A30: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A28;
A31: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A8, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A10, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A29, XXREAL_0:2;
then ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A31;
then A32: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A30, XXREAL_2:def_12;
A33: ex s being Real st
( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A26;
then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19;
then A34: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9;
min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17;
then x0 - x < x0 - r1 by A34, XXREAL_0:2;
then - (x0 - x) > - (x0 - r1) by XREAL_1:24;
then A35: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A11, XBOOLE_0:def_4;
then A36: (f | X) . r1 <= (f | X) . x by A4, A35, A27, RFUNCT_2:22, A24;
x - x0 < min ((x0 - r1),(r2 - x0)) by A33, XREAL_1:19;
then x - x0 < r2 - x0 by A23, XXREAL_0:2;
then A37: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A17, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A4, A37, A27, RFUNCT_2:22, A24;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A12, A18, A36;
hence (f | X) . x in N1 by A9, A32; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
suppose f | X is non-increasing ; ::_thesis: f | X is continuous
then A38: (f | X) | X is non-increasing ;
for x0 being real number st x0 in dom (f | X) holds
f | X is_continuous_in x0
proof
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
A39: x0 in REAL by XREAL_0:def_1;
A40: (f | X) .: X = f .: X by RELAT_1:129;
assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then x0 in X ;
then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4;
then A41: x0 in dom (f | X) by RELAT_1:61;
now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_
(f_|_X)_._x_in_N1
let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st
for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
consider r being real number such that
A42: r > 0 and
A43: N1 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
A44: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A42, XREAL_1:29, XREAL_1:215;
set M1 = ((f | X) . x0) - (r / 2);
consider r1 being Real such that
A45: ( r1 in dom (f | X) & r1 in X ) and
A46: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A40, PARTFUN2:59;
A47: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A42, XREAL_1:29, XREAL_1:215;
then A48: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19;
A49: now__::_thesis:_not_x0_>_r1
assume A50: x0 > r1 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A41, A45, XBOOLE_0:def_4;
hence contradiction by A38, A46, A48, A50, RFUNCT_2:23, A39; ::_thesis: verum
end;
set M2 = ((f | X) . x0) + (r / 2);
consider r2 being Real such that
A51: ( r2 in dom (f | X) & r2 in X ) and
A52: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A40, PARTFUN2:59;
A53: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A42, XREAL_1:29, XREAL_1:215;
A54: now__::_thesis:_not_r2_>_x0
assume A55: r2 > x0 ; ::_thesis: contradiction
( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A41, A51, XBOOLE_0:def_4;
hence contradiction by A38, A52, A53, A55, RFUNCT_2:23, A39; ::_thesis: verum
end;
x0 <> r2 by A42, A52, XREAL_1:29, XREAL_1:215;
then x0 > r2 by A54, XXREAL_0:1;
then A56: x0 - r2 > 0 by XREAL_1:50;
set R = min ((r1 - x0),(x0 - r2));
A57: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17;
r1 <> x0 by A46, A47, XREAL_1:19;
then r1 > x0 by A49, XXREAL_0:1;
then r1 - x0 > 0 by XREAL_1:50;
then min ((r1 - x0),(x0 - r2)) > 0 by A56, XXREAL_0:15;
then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6;
take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds
(f | X) . x in N1
let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 )
A58: x in REAL by XREAL_0:def_1;
assume that
A59: x in dom (f | X) and
A60: x in N ; ::_thesis: (f | X) . x in N1
A61: x in X /\ (dom (f | X)) by A59, XBOOLE_1:28;
A62: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A42, XREAL_1:29, XREAL_1:215;
A63: (f | X) . x0 < ((f | X) . x0) + r by A42, XREAL_1:29;
then ((f | X) . x0) - r < (((f | X) . x0) + r) - r by XREAL_1:9;
then ((f | X) . x0) - r < ((f | X) . x0) + (r / 2) by A44, XXREAL_0:2;
then A64: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62;
A65: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A42, XREAL_1:29, XREAL_1:215;
((f | X) . x0) - (r / 2) < (f | X) . x0 by A44, XREAL_1:19;
then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A63, XXREAL_0:2;
then ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A65;
then A66: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A64, XXREAL_2:def_12;
A67: ex s being Real st
( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A60;
then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19;
then A68: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9;
x - x0 < min ((r1 - x0),(x0 - r2)) by A67, XREAL_1:19;
then x - x0 < r1 - x0 by A57, XXREAL_0:2;
then A69: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6;
r1 in X /\ (dom (f | X)) by A45, XBOOLE_0:def_4;
then A70: (f | X) . r1 <= (f | X) . x by A38, A69, A61, RFUNCT_2:23, A58;
min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17;
then x0 - x < x0 - r2 by A68, XXREAL_0:2;
then - (x0 - x) > - (x0 - r2) by XREAL_1:24;
then A71: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6;
r2 in X /\ (dom (f | X)) by A51, XBOOLE_0:def_4;
then (f | X) . x <= (f | X) . r2 by A38, A71, A61, RFUNCT_2:23, A58;
then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A46, A52, A70;
hence (f | X) . x in N1 by A43, A66; ::_thesis: verum
end;
hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum
end;
hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum
end;
end;
end;
hence f | X is continuous ; ::_thesis: verum
end;
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 ) & ].p,g.[ c= dom f holds
((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous
proof
let p, g be Real; ::_thesis: for f being 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
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) & ].p,g.[ c= dom f implies ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous )
assume that
A1: ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) and
A2: ].p,g.[ c= dom f ; ::_thesis: ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous
now__::_thesis:_((f_|_].p,g.[)_")_|_(f_.:_].p,g.[)_is_continuous
percases ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) by A1;
supposeA3: f | ].p,g.[ is increasing ; ::_thesis: ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous
A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_].p,g.[_holds_
r_in_dom_((f_|_].p,g.[)_")
let r be Real; ::_thesis: ( r in f .: ].p,g.[ implies r in dom ((f | ].p,g.[) ") )
assume r in f .: ].p,g.[ ; ::_thesis: r in dom ((f | ].p,g.[) ")
then consider s being Real such that
A5: ( s in dom f & s in ].p,g.[ ) and
A6: r = f . s by PARTFUN2:59;
s in (dom f) /\ ].p,g.[ by A5, XBOOLE_0:def_4;
then A7: s in dom (f | ].p,g.[) by RELAT_1:61;
then r = (f | ].p,g.[) . s by A6, FUNCT_1:47;
then r in rng (f | ].p,g.[) by A7, FUNCT_1:def_3;
hence r in dom ((f | ].p,g.[) ") by FUNCT_1:33; ::_thesis: verum
end;
A8: ((f | ].p,g.[) ") .: (f .: ].p,g.[) = ((f | ].p,g.[) ") .: (rng (f | ].p,g.[)) by RELAT_1:115
.= ((f | ].p,g.[) ") .: (dom ((f | ].p,g.[) ")) by FUNCT_1:33
.= rng ((f | ].p,g.[) ") by RELAT_1:113
.= dom (f | ].p,g.[) by FUNCT_1:33
.= (dom f) /\ ].p,g.[ by RELAT_1:61
.= ].p,g.[ by A2, XBOOLE_1:28 ;
((f | ].p,g.[) ") | (f .: ].p,g.[) is increasing by A3, Th9;
hence ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous by A4, A8, Th15, SUBSET_1:2; ::_thesis: verum
end;
supposeA9: f | ].p,g.[ is decreasing ; ::_thesis: ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous
A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_].p,g.[_holds_
r_in_dom_((f_|_].p,g.[)_")
let r be Real; ::_thesis: ( r in f .: ].p,g.[ implies r in dom ((f | ].p,g.[) ") )
assume r in f .: ].p,g.[ ; ::_thesis: r in dom ((f | ].p,g.[) ")
then consider s being Real such that
A11: ( s in dom f & s in ].p,g.[ ) and
A12: r = f . s by PARTFUN2:59;
s in (dom f) /\ ].p,g.[ by A11, XBOOLE_0:def_4;
then A13: s in dom (f | ].p,g.[) by RELAT_1:61;
then r = (f | ].p,g.[) . s by A12, FUNCT_1:47;
then r in rng (f | ].p,g.[) by A13, FUNCT_1:def_3;
hence r in dom ((f | ].p,g.[) ") by FUNCT_1:33; ::_thesis: verum
end;
A14: ((f | ].p,g.[) ") .: (f .: ].p,g.[) = ((f | ].p,g.[) ") .: (rng (f | ].p,g.[)) by RELAT_1:115
.= ((f | ].p,g.[) ") .: (dom ((f | ].p,g.[) ")) by FUNCT_1:33
.= rng ((f | ].p,g.[) ") by RELAT_1:113
.= dom (f | ].p,g.[) by FUNCT_1:33
.= (dom f) /\ ].p,g.[ by RELAT_1:61
.= ].p,g.[ by A2, XBOOLE_1:28 ;
((f | ].p,g.[) ") | (f .: ].p,g.[) is decreasing by A9, Th10;
hence ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous by A10, A14, Th15, SUBSET_1:2; ::_thesis: verum
end;
end;
end;
hence ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous ; ::_thesis: verum
end;
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 ) & left_open_halfline p c= dom f holds
((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous
proof
let p be Real; ::_thesis: 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 ) & left_open_halfline p c= dom f holds
((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) & left_open_halfline p c= dom f implies ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous )
set L = left_open_halfline p;
assume that
A1: ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) and
A2: left_open_halfline p c= dom f ; ::_thesis: ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous
now__::_thesis:_((f_|_(left_open_halfline_p))_")_|_(f_.:_(left_open_halfline_p))_is_continuous
percases ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) by A1;
supposeA3: f | (left_open_halfline p) is increasing ; ::_thesis: ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous
A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_open_halfline_p)_holds_
r_in_dom_((f_|_(left_open_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (left_open_halfline p) implies r in dom ((f | (left_open_halfline p)) ") )
assume r in f .: (left_open_halfline p) ; ::_thesis: r in dom ((f | (left_open_halfline p)) ")
then consider s being Real such that
A5: ( s in dom f & s in left_open_halfline p ) and
A6: r = f . s by PARTFUN2:59;
s in (dom f) /\ (left_open_halfline p) by A5, XBOOLE_0:def_4;
then A7: s in dom (f | (left_open_halfline p)) by RELAT_1:61;
then r = (f | (left_open_halfline p)) . s by A6, FUNCT_1:47;
then r in rng (f | (left_open_halfline p)) by A7, FUNCT_1:def_3;
hence r in dom ((f | (left_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A8: ((f | (left_open_halfline p)) ") .: (f .: (left_open_halfline p)) = ((f | (left_open_halfline p)) ") .: (rng (f | (left_open_halfline p))) by RELAT_1:115
.= ((f | (left_open_halfline p)) ") .: (dom ((f | (left_open_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (left_open_halfline p)) ") by RELAT_1:113
.= dom (f | (left_open_halfline p)) by FUNCT_1:33
.= (dom f) /\ (left_open_halfline p) by RELAT_1:61
.= left_open_halfline p by A2, XBOOLE_1:28 ;
((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is increasing by A3, Th9;
hence ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous by A4, A8, Th11, SUBSET_1:2; ::_thesis: verum
end;
supposeA9: f | (left_open_halfline p) is decreasing ; ::_thesis: ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous
A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_open_halfline_p)_holds_
r_in_dom_((f_|_(left_open_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (left_open_halfline p) implies r in dom ((f | (left_open_halfline p)) ") )
assume r in f .: (left_open_halfline p) ; ::_thesis: r in dom ((f | (left_open_halfline p)) ")
then consider s being Real such that
A11: ( s in dom f & s in left_open_halfline p ) and
A12: r = f . s by PARTFUN2:59;
s in (dom f) /\ (left_open_halfline p) by A11, XBOOLE_0:def_4;
then A13: s in dom (f | (left_open_halfline p)) by RELAT_1:61;
then r = (f | (left_open_halfline p)) . s by A12, FUNCT_1:47;
then r in rng (f | (left_open_halfline p)) by A13, FUNCT_1:def_3;
hence r in dom ((f | (left_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A14: ((f | (left_open_halfline p)) ") .: (f .: (left_open_halfline p)) = ((f | (left_open_halfline p)) ") .: (rng (f | (left_open_halfline p))) by RELAT_1:115
.= ((f | (left_open_halfline p)) ") .: (dom ((f | (left_open_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (left_open_halfline p)) ") by RELAT_1:113
.= dom (f | (left_open_halfline p)) by FUNCT_1:33
.= (dom f) /\ (left_open_halfline p) by RELAT_1:61
.= left_open_halfline p by A2, XBOOLE_1:28 ;
((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is decreasing by A9, Th10;
hence ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous by A10, A14, Th11, SUBSET_1:2; ::_thesis: verum
end;
end;
end;
hence ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous ; ::_thesis: verum
end;
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 ) & right_open_halfline p c= dom f holds
((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous
proof
let p be Real; ::_thesis: 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 ) & right_open_halfline p c= dom f holds
((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) & right_open_halfline p c= dom f implies ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous )
set L = right_open_halfline p;
assume that
A1: ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) and
A2: right_open_halfline p c= dom f ; ::_thesis: ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous
now__::_thesis:_((f_|_(right_open_halfline_p))_")_|_(f_.:_(right_open_halfline_p))_is_continuous
percases ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) by A1;
supposeA3: f | (right_open_halfline p) is increasing ; ::_thesis: ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous
A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_open_halfline_p)_holds_
r_in_dom_((f_|_(right_open_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (right_open_halfline p) implies r in dom ((f | (right_open_halfline p)) ") )
assume r in f .: (right_open_halfline p) ; ::_thesis: r in dom ((f | (right_open_halfline p)) ")
then consider s being Real such that
A5: ( s in dom f & s in right_open_halfline p ) and
A6: r = f . s by PARTFUN2:59;
s in (dom f) /\ (right_open_halfline p) by A5, XBOOLE_0:def_4;
then A7: s in dom (f | (right_open_halfline p)) by RELAT_1:61;
then r = (f | (right_open_halfline p)) . s by A6, FUNCT_1:47;
then r in rng (f | (right_open_halfline p)) by A7, FUNCT_1:def_3;
hence r in dom ((f | (right_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A8: ((f | (right_open_halfline p)) ") .: (f .: (right_open_halfline p)) = ((f | (right_open_halfline p)) ") .: (rng (f | (right_open_halfline p))) by RELAT_1:115
.= ((f | (right_open_halfline p)) ") .: (dom ((f | (right_open_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (right_open_halfline p)) ") by RELAT_1:113
.= dom (f | (right_open_halfline p)) by FUNCT_1:33
.= (dom f) /\ (right_open_halfline p) by RELAT_1:61
.= right_open_halfline p by A2, XBOOLE_1:28 ;
((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is increasing by A3, Th9;
hence ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous by A4, A8, Th12, SUBSET_1:2; ::_thesis: verum
end;
supposeA9: f | (right_open_halfline p) is decreasing ; ::_thesis: ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous
A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_open_halfline_p)_holds_
r_in_dom_((f_|_(right_open_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (right_open_halfline p) implies r in dom ((f | (right_open_halfline p)) ") )
assume r in f .: (right_open_halfline p) ; ::_thesis: r in dom ((f | (right_open_halfline p)) ")
then consider s being Real such that
A11: ( s in dom f & s in right_open_halfline p ) and
A12: r = f . s by PARTFUN2:59;
s in (dom f) /\ (right_open_halfline p) by A11, XBOOLE_0:def_4;
then A13: s in dom (f | (right_open_halfline p)) by RELAT_1:61;
then r = (f | (right_open_halfline p)) . s by A12, FUNCT_1:47;
then r in rng (f | (right_open_halfline p)) by A13, FUNCT_1:def_3;
hence r in dom ((f | (right_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A14: ((f | (right_open_halfline p)) ") .: (f .: (right_open_halfline p)) = ((f | (right_open_halfline p)) ") .: (rng (f | (right_open_halfline p))) by RELAT_1:115
.= ((f | (right_open_halfline p)) ") .: (dom ((f | (right_open_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (right_open_halfline p)) ") by RELAT_1:113
.= dom (f | (right_open_halfline p)) by FUNCT_1:33
.= (dom f) /\ (right_open_halfline p) by RELAT_1:61
.= right_open_halfline p by A2, XBOOLE_1:28 ;
((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is decreasing by A9, Th10;
hence ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous by A10, A14, Th12, SUBSET_1:2; ::_thesis: verum
end;
end;
end;
hence ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous ; ::_thesis: verum
end;
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 ) & left_closed_halfline p c= dom f holds
((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous
proof
let p be Real; ::_thesis: 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 ) & left_closed_halfline p c= dom f holds
((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) & left_closed_halfline p c= dom f implies ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous )
set L = left_closed_halfline p;
assume that
A1: ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) and
A2: left_closed_halfline p c= dom f ; ::_thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous
now__::_thesis:_((f_|_(left_closed_halfline_p))_")_|_(f_.:_(left_closed_halfline_p))_is_continuous
percases ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) by A1;
supposeA3: f | (left_closed_halfline p) is increasing ; ::_thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous
A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_closed_halfline_p)_holds_
r_in_dom_((f_|_(left_closed_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (left_closed_halfline p) implies r in dom ((f | (left_closed_halfline p)) ") )
assume r in f .: (left_closed_halfline p) ; ::_thesis: r in dom ((f | (left_closed_halfline p)) ")
then consider s being Real such that
A5: ( s in dom f & s in left_closed_halfline p ) and
A6: r = f . s by PARTFUN2:59;
s in (dom f) /\ (left_closed_halfline p) by A5, XBOOLE_0:def_4;
then A7: s in dom (f | (left_closed_halfline p)) by RELAT_1:61;
then r = (f | (left_closed_halfline p)) . s by A6, FUNCT_1:47;
then r in rng (f | (left_closed_halfline p)) by A7, FUNCT_1:def_3;
hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A8: ((f | (left_closed_halfline p)) ") .: (f .: (left_closed_halfline p)) = ((f | (left_closed_halfline p)) ") .: (rng (f | (left_closed_halfline p))) by RELAT_1:115
.= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113
.= dom (f | (left_closed_halfline p)) by FUNCT_1:33
.= (dom f) /\ (left_closed_halfline p) by RELAT_1:61
.= left_closed_halfline p by A2, XBOOLE_1:28 ;
((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is increasing by A3, Th9;
hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A4, A8, Th13, SUBSET_1:2; ::_thesis: verum
end;
supposeA9: f | (left_closed_halfline p) is decreasing ; ::_thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous
A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_closed_halfline_p)_holds_
r_in_dom_((f_|_(left_closed_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (left_closed_halfline p) implies r in dom ((f | (left_closed_halfline p)) ") )
assume r in f .: (left_closed_halfline p) ; ::_thesis: r in dom ((f | (left_closed_halfline p)) ")
then consider s being Real such that
A11: ( s in dom f & s in left_closed_halfline p ) and
A12: r = f . s by PARTFUN2:59;
s in (dom f) /\ (left_closed_halfline p) by A11, XBOOLE_0:def_4;
then A13: s in dom (f | (left_closed_halfline p)) by RELAT_1:61;
then r = (f | (left_closed_halfline p)) . s by A12, FUNCT_1:47;
then r in rng (f | (left_closed_halfline p)) by A13, FUNCT_1:def_3;
hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A14: ((f | (left_closed_halfline p)) ") .: (f .: (left_closed_halfline p)) = ((f | (left_closed_halfline p)) ") .: (rng (f | (left_closed_halfline p))) by RELAT_1:115
.= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113
.= dom (f | (left_closed_halfline p)) by FUNCT_1:33
.= (dom f) /\ (left_closed_halfline p) by RELAT_1:61
.= left_closed_halfline p by A2, XBOOLE_1:28 ;
((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is decreasing by A9, Th10;
hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A10, A14, Th13, SUBSET_1:2; ::_thesis: verum
end;
end;
end;
hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous ; ::_thesis: verum
end;
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 ) & right_closed_halfline p c= dom f holds
((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous
proof
let p be Real; ::_thesis: 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 ) & right_closed_halfline p c= dom f holds
((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (right_closed_halfline p) is increasing or f | (right_closed_halfline p) is decreasing ) & right_closed_halfline p c= dom f implies ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous )
set L = right_closed_halfline p;
assume that
A1: ( f | (right_closed_halfline p) is increasing or f | (right_closed_halfline p) is decreasing ) and
A2: right_closed_halfline p c= dom f ; ::_thesis: ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous
now__::_thesis:_((f_|_(right_closed_halfline_p))_")_|_(f_.:_(right_closed_halfline_p))_is_continuous
percases ( f | (right_closed_halfline p) is increasing or f | (right_closed_halfline p) is decreasing ) by A1;
supposeA3: f | (right_closed_halfline p) is increasing ; ::_thesis: ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous
A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_closed_halfline_p)_holds_
r_in_dom_((f_|_(right_closed_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (right_closed_halfline p) implies r in dom ((f | (right_closed_halfline p)) ") )
assume r in f .: (right_closed_halfline p) ; ::_thesis: r in dom ((f | (right_closed_halfline p)) ")
then consider s being Real such that
A5: ( s in dom f & s in right_closed_halfline p ) and
A6: r = f . s by PARTFUN2:59;
s in (dom f) /\ (right_closed_halfline p) by A5, XBOOLE_0:def_4;
then A7: s in dom (f | (right_closed_halfline p)) by RELAT_1:61;
then r = (f | (right_closed_halfline p)) . s by A6, FUNCT_1:47;
then r in rng (f | (right_closed_halfline p)) by A7, FUNCT_1:def_3;
hence r in dom ((f | (right_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A8: ((f | (right_closed_halfline p)) ") .: (f .: (right_closed_halfline p)) = ((f | (right_closed_halfline p)) ") .: (rng (f | (right_closed_halfline p))) by RELAT_1:115
.= ((f | (right_closed_halfline p)) ") .: (dom ((f | (right_closed_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (right_closed_halfline p)) ") by RELAT_1:113
.= dom (f | (right_closed_halfline p)) by FUNCT_1:33
.= (dom f) /\ (right_closed_halfline p) by RELAT_1:61
.= right_closed_halfline p by A2, XBOOLE_1:28 ;
((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is increasing by A3, Th9;
hence ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous by A4, A8, Th14, SUBSET_1:2; ::_thesis: verum
end;
supposeA9: f | (right_closed_halfline p) is decreasing ; ::_thesis: ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous
A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_closed_halfline_p)_holds_
r_in_dom_((f_|_(right_closed_halfline_p))_")
let r be Real; ::_thesis: ( r in f .: (right_closed_halfline p) implies r in dom ((f | (right_closed_halfline p)) ") )
assume r in f .: (right_closed_halfline p) ; ::_thesis: r in dom ((f | (right_closed_halfline p)) ")
then consider s being Real such that
A11: ( s in dom f & s in right_closed_halfline p ) and
A12: r = f . s by PARTFUN2:59;
s in (dom f) /\ (right_closed_halfline p) by A11, XBOOLE_0:def_4;
then A13: s in dom (f | (right_closed_halfline p)) by RELAT_1:61;
then r = (f | (right_closed_halfline p)) . s by A12, FUNCT_1:47;
then r in rng (f | (right_closed_halfline p)) by A13, FUNCT_1:def_3;
hence r in dom ((f | (right_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum
end;
A14: ((f | (right_closed_halfline p)) ") .: (f .: (right_closed_halfline p)) = ((f | (right_closed_halfline p)) ") .: (rng (f | (right_closed_halfline p))) by RELAT_1:115
.= ((f | (right_closed_halfline p)) ") .: (dom ((f | (right_closed_halfline p)) ")) by FUNCT_1:33
.= rng ((f | (right_closed_halfline p)) ") by RELAT_1:113
.= dom (f | (right_closed_halfline p)) by FUNCT_1:33
.= (dom f) /\ (right_closed_halfline p) by RELAT_1:61
.= right_closed_halfline p by A2, XBOOLE_1:28 ;
((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is decreasing by A9, Th10;
hence ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous by A10, A14, Th14, SUBSET_1:2; ::_thesis: verum
end;
end;
end;
hence ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous ; ::_thesis: verum
end;
theorem :: FCONT_3:22
for f being 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
proof
set L = [#] REAL;
let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) & f is total implies (f ") | (rng f) is continuous )
assume that
A1: ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) and
A2: f is total ; ::_thesis: (f ") | (rng f) is continuous
A3: dom f = [#] REAL by A2, PARTFUN1:def_2;
now__::_thesis:_(f_")_|_(rng_f)_is_continuous
percases ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) by A1;
supposeA4: f | ([#] REAL) is increasing ; ::_thesis: (f ") | (rng f) is continuous
A5: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_([#]_REAL)_holds_
r_in_dom_((f_|_([#]_REAL))_")
let r be Real; ::_thesis: ( r in f .: ([#] REAL) implies r in dom ((f | ([#] REAL)) ") )
assume r in f .: ([#] REAL) ; ::_thesis: r in dom ((f | ([#] REAL)) ")
then consider s being Real such that
A6: s in dom f and
s in [#] REAL and
A7: r = f . s by PARTFUN2:59;
s in (dom f) /\ ([#] REAL) by A6, XBOOLE_0:def_4;
then A8: s in dom (f | ([#] REAL)) by RELAT_1:61;
then r = (f | ([#] REAL)) . s by A7, FUNCT_1:47;
then r in rng (f | ([#] REAL)) by A8, FUNCT_1:def_3;
hence r in dom ((f | ([#] REAL)) ") by FUNCT_1:33; ::_thesis: verum
end;
A9: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) = ((f | ([#] REAL)) ") .: (rng (f | ([#] REAL))) by RELAT_1:115
.= ((f | ([#] REAL)) ") .: (dom ((f | ([#] REAL)) ")) by FUNCT_1:33
.= rng ((f | ([#] REAL)) ") by RELAT_1:113
.= dom (f | ([#] REAL)) by FUNCT_1:33
.= (dom f) /\ ([#] REAL) by RELAT_1:61
.= REAL by A3 ;
((f | ([#] REAL)) ") | (f .: ([#] REAL)) is increasing by A4, Th9;
then ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is continuous by A5, A9, Th16, SUBSET_1:2;
then ((f | ([#] REAL)) ") | (rng f) is continuous by A3, RELAT_1:113;
hence (f ") | (rng f) is continuous by A3, RELAT_1:68; ::_thesis: verum
end;
supposeA10: f | ([#] REAL) is decreasing ; ::_thesis: (f ") | (rng f) is continuous
A11: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_([#]_REAL)_holds_
r_in_dom_((f_|_([#]_REAL))_")
let r be Real; ::_thesis: ( r in f .: ([#] REAL) implies r in dom ((f | ([#] REAL)) ") )
assume r in f .: ([#] REAL) ; ::_thesis: r in dom ((f | ([#] REAL)) ")
then consider s being Real such that
A12: s in dom f and
s in [#] REAL and
A13: r = f . s by PARTFUN2:59;
s in (dom f) /\ ([#] REAL) by A12, XBOOLE_0:def_4;
then A14: s in dom (f | ([#] REAL)) by RELAT_1:61;
then r = (f | ([#] REAL)) . s by A13, FUNCT_1:47;
then r in rng (f | ([#] REAL)) by A14, FUNCT_1:def_3;
hence r in dom ((f | ([#] REAL)) ") by FUNCT_1:33; ::_thesis: verum
end;
A15: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) = ((f | ([#] REAL)) ") .: (rng (f | ([#] REAL))) by RELAT_1:115
.= ((f | ([#] REAL)) ") .: (dom ((f | ([#] REAL)) ")) by FUNCT_1:33
.= rng ((f | ([#] REAL)) ") by RELAT_1:113
.= dom (f | ([#] REAL)) by FUNCT_1:33
.= (dom f) /\ ([#] REAL) by RELAT_1:61
.= REAL by A3 ;
((f | ([#] REAL)) ") | (f .: ([#] REAL)) is decreasing by A10, Th10;
then ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is continuous by A11, A15, Th16, SUBSET_1:2;
then ((f | ([#] REAL)) ") | (rng f) is continuous by A3, RELAT_1:113;
hence (f ") | (rng f) is continuous by A3, RELAT_1:68; ::_thesis: verum
end;
end;
end;
hence (f ") | (rng f) is continuous ; ::_thesis: verum
end;
theorem :: FCONT_3:23
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f | ].p,g.[ is continuous & ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) holds
rng (f | ].p,g.[) is open
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f | ].p,g.[ is continuous & ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) holds
rng (f | ].p,g.[) is open
let f be PartFunc of REAL,REAL; ::_thesis: ( ].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 )
assume that
A1: ].p,g.[ c= dom f and
A2: f | ].p,g.[ is continuous and
A3: ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) ; ::_thesis: rng (f | ].p,g.[) is open
now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_(f_|_].p,g.[)_holds_
ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_(f_|_].p,g.[)
let r1 be real number ; ::_thesis: ( r1 in rng (f | ].p,g.[) implies ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[) )
set f1 = f | ].p,g.[;
assume r1 in rng (f | ].p,g.[) ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[)
then consider x0 being Real such that
A4: x0 in dom (f | ].p,g.[) and
A5: (f | ].p,g.[) . x0 = r1 by PARTFUN1:3;
A6: r1 = f . x0 by A4, A5, FUNCT_1:47;
A7: x0 in (dom f) /\ ].p,g.[ by A4, RELAT_1:61;
then x0 in ].p,g.[ by XBOOLE_0:def_4;
then consider N being Neighbourhood of x0 such that
A8: N c= ].p,g.[ by RCOMP_1:18;
consider r being real number such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
0 < r / 2 by A9, XREAL_1:215;
then A11: x0 - (r / 2) < x0 - 0 by XREAL_1:15;
A12: r / 2 < r by A9, XREAL_1:216;
then A13: x0 - r < x0 - (r / 2) by XREAL_1:15;
A14: N c= dom f by A1, A8, XBOOLE_1:1;
set fp = f . (x0 + (r / 2));
set fm = f . (x0 - (r / 2));
A15: x0 + (r / 2) < x0 + r by A12, XREAL_1:8;
A16: x0 < x0 + (r / 2) by A9, XREAL_1:29, XREAL_1:215;
then A17: x0 - (r / 2) < x0 + (r / 2) by A11, XXREAL_0:2;
x0 < x0 + r by A9, XREAL_1:29;
then x0 - (r / 2) < x0 + r by A11, XXREAL_0:2;
then A18: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A13;
then A19: x0 - (r / 2) in ].p,g.[ /\ (dom f) by A8, A10, A14, XBOOLE_0:def_4;
x0 - r < x0 by A9, XREAL_1:44;
then x0 - r < x0 + (r / 2) by A16, XXREAL_0:2;
then A20: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A15;
then A21: x0 + (r / 2) in ].p,g.[ /\ (dom f) by A8, A10, A14, XBOOLE_0:def_4;
A22: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A18, A20, XXREAL_2:def_12;
A23: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].p,g.[ by A8, A10, A18, A20, XXREAL_2:def_12;
then A24: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A2, FCONT_1:16;
now__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_(f_|_].p,g.[)
percases ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) by A3;
supposeA25: f | ].p,g.[ is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | ].p,g.[)
set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)));
f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20;
then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;
f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20;
then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;
then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng (f | ].p,g.[)
f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20;
then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;
then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;
thus N1 c= rng (f | ].p,g.[) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | ].p,g.[) )
A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng (f | ].p,g.[)
then consider r2 being Real such that
A29: r2 = x and
A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and
A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;
then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13;
then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2;
then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32;
then consider s being Real such that
A33: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A34: x = f . s by A1, A23, A24, A17, A27, A29, A28, FCONT_2:15, XBOOLE_1:1;
s in N by A10, A22, A33;
then s in (dom f) /\ ].p,g.[ by A8, A14, XBOOLE_0:def_4;
then A35: s in dom (f | ].p,g.[) by RELAT_1:61;
then x = (f | ].p,g.[) . s by A34, FUNCT_1:47;
hence x in rng (f | ].p,g.[) by A35, FUNCT_1:def_3; ::_thesis: verum
end;
end;
supposeA36: f | ].p,g.[ is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | ].p,g.[)
set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))));
f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21;
then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;
f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21;
then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;
then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng (f | ].p,g.[)
f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21;
then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;
then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;
thus N1 c= rng (f | ].p,g.[) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | ].p,g.[) )
A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng (f | ].p,g.[)
then consider r2 being Real such that
A40: r2 = x and
A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and
A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;
then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13;
then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2;
then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43;
then consider s being Real such that
A44: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A45: x = f . s by A1, A23, A24, A17, A38, A40, A39, FCONT_2:15, XBOOLE_1:1;
s in N by A10, A22, A44;
then s in (dom f) /\ ].p,g.[ by A8, A14, XBOOLE_0:def_4;
then A46: s in dom (f | ].p,g.[) by RELAT_1:61;
then x = (f | ].p,g.[) . s by A45, FUNCT_1:47;
hence x in rng (f | ].p,g.[) by A46, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
end;
hence ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[) ; ::_thesis: verum
end;
hence rng (f | ].p,g.[) is open by RCOMP_1:20; ::_thesis: verum
end;
theorem :: FCONT_3:24
for p being Real
for f being PartFunc of REAL,REAL st 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 ) holds
rng (f | (left_open_halfline p)) is open
proof
let p be Real; ::_thesis: for f being PartFunc of REAL,REAL st 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 ) holds
rng (f | (left_open_halfline p)) is open
let f be PartFunc of REAL,REAL; ::_thesis: ( 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 )
set L = left_open_halfline p;
assume that
A1: left_open_halfline p c= dom f and
A2: f | (left_open_halfline p) is continuous and
A3: ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) ; ::_thesis: rng (f | (left_open_halfline p)) is open
now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_(f_|_(left_open_halfline_p))_holds_
ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_(f_|_(left_open_halfline_p))
let r1 be real number ; ::_thesis: ( r1 in rng (f | (left_open_halfline p)) implies ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) )
set f1 = f | (left_open_halfline p);
assume r1 in rng (f | (left_open_halfline p)) ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p))
then consider x0 being Real such that
A4: x0 in dom (f | (left_open_halfline p)) and
A5: (f | (left_open_halfline p)) . x0 = r1 by PARTFUN1:3;
A6: r1 = f . x0 by A4, A5, FUNCT_1:47;
A7: x0 in (dom f) /\ (left_open_halfline p) by A4, RELAT_1:61;
then x0 in left_open_halfline p by XBOOLE_0:def_4;
then consider N being Neighbourhood of x0 such that
A8: N c= left_open_halfline p by RCOMP_1:18;
consider r being real number such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
0 < r / 2 by A9, XREAL_1:215;
then A11: x0 - (r / 2) < x0 - 0 by XREAL_1:15;
A12: r / 2 < r by A9, XREAL_1:216;
then A13: x0 - r < x0 - (r / 2) by XREAL_1:15;
A14: N c= dom f by A1, A8, XBOOLE_1:1;
set fp = f . (x0 + (r / 2));
set fm = f . (x0 - (r / 2));
A15: x0 + (r / 2) < x0 + r by A12, XREAL_1:8;
A16: x0 < x0 + (r / 2) by A9, XREAL_1:29, XREAL_1:215;
then A17: x0 - (r / 2) < x0 + (r / 2) by A11, XXREAL_0:2;
x0 < x0 + r by A9, XREAL_1:29;
then x0 - (r / 2) < x0 + r by A11, XXREAL_0:2;
then A18: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A13;
then A19: x0 - (r / 2) in (left_open_halfline p) /\ (dom f) by A8, A10, A14, XBOOLE_0:def_4;
x0 - r < x0 by A9, XREAL_1:44;
then x0 - r < x0 + (r / 2) by A16, XXREAL_0:2;
then A20: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A15;
then A21: x0 + (r / 2) in (left_open_halfline p) /\ (dom f) by A8, A10, A14, XBOOLE_0:def_4;
A22: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A18, A20, XXREAL_2:def_12;
f | N is continuous by A2, A8, FCONT_1:16;
then A23: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A10, A22, FCONT_1:16;
A24: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= left_open_halfline p by A8, A10, A18, A20, XXREAL_2:def_12;
now__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_(f_|_(left_open_halfline_p))
percases ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) by A3;
supposeA25: f | (left_open_halfline p) is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p))
set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)));
f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20;
then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;
f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20;
then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;
then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng (f | (left_open_halfline p))
f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20;
then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;
then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;
thus N1 c= rng (f | (left_open_halfline p)) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (left_open_halfline p)) )
A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng (f | (left_open_halfline p))
then consider r2 being Real such that
A29: r2 = x and
A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and
A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;
then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13;
then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2;
then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32;
then consider s being Real such that
A33: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A34: x = f . s by A1, A24, A23, A17, A27, A29, A28, FCONT_2:15, XBOOLE_1:1;
s in N by A10, A22, A33;
then s in (dom f) /\ (left_open_halfline p) by A8, A14, XBOOLE_0:def_4;
then A35: s in dom (f | (left_open_halfline p)) by RELAT_1:61;
then x = (f | (left_open_halfline p)) . s by A34, FUNCT_1:47;
hence x in rng (f | (left_open_halfline p)) by A35, FUNCT_1:def_3; ::_thesis: verum
end;
end;
supposeA36: f | (left_open_halfline p) is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p))
set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))));
f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21;
then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;
f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21;
then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;
then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng (f | (left_open_halfline p))
f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21;
then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;
then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;
thus N1 c= rng (f | (left_open_halfline p)) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (left_open_halfline p)) )
A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng (f | (left_open_halfline p))
then consider r2 being Real such that
A40: r2 = x and
A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and
A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;
then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13;
then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2;
then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43;
then consider s being Real such that
A44: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A45: x = f . s by A1, A24, A23, A17, A38, A40, A39, FCONT_2:15, XBOOLE_1:1;
s in N by A10, A22, A44;
then s in (dom f) /\ (left_open_halfline p) by A8, A14, XBOOLE_0:def_4;
then A46: s in dom (f | (left_open_halfline p)) by RELAT_1:61;
then x = (f | (left_open_halfline p)) . s by A45, FUNCT_1:47;
hence x in rng (f | (left_open_halfline p)) by A46, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
end;
hence ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) ; ::_thesis: verum
end;
hence rng (f | (left_open_halfline p)) is open by RCOMP_1:20; ::_thesis: verum
end;
theorem :: FCONT_3:25
for p being Real
for f being PartFunc of REAL,REAL st 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 ) holds
rng (f | (right_open_halfline p)) is open
proof
let p be Real; ::_thesis: for f being PartFunc of REAL,REAL st 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 ) holds
rng (f | (right_open_halfline p)) is open
let f be PartFunc of REAL,REAL; ::_thesis: ( 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 )
set L = right_open_halfline p;
assume that
A1: right_open_halfline p c= dom f and
A2: f | (right_open_halfline p) is continuous and
A3: ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) ; ::_thesis: rng (f | (right_open_halfline p)) is open
now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_(f_|_(right_open_halfline_p))_holds_
ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_(f_|_(right_open_halfline_p))
let r1 be real number ; ::_thesis: ( r1 in rng (f | (right_open_halfline p)) implies ex N being Neighbourhood of r1 st N c= rng (f | (right_open_halfline p)) )
set f1 = f | (right_open_halfline p);
assume r1 in rng (f | (right_open_halfline p)) ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng (f | (right_open_halfline p))
then consider x0 being Real such that
A4: x0 in dom (f | (right_open_halfline p)) and
A5: (f | (right_open_halfline p)) . x0 = r1 by PARTFUN1:3;
A6: r1 = f . x0 by A4, A5, FUNCT_1:47;
A7: x0 in (dom f) /\ (right_open_halfline p) by A4, RELAT_1:61;
then x0 in right_open_halfline p by XBOOLE_0:def_4;
then consider N being Neighbourhood of x0 such that
A8: N c= right_open_halfline p by RCOMP_1:18;
consider r being real number such that
A9: 0 < r and
A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
0 < r / 2 by A9, XREAL_1:215;
then A11: x0 - (r / 2) < x0 - 0 by XREAL_1:15;
A12: r / 2 < r by A9, XREAL_1:216;
then A13: x0 - r < x0 - (r / 2) by XREAL_1:15;
A14: N c= dom f by A1, A8, XBOOLE_1:1;
set fp = f . (x0 + (r / 2));
set fm = f . (x0 - (r / 2));
A15: x0 + (r / 2) < x0 + r by A12, XREAL_1:8;
A16: x0 < x0 + (r / 2) by A9, XREAL_1:29, XREAL_1:215;
then A17: x0 - (r / 2) < x0 + (r / 2) by A11, XXREAL_0:2;
x0 < x0 + r by A9, XREAL_1:29;
then x0 - (r / 2) < x0 + r by A11, XXREAL_0:2;
then A18: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A13;
then A19: x0 - (r / 2) in (right_open_halfline p) /\ (dom f) by A8, A10, A14, XBOOLE_0:def_4;
x0 - r < x0 by A9, XREAL_1:44;
then x0 - r < x0 + (r / 2) by A16, XXREAL_0:2;
then A20: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A15;
then A21: x0 + (r / 2) in (right_open_halfline p) /\ (dom f) by A8, A10, A14, XBOOLE_0:def_4;
A22: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A18, A20, XXREAL_2:def_12;
f | N is continuous by A2, A8, FCONT_1:16;
then A23: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A10, A22, FCONT_1:16;
A24: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= right_open_halfline p by A8, A10, A18, A20, XXREAL_2:def_12;
now__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_(f_|_(right_open_halfline_p))
percases ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) by A3;
supposeA25: f | (right_open_halfline p) is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (right_open_halfline p))
set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)));
f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20;
then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;
f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20;
then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;
then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng (f | (right_open_halfline p))
f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20;
then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;
then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;
thus N1 c= rng (f | (right_open_halfline p)) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (right_open_halfline p)) )
A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng (f | (right_open_halfline p))
then consider r2 being Real such that
A29: r2 = x and
A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and
A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;
then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13;
then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2;
then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32;
then consider s being Real such that
A33: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A34: x = f . s by A1, A24, A23, A17, A27, A29, A28, FCONT_2:15, XBOOLE_1:1;
s in N by A10, A22, A33;
then s in (dom f) /\ (right_open_halfline p) by A8, A14, XBOOLE_0:def_4;
then A35: s in dom (f | (right_open_halfline p)) by RELAT_1:61;
then x = (f | (right_open_halfline p)) . s by A34, FUNCT_1:47;
hence x in rng (f | (right_open_halfline p)) by A35, FUNCT_1:def_3; ::_thesis: verum
end;
end;
supposeA36: f | (right_open_halfline p) is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (right_open_halfline p))
set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))));
f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21;
then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;
f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21;
then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;
then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng (f | (right_open_halfline p))
f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21;
then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;
then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;
thus N1 c= rng (f | (right_open_halfline p)) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (right_open_halfline p)) )
A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng (f | (right_open_halfline p))
then consider r2 being Real such that
A40: r2 = x and
A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and
A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;
then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13;
then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2;
then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43;
then consider s being Real such that
A44: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A45: x = f . s by A1, A24, A23, A17, A38, A40, A39, FCONT_2:15, XBOOLE_1:1;
s in N by A10, A22, A44;
then s in (dom f) /\ (right_open_halfline p) by A8, A14, XBOOLE_0:def_4;
then A46: s in dom (f | (right_open_halfline p)) by RELAT_1:61;
then x = (f | (right_open_halfline p)) . s by A45, FUNCT_1:47;
hence x in rng (f | (right_open_halfline p)) by A46, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
end;
hence ex N being Neighbourhood of r1 st N c= rng (f | (right_open_halfline p)) ; ::_thesis: verum
end;
hence rng (f | (right_open_halfline p)) is open by RCOMP_1:20; ::_thesis: verum
end;
theorem :: FCONT_3:26
for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f | ([#] REAL) is continuous & ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) holds
rng f is open
proof
let f be PartFunc of REAL,REAL; ::_thesis: ( [#] REAL c= dom f & f | ([#] REAL) is continuous & ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) implies rng f is open )
set L = [#] REAL;
assume that
A1: [#] REAL c= dom f and
A2: f | ([#] REAL) is continuous and
A3: ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) ; ::_thesis: rng f is open
now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_f_holds_
ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_f
let r1 be real number ; ::_thesis: ( r1 in rng f implies ex N being Neighbourhood of r1 st N c= rng f )
assume r1 in rng f ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng f
then consider x0 being Real such that
A4: x0 in dom f and
A5: f . x0 = r1 by PARTFUN1:3;
A6: x0 in ([#] REAL) /\ (dom f) by A4, XBOOLE_0:def_4;
set N = the Neighbourhood of x0;
consider r being real number such that
A7: 0 < r and
A8: the Neighbourhood of x0 = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
0 < r / 2 by A7, XREAL_1:215;
then A9: x0 - (r / 2) < x0 - 0 by XREAL_1:15;
A10: r / 2 < r by A7, XREAL_1:216;
then A11: x0 - r < x0 - (r / 2) by XREAL_1:15;
A12: x0 + (r / 2) < x0 + r by A10, XREAL_1:8;
A13: the Neighbourhood of x0 c= dom f by A1, XBOOLE_1:1;
set fp = f . (x0 + (r / 2));
set fm = f . (x0 - (r / 2));
A14: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A2, FCONT_1:16;
A15: x0 < x0 + (r / 2) by A7, XREAL_1:29, XREAL_1:215;
then A16: x0 - (r / 2) < x0 + (r / 2) by A9, XXREAL_0:2;
x0 - r < x0 by A7, XREAL_1:44;
then x0 - r < x0 + (r / 2) by A15, XXREAL_0:2;
then A17: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A12;
then A18: x0 + (r / 2) in ([#] REAL) /\ (dom f) by A8, A13, XBOOLE_0:def_4;
x0 < x0 + r by A7, XREAL_1:29;
then x0 - (r / 2) < x0 + r by A9, XXREAL_0:2;
then A19: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A11;
then A20: x0 - (r / 2) in ([#] REAL) /\ (dom f) by A8, A13, XBOOLE_0:def_4;
A21: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A19, A17, XXREAL_2:def_12;
now__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_f
percases ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) by A3;
supposeA22: f | ([#] REAL) is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng f
set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)));
f . x0 < f . (x0 + (r / 2)) by A15, A18, A6, A22, RFUNCT_2:20;
then A23: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;
f . (x0 - (r / 2)) < f . x0 by A9, A20, A6, A22, RFUNCT_2:20;
then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;
then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A23, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng f
f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A16, A18, A20, A22, RFUNCT_2:20;
then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;
then A24: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;
thus N1 c= rng f ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng f )
A25: ( [.(x0 - (r / 2)),(x0 + (r / 2)).] c= dom f & ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ) by A1, XBOOLE_1:1, XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng f
then consider r2 being Real such that
A26: r2 = x and
A27: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and
A28: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A5;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;
then A29: r2 < f . (x0 + (r / 2)) by A28, XXREAL_0:2;
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13;
then f . (x0 - (r / 2)) < r2 by A27, XXREAL_0:2;
then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A29;
then consider s being Real such that
A30: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A31: x = f . s by A9, A15, A14, A24, A26, A25, FCONT_2:15, XXREAL_0:2;
s in the Neighbourhood of x0 by A8, A21, A30;
hence x in rng f by A13, A31, FUNCT_1:def_3; ::_thesis: verum
end;
end;
supposeA32: f | ([#] REAL) is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng f
set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))));
f . (x0 + (r / 2)) < f . x0 by A15, A18, A6, A32, RFUNCT_2:21;
then A33: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;
f . x0 < f . (x0 - (r / 2)) by A9, A20, A6, A32, RFUNCT_2:21;
then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;
then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A33, XXREAL_0:15;
then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6;
take N1 = N1; ::_thesis: N1 c= rng f
f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A16, A18, A20, A32, RFUNCT_2:21;
then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;
then A34: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;
thus N1 c= rng f ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng f )
A35: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;
assume x in N1 ; ::_thesis: x in rng f
then consider r2 being Real such that
A36: r2 = x and
A37: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and
A38: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A5;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;
then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;
then A39: r2 < f . (x0 - (r / 2)) by A38, XXREAL_0:2;
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17;
then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13;
then f . (x0 + (r / 2)) < r2 by A37, XXREAL_0:2;
then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A39;
then consider s being Real such that
A40: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and
A41: x = f . s by A1, A14, A16, A34, A36, A35, FCONT_2:15, XBOOLE_1:1;
s in the Neighbourhood of x0 by A8, A21, A40;
hence x in rng f by A13, A41, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
end;
hence ex N being Neighbourhood of r1 st N c= rng f ; ::_thesis: verum
end;
hence rng f is open by RCOMP_1:20; ::_thesis: verum
end;