:: FCONT_1 semantic presentation

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be real number ;
pred c1 is_continuous_in c2 means :Def1: :: FCONT_1:def 1
( a2 in dom a1 & ( for b1 being Real_Sequence st rng b1 c= dom a1 & b1 is convergent & lim b1 = a2 holds
( a1 * b1 is convergent & a1 . a2 = lim (a1 * b1) ) ) );
end;

:: deftheorem Def1 defines is_continuous_in FCONT_1:def 1 :
for b1 being PartFunc of REAL , REAL
for b2 being real number holds
( b1 is_continuous_in b2 iff ( b2 in dom b1 & ( for b3 being Real_Sequence st rng b3 c= dom b1 & b3 is convergent & lim b3 = b2 holds
( b1 * b3 is convergent & b1 . b2 = lim (b1 * b3) ) ) ) );

theorem Th1: :: FCONT_1:1
canceled;

theorem Th2: :: FCONT_1:2
for b1 being real number
for b2 being PartFunc of REAL , REAL holds
( b2 is_continuous_in b1 iff ( b1 in dom b2 & ( for b3 being Real_Sequence st rng b3 c= dom b2 & b3 is convergent & lim b3 = b1 & ( for b4 being Nat holds b3 . b4 <> b1 ) holds
( b2 * b3 is convergent & b2 . b1 = lim (b2 * b3) ) ) ) )
proof end;

theorem Th3: :: FCONT_1:3
for b1 being real number
for b2 being PartFunc of REAL , REAL holds
( b2 is_continuous_in b1 iff ( b1 in dom b2 & ( for b3 being real number st 0 < b3 holds
ex b4 being real number st
( 0 < b4 & ( for b5 being real number st b5 in dom b2 & abs (b5 - b1) < b4 holds
abs ((b2 . b5) - (b2 . b1)) < b3 ) ) ) ) )
proof end;

theorem Th4: :: FCONT_1:4
for b1 being PartFunc of REAL , REAL
for b2 being real number holds
( b1 is_continuous_in b2 iff ( b2 in dom b1 & ( for b3 being Neighbourhood of b1 . b2 ex b4 being Neighbourhood of b2 st
for b5 being real number st b5 in dom b1 & b5 in b4 holds
b1 . b5 in b3 ) ) )
proof end;

theorem Th5: :: FCONT_1:5
for b1 being PartFunc of REAL , REAL
for b2 being real number holds
( b1 is_continuous_in b2 iff ( b2 in dom b1 & ( for b3 being Neighbourhood of b1 . b2 ex b4 being Neighbourhood of b2 st b1 .: b4 c= b3 ) ) )
proof end;

theorem Th6: :: FCONT_1:6
for b1 being real number
for b2 being PartFunc of REAL , REAL st b1 in dom b2 & ex b3 being Neighbourhood of b1 st (dom b2) /\ b3 = {b1} holds
b2 is_continuous_in b1
proof end;

theorem Th7: :: FCONT_1:7
for b1 being real number
for b2, b3 being PartFunc of REAL , REAL st b2 is_continuous_in b1 & b3 is_continuous_in b1 holds
( b2 + b3 is_continuous_in b1 & b2 - b3 is_continuous_in b1 & b2 (#) b3 is_continuous_in b1 )
proof end;

theorem Th8: :: FCONT_1:8
for b1, b2 being real number
for b3 being PartFunc of REAL , REAL st b3 is_continuous_in b1 holds
b2 (#) b3 is_continuous_in b1
proof end;

theorem Th9: :: FCONT_1:9
for b1 being real number
for b2 being PartFunc of REAL , REAL st b2 is_continuous_in b1 holds
( abs b2 is_continuous_in b1 & - b2 is_continuous_in b1 )
proof end;

theorem Th10: :: FCONT_1:10
for b1 being real number
for b2 being PartFunc of REAL , REAL st b2 is_continuous_in b1 & b2 . b1 <> 0 holds
b2 ^ is_continuous_in b1
proof end;

theorem Th11: :: FCONT_1:11
for b1 being real number
for b2, b3 being PartFunc of REAL , REAL st b2 is_continuous_in b1 & b2 . b1 <> 0 & b3 is_continuous_in b1 holds
b3 / b2 is_continuous_in b1
proof end;

theorem Th12: :: FCONT_1:12
for b1 being real number
for b2, b3 being PartFunc of REAL , REAL st b2 is_continuous_in b1 & b3 is_continuous_in b2 . b1 holds
b3 * b2 is_continuous_in b1
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_continuous_on c2 means :Def2: :: FCONT_1:def 2
( a2 c= dom a1 & ( for b1 being real number st b1 in a2 holds
a1 | a2 is_continuous_in b1 ) );
end;

:: deftheorem Def2 defines is_continuous_on FCONT_1:def 2 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_continuous_on b2 iff ( b2 c= dom b1 & ( for b3 being real number st b3 in b2 holds
b1 | b2 is_continuous_in b3 ) ) );

theorem Th13: :: FCONT_1:13
canceled;

theorem Th14: :: FCONT_1:14
for b1 being set
for b2 being PartFunc of REAL , REAL holds
( b2 is_continuous_on b1 iff ( b1 c= dom b2 & ( for b3 being Real_Sequence st rng b3 c= b1 & b3 is convergent & lim b3 in b1 holds
( b2 * b3 is convergent & b2 . (lim b3) = lim (b2 * b3) ) ) ) )
proof end;

theorem Th15: :: FCONT_1:15
for b1 being set
for b2 being PartFunc of REAL , REAL holds
( b2 is_continuous_on b1 iff ( b1 c= dom b2 & ( for b3, b4 being real number st b3 in b1 & 0 < b4 holds
ex b5 being real number st
( 0 < b5 & ( for b6 being real number st b6 in b1 & abs (b6 - b3) < b5 holds
abs ((b2 . b6) - (b2 . b3)) < b4 ) ) ) ) )
proof end;

theorem Th16: :: FCONT_1:16
for b1 being set
for b2 being PartFunc of REAL , REAL holds
( b2 is_continuous_on b1 iff b2 | b1 is_continuous_on b1 )
proof end;

theorem Th17: :: FCONT_1:17
for b1, b2 being set
for b3 being PartFunc of REAL , REAL st b3 is_continuous_on b1 & b2 c= b1 holds
b3 is_continuous_on b2
proof end;

theorem Th18: :: FCONT_1:18
for b1 being real number
for b2 being PartFunc of REAL , REAL st b1 in dom b2 holds
b2 is_continuous_on {b1}
proof end;

theorem Th19: :: FCONT_1:19
for b1 being set
for b2, b3 being PartFunc of REAL , REAL st b2 is_continuous_on b1 & b3 is_continuous_on b1 holds
( b2 + b3 is_continuous_on b1 & b2 - b3 is_continuous_on b1 & b2 (#) b3 is_continuous_on b1 )
proof end;

theorem Th20: :: FCONT_1:20
for b1, b2 being set
for b3, b4 being PartFunc of REAL , REAL st b3 is_continuous_on b1 & b4 is_continuous_on b2 holds
( b3 + b4 is_continuous_on b1 /\ b2 & b3 - b4 is_continuous_on b1 /\ b2 & b3 (#) b4 is_continuous_on b1 /\ b2 )
proof end;

theorem Th21: :: FCONT_1:21
for b1 being real number
for b2 being set
for b3 being PartFunc of REAL , REAL st b3 is_continuous_on b2 holds
b1 (#) b3 is_continuous_on b2
proof end;

theorem Th22: :: FCONT_1:22
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_continuous_on b1 holds
( abs b2 is_continuous_on b1 & - b2 is_continuous_on b1 )
proof end;

theorem Th23: :: FCONT_1:23
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_continuous_on b1 & b2 " {0} = {} holds
b2 ^ is_continuous_on b1
proof end;

theorem Th24: :: FCONT_1:24
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_continuous_on b1 & (b2 | b1) " {0} = {} holds
b2 ^ is_continuous_on b1
proof end;

theorem Th25: :: FCONT_1:25
for b1 being set
for b2, b3 being PartFunc of REAL , REAL st b2 is_continuous_on b1 & b2 " {0} = {} & b3 is_continuous_on b1 holds
b3 / b2 is_continuous_on b1
proof end;

theorem Th26: :: FCONT_1:26
for b1 being set
for b2, b3 being PartFunc of REAL , REAL st b2 is_continuous_on b1 & b3 is_continuous_on b2 .: b1 holds
b3 * b2 is_continuous_on b1
proof end;

theorem Th27: :: FCONT_1:27
for b1, b2 being set
for b3, b4 being PartFunc of REAL , REAL st b3 is_continuous_on b1 & b4 is_continuous_on b2 holds
b4 * b3 is_continuous_on b1 /\ (b3 " b2)
proof end;

theorem Th28: :: FCONT_1:28
for b1 being PartFunc of REAL , REAL st b1 is total & ( for b2, b3 being real number holds b1 . (b2 + b3) = (b1 . b2) + (b1 . b3) ) & ex b2 being real number st b1 is_continuous_in b2 holds
b1 is_continuous_on REAL
proof end;

theorem Th29: :: FCONT_1:29
for b1 being PartFunc of REAL , REAL st dom b1 is compact & b1 is_continuous_on dom b1 holds
rng b1 is compact
proof end;

theorem Th30: :: FCONT_1:30
for b1 being Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & b1 is compact & b2 is_continuous_on b1 holds
b2 .: b1 is compact
proof end;

theorem Th31: :: FCONT_1:31
for b1 being PartFunc of REAL , REAL st dom b1 <> {} & dom b1 is compact & b1 is_continuous_on dom b1 holds
ex b2, b3 being real number st
( b2 in dom b1 & b3 in dom b1 & b1 . b2 = upper_bound (rng b1) & b1 . b3 = lower_bound (rng b1) )
proof end;

theorem Th32: :: FCONT_1:32
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL st b2 <> {} & b2 c= dom b1 & b2 is compact & b1 is_continuous_on b2 holds
ex b3, b4 being real number st
( b3 in b2 & b4 in b2 & b1 . b3 = upper_bound (b1 .: b2) & b1 . b4 = lower_bound (b1 .: b2) )
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be set ;
pred c1 is_Lipschitzian_on c2 means :Def3: :: FCONT_1:def 3
( a2 c= dom a1 & ex b1 being real number st
( 0 < b1 & ( for b2, b3 being real number st b2 in a2 & b3 in a2 holds
abs ((a1 . b2) - (a1 . b3)) <= b1 * (abs (b2 - b3)) ) ) );
end;

:: deftheorem Def3 defines is_Lipschitzian_on FCONT_1:def 3 :
for b1 being PartFunc of REAL , REAL
for b2 being set holds
( b1 is_Lipschitzian_on b2 iff ( b2 c= dom b1 & ex b3 being real number st
( 0 < b3 & ( for b4, b5 being real number st b4 in b2 & b5 in b2 holds
abs ((b1 . b4) - (b1 . b5)) <= b3 * (abs (b4 - b5)) ) ) ) );

theorem Th33: :: FCONT_1:33
canceled;

theorem Th34: :: FCONT_1:34
for b1, b2 being set
for b3 being PartFunc of REAL , REAL st b3 is_Lipschitzian_on b1 & b2 c= b1 holds
b3 is_Lipschitzian_on b2
proof end;

theorem Th35: :: FCONT_1:35
for b1, b2 being set
for b3, b4 being PartFunc of REAL , REAL st b3 is_Lipschitzian_on b1 & b4 is_Lipschitzian_on b2 holds
b3 + b4 is_Lipschitzian_on b1 /\ b2
proof end;

theorem Th36: :: FCONT_1:36
for b1, b2 being set
for b3, b4 being PartFunc of REAL , REAL st b3 is_Lipschitzian_on b1 & b4 is_Lipschitzian_on b2 holds
b3 - b4 is_Lipschitzian_on b1 /\ b2
proof end;

theorem Th37: :: FCONT_1:37
for b1, b2, b3, b4 being set
for b5, b6 being PartFunc of REAL , REAL st b5 is_Lipschitzian_on b1 & b6 is_Lipschitzian_on b2 & b5 is_bounded_on b3 & b6 is_bounded_on b4 holds
b5 (#) b6 is_Lipschitzian_on ((b1 /\ b3) /\ b2) /\ b4
proof end;

theorem Th38: :: FCONT_1:38
for b1 being set
for b2 being real number
for b3 being PartFunc of REAL , REAL st b3 is_Lipschitzian_on b1 holds
b2 (#) b3 is_Lipschitzian_on b1
proof end;

theorem Th39: :: FCONT_1:39
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_Lipschitzian_on b1 holds
( - b2 is_Lipschitzian_on b1 & abs b2 is_Lipschitzian_on b1 )
proof end;

theorem Th40: :: FCONT_1:40
for b1 being set
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 is_constant_on b1 holds
b2 is_Lipschitzian_on b1
proof end;

theorem Th41: :: FCONT_1:41
for b1 being Subset of REAL holds id b1 is_Lipschitzian_on b1
proof end;

theorem Th42: :: FCONT_1:42
for b1 being set
for b2 being PartFunc of REAL , REAL st b2 is_Lipschitzian_on b1 holds
b2 is_continuous_on b1
proof end;

theorem Th43: :: FCONT_1:43
for b1 being PartFunc of REAL , REAL st ex b2 being real number st rng b1 = {b2} holds
b1 is_continuous_on dom b1
proof end;

theorem Th44: :: FCONT_1:44
for b1 being set
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 is_constant_on b1 holds
b2 is_continuous_on b1
proof end;

theorem Th45: :: FCONT_1:45
for b1 being PartFunc of REAL , REAL st ( for b2 being real number st b2 in dom b1 holds
b1 . b2 = b2 ) holds
b1 is_continuous_on dom b1
proof end;

theorem Th46: :: FCONT_1:46
for b1 being PartFunc of REAL , REAL st b1 = id (dom b1) holds
b1 is_continuous_on dom b1
proof end;

theorem Th47: :: FCONT_1:47
for b1 being Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 | b1 = id b1 holds
b2 is_continuous_on b1
proof end;

theorem Th48: :: FCONT_1:48
for b1 being set
for b2, b3 being real number
for b4 being PartFunc of REAL , REAL st b1 c= dom b4 & ( for b5 being real number st b5 in b1 holds
b4 . b5 = (b2 * b5) + b3 ) holds
b4 is_continuous_on b1
proof end;

theorem Th49: :: FCONT_1:49
for b1 being PartFunc of REAL , REAL st ( for b2 being real number st b2 in dom b1 holds
b1 . b2 = b2 ^2 ) holds
b1 is_continuous_on dom b1
proof end;

theorem Th50: :: FCONT_1:50
for b1 being set
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & ( for b3 being real number st b3 in b1 holds
b2 . b3 = b3 ^2 ) holds
b2 is_continuous_on b1
proof end;

theorem Th51: :: FCONT_1:51
for b1 being PartFunc of REAL , REAL st ( for b2 being real number st b2 in dom b1 holds
b1 . b2 = abs b2 ) holds
b1 is_continuous_on dom b1
proof end;

theorem Th52: :: FCONT_1:52
for b1 being set
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & ( for b3 being real number st b3 in b1 holds
b2 . b3 = abs b3 ) holds
b2 is_continuous_on b1
proof end;

theorem Th53: :: FCONT_1:53
for b1 being set
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & b2 is_monotone_on b1 & ex b3, b4 being real number st
( b3 <= b4 & b2 .: b1 = [.b3,b4.] ) holds
b2 is_continuous_on b1
proof end;

theorem Th54: :: FCONT_1:54
for b1, b2 being real number
for b3 being one-to-one PartFunc of REAL , REAL st b1 <= b2 & [.b1,b2.] c= dom b3 & ( b3 is_increasing_on [.b1,b2.] or b3 is_decreasing_on [.b1,b2.] ) holds
(b3 | [.b1,b2.]) " is_continuous_on b3 .: [.b1,b2.]
proof end;