:: by Noboru Endou

::

:: Received August 20, 2004

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

definition

let CNS be ComplexNormSpace;

let x0 be Point of CNS;

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

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

end;
let x0 be Point of CNS;

mode Neighbourhood of x0 -> Subset of CNS means :Def1: :: NCFCONT1:def 1

ex g being Real st

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

existence ex g being Real st

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

ex b

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

proof end;

:: deftheorem Def1 defines Neighbourhood NCFCONT1:def 1 :

for CNS being ComplexNormSpace

for x0 being Point of CNS

for b_{3} being Subset of CNS holds

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

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

for CNS being ComplexNormSpace

for x0 being Point of CNS

for b

( b

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

theorem Th2: :: NCFCONT1:2

for CNS being ComplexNormSpace

for x0 being Point of CNS

for g being Real st 0 < g holds

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

for x0 being Point of CNS

for g being Real st 0 < g holds

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

proof end;

theorem Th3: :: NCFCONT1:3

for CNS being ComplexNormSpace

for x0 being Point of CNS

for N being Neighbourhood of x0 holds x0 in N

for x0 being Point of CNS

for N being Neighbourhood of x0 holds x0 in N

proof end;

definition

let CNS be ComplexNormSpace;

let X be Subset of CNS;

end;
let X be Subset of CNS;

attr X is compact means :: NCFCONT1:def 2

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

ex s2 being sequence of CNS st

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

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

ex s2 being sequence of CNS st

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

:: deftheorem defines compact NCFCONT1:def 2 :

for CNS being ComplexNormSpace

for X being Subset of CNS holds

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

ex s2 being sequence of CNS st

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

for CNS being ComplexNormSpace

for X being Subset of CNS holds

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

ex s2 being sequence of CNS st

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

definition

let CNS be ComplexNormSpace;

let X be Subset of CNS;

end;
let X be Subset of CNS;

attr X is closed means :: NCFCONT1:def 3

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

lim s1 in X;

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

lim s1 in X;

:: deftheorem defines closed NCFCONT1:def 3 :

for CNS being ComplexNormSpace

for X being Subset of CNS holds

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

lim s1 in X );

for CNS being ComplexNormSpace

for X being Subset of CNS holds

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

lim s1 in X );

:: deftheorem defines open NCFCONT1:def 4 :

for CNS being ComplexNormSpace

for X being Subset of CNS holds

( X is open iff X ` is closed );

for CNS being ComplexNormSpace

for X being Subset of CNS holds

( X is open iff X ` is closed );

definition

let CNS1, CNS2 be ComplexNormSpace;

let f be PartFunc of CNS1,CNS2;

let x0 be Point of CNS1;

end;
let f be PartFunc of CNS1,CNS2;

let x0 be Point of CNS1;

pred f is_continuous_in x0 means :: NCFCONT1:def 5

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

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

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

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

:: deftheorem defines is_continuous_in NCFCONT1:def 5 :

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 holds

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

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

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 holds

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

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

definition

let CNS be ComplexNormSpace;

let RNS be RealNormSpace;

let f be PartFunc of CNS,RNS;

let x0 be Point of CNS;

end;
let RNS be RealNormSpace;

let f be PartFunc of CNS,RNS;

let x0 be Point of CNS;

pred f is_continuous_in x0 means :: NCFCONT1:def 6

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

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

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

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

:: deftheorem defines is_continuous_in NCFCONT1:def 6 :

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS holds

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

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

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS holds

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

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

definition

let RNS be RealNormSpace;

let CNS be ComplexNormSpace;

let f be PartFunc of RNS,CNS;

let x0 be Point of RNS;

end;
let CNS be ComplexNormSpace;

let f be PartFunc of RNS,CNS;

let x0 be Point of RNS;

pred f is_continuous_in x0 means :: NCFCONT1:def 7

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

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

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

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

:: deftheorem defines is_continuous_in NCFCONT1:def 7 :

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS holds

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

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

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS holds

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

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

definition

let CNS be ComplexNormSpace;

let f be PartFunc of the carrier of CNS,COMPLEX;

let x0 be Point of CNS;

end;
let f be PartFunc of the carrier of CNS,COMPLEX;

let x0 be Point of CNS;

pred f is_continuous_in x0 means :: NCFCONT1:def 8

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

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

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

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

:: deftheorem defines is_continuous_in NCFCONT1:def 8 :

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX

for x0 being Point of CNS holds

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

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

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX

for x0 being Point of CNS holds

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

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

definition

let CNS be ComplexNormSpace;

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

let x0 be Point of CNS;

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

let x0 be Point of CNS;

pred f is_continuous_in x0 means :: NCFCONT1:def 9

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

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

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

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

:: deftheorem defines is_continuous_in NCFCONT1:def 9 :

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL

for x0 being Point of CNS holds

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

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

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL

for x0 being Point of CNS holds

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

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

definition

let RNS be RealNormSpace;

let f be PartFunc of the carrier of RNS,COMPLEX;

let x0 be Point of RNS;

end;
let f be PartFunc of the carrier of RNS,COMPLEX;

let x0 be Point of RNS;

pred f is_continuous_in x0 means :: NCFCONT1:def 10

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

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

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

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

:: deftheorem defines is_continuous_in NCFCONT1:def 10 :

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX

for x0 being Point of RNS holds

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

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

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX

for x0 being Point of RNS holds

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

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

theorem Th4: :: NCFCONT1:4

for CNS1, CNS2 being ComplexNormSpace

for n being Nat

for seq being sequence of CNS1

for h being PartFunc of CNS1,CNS2 st rng seq c= dom h holds

seq . n in dom h

for n being Nat

for seq being sequence of CNS1

for h being PartFunc of CNS1,CNS2 st rng seq c= dom h holds

seq . n in dom h

proof end;

theorem Th5: :: NCFCONT1:5

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for n being Nat

for seq being sequence of CNS

for h being PartFunc of CNS,RNS st rng seq c= dom h holds

seq . n in dom h

for RNS being RealNormSpace

for n being Nat

for seq being sequence of CNS

for h being PartFunc of CNS,RNS st rng seq c= dom h holds

seq . n in dom h

proof end;

theorem Th6: :: NCFCONT1:6

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for n being Nat

for seq being sequence of RNS

for h being PartFunc of RNS,CNS st rng seq c= dom h holds

seq . n in dom h

for RNS being RealNormSpace

for n being Nat

for seq being sequence of RNS

for h being PartFunc of RNS,CNS st rng seq c= dom h holds

seq . n in dom h

proof end;

theorem Th7: :: NCFCONT1:7

for CNS being ComplexNormSpace

for seq being sequence of CNS

for x being set holds

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

for seq being sequence of CNS

for x being set holds

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

proof end;

theorem Th8: :: NCFCONT1:8

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 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 CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds

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

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 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 CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds

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

proof end;

theorem Th9: :: NCFCONT1:9

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS 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 CNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS 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 CNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

proof end;

theorem Th10: :: NCFCONT1:10

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS 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 RNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS 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 RNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

proof end;

theorem Th11: :: NCFCONT1:11

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL

for x0 being Point of CNS 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 CNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

for f being PartFunc of the carrier of CNS,REAL

for x0 being Point of CNS 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 CNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

proof end;

theorem Th12: :: NCFCONT1:12

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX

for x0 being Point of CNS 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 CNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

for f being PartFunc of the carrier of CNS,COMPLEX

for x0 being Point of CNS 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 CNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

proof end;

theorem Th13: :: NCFCONT1:13

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX

for x0 being Point of RNS 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 RNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

for f being PartFunc of the carrier of RNS,COMPLEX

for x0 being Point of RNS 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 RNS st x1 in dom f & ||.(x1 - x0).|| < s holds

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

proof end;

theorem Th14: :: NCFCONT1:14

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

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

f /. x1 in N1 ) ) )

for f being PartFunc of CNS1,CNS2

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

f /. x1 in N1 ) ) )

proof end;

theorem Th15: :: NCFCONT1:15

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

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

f /. x1 in N1 ) ) )

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

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

f /. x1 in N1 ) ) )

proof end;

theorem Th16: :: NCFCONT1:16

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

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

f /. x1 in N1 ) ) )

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

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

f /. x1 in N1 ) ) )

proof end;

theorem Th17: :: NCFCONT1:17

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 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 CNS1,CNS2

for x0 being Point of CNS1 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 Th18: :: NCFCONT1:18

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS 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 RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS 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 Th19: :: NCFCONT1:19

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS 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 RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS 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 :: NCFCONT1:20

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 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 CNS1,CNS2

for x0 being Point of CNS1 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 :: NCFCONT1:21

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

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

f is_continuous_in x0

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS 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 :: NCFCONT1:22

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

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

f is_continuous_in x0

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS 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 Th23: :: NCFCONT1:23

for CNS1, CNS2 being ComplexNormSpace

for h1, h2 being PartFunc of CNS1,CNS2

for seq being sequence of CNS1 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 CNS1,CNS2

for seq being sequence of CNS1 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 Th24: :: NCFCONT1:24

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for h1, h2 being PartFunc of CNS,RNS

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

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

for RNS being RealNormSpace

for h1, h2 being PartFunc of CNS,RNS

for seq being sequence of CNS 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 Th25: :: NCFCONT1:25

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for h1, h2 being PartFunc of RNS,CNS

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

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

for RNS being RealNormSpace

for h1, h2 being PartFunc of RNS,CNS

for seq being sequence of RNS 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 Th26: :: NCFCONT1:26

for CNS1, CNS2 being ComplexNormSpace

for h being PartFunc of CNS1,CNS2

for seq being sequence of CNS1

for z being Complex st rng seq c= dom h holds

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

for h being PartFunc of CNS1,CNS2

for seq being sequence of CNS1

for z being Complex st rng seq c= dom h holds

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

proof end;

theorem Th27: :: NCFCONT1:27

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for h being PartFunc of CNS,RNS

for seq being sequence of CNS

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

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

for RNS being RealNormSpace

for h being PartFunc of CNS,RNS

for seq being sequence of CNS

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

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

proof end;

theorem Th28: :: NCFCONT1:28

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for h being PartFunc of RNS,CNS

for seq being sequence of RNS

for z being Complex st rng seq c= dom h holds

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

for RNS being RealNormSpace

for h being PartFunc of RNS,CNS

for seq being sequence of RNS

for z being Complex st rng seq c= dom h holds

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

proof end;

theorem Th29: :: NCFCONT1:29

for CNS1, CNS2 being ComplexNormSpace

for h being PartFunc of CNS1,CNS2

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

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

for h being PartFunc of CNS1,CNS2

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

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

proof end;

theorem Th30: :: NCFCONT1:30

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for h being PartFunc of CNS,RNS

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

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

for RNS being RealNormSpace

for h being PartFunc of CNS,RNS

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

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

proof end;

theorem Th31: :: NCFCONT1:31

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for h being PartFunc of RNS,CNS

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

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

for RNS being RealNormSpace

for h being PartFunc of RNS,CNS

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

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

proof end;

theorem :: NCFCONT1:32

for CNS1, CNS2 being ComplexNormSpace

for f1, f2 being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 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 CNS1,CNS2

for x0 being Point of CNS1 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 :: NCFCONT1:33

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f1, f2 being PartFunc of CNS,RNS

for x0 being Point of CNS 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 RNS being RealNormSpace

for f1, f2 being PartFunc of CNS,RNS

for x0 being Point of CNS 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 :: NCFCONT1:34

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f1, f2 being PartFunc of RNS,CNS

for x0 being Point of RNS 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 RNS being RealNormSpace

for f1, f2 being PartFunc of RNS,CNS

for x0 being Point of RNS 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 Th35: :: NCFCONT1:35

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1

for z being Complex st f is_continuous_in x0 holds

z (#) f is_continuous_in x0

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1

for z being Complex st f is_continuous_in x0 holds

z (#) f is_continuous_in x0

proof end;

theorem Th36: :: NCFCONT1:36

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS

for r being Real st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS

for r being Real st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

proof end;

theorem Th37: :: NCFCONT1:37

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS

for z being Complex st f is_continuous_in x0 holds

z (#) f is_continuous_in x0

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS

for z being Complex st f is_continuous_in x0 holds

z (#) f is_continuous_in x0

proof end;

theorem :: NCFCONT1:38

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 st f is_continuous_in x0 holds

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

for f being PartFunc of CNS1,CNS2

for x0 being Point of CNS1 st f is_continuous_in x0 holds

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

proof end;

theorem :: NCFCONT1:39

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS st f is_continuous_in x0 holds

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

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for x0 being Point of CNS st f is_continuous_in x0 holds

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

proof end;

theorem :: NCFCONT1:40

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS st f is_continuous_in x0 holds

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

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

for x0 being Point of RNS st f is_continuous_in x0 holds

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

proof end;

definition

let CNS1, CNS2 be ComplexNormSpace;

let f be PartFunc of CNS1,CNS2;

let X be set ;

end;
let f be PartFunc of CNS1,CNS2;

let X be set ;

pred f is_continuous_on X means :: NCFCONT1:def 11

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

f | X is_continuous_in x0 ) );

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

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NCFCONT1:def 11 :

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for X being set holds

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

f | X is_continuous_in x0 ) ) );

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for X being set holds

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

f | X is_continuous_in x0 ) ) );

definition

let CNS be ComplexNormSpace;

let RNS be RealNormSpace;

let f be PartFunc of CNS,RNS;

let X be set ;

end;
let RNS be RealNormSpace;

let f be PartFunc of CNS,RNS;

let X be set ;

pred f is_continuous_on X means :: NCFCONT1:def 12

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

f | X is_continuous_in x0 ) );

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

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NCFCONT1:def 12 :

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for X being set holds

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

f | X is_continuous_in x0 ) ) );

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

for X being set holds

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

f | X is_continuous_in x0 ) ) );

definition

let RNS be RealNormSpace;

let CNS be ComplexNormSpace;

let g be PartFunc of RNS,CNS;

let X be set ;

end;
let CNS be ComplexNormSpace;

let g be PartFunc of RNS,CNS;

let X be set ;

pred g is_continuous_on X means :: NCFCONT1:def 13

( X c= dom g & ( for x0 being Point of RNS st x0 in X holds

g | X is_continuous_in x0 ) );

( X c= dom g & ( for x0 being Point of RNS st x0 in X holds

g | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NCFCONT1:def 13 :

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for g being PartFunc of RNS,CNS

for X being set holds

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

g | X is_continuous_in x0 ) ) );

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for g being PartFunc of RNS,CNS

for X being set holds

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

g | X is_continuous_in x0 ) ) );

definition

let CNS be ComplexNormSpace;

let f be PartFunc of the carrier of CNS,COMPLEX;

let X be set ;

end;
let f be PartFunc of the carrier of CNS,COMPLEX;

let X be set ;

pred f is_continuous_on X means :: NCFCONT1:def 14

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

f | X is_continuous_in x0 ) );

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

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NCFCONT1:def 14 :

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX

for X being set holds

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

f | X is_continuous_in x0 ) ) );

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX

for X being set holds

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

f | X is_continuous_in x0 ) ) );

definition

let CNS be ComplexNormSpace;

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

let X be set ;

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

let X be set ;

pred f is_continuous_on X means :: NCFCONT1:def 15

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

f | X is_continuous_in x0 ) );

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

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NCFCONT1:def 15 :

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL

for X being set holds

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

f | X is_continuous_in x0 ) ) );

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL

for X being set holds

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

f | X is_continuous_in x0 ) ) );

definition

let RNS be RealNormSpace;

let f be PartFunc of the carrier of RNS,COMPLEX;

let X be set ;

end;
let f be PartFunc of the carrier of RNS,COMPLEX;

let X be set ;

pred f is_continuous_on X means :: NCFCONT1:def 16

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

f | X is_continuous_in x0 ) );

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

f | X is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on NCFCONT1:def 16 :

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX

for X being set holds

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

f | X is_continuous_in x0 ) ) );

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX

for X being set holds

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

f | X is_continuous_in x0 ) ) );

theorem Th41: :: NCFCONT1:41

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 holds

( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of CNS1 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 CNS1,CNS2 holds

( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of CNS1 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 Th42: :: NCFCONT1:42

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

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

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of CNS 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 Th43: :: NCFCONT1:43

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

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

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of RNS 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 Th44: :: NCFCONT1:44

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 holds

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

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

ex s being Real st

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

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

for X being set

for f being PartFunc of CNS1,CNS2 holds

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

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

ex s being Real st

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

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

proof end;

theorem Th45: :: NCFCONT1:45

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

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

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

ex s being Real st

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

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

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

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

ex s being Real st

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

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

proof end;

theorem Th46: :: NCFCONT1:46

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

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

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

ex s being Real st

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

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

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

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

ex s being Real st

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

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

proof end;

theorem :: NCFCONT1:47

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX holds

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

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

ex s being Real st

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

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

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX holds

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

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

ex s being Real st

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

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

proof end;

theorem :: NCFCONT1:48

for CNS being ComplexNormSpace

for X being set

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

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

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

ex s being Real st

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

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

for X being set

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

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

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

ex s being Real st

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

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

proof end;

theorem :: NCFCONT1:49

for RNS being RealNormSpace

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX holds

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

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

ex s being Real st

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

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

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX holds

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

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

ex s being Real st

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

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

proof end;

theorem :: NCFCONT1:50

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 holds

( f is_continuous_on X iff f | X is_continuous_on X )

for X being set

for f being PartFunc of CNS1,CNS2 holds

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem :: NCFCONT1:51

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

( f is_continuous_on X iff f | X is_continuous_on X )

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem :: NCFCONT1:52

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

( f is_continuous_on X iff f | X is_continuous_on X )

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem :: NCFCONT1:53

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX holds

( f is_continuous_on X iff f | X is_continuous_on X )

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX holds

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem Th54: :: NCFCONT1:54

for CNS being ComplexNormSpace

for X being set

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

( f is_continuous_on X iff f | X is_continuous_on X )

for X being set

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

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem :: NCFCONT1:55

for RNS being RealNormSpace

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX holds

( f is_continuous_on X iff f | X is_continuous_on X )

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX holds

( f is_continuous_on X iff f | X is_continuous_on X )

proof end;

theorem Th56: :: NCFCONT1:56

for CNS1, CNS2 being ComplexNormSpace

for X, X1 being set

for f being PartFunc of CNS1,CNS2 st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

for X, X1 being set

for f being PartFunc of CNS1,CNS2 st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

proof end;

theorem Th57: :: NCFCONT1:57

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of CNS,RNS st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of CNS,RNS st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

proof end;

theorem Th58: :: NCFCONT1:58

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of RNS,CNS st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of RNS,CNS st f is_continuous_on X & X1 c= X holds

f is_continuous_on X1

proof end;

theorem :: NCFCONT1:59

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

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

f is_continuous_on {x0}

for f being PartFunc of CNS1,CNS2

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

f is_continuous_on {x0}

proof end;

theorem :: NCFCONT1:60

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

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

f is_continuous_on {x0}

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

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

f is_continuous_on {x0}

proof end;

theorem :: NCFCONT1:61

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

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

f is_continuous_on {x0}

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

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

f is_continuous_on {x0}

proof end;

theorem Th62: :: NCFCONT1:62

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f1, f2 being PartFunc of CNS1,CNS2 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 CNS1,CNS2 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 Th63: :: NCFCONT1:63

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f1, f2 being PartFunc of CNS,RNS 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 RNS being RealNormSpace

for X being set

for f1, f2 being PartFunc of CNS,RNS 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 Th64: :: NCFCONT1:64

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f1, f2 being PartFunc of RNS,CNS 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 RNS being RealNormSpace

for X being set

for f1, f2 being PartFunc of RNS,CNS 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 :: NCFCONT1:65

for CNS1, CNS2 being ComplexNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS1,CNS2 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 CNS1,CNS2 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 :: NCFCONT1:66

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS,RNS 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 RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS,RNS 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 :: NCFCONT1:67

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of RNS,CNS 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 RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of RNS,CNS 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 Th68: :: NCFCONT1:68

for z being Complex

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st f is_continuous_on X holds

z (#) f is_continuous_on X

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st f is_continuous_on X holds

z (#) f is_continuous_on X

proof end;

theorem Th69: :: NCFCONT1:69

for r being Real

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_continuous_on X holds

r (#) f is_continuous_on X

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_continuous_on X holds

r (#) f is_continuous_on X

proof end;

theorem Th70: :: NCFCONT1:70

for z being Complex

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_continuous_on X holds

z (#) f is_continuous_on X

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_continuous_on X holds

z (#) f is_continuous_on X

proof end;

theorem Th71: :: NCFCONT1:71

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st f is_continuous_on X holds

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

for X being set

for f being PartFunc of CNS1,CNS2 st f is_continuous_on X holds

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

proof end;

theorem Th72: :: NCFCONT1:72

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_continuous_on X holds

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_continuous_on X holds

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

proof end;

theorem Th73: :: NCFCONT1:73

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_continuous_on X holds

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_continuous_on X holds

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

proof end;

theorem :: NCFCONT1:74

for CNS1, CNS2 being ComplexNormSpace

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

f is_continuous_on the carrier of CNS1

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

f is_continuous_on the carrier of CNS1

proof end;

theorem :: NCFCONT1:75

for CNS being ComplexNormSpace

for RNS being RealNormSpace

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

f is_continuous_on the carrier of CNS

for RNS being RealNormSpace

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

f is_continuous_on the carrier of CNS

proof end;

theorem :: NCFCONT1:76

for CNS being ComplexNormSpace

for RNS being RealNormSpace

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

f is_continuous_on the carrier of RNS

for RNS being RealNormSpace

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

f is_continuous_on the carrier of RNS

proof end;

theorem Th77: :: NCFCONT1:77

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st dom f is compact & f is_continuous_on dom f holds

rng f is compact

for f being PartFunc of CNS1,CNS2 st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem Th78: :: NCFCONT1:78

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS st dom f is compact & f is_continuous_on dom f holds

rng f is compact

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem Th79: :: NCFCONT1:79

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS st dom f is compact & f is_continuous_on dom f holds

rng f is compact

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem :: NCFCONT1:80

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX st dom f is compact & f is_continuous_on dom f holds

rng f is compact

for f being PartFunc of the carrier of CNS,COMPLEX st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem Th81: :: NCFCONT1:81

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,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 CNS,REAL st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem :: NCFCONT1:82

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX st dom f is compact & f is_continuous_on dom f holds

rng f is compact

for f being PartFunc of the carrier of RNS,COMPLEX st dom f is compact & f is_continuous_on dom f holds

rng f is compact

proof end;

theorem :: NCFCONT1:83

for CNS1, CNS2 being ComplexNormSpace

for Y being Subset of CNS1

for f being PartFunc of CNS1,CNS2 st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

for Y being Subset of CNS1

for f being PartFunc of CNS1,CNS2 st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

proof end;

theorem :: NCFCONT1:84

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for Y being Subset of CNS

for f being PartFunc of CNS,RNS st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

for RNS being RealNormSpace

for Y being Subset of CNS

for f being PartFunc of CNS,RNS st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

proof end;

theorem :: NCFCONT1:85

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for Y being Subset of RNS

for f being PartFunc of RNS,CNS st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

for RNS being RealNormSpace

for Y being Subset of RNS

for f being PartFunc of RNS,CNS st Y c= dom f & Y is compact & f is_continuous_on Y holds

f .: Y is compact

proof end;

theorem Th86: :: NCFCONT1:86

for CNS being ComplexNormSpace

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

ex x1, x2 being Point of CNS 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 CNS,REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f holds

ex x1, x2 being Point of CNS st

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

proof end;

theorem Th87: :: NCFCONT1:87

for CNS1, CNS2 being ComplexNormSpace

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

ex x1, x2 being Point of CNS1 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 CNS1,CNS2 st dom f <> {} & dom f is compact & f is_continuous_on dom f holds

ex x1, x2 being Point of CNS1 st

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

proof end;

theorem Th88: :: NCFCONT1:88

for CNS being ComplexNormSpace

for RNS being RealNormSpace

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

ex x1, x2 being Point of CNS st

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

for RNS being RealNormSpace

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

ex x1, x2 being Point of CNS st

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

proof end;

theorem Th89: :: NCFCONT1:89

for CNS being ComplexNormSpace

for RNS being RealNormSpace

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

ex x1, x2 being Point of RNS st

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

for RNS being RealNormSpace

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

ex x1, x2 being Point of RNS st

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

proof end;

theorem Th90: :: NCFCONT1:90

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 holds ||.f.|| | X = ||.(f | X).||

for X being set

for f being PartFunc of CNS1,CNS2 holds ||.f.|| | X = ||.(f | X).||

proof end;

theorem Th91: :: NCFCONT1:91

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds ||.f.|| | X = ||.(f | X).||

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds ||.f.|| | X = ||.(f | X).||

proof end;

theorem Th92: :: NCFCONT1:92

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds ||.f.|| | X = ||.(f | X).||

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS holds ||.f.|| | X = ||.(f | X).||

proof end;

theorem :: NCFCONT1:93

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

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

ex x1, x2 being Point of CNS1 st

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

for f being PartFunc of CNS1,CNS2

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

ex x1, x2 being Point of CNS1 st

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

proof end;

theorem :: NCFCONT1:94

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

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

ex x1, x2 being Point of CNS st

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

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS

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

ex x1, x2 being Point of CNS st

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

proof end;

theorem :: NCFCONT1:95

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

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

ex x1, x2 being Point of RNS st

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

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS

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

ex x1, x2 being Point of RNS st

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

proof end;

theorem :: NCFCONT1:96

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL

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

ex x1, x2 being Point of CNS 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 CNS,REAL

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

ex x1, x2 being Point of CNS 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 NCFCONT1:def 17 :

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 holds

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

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

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

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 holds

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

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

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

definition
end;

:: deftheorem defines is_Lipschitzian_on NCFCONT1:def 18 :

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

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

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

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

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS holds

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

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

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

definition
end;

:: deftheorem defines is_Lipschitzian_on NCFCONT1:def 19 :

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

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

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

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

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of RNS,CNS holds

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

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

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

definition
end;

:: deftheorem defines is_Lipschitzian_on NCFCONT1:def 20 :

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX holds

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

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

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

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX holds

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

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

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

definition
end;

:: deftheorem defines is_Lipschitzian_on NCFCONT1:def 21 :

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of the carrier of CNS,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 CNS st x1 in X & x2 in X holds

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

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of the carrier of CNS,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 CNS st x1 in X & x2 in X holds

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

definition
end;

:: deftheorem defines is_Lipschitzian_on NCFCONT1:def 22 :

for RNS being RealNormSpace

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX holds

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

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

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX holds

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

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

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

theorem Th97: :: NCFCONT1:97

for CNS1, CNS2 being ComplexNormSpace

for X, X1 being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

for X, X1 being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

proof end;

theorem Th98: :: NCFCONT1:98

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

proof end;

theorem Th99: :: NCFCONT1:99

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

for RNS being RealNormSpace

for X, X1 being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X & X1 c= X holds

f is_Lipschitzian_on X1

proof end;

theorem :: NCFCONT1:100

for CNS1, CNS2 being ComplexNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

for X, X1 being set

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: NCFCONT1:101

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: NCFCONT1:102

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 + f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: NCFCONT1:103

for CNS1, CNS2 being ComplexNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

for X, X1 being set

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: NCFCONT1:104

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of CNS,RNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

proof end;

theorem :: NCFCONT1:105

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

for RNS being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of RNS,CNS st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds

f1 - f2 is_Lipschitzian_on X /\ X1

proof end;

theorem Th106: :: NCFCONT1:106

for z being Complex

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

z (#) f is_Lipschitzian_on X

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

z (#) f is_Lipschitzian_on X

proof end;

theorem Th107: :: NCFCONT1:107

for r being Real

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

r (#) f is_Lipschitzian_on X

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

r (#) f is_Lipschitzian_on X

proof end;

theorem Th108: :: NCFCONT1:108

for z being Complex

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

z (#) f is_Lipschitzian_on X

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

z (#) f is_Lipschitzian_on X

proof end;

theorem :: NCFCONT1:109

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

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

for X being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

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

proof end;

theorem :: NCFCONT1:110

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

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

proof end;

theorem :: NCFCONT1:111

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

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

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

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

proof end;

theorem Th112: :: NCFCONT1:112

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is V22() holds

f is_Lipschitzian_on X

for X being set

for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is V22() holds

f is_Lipschitzian_on X

proof end;

theorem Th113: :: NCFCONT1:113

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st X c= dom f & f | X is V22() holds

f is_Lipschitzian_on X

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st X c= dom f & f | X is V22() holds

f is_Lipschitzian_on X

proof end;

theorem Th114: :: NCFCONT1:114

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st X c= dom f & f | X is V22() holds

f is_Lipschitzian_on X

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st X c= dom f & f | X is V22() holds

f is_Lipschitzian_on X

proof end;

theorem Th116: :: NCFCONT1:116

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

f is_continuous_on X

for X being set

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

f is_continuous_on X

proof end;

theorem Th117: :: NCFCONT1:117

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

f is_continuous_on X

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

f is_continuous_on X

proof end;

theorem Th118: :: NCFCONT1:118

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

f is_continuous_on X

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

f is_continuous_on X

proof end;

theorem :: NCFCONT1:119

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX st f is_Lipschitzian_on X holds

f is_continuous_on X

for X being set

for f being PartFunc of the carrier of CNS,COMPLEX st f is_Lipschitzian_on X holds

f is_continuous_on X

proof end;

theorem Th120: :: NCFCONT1:120

for CNS being ComplexNormSpace

for X being set

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

f is_continuous_on X

for X being set

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

f is_continuous_on X

proof end;

theorem :: NCFCONT1:121

for RNS being RealNormSpace

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX st f is_Lipschitzian_on X holds

f is_continuous_on X

for X being set

for f being PartFunc of the carrier of RNS,COMPLEX st f is_Lipschitzian_on X holds

f is_continuous_on X

proof end;

theorem :: NCFCONT1:122

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st ex r being Point of CNS2 st rng f = {r} holds

f is_continuous_on dom f

for f being PartFunc of CNS1,CNS2 st ex r being Point of CNS2 st rng f = {r} holds

f is_continuous_on dom f

proof end;

theorem :: NCFCONT1:123

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS st ex r being Point of RNS st rng f = {r} holds

f is_continuous_on dom f

for RNS being RealNormSpace

for f being PartFunc of CNS,RNS st ex r being Point of RNS st rng f = {r} holds

f is_continuous_on dom f

proof end;

theorem :: NCFCONT1:124

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS st ex r being Point of CNS st rng f = {r} holds

f is_continuous_on dom f

for RNS being RealNormSpace

for f being PartFunc of RNS,CNS st ex r being Point of CNS st rng f = {r} holds

f is_continuous_on dom f

proof end;

theorem :: NCFCONT1:125

for CNS1, CNS2 being ComplexNormSpace

for X being set

for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is V22() holds

f is_continuous_on X by Th112, Th116;

for X being set

for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is V22() holds

f is_continuous_on X by Th112, Th116;

theorem :: NCFCONT1:126

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st X c= dom f & f | X is V22() holds

f is_continuous_on X by Th113, Th117;

for RNS being RealNormSpace

for X being set

for f being PartFunc of CNS,RNS st X c= dom f & f | X is V22() holds

f is_continuous_on X by Th113, Th117;

theorem :: NCFCONT1:127

for CNS being ComplexNormSpace

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st X c= dom f & f | X is V22() holds

f is_continuous_on X by Th114, Th118;

for RNS being RealNormSpace

for X being set

for f being PartFunc of RNS,CNS st X c= dom f & f | X is V22() holds

f is_continuous_on X by Th114, Th118;

theorem Th128: :: NCFCONT1:128

for CNS being ComplexNormSpace

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

f /. x0 = x0 ) holds

f is_continuous_on dom f

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

f /. x0 = x0 ) holds

f is_continuous_on dom f

proof end;

theorem :: NCFCONT1:129

for CNS being ComplexNormSpace

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

f is_continuous_on dom f

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

f is_continuous_on dom f

proof end;

theorem :: NCFCONT1:130

for CNS being ComplexNormSpace

for f being PartFunc of CNS,CNS

for Y being Subset of CNS st Y c= dom f & f | Y = id Y holds

f is_continuous_on Y

for f being PartFunc of CNS,CNS

for Y being Subset of CNS st Y c= dom f & f | Y = id Y holds

f is_continuous_on Y

proof end;

theorem :: NCFCONT1:131

for CNS being ComplexNormSpace

for X being set

for f being PartFunc of CNS,CNS

for z being Complex

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

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

f is_continuous_on X

for X being set

for f being PartFunc of CNS,CNS

for z being Complex

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

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

f is_continuous_on X

proof end;

theorem Th132: :: NCFCONT1:132

for CNS being ComplexNormSpace

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

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

f is_continuous_on dom f

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

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

f is_continuous_on dom f

proof end;

theorem :: NCFCONT1:133

for CNS being ComplexNormSpace

for X being set

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

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

f is_continuous_on X

for X being set

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

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

f is_continuous_on X

proof end;