:: NFCONT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let S, T be 1-sorted ;
mode PartFunc of S,T is PartFunc of the carrier of S,the carrier of T;
end;

definition
let RNS be RealLinearSpace;
let S1 be sequence of RNS;
func - S1 -> sequence of RNS means :Def1: :: NFCONT_1:def 1
for n being Nat holds it . n = - (S1 . n);
existence
ex b1 being sequence of RNS st
for n being Nat holds b1 . n = - (S1 . n)
proof end;
uniqueness
for b1, b2 being sequence of RNS st ( for n being Nat holds b1 . n = - (S1 . n) ) & ( for n being Nat holds b2 . n = - (S1 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines - NFCONT_1:def 1 :
for RNS being RealLinearSpace
for S1, b3 being sequence of RNS holds
( b3 = - S1 iff for n being Nat holds b3 . n = - (S1 . n) );

theorem :: NFCONT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for seq1, seq2 being sequence of S holds seq1 - seq2 = seq1 + (- seq2)
proof end;

theorem Th2: :: NFCONT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for seq being sequence of S holds - seq = (- 1) * seq
proof end;

definition
let S, T be RealNormSpace;
let f be PartFunc of S,T;
func ||.f.|| -> PartFunc of the carrier of S, REAL means :Def2: :: NFCONT_1:def 2
( dom it = dom f & ( for c being Point of S st c in dom it holds
it . c = ||.(f /. c).|| ) );
existence
ex b1 being PartFunc of the carrier of S, REAL st
( dom b1 = dom f & ( for c being Point of S st c in dom b1 holds
b1 . c = ||.(f /. c).|| ) )
proof end;
uniqueness
for b1, b2 being PartFunc of the carrier of S, REAL st dom b1 = dom f & ( for c being Point of S st c in dom b1 holds
b1 . c = ||.(f /. c).|| ) & dom b2 = dom f & ( for c being Point of S st c in dom b2 holds
b2 . c = ||.(f /. c).|| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ||. NFCONT_1:def 2 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for b4 being PartFunc of the carrier of S, REAL holds
( b4 = ||.f.|| iff ( dom b4 = dom f & ( for c being Point of S st c in dom b4 holds
b4 . c = ||.(f /. c).|| ) ) );

definition
let S be RealNormSpace;
let x0 be Point of S;
mode Neighbourhood of x0 -> Subset of S means :Def3: :: NFCONT_1:def 3
ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= it );
existence
ex b1 being Subset of S ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b1 )
proof end;
end;

:: deftheorem Def3 defines Neighbourhood NFCONT_1:def 3 :
for S being RealNormSpace
for x0 being Point of S
for b3 being Subset of S holds
( b3 is Neighbourhood of x0 iff ex g being Real st
( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b3 ) );

theorem Th3: :: NFCONT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th4: :: NFCONT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for x0 being Point of S
for N being Neighbourhood of x0 holds x0 in N
proof end;

definition
let S be RealNormSpace;
let X be Subset of S;
attr X is compact means :Def4: :: NFCONT_1:def 4
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 );
end;

:: deftheorem Def4 defines compact NFCONT_1:def 4 :
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;
attr X is closed means :: NFCONT_1:def 5
for s1 being sequence of S st rng s1 c= X & s1 is convergent holds
lim s1 in X;
end;

:: deftheorem defines closed NFCONT_1:def 5 :
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
let S be RealNormSpace;
let X be Subset of S;
attr X is open means :: NFCONT_1:def 6
X ` is closed;
end;

:: deftheorem defines open NFCONT_1:def 6 :
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 seq be sequence of S;
assume A1: rng seq c= dom f ;
func f * seq -> sequence of T equals :Def7: :: NFCONT_1:def 7
f * seq;
coherence
f * seq is sequence of T
proof end;
end;

:: deftheorem Def7 defines * NFCONT_1:def 7 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for seq being sequence of S st rng seq c= dom f holds
f * seq = f * seq;

definition
let S be RealNormSpace;
let f be PartFunc of the carrier of S, REAL ;
let seq be sequence of S;
assume A1: rng seq c= dom f ;
func f * seq -> Real_Sequence equals :Def8: :: NFCONT_1:def 8
f * seq;
coherence
f * seq is Real_Sequence
proof end;
end;

:: deftheorem Def8 defines * NFCONT_1:def 8 :
for S being RealNormSpace
for f being PartFunc of the carrier of S, REAL
for seq being sequence of S st rng seq c= dom f holds
f * seq = f * seq;

definition
let S, T be RealNormSpace;
let f be PartFunc of S,T;
let x0 be Point of S;
pred f is_continuous_in x0 means :Def9: :: NFCONT_1:def 9
( 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) ) ) );
end;

:: deftheorem Def9 defines is_continuous_in NFCONT_1:def 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 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;
pred f is_continuous_in x0 means :Def10: :: NFCONT_1:def 10
( 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) ) ) );
end;

:: deftheorem Def10 defines is_continuous_in NFCONT_1:def 10 :
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th6: :: NFCONT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th7: :: NFCONT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for seq, seq1 being sequence of S st seq1 is subsequence of seq holds
rng seq1 c= rng seq
proof end;

theorem Th8: :: NFCONT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S being RealNormSpace
for f being PartFunc of S,T
for s1 being sequence of S st rng s1 c= dom f holds
for n being Nat holds (f * s1) . n = f /. (s1 . n)
proof end;

theorem Th9: :: NFCONT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for f being PartFunc of the carrier of S, REAL
for s1 being sequence of S st rng s1 c= dom f holds
for n being Nat holds (f * s1) . n = f /. (s1 . n)
proof end;

theorem Th10: :: NFCONT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being RealNormSpace
for h being PartFunc of S,T
for seq being sequence of S
for Ns being increasing Seq_of_Nat st rng seq c= dom h holds
(h * seq) * Ns = h * (seq * Ns)
proof end;

theorem Th11: :: NFCONT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for h being PartFunc of the carrier of S, REAL
for seq being sequence of S
for Ns being increasing Seq_of_Nat st rng seq c= dom h holds
(h * seq) * Ns = h * (seq * Ns)
proof end;

theorem Th12: :: NFCONT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being RealNormSpace
for h being PartFunc of S,T
for seq1, seq2 being sequence of S st rng seq1 c= dom h & seq2 is subsequence of seq1 holds
h * seq2 is subsequence of h * seq1
proof end;

theorem Th13: :: NFCONT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for h being PartFunc of the carrier of S, REAL
for seq1, seq2 being sequence of S st rng seq1 c= dom h & seq2 is subsequence of seq1 holds
h * seq2 is subsequence of h * seq1
proof end;

theorem Th14: :: NFCONT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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 ) ) ) ) )
proof end;

theorem Th15: :: NFCONT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
abs ((f /. x1) - (f /. x0)) < r ) ) ) ) )
proof end;

theorem Th16: :: NFCONT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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 ) ) )
proof end;

theorem Th17: :: NFCONT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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 ) ) )
proof end;

theorem :: NFCONT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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
proof end;

theorem Th19: :: NFCONT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th20: :: NFCONT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th21: :: NFCONT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: NFCONT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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 )
proof end;

theorem Th23: :: NFCONT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real
for T, S 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:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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 )
proof end;

definition
let S, T be RealNormSpace;
let f be PartFunc of S,T;
let X be set ;
pred f is_continuous_on X means :Def11: :: NFCONT_1:def 11
( X c= dom f & ( for x0 being Point of S st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def11 defines is_continuous_on NFCONT_1:def 11 :
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 ;
pred f is_continuous_on X means :Def12: :: NFCONT_1:def 12
( X c= dom f & ( for x0 being Point of S st x0 in X holds
f | X is_continuous_in x0 ) );
end;

:: deftheorem Def12 defines is_continuous_on NFCONT_1:def 12 :
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 Th25: :: NFCONT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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) ) ) ) )
proof end;

theorem Th26: :: NFCONT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for T, S 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:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
abs ((f /. x1) - (f /. x0)) < r ) ) ) ) )
proof end;

theorem :: NFCONT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th29: :: NFCONT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th30: :: NFCONT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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}
proof end;

theorem Th32: :: NFCONT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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 )
proof end;

theorem :: NFCONT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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 )
proof end;

theorem Th34: :: NFCONT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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
proof end;

theorem Th35: :: NFCONT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: NFCONT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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
proof end;

theorem Th37: :: NFCONT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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
proof end;

theorem Th38: :: NFCONT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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
proof end;

theorem Th40: :: NFCONT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th41: :: NFCONT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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.||) )
proof end;

theorem Th42: :: NFCONT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).||
proof end;

theorem :: NFCONT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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) )
proof end;

theorem :: NFCONT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

definition
let S, T be RealNormSpace;
let X be set ;
let f be PartFunc of S,T;
pred f is_Lipschitzian_on X means :Def13: :: NFCONT_1:def 13
( 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).|| ) ) );
end;

:: deftheorem Def13 defines is_Lipschitzian_on NFCONT_1:def 13 :
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).|| ) ) ) );

definition
let S be RealNormSpace;
let X be set ;
let f be PartFunc of the carrier of S, REAL ;
pred f is_Lipschitzian_on X means :Def14: :: NFCONT_1:def 14
( 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
abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) );
end;

:: deftheorem Def14 defines is_Lipschitzian_on NFCONT_1:def 14 :
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
abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) ) );

theorem Th45: :: NFCONT_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th48: :: NFCONT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th50: :: NFCONT_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st X c= dom f & f is_constant_on X holds
f is_Lipschitzian_on X
proof end;

theorem :: NFCONT_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for Y being Subset of S holds id Y is_Lipschitzian_on Y
proof end;

theorem Th52: :: NFCONT_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th53: :: NFCONT_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, S 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
proof end;

theorem :: NFCONT_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T st X c= dom f & f is_constant_on X holds
f is_continuous_on X
proof end;

theorem Th56: :: NFCONT_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being RealNormSpace
for f being PartFunc of S,S st f = id (dom f) holds
f is_continuous_on dom f
proof end;

theorem :: NFCONT_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th60: :: NFCONT_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: NFCONT_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;