[#] REAL is closed

{} REAL is open

{} REAL is closed

[#] REAL is open

for r being real number holds right_closed_halfline r is closed

for r being real number holds left_closed_halfline r is closed

for r being real number holds right_open_halfline r is open

for r being real number holds left_open_halfline r is open

for g, x0 being Real
for r being real number holds
( ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) iff ex r1 being Real st
( g = x0 + r1 & abs r1 < r ) )

for g, x0 being Real
for r being real number holds
( ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) iff g - x0 in ].(- r),r.[ )

for p being Real holds left_closed_halfline p = {p} \/ (left_open_halfline p)

for p being Real holds right_closed_halfline p = {p} \/ (right_open_halfline p)

for p being Real
for a being Real_Sequence
for x0 being real number st ( for n being Nat holds a . n = x0 - (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )

for p being Real
for a being Real_Sequence
for x0 being real number st ( for n being Nat holds a . n = x0 + (p / (n + 1)) ) holds
( a is convergent & lim a = x0 )

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 ) )

for X being set
for f being PartFunc of REAL , REAL st ( f is_increasing_on X or f is_decreasing_on X ) holds
f | X is one-to-one

for X being set
for f being one-to-one PartFunc of REAL , REAL st f is_increasing_on X holds
(f | X) " is_increasing_on f .: X

for X being set
for f being one-to-one PartFunc of REAL , REAL st f is_decreasing_on X holds
(f | X) " is_decreasing_on f .: X

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_monotone_on X & ex p being Real st f .: X = left_open_halfline p holds
f is_continuous_on X

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_monotone_on X & ex p being Real st f .: X = right_open_halfline p holds
f is_continuous_on X

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_monotone_on X & ex p being Real st f .: X = left_closed_halfline p holds
f is_continuous_on X

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_monotone_on X & ex p being Real st f .: X = right_closed_halfline p holds
f is_continuous_on X

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_monotone_on X & ex p, g being Real st f .: X = ].p,g.[ holds
f is_continuous_on X

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_monotone_on X & f .: X = REAL holds
f is_continuous_on X

for p, g being Real
for f being one-to-one PartFunc of REAL , REAL st ( f is_increasing_on ].p,g.[ or f is_decreasing_on ].p,g.[ ) & ].p,g.[ c= dom f holds
(f | ].p,g.[) " is_continuous_on f .: ].p,g.[

for p being Real
for f being one-to-one PartFunc of REAL , REAL st ( f is_increasing_on left_open_halfline p or f is_decreasing_on left_open_halfline p ) & left_open_halfline p c= dom f holds
(f | (left_open_halfline p)) " is_continuous_on f .: (left_open_halfline p)

for p being Real
for f being one-to-one PartFunc of REAL , REAL st ( f is_increasing_on right_open_halfline p or f is_decreasing_on right_open_halfline p ) & right_open_halfline p c= dom f holds
(f | (right_open_halfline p)) " is_continuous_on f .: (right_open_halfline p)

for p being Real
for f being one-to-one PartFunc of REAL , REAL st ( f is_increasing_on left_closed_halfline p or f is_decreasing_on left_closed_halfline p ) & left_closed_halfline p c= dom f holds
(f | (left_closed_halfline p)) " is_continuous_on f .: (left_closed_halfline p)

for p being Real
for f being one-to-one PartFunc of REAL , REAL st ( f is_increasing_on right_closed_halfline p or f is_decreasing_on right_closed_halfline p ) & right_closed_halfline p c= dom f holds
(f | (right_closed_halfline p)) " is_continuous_on f .: (right_closed_halfline p)

for f being one-to-one PartFunc of REAL , REAL st ( f is_increasing_on [#] REAL or f is_decreasing_on [#] REAL ) & f is total holds
f " is_continuous_on rng f

for p, g being Real
for f being PartFunc of REAL , REAL st f is_continuous_on ].p,g.[ & ( f is_increasing_on ].p,g.[ or f is_decreasing_on ].p,g.[ ) holds
rng (f | ].p,g.[) is open

for p being Real
for f being PartFunc of REAL , REAL st f is_continuous_on left_open_halfline p & ( f is_increasing_on left_open_halfline p or f is_decreasing_on left_open_halfline p ) holds
rng (f | (left_open_halfline p)) is open

for p being Real
for f being PartFunc of REAL , REAL st f is_continuous_on right_open_halfline p & ( f is_increasing_on right_open_halfline p or f is_decreasing_on right_open_halfline p ) holds
rng (f | (right_open_halfline p)) is open

for f being PartFunc of REAL , REAL st f is_continuous_on [#] REAL & ( f is_increasing_on [#] REAL or f is_decreasing_on [#] REAL ) holds
rng f is open