:: by Konrad Raczkowski and Pawe{\l} Sadowski

::

:: Received June 18, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let f be PartFunc of REAL,REAL;

let x0 be real number ;

end;
let x0 be real number ;

pred f is_continuous_in x0 means :Def1: :: FCONT_1:def 1

for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f . x0 = lim (f /* s1) );

for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f . x0 = lim (f /* s1) );

:: deftheorem Def1 defines is_continuous_in FCONT_1:def 1 :

for f being PartFunc of REAL,REAL

for x0 being real number holds

( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f . x0 = lim (f /* s1) ) );

for f being PartFunc of REAL,REAL

for x0 being real number holds

( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f . x0 = lim (f /* s1) ) );

theorem Th1: :: FCONT_1:1

for X being set

for x0 being real number

for f being PartFunc of REAL,REAL st x0 in X & f is_continuous_in x0 holds

f | X is_continuous_in x0

for x0 being real number

for f being PartFunc of REAL,REAL st x0 in X & f is_continuous_in x0 holds

f | X is_continuous_in x0

proof end;

theorem :: FCONT_1:2

for x0 being real number

for f being PartFunc of REAL,REAL holds

( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )

for f being PartFunc of REAL,REAL holds

( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )

proof end;

theorem Th3: :: FCONT_1:3

for x0 being real number

for f being PartFunc of REAL,REAL holds

( f is_continuous_in x0 iff for r being real number st 0 < r holds

ex s being real number st

( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds

abs ((f . x1) - (f . x0)) < r ) ) )

for f being PartFunc of REAL,REAL holds

( f is_continuous_in x0 iff for r being real number st 0 < r holds

ex s being real number st

( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds

abs ((f . x1) - (f . x0)) < r ) ) )

proof end;

theorem Th4: :: FCONT_1:4

for f being PartFunc of REAL,REAL

for x0 being real number holds

( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st

for x1 being real number st x1 in dom f & x1 in N holds

f . x1 in N1 )

for x0 being real number holds

( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st

for x1 being real number st x1 in dom f & x1 in N holds

f . x1 in N1 )

proof end;

theorem Th5: :: FCONT_1:5

for f being PartFunc of REAL,REAL

for x0 being real number holds

( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )

for x0 being real number holds

( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )

proof end;

theorem :: FCONT_1:6

for x0 being real number

for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

proof end;

theorem Th7: :: FCONT_1:7

for x0 being real number

for f1, f2 being PartFunc of REAL,REAL st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds

( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )

for f1, f2 being PartFunc of REAL,REAL st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds

( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )

proof end;

theorem Th8: :: FCONT_1:8

for x0, r being real number

for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds

r (#) f is_continuous_in x0

for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds

r (#) f is_continuous_in x0

proof end;

theorem :: FCONT_1:9

for x0 being real number

for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds

( abs f is_continuous_in x0 & - f is_continuous_in x0 )

for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds

( abs f is_continuous_in x0 & - f is_continuous_in x0 )

proof end;

theorem Th10: :: FCONT_1:10

for x0 being real number

for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> 0 holds

f ^ is_continuous_in x0

for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> 0 holds

f ^ is_continuous_in x0

proof end;

theorem :: FCONT_1:11

for x0 being real number

for f2, f1 being PartFunc of REAL,REAL st x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 holds

f2 / f1 is_continuous_in x0

for f2, f1 being PartFunc of REAL,REAL st x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 holds

f2 / f1 is_continuous_in x0

proof end;

theorem Th12: :: FCONT_1:12

for x0 being real number

for f2, f1 being PartFunc of REAL,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 holds

f2 * f1 is_continuous_in x0

for f2, f1 being PartFunc of REAL,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 . x0 holds

f2 * f1 is_continuous_in x0

proof end;

definition

let f be PartFunc of REAL,REAL;

end;
attr f is continuous means :Def2: :: FCONT_1:def 2

for x0 being real number st x0 in dom f holds

f is_continuous_in x0;

for x0 being real number st x0 in dom f holds

f is_continuous_in x0;

:: deftheorem Def2 defines continuous FCONT_1:def 2 :

for f being PartFunc of REAL,REAL holds

( f is continuous iff for x0 being real number st x0 in dom f holds

f is_continuous_in x0 );

for f being PartFunc of REAL,REAL holds

( f is continuous iff for x0 being real number st x0 in dom f holds

f is_continuous_in x0 );

theorem Th13: :: FCONT_1:13

for X being set

for f being PartFunc of REAL,REAL st X c= dom f holds

( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )

for f being PartFunc of REAL,REAL st X c= dom f holds

( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )

proof end;

theorem Th14: :: FCONT_1:14

for X being set

for f being PartFunc of REAL,REAL st X c= dom f holds

( f | X is continuous iff for x0, r being real number st x0 in X & 0 < r holds

ex s being real number st

( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds

abs ((f . x1) - (f . x0)) < r ) ) )

for f being PartFunc of REAL,REAL st X c= dom f holds

( f | X is continuous iff for x0, r being real number st x0 in X & 0 < r holds

ex s being real number st

( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds

abs ((f . x1) - (f . x0)) < r ) ) )

proof end;

registration

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} is V8() holds

b_{1} is continuous

end;
for b

b

proof end;

registration

ex b_{1} being PartFunc of REAL,REAL st b_{1} is continuous
end;

cluster Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued continuous for Element of bool [:REAL,REAL:];

existence ex b

proof end;

registration

let f be continuous PartFunc of REAL,REAL;

let X be set ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is continuous

end;
let X be set ;

coherence

for b

b

proof end;

theorem :: FCONT_1:15

for X being set

for f being PartFunc of REAL,REAL holds

( f | X is continuous iff (f | X) | X is continuous ) ;

for f being PartFunc of REAL,REAL holds

( f | X is continuous iff (f | X) | X is continuous ) ;

theorem Th16: :: FCONT_1:16

for X, X1 being set

for f being PartFunc of REAL,REAL st f | X is continuous & X1 c= X holds

f | X1 is continuous

for f being PartFunc of REAL,REAL st f | X is continuous & X1 c= X holds

f | X1 is continuous

proof end;

registration
end;

registration

let f be PartFunc of REAL,REAL;

let X be trivial set ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is continuous

end;
let X be trivial set ;

coherence

for b

b

proof end;

theorem :: FCONT_1:17

registration

let f1, f2 be continuous PartFunc of REAL,REAL;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = f1 + f2 holds

b_{1} is continuous

for b_{1} being PartFunc of REAL,REAL st b_{1} = f1 - f2 holds

b_{1} is continuous

for b_{1} being PartFunc of REAL,REAL st b_{1} = f1 (#) f2 holds

b_{1} is continuous

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

theorem Th18: :: FCONT_1:18

for X being set

for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds

( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )

for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds

( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous & (f1 (#) f2) | X is continuous )

proof end;

theorem :: FCONT_1:19

for X, X1 being set

for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds

( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous )

for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds

( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous & (f1 (#) f2) | (X /\ X1) is continuous )

proof end;

registration

let f be continuous PartFunc of REAL,REAL;

let r be real number ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = r (#) f holds

b_{1} is continuous

end;
let r be real number ;

coherence

for b

b

proof end;

theorem Th20: :: FCONT_1:20

for r being real number

for X being set

for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

for X being set

for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

proof end;

theorem :: FCONT_1:21

for X being set

for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

( (abs f) | X is continuous & (- f) | X is continuous )

for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds

( (abs f) | X is continuous & (- f) | X is continuous )

proof end;

theorem Th22: :: FCONT_1:22

for X being set

for f being PartFunc of REAL,REAL st f | X is continuous & f " {0} = {} holds

(f ^) | X is continuous

for f being PartFunc of REAL,REAL st f | X is continuous & f " {0} = {} holds

(f ^) | X is continuous

proof end;

theorem :: FCONT_1:23

for X being set

for f being PartFunc of REAL,REAL st f | X is continuous & (f | X) " {0} = {} holds

(f ^) | X is continuous

for f being PartFunc of REAL,REAL st f | X is continuous & (f | X) " {0} = {} holds

(f ^) | X is continuous

proof end;

theorem :: FCONT_1:24

for X being set

for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " {0} = {} & f2 | X is continuous holds

(f2 / f1) | X is continuous

for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " {0} = {} & f2 | X is continuous holds

(f2 / f1) | X is continuous

proof end;

registration

let f1, f2 be continuous PartFunc of REAL,REAL;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = f2 * f1 holds

b_{1} is continuous

end;
coherence

for b

b

proof end;

theorem :: FCONT_1:25

for X being set

for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | (f1 .: X) is continuous holds

(f2 * f1) | X is continuous

for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | (f1 .: X) is continuous holds

(f2 * f1) | X is continuous

proof end;

theorem :: FCONT_1:26

for X, X1 being set

for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | X1 is continuous holds

(f2 * f1) | (X /\ (f1 " X1)) is continuous

for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | X1 is continuous holds

(f2 * f1) | (X /\ (f1 " X1)) is continuous

proof end;

theorem :: FCONT_1:27

for f being PartFunc of REAL,REAL st f is total & ( for x1, x2 being real number holds f . (x1 + x2) = (f . x1) + (f . x2) ) & ex x0 being real number st f is_continuous_in x0 holds

f | REAL is continuous

f | REAL is continuous

proof end;

theorem Th28: :: FCONT_1:28

for f being PartFunc of REAL,REAL st dom f is compact & f | (dom f) is continuous holds

rng f is compact

rng f is compact

proof end;

theorem :: FCONT_1:29

for Y being Subset of REAL

for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

proof end;

theorem Th30: :: FCONT_1:30

for f being PartFunc of REAL,REAL st dom f <> {} & dom f is compact & f | (dom f) is continuous holds

ex x1, x2 being real number st

( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )

ex x1, x2 being real number st

( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )

proof end;

:: Weierstrass Extreme Value Theorem

theorem :: FCONT_1:31

for f being PartFunc of REAL,REAL

for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is continuous holds

ex x1, x2 being real number st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is continuous holds

ex x1, x2 being real number st

( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )

proof end;

:: deftheorem Def3 defines Lipschitzian FCONT_1:def 3 :

for f being PartFunc of REAL,REAL holds

( f is Lipschitzian iff ex r being real number st

( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds

abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) );

for f being PartFunc of REAL,REAL holds

( f is Lipschitzian iff ex r being real number st

( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds

abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) );

theorem Th32: :: FCONT_1:32

for X being set

for f being PartFunc of REAL,REAL holds

( f | X is Lipschitzian iff ex r being real number st

( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds

abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) )

for f being PartFunc of REAL,REAL holds

( f | X is Lipschitzian iff ex r being real number st

( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds

abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) )

proof end;

registration

coherence

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

b_{1} is Lipschitzian

end;
for b

b

proof end;

registration

ex b_{1} being PartFunc of REAL,REAL st b_{1} is empty
end;

cluster Relation-like REAL -defined REAL -valued Function-like empty complex-valued ext-real-valued real-valued for Element of bool [:REAL,REAL:];

existence ex b

proof end;

registration

let f be Lipschitzian PartFunc of REAL,REAL;

let X be set ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = f | X holds

b_{1} is Lipschitzian

end;
let X be set ;

coherence

for b

b

proof end;

theorem :: FCONT_1:33

for X, X1 being set

for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X1 c= X holds

f | X1 is Lipschitzian

for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X1 c= X holds

f | X1 is Lipschitzian

proof end;

registration

let f1, f2 be Lipschitzian PartFunc of REAL,REAL;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = f1 + f2 holds

b_{1} is Lipschitzian

for b_{1} being PartFunc of REAL,REAL st b_{1} = f1 - f2 holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

theorem :: FCONT_1:34

for X, X1 being set

for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 + f2) | (X /\ X1) is Lipschitzian

for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 + f2) | (X /\ X1) is Lipschitzian

proof end;

theorem :: FCONT_1:35

for X, X1 being set

for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

proof end;

registration

let f1, f2 be bounded Lipschitzian PartFunc of REAL,REAL;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = f1 (#) f2 holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

theorem :: FCONT_1:36

for X, X1, Z, Z1 being set

for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded holds

(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian

for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded holds

(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian

proof end;

registration

let f be Lipschitzian PartFunc of REAL,REAL;

let p be real number ;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = p (#) f holds

b_{1} is Lipschitzian

end;
let p be real number ;

coherence

for b

b

proof end;

theorem :: FCONT_1:37

for X being set

for p being real number

for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

for p being real number

for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

proof end;

registration

let f be Lipschitzian PartFunc of REAL,REAL;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = abs f holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

theorem :: FCONT_1:38

for X being set

for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds

( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )

for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds

( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )

proof end;

registration

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} is V8() holds

b_{1} is Lipschitzian

end;
for b

b

proof end;

registration

let Y be Subset of REAL;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = id Y holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

registration

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} is Lipschitzian holds

b_{1} is continuous

end;
for b

b

proof end;

theorem :: FCONT_1:40

for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in dom f holds

f . x0 = x0 ) holds

f is continuous

f . x0 = x0 ) holds

f is continuous

proof end;

theorem Th41: :: FCONT_1:41

for X being set

for r, p being real number

for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds

f . x0 = (r * x0) + p ) holds

f | X is continuous

for r, p being real number

for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds

f . x0 = (r * x0) + p ) holds

f | X is continuous

proof end;

theorem Th42: :: FCONT_1:42

for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in dom f holds

f . x0 = x0 ^2 ) holds

f | (dom f) is continuous

f . x0 = x0 ^2 ) holds

f | (dom f) is continuous

proof end;

theorem :: FCONT_1:43

for X being set

for f being PartFunc of REAL,REAL st X c= dom f & ( for x0 being real number st x0 in X holds

f . x0 = x0 ^2 ) holds

f | X is continuous

for f being PartFunc of REAL,REAL st X c= dom f & ( for x0 being real number st x0 in X holds

f . x0 = x0 ^2 ) holds

f | X is continuous

proof end;

theorem Th44: :: FCONT_1:44

for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in dom f holds

f . x0 = abs x0 ) holds

f is continuous

f . x0 = abs x0 ) holds

f is continuous

proof end;

theorem :: FCONT_1:45

for X being set

for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds

f . x0 = abs x0 ) holds

f | X is continuous

for f being PartFunc of REAL,REAL st ( for x0 being real number st x0 in X holds

f . x0 = abs x0 ) holds

f | X is continuous

proof end;

theorem Th46: :: FCONT_1:46

for X being set

for f being PartFunc of REAL,REAL st f | X is monotone & ex p, g being real number st

( p <= g & f .: X = [.p,g.] ) holds

f | X is continuous

for f being PartFunc of REAL,REAL st f | X is monotone & ex p, g being real number st

( p <= g & f .: X = [.p,g.] ) holds

f | X is continuous

proof end;

theorem :: FCONT_1:47

for p, g being real number

for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) holds

((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous

for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) holds

((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous

proof end;

:: from

definition

let a, b be real number ;

ex b_{1} being Function of REAL,REAL st

for x being real number holds b_{1} . x = (a * x) + b

for b_{1}, b_{2} being Function of REAL,REAL st ( for x being real number holds b_{1} . x = (a * x) + b ) & ( for x being real number holds b_{2} . x = (a * x) + b ) holds

b_{1} = b_{2}

end;
func AffineMap (a,b) -> Function of REAL,REAL means :Def4: :: FCONT_1:def 4

for x being real number holds it . x = (a * x) + b;

existence for x being real number holds it . x = (a * x) + b;

ex b

for x being real number holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines AffineMap FCONT_1:def 4 :

for a, b being real number

for b_{3} being Function of REAL,REAL holds

( b_{3} = AffineMap (a,b) iff for x being real number holds b_{3} . x = (a * x) + b );

for a, b being real number

for b

( b

registration

ex b_{1} being Function of REAL,REAL st b_{1} is continuous
end;

cluster Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous for Element of bool [:REAL,REAL:];

existence ex b

proof end;

theorem :: FCONT_1:51

for a, b, x, y being real number st a > 0 & x < y holds

(AffineMap (a,b)) . x < (AffineMap (a,b)) . y

(AffineMap (a,b)) . x < (AffineMap (a,b)) . y

proof end;

theorem :: FCONT_1:52

for a, b, x, y being real number st a < 0 & x < y holds

(AffineMap (a,b)) . x > (AffineMap (a,b)) . y

(AffineMap (a,b)) . x > (AffineMap (a,b)) . y

proof end;

theorem Th53: :: FCONT_1:53

for a, b, x, y being real number st a >= 0 & x <= y holds

(AffineMap (a,b)) . x <= (AffineMap (a,b)) . y

(AffineMap (a,b)) . x <= (AffineMap (a,b)) . y

proof end;

theorem :: FCONT_1:54

for a, b, x, y being real number st a <= 0 & x <= y holds

(AffineMap (a,b)) . x >= (AffineMap (a,b)) . y

(AffineMap (a,b)) . x >= (AffineMap (a,b)) . y

proof end;