:: by Takaya Nishiyama, Keiji Ohkubo and Yasunari Shidama

::

:: Received April 6, 2004

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

theorem :: NFCONT_1:1

for S being non empty addLoopStr

for seq1, seq2 being sequence of S holds seq1 - seq2 = seq1 + (- seq2)

for seq1, seq2 being sequence of S holds seq1 - seq2 = seq1 + (- seq2)

proof end;

definition

let S be RealNormSpace;

let x0 be Point of S;

ex b_{1} being Subset of S ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b_{1} )

end;
let x0 be Point of S;

mode Neighbourhood of x0 -> Subset of S means :Def1: :: NFCONT_1:def 1

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= it );

existence ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= it );

ex b

( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b

proof end;

:: deftheorem Def1 defines Neighbourhood NFCONT_1:def 1 :

for S being RealNormSpace

for x0 being Point of S

for b_{3} being Subset of S holds

( b_{3} is Neighbourhood of x0 iff ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b_{3} ) );

for S being RealNormSpace

for x0 being Point of S

for b

( b

( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b

theorem Th3: :: NFCONT_1:3

for S being RealNormSpace

for x0 being Point of S

for g being Real st 0 < g holds

{ y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0

for x0 being Point of S

for g being Real st 0 < g holds

{ y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0

proof end;

definition

let S be RealNormSpace;

let X be Subset of S;

end;
let X be Subset of S;

attr X is compact means :: NFCONT_1:def 2

for s1 being sequence of S st rng s1 c= X holds

ex s2 being sequence of S st

( s2 is subsequence of s1 & s2 is convergent & lim s2 in X );

for s1 being sequence of S st rng s1 c= X holds

ex s2 being sequence of S st

( s2 is subsequence of s1 & s2 is convergent & lim s2 in X );

:: deftheorem defines compact NFCONT_1:def 2 :

for S being RealNormSpace

for X being Subset of S holds

( X is compact iff for s1 being sequence of S st rng s1 c= X holds

ex s2 being sequence of S st

( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );

for S being RealNormSpace

for X being Subset of S holds

( X is compact iff for s1 being sequence of S st rng s1 c= X holds

ex s2 being sequence of S st

( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );

definition

let S be RealNormSpace;

let X be Subset of S;

end;
let X be Subset of S;

attr X is closed means :: NFCONT_1:def 3

for s1 being sequence of S st rng s1 c= X & s1 is convergent holds

lim s1 in X;

for s1 being sequence of S st rng s1 c= X & s1 is convergent holds

lim s1 in X;

:: deftheorem defines closed NFCONT_1:def 3 :

for S being RealNormSpace

for X being Subset of S holds

( X is closed iff for s1 being sequence of S st rng s1 c= X & s1 is convergent holds

lim s1 in X );

for S being RealNormSpace

for X being Subset of S holds

( X is closed iff for s1 being sequence of S st rng s1 c= X & s1 is convergent holds

lim s1 in X );

definition
end;

:: deftheorem defines open NFCONT_1:def 4 :

for S being RealNormSpace

for X being Subset of S holds

( X is open iff X ` is closed );

for S being RealNormSpace

for X being Subset of S holds

( X is open iff X ` is closed );

definition

let S, T be RealNormSpace;

let f be PartFunc of S,T;

let x0 be Point of S;

end;
let f be PartFunc of S,T;

let x0 be Point of S;

pred f is_continuous_in x0 means :: NFCONT_1:def 5

( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

:: deftheorem defines is_continuous_in NFCONT_1:def 5 :

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

definition

let S be RealNormSpace;

let f be PartFunc of the carrier of S,REAL;

let x0 be Point of S;

end;
let f be PartFunc of the carrier of S,REAL;

let x0 be Point of S;

pred f is_continuous_in x0 means :: NFCONT_1:def 6

( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

:: deftheorem defines is_continuous_in NFCONT_1:def 6 :

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

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

theorem Th5: :: NFCONT_1:5

for n being Nat

for S, T being RealNormSpace

for seq being sequence of S

for h being PartFunc of S,T st rng seq c= dom h holds

seq . n in dom h

for S, T being RealNormSpace

for seq being sequence of S

for h being PartFunc of S,T st rng seq c= dom h holds

seq . n in dom h

proof end;

theorem Th6: :: NFCONT_1:6

for S being RealNormSpace

for seq being sequence of S

for x being set holds

( x in rng seq iff ex n being Nat st x = seq . n )

for seq being sequence of S

for x being set holds

( x in rng seq iff ex n being Nat st x = seq . n )

proof end;

theorem Th7: :: NFCONT_1:7

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )

for f being PartFunc of S,T

for x0 being Point of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )

proof end;

theorem Th8: :: NFCONT_1:8

for S being RealNormSpace

for x0 being Point of S

for f being PartFunc of the carrier of S,REAL holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds

|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

for x0 being Point of S

for f being PartFunc of the carrier of S,REAL holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds

|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

proof end;

theorem Th9: :: NFCONT_1:9

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S 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 Point of S st x1 in dom f & x1 in N holds

f /. x1 in N1 ) ) )

for f being PartFunc of S,T

for x0 being Point of S 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 Point of S st x1 in dom f & x1 in N holds

f /. x1 in N1 ) ) )

proof end;

theorem Th10: :: NFCONT_1:10

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S 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 ) ) )

for f being PartFunc of S,T

for x0 being Point of S 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 :: NFCONT_1:11

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

for f being PartFunc of S,T

for x0 being Point of S 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 Th12: :: NFCONT_1:12

for S, T being RealNormSpace

for h1, h2 being PartFunc of S,T

for seq being sequence of S st rng seq c= (dom h1) /\ (dom h2) holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

for h1, h2 being PartFunc of S,T

for seq being sequence of S st rng seq c= (dom h1) /\ (dom h2) holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

proof end;

theorem Th13: :: NFCONT_1:13

for S, T being RealNormSpace

for h being PartFunc of S,T

for seq being sequence of S

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

for h being PartFunc of S,T

for seq being sequence of S

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

proof end;

reconsider jj = 1 as Real ;

theorem Th14: :: NFCONT_1:14

for S, T being RealNormSpace

for h being PartFunc of S,T

for seq being sequence of S st rng seq c= dom h holds

( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )

for h being PartFunc of S,T

for seq being sequence of S st rng seq c= dom h holds

( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )

proof end;

theorem :: NFCONT_1:15

for S, T being RealNormSpace

for f1, f2 being PartFunc of S,T

for x0 being Point of S st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds

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

for f1, f2 being PartFunc of S,T

for x0 being Point of S st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds

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

proof end;

theorem Th16: :: NFCONT_1:16

for r being Real

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

proof end;

theorem :: NFCONT_1:17

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st f is_continuous_in x0 holds

( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )

for f being PartFunc of S,T

for x0 being Point of S st f is_continuous_in x0 holds

( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )

proof end;

definition

let S, T be RealNormSpace;

let f be PartFunc of S,T;

let X be set ;

end;
let f be PartFunc of S,T;

let X be set ;

pred f is_continuous_on X means :: NFCONT_1:def 7

( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) );

( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NFCONT_1:def 7 :

for S, T being RealNormSpace

for f being PartFunc of S,T

for X being set holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) ) );

for S, T being RealNormSpace

for f being PartFunc of S,T

for X being set holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) ) );

definition

let S be RealNormSpace;

let f be PartFunc of the carrier of S,REAL;

let X be set ;

end;
let f be PartFunc of the carrier of S,REAL;

let X be set ;

pred f is_continuous_on X means :: NFCONT_1:def 8

( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) );

( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NFCONT_1:def 8 :

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL

for X being set holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) ) );

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL

for X being set holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds

f | X is_continuous_in x0 ) ) );

theorem Th18: :: NFCONT_1:18

for S, T being RealNormSpace

for X being set

for f being PartFunc of S,T holds

( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S st rng s1 c= X & s1 is convergent & lim s1 in X holds

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

for X being set

for f being PartFunc of S,T holds

( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S 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 Th19: :: NFCONT_1:19

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )

for S, T being RealNormSpace

for f being PartFunc of S,T holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )

proof end;

theorem :: NFCONT_1:20

for X being set

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds

|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL holds

( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S

for r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds

|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )

proof end;

theorem :: NFCONT_1:21

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T holds

( f is_continuous_on X iff f | X is_continuous_on X )

for S, T being RealNormSpace

for f being PartFunc of S,T holds

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem Th22: :: NFCONT_1:22

for X being set

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL holds

( f is_continuous_on X iff f | X is_continuous_on X )

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL holds

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem Th23: :: NFCONT_1:23

for X, X1 being set

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

proof end;

theorem :: NFCONT_1:24

for S, T being RealNormSpace

for f being PartFunc of S,T

for x0 being Point of S st x0 in dom f holds

f is_continuous_on {x0}

for f being PartFunc of S,T

for x0 being Point of S st x0 in dom f holds

f is_continuous_on {x0}

proof end;

theorem Th25: :: NFCONT_1:25

for S, T being RealNormSpace

for X being set

for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X holds

( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X )

for X being set

for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X holds

( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X )

proof end;

theorem :: NFCONT_1:26

for S, T being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of S,T 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 )

for X, X1 being set

for f1, f2 being PartFunc of S,T 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 )

proof end;

theorem Th27: :: NFCONT_1:27

for S, T being RealNormSpace

for r being Real

for X being set

for f being PartFunc of S,T st f is_continuous_on X holds

r (#) f is_continuous_on X

for r being Real

for X being set

for f being PartFunc of S,T st f is_continuous_on X holds

r (#) f is_continuous_on X

proof end;

theorem Th28: :: NFCONT_1:28

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_continuous_on X holds

( ||.f.|| is_continuous_on X & - f is_continuous_on X )

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_continuous_on X holds

( ||.f.|| is_continuous_on X & - f is_continuous_on X )

proof end;

theorem :: NFCONT_1:29

for S, T being RealNormSpace

for f being PartFunc of S,T st f is total & ( for x1, x2 being Point of S holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of S st f is_continuous_in x0 holds

f is_continuous_on the carrier of S

for f being PartFunc of S,T st f is total & ( for x1, x2 being Point of S holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of S st f is_continuous_in x0 holds

f is_continuous_on the carrier of S

proof end;

theorem Th30: :: NFCONT_1:30

for S, T being RealNormSpace

for f being PartFunc of S,T st dom f is compact & f is_continuous_on dom f holds

rng f is compact

for f being PartFunc of S,T st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem Th31: :: NFCONT_1:31

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL st dom f is compact & f is_continuous_on dom f holds

rng f is compact

for f being PartFunc of the carrier of S,REAL st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem :: NFCONT_1:32

for S, T being RealNormSpace

for f being PartFunc of S,T

for Y being Subset of S st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

for f being PartFunc of S,T

for Y being Subset of S st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

proof end;

theorem Th33: :: NFCONT_1:33

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f holds

ex x1, x2 being Point of S st

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

for f being PartFunc of the carrier of S,REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f holds

ex x1, x2 being Point of S st

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

proof end;

theorem Th34: :: NFCONT_1:34

for S, T being RealNormSpace

for f being PartFunc of S,T st dom f <> {} & dom f is compact & f is_continuous_on dom f holds

ex x1, x2 being Point of S st

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

for f being PartFunc of S,T st dom f <> {} & dom f is compact & f is_continuous_on dom f holds

ex x1, x2 being Point of S st

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

proof end;

theorem Th35: :: NFCONT_1:35

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).||

for S, T being RealNormSpace

for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).||

proof end;

theorem :: NFCONT_1:36

for S, T being RealNormSpace

for f being PartFunc of S,T

for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds

ex x1, x2 being Point of S st

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

for f being PartFunc of S,T

for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds

ex x1, x2 being Point of S st

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

proof end;

theorem :: NFCONT_1:37

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL

for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds

ex x1, x2 being Point of S st

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

for f being PartFunc of the carrier of S,REAL

for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds

ex x1, x2 being Point of S st

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

proof end;

:: deftheorem defines is_Lipschitzian_on NFCONT_1:def 9 :

for S, T being RealNormSpace

for X being set

for f being PartFunc of S,T holds

( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st

( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds

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

for S, T being RealNormSpace

for X being set

for f being PartFunc of S,T holds

( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st

( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds

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

:: deftheorem defines is_Lipschitzian_on NFCONT_1:def 10 :

for S being RealNormSpace

for X being set

for f being PartFunc of the carrier of S,REAL holds

( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st

( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds

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

for S being RealNormSpace

for X being set

for f being PartFunc of the carrier of S,REAL holds

( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st

( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds

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

theorem Th38: :: NFCONT_1:38

for X, X1 being set

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

proof end;

theorem :: NFCONT_1:39

for X, X1 being set

for S, T being RealNormSpace

for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

for S, T being RealNormSpace

for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: NFCONT_1:40

for X, X1 being set

for S, T being RealNormSpace

for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

for S, T being RealNormSpace

for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

proof end;

theorem Th41: :: NFCONT_1:41

for X being set

for p being Real

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X holds

p (#) f is_Lipschitzian_on X

for p being Real

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X holds

p (#) f is_Lipschitzian_on X

proof end;

theorem :: NFCONT_1:42

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X holds

( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X )

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X holds

( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X )

proof end;

theorem Th43: :: NFCONT_1:43

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T st X c= dom f & f | X is V26() holds

f is_Lipschitzian_on X

for S, T being RealNormSpace

for f being PartFunc of S,T st X c= dom f & f | X is V26() holds

f is_Lipschitzian_on X

proof end;

theorem Th45: :: NFCONT_1:45

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X holds

f is_continuous_on X

for S, T being RealNormSpace

for f being PartFunc of S,T st f is_Lipschitzian_on X holds

f is_continuous_on X

proof end;

theorem Th46: :: NFCONT_1:46

for X being set

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds

f is_continuous_on X

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds

f is_continuous_on X

proof end;

theorem :: NFCONT_1:47

for S, T being RealNormSpace

for f being PartFunc of S,T st ex r being Point of T st rng f = {r} holds

f is_continuous_on dom f

for f being PartFunc of S,T st ex r being Point of T st rng f = {r} holds

f is_continuous_on dom f

proof end;

theorem :: NFCONT_1:48

for X being set

for S, T being RealNormSpace

for f being PartFunc of S,T st X c= dom f & f | X is V26() holds

f is_continuous_on X by Th43, Th45;

for S, T being RealNormSpace

for f being PartFunc of S,T st X c= dom f & f | X is V26() holds

f is_continuous_on X by Th43, Th45;

theorem Th49: :: NFCONT_1:49

for S being RealNormSpace

for f being PartFunc of S,S st ( for x0 being Point of S st x0 in dom f holds

f /. x0 = x0 ) holds

f is_continuous_on dom f

for f being PartFunc of S,S st ( for x0 being Point of S st x0 in dom f holds

f /. x0 = x0 ) holds

f is_continuous_on dom f

proof end;

theorem :: NFCONT_1:50

for S being RealNormSpace

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

f is_continuous_on dom f

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

f is_continuous_on dom f

proof end;

theorem :: NFCONT_1:51

for S being RealNormSpace

for Y being Subset of S

for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds

f is_continuous_on Y

for Y being Subset of S

for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds

f is_continuous_on Y

proof end;

theorem :: NFCONT_1:52

for X being set

for S being RealNormSpace

for f being PartFunc of S,S

for r being Real

for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds

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

f is_continuous_on X

for S being RealNormSpace

for f being PartFunc of S,S

for r being Real

for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds

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

f is_continuous_on X

proof end;

theorem Th53: :: NFCONT_1:53

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL st ( for x0 being Point of S st x0 in dom f holds

f /. x0 = ||.x0.|| ) holds

f is_continuous_on dom f

for f being PartFunc of the carrier of S,REAL st ( for x0 being Point of S st x0 in dom f holds

f /. x0 = ||.x0.|| ) holds

f is_continuous_on dom f

proof end;

theorem :: NFCONT_1:54

for X being set

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL st X c= dom f & ( for x0 being Point of S st x0 in X holds

f /. x0 = ||.x0.|| ) holds

f is_continuous_on X

for S being RealNormSpace

for f being PartFunc of the carrier of S,REAL st X c= dom f & ( for x0 being Point of S st x0 in X holds

f /. x0 = ||.x0.|| ) holds

f is_continuous_on X

proof end;