:: FCONT_1 semantic presentation

definition

let f be PartFunc of REAL , REAL ;
let x0 be real number ;
pred f is_continuous_in x0 means :Def1: :: FCONT_1:def 1
( x0 in dom f & ( 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) ) ) );

end;

:: deftheorem Def1 defines is_continuous_in FCONT_1:def 1 :

theorem :: FCONT_1:1

canceled;

theorem :: FCONT_1:2

for x0 being real number
for f being PartFunc of REAL , REAL holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being 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 ( x0 in dom f & ( 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 ( x0 in dom f & ( 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 ( x0 in dom f & ( 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 x0 in dom f & 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 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 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 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

proof end;

theorem :: FCONT_1:11

for x0 being real number
for f1, f2 being PartFunc of REAL , REAL st 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 f1, f2 being PartFunc of REAL , REAL st 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 ;
let X be set ;
pred f is_continuous_on X means :Def2: :: FCONT_1:def 2
( X c= dom f & ( for x0 being real number st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def2 defines is_continuous_on FCONT_1:def 2 :

theorem :: FCONT_1:13

canceled;

theorem Th14: :: FCONT_1:14

for X being set
for f being PartFunc of REAL , REAL holds
( f is_continuous_on X iff ( X c= dom f & ( 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 Th15: :: FCONT_1:15

for X being set
for f being PartFunc of REAL , REAL holds
( f is_continuous_on X iff ( X c= dom f & ( 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;

theorem Th16: :: FCONT_1:16

for X being set
for f being PartFunc of REAL , REAL holds
( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem Th17: :: FCONT_1:17

for X, X1 being set
for f being PartFunc of REAL , REAL st f is_continuous_on X & X1 c= X holds
f is_continuous_on X1

proof end;

theorem :: FCONT_1:18

for x0 being real number
for f being PartFunc of REAL , REAL st x0 in dom f holds
f is_continuous_on {x0}

proof end;

theorem Th19: :: FCONT_1:19

for X being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_continuous_on X & f2 is_continuous_on X holds
( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X & f1 (#) f2 is_continuous_on X )

proof end;

theorem :: FCONT_1:20

for X, X1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_continuous_on X & f2 is_continuous_on X1 holds
( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 & f1 (#) f2 is_continuous_on X /\ X1 )

proof end;

theorem Th21: :: FCONT_1:21

for r being real number
for X being set
for f being PartFunc of REAL , REAL st f is_continuous_on X holds
r (#) f is_continuous_on X

proof end;

theorem :: FCONT_1:22

for X being set
for f being PartFunc of REAL , REAL st f is_continuous_on X holds
( abs f is_continuous_on X & - f is_continuous_on X )

proof end;

theorem Th23: :: FCONT_1:23

for X being set
for f being PartFunc of REAL , REAL st f is_continuous_on X & f " {0} = {} holds
f ^ is_continuous_on X

proof end;

theorem :: FCONT_1:24

for X being set
for f being PartFunc of REAL , REAL st f is_continuous_on X & (f | X) " {0} = {} holds
f ^ is_continuous_on X

proof end;

theorem :: FCONT_1:25

for X being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_continuous_on X & f1 " {0} = {} & f2 is_continuous_on X holds
f2 / f1 is_continuous_on X

proof end;

theorem :: FCONT_1:26

for X being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_continuous_on X & f2 is_continuous_on f1 .: X holds
f2 * f1 is_continuous_on X

proof end;

theorem :: FCONT_1:27

for X, X1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_continuous_on X & f2 is_continuous_on X1 holds
f2 * f1 is_continuous_on X /\ (f1 " X1)

proof end;

theorem :: FCONT_1:28

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

proof end;

theorem Th29: :: FCONT_1:29

for f being PartFunc of REAL , REAL st dom f is compact & f is_continuous_on dom f holds
rng f is compact

proof end;

theorem :: FCONT_1:30

for Y being Subset of REAL
for f being PartFunc of REAL , REAL st Y c= dom f & Y is compact & f is_continuous_on Y holds
f .: Y is compact

proof end;

theorem Th31: :: FCONT_1:31

for f being PartFunc of REAL , REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f 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) )

proof end;

theorem :: FCONT_1:32

for f being PartFunc of REAL , REAL
for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y 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;

definition

let f be PartFunc of REAL , REAL ;
let X be set ;
pred f is_Lipschitzian_on X means :Def3: :: FCONT_1:def 3
( X c= dom f & ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in X & x2 in X holds
abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) ) ) );

end;

:: deftheorem Def3 defines is_Lipschitzian_on FCONT_1:def 3 :

theorem :: FCONT_1:33

canceled;

theorem Th34: :: FCONT_1:34

for X, X1 being set
for f being PartFunc of REAL , REAL st f is_Lipschitzian_on X & X1 c= X holds
f is_Lipschitzian_on X1

proof end;

theorem :: FCONT_1:35

for X, X1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 + f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: FCONT_1:36

for X, X1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds
f1 - f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: FCONT_1:37

for X, X1, Z, Z1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 & f1 is_bounded_on Z & f2 is_bounded_on Z1 holds
f1 (#) f2 is_Lipschitzian_on ((X /\ Z) /\ X1) /\ Z1

proof end;

theorem Th38: :: FCONT_1:38

for X being set
for p being real number
for f being PartFunc of REAL , REAL st f is_Lipschitzian_on X holds
p (#) f is_Lipschitzian_on X

proof end;

theorem :: FCONT_1:39

for X being set
for f being PartFunc of REAL , REAL st f is_Lipschitzian_on X holds
( - f is_Lipschitzian_on X & abs f is_Lipschitzian_on X )

proof end;

theorem Th40: :: FCONT_1:40

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_constant_on X holds
f is_Lipschitzian_on X

proof end;

theorem :: FCONT_1:41

for Y being Subset of REAL holds id Y is_Lipschitzian_on Y

proof end;

theorem Th42: :: FCONT_1:42

for X being set
for f being PartFunc of REAL , REAL st f is_Lipschitzian_on X holds
f is_continuous_on X

proof end;

theorem :: FCONT_1:43

for f being PartFunc of REAL , REAL st ex r being real number st rng f = {r} holds
f is_continuous_on dom f

proof end;

theorem Th44: :: FCONT_1:44

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

proof end;

theorem Th45: :: FCONT_1:45

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_on dom f

proof end;

theorem :: FCONT_1:46

for f being PartFunc of REAL , REAL st f = id (dom f) holds
f is_continuous_on dom f

proof end;

theorem :: FCONT_1:47

for Y being Subset of REAL
for f being PartFunc of REAL , REAL st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y

proof end;

theorem :: FCONT_1:48

for X being set
for r, p being real number
for f being PartFunc of REAL , REAL st X c= dom f & ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) holds
f is_continuous_on X

proof end;

theorem Th49: :: FCONT_1:49

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 is_continuous_on dom f

proof end;

theorem :: FCONT_1:50

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

proof end;

theorem Th51: :: FCONT_1:51

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_on dom f

proof end;

theorem :: FCONT_1:52

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 = abs x0 ) holds
f is_continuous_on X

proof end;

theorem Th53: :: FCONT_1:53

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 number st
( p <= g & f .: X = [.p,g.] ) holds
f is_continuous_on X

proof end;

theorem :: FCONT_1:54

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 is_increasing_on [.p,g.] or f is_decreasing_on [.p,g.] ) holds
(f | [.p,g.]) " is_continuous_on f .: [.p,g.]

proof end;