:: by Jaros{\l}aw Kotowicz

::

:: Received January 10, 1991

:: Copyright (c) 1991-2019 Association of Mizar Users

registration

coherence

[#] REAL is closed by XREAL_0:def 1;

coherence

for b_{1} being Subset of REAL st b_{1} is empty holds

b_{1} is closed
by XBOOLE_1:3;

end;
[#] REAL is closed by XREAL_0:def 1;

coherence

for b

b

registration

coherence

[#] REAL is open

for b_{1} being Subset of REAL st b_{1} is empty holds

b_{1} is open

end;
[#] REAL is open

proof end;

coherence for b

b

proof end;

registration

let r be Real;

coherence

right_closed_halfline r is closed

left_closed_halfline r is closed

right_open_halfline r is open

halfline r is open

end;
coherence

right_closed_halfline r is closed

proof end;

coherence left_closed_halfline r is closed

proof end;

coherence right_open_halfline r is open

proof end;

coherence halfline r is open

proof end;

theorem Th3: :: FCONT_3:3

for x0, r1, g, r being Real st g = x0 + r1 & |.r1.| < r holds

( 0 < r & g in ].(x0 - r),(x0 + r).[ )

( 0 < r & g in ].(x0 - r),(x0 + r).[ )

proof end;

theorem Th5: :: FCONT_3:5

for p being Real

for a being Real_Sequence

for x0 being Real st ( for n being Nat holds a . n = x0 - (p / (n + 1)) ) holds

( a is convergent & lim a = x0 )

for a being Real_Sequence

for x0 being Real st ( for n being Nat holds a . n = x0 - (p / (n + 1)) ) holds

( a is convergent & lim a = x0 )

proof end;

theorem Th6: :: FCONT_3:6

for p being Real

for a being Real_Sequence

for x0 being Real st ( for n being Nat holds a . n = x0 + (p / (n + 1)) ) holds

( a is convergent & lim a = x0 )

for a being Real_Sequence

for x0 being Real st ( for n being Nat holds a . n = x0 + (p / (n + 1)) ) holds

( a is convergent & lim a = x0 )

proof end;

theorem :: FCONT_3:7

for x0, r being Real

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

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

for f being one-to-one PartFunc of REAL,REAL st f | X is increasing holds

((f | X) ") | (f .: X) is increasing

proof 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

for f being one-to-one PartFunc of REAL,REAL st f | X is decreasing holds

((f | X) ") | (f .: X) is decreasing

proof 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

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

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

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

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

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

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

theorem :: FCONT_3:17

for g, p 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

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

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

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

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

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

(f ") | (rng f) is continuous

proof end;

theorem :: FCONT_3:23

for g, p 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

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

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

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

rng f is open

proof end;