:: NCFCONT1 semantic presentation

definition

let CLS be ComplexLinearSpace;
let seq be sequence of CLS;
func - seq -> sequence of CLS means :Def1: :: NCFCONT1:def 1
for n being Nat holds it . n = - (seq . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines - NCFCONT1:def 1 :

theorem :: NCFCONT1:1

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

proof end;

theorem Th2: :: NCFCONT1:2

for CNS being ComplexNormSpace
for seq being sequence of CNS holds - seq = (- 1r ) * seq

proof end;

definition

let CNS1, CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
func ||.f.|| -> PartFunc of the carrier of CNS1, REAL means :Def2: :: NCFCONT1:def 2
( dom it = dom f & ( for c being Point of CNS1 st c in dom it holds
it . c = ||.(f /. c).|| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ||. NCFCONT1:def 2 :

definition

let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of CNS,RNS;
func ||.f.|| -> PartFunc of the carrier of CNS, REAL means :Def3: :: NCFCONT1:def 3
( dom it = dom f & ( for c being Point of CNS st c in dom it holds
it . c = ||.(f /. c).|| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ||. NCFCONT1:def 3 :

definition

let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of RNS,CNS;
func ||.f.|| -> PartFunc of the carrier of RNS, REAL means :Def4: :: NCFCONT1:def 4
( dom it = dom f & ( for c being Point of RNS st c in dom it holds
it . c = ||.(f /. c).|| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ||. NCFCONT1:def 4 :

definition

let CNS be ComplexNormSpace;
let x0 be Point of CNS;
mode Neighbourhood of x0 -> Subset of CNS means :Def5: :: NCFCONT1:def 5
ex g being Real st
( 0 < g & { y where y is Point of CNS : ||.(y - x0).|| < g } c= it );
existence

proof end;

end;

:: deftheorem Def5 defines Neighbourhood NCFCONT1:def 5 :

theorem Th3: :: NCFCONT1:3

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

proof end;

theorem Th4: :: NCFCONT1:4

for CNS being ComplexNormSpace
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;
attr X is compact means :Def6: :: NCFCONT1:def 6
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 );

end;

:: deftheorem Def6 defines compact NCFCONT1:def 6 :

definition

let CNS be ComplexNormSpace;
let X be Subset of CNS;
attr X is closed means :: NCFCONT1:def 7
for s1 being sequence of CNS st rng s1 c= X & s1 is convergent holds
lim s1 in X;

end;

:: deftheorem defines closed NCFCONT1:def 7 :

definition

let CNS be ComplexNormSpace;
let X be Subset of CNS;
attr X is open means :: NCFCONT1:def 8
X ` is closed;

end;

:: deftheorem defines open NCFCONT1:def 8 :

definition

let CNS1, CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
let seq be sequence of CNS1;
assume A1: rng seq c= dom f ;
func f * seq -> sequence of CNS2 equals :Def9: :: NCFCONT1:def 9
f * seq;
coherence

proof end;

end;

:: deftheorem Def9 defines * NCFCONT1:def 9 :

definition

let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of CNS,RNS;
let seq be sequence of CNS;
assume A1: rng seq c= dom f ;
func f * seq -> sequence of RNS equals :Def10: :: NCFCONT1:def 10
f * seq;
coherence

proof end;

end;

:: deftheorem Def10 defines * NCFCONT1:def 10 :

definition

let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of RNS,CNS;
let seq be sequence of RNS;
assume A1: rng seq c= dom f ;
func f * seq -> sequence of CNS equals :Def11: :: NCFCONT1:def 11
f * seq;
coherence

proof end;

end;

:: deftheorem Def11 defines * NCFCONT1:def 11 :

definition

let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, COMPLEX ;
let seq be sequence of CNS;
assume A1: rng seq c= dom f ;
func f * seq -> Complex_Sequence equals :Def12: :: NCFCONT1:def 12
f * seq;
coherence

proof end;

end;

:: deftheorem Def12 defines * NCFCONT1:def 12 :

definition

let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS, COMPLEX ;
let seq be sequence of RNS;
assume A1: rng seq c= dom f ;
func f * seq -> Complex_Sequence equals :Def13: :: NCFCONT1:def 13
f * seq;
coherence

proof end;

end;

:: deftheorem Def13 defines * NCFCONT1:def 13 :

definition

let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, REAL ;
let seq be sequence of CNS;
assume A1: rng seq c= dom f ;
func f * seq -> Real_Sequence equals :Def14: :: NCFCONT1:def 14
f * seq;
coherence

proof end;

end;

:: deftheorem Def14 defines * NCFCONT1:def 14 :

definition

let CNS1, CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
let x0 be Point of CNS1;
pred f is_continuous_in x0 means :Def15: :: NCFCONT1:def 15
( 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) ) ) );

end;

:: deftheorem Def15 defines is_continuous_in NCFCONT1:def 15 :

definition

let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of CNS,RNS;
let x0 be Point of CNS;
pred f is_continuous_in x0 means :Def16: :: NCFCONT1:def 16
( 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) ) ) );

end;

:: deftheorem Def16 defines is_continuous_in NCFCONT1:def 16 :

definition

let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of RNS,CNS;
let x0 be Point of RNS;
pred f is_continuous_in x0 means :Def17: :: NCFCONT1:def 17
( 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) ) ) );

end;

:: deftheorem Def17 defines is_continuous_in NCFCONT1:def 17 :

definition

let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, COMPLEX ;
let x0 be Point of CNS;
pred f is_continuous_in x0 means :Def18: :: NCFCONT1:def 18
( 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) ) ) );

end;

:: deftheorem Def18 defines is_continuous_in NCFCONT1:def 18 :

definition

let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, REAL ;
let x0 be Point of CNS;
pred f is_continuous_in x0 means :Def19: :: NCFCONT1:def 19
( 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) ) ) );

end;

:: deftheorem Def19 defines is_continuous_in NCFCONT1:def 19 :

definition

let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS, COMPLEX ;
let x0 be Point of RNS;
pred f is_continuous_in x0 means :Def20: :: NCFCONT1:def 20
( 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) ) ) );

end;

:: deftheorem Def20 defines is_continuous_in NCFCONT1:def 20 :

theorem Th5: :: NCFCONT1:5

for n being Nat
for CNS1, CNS2 being ComplexNormSpace
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 Th6: :: NCFCONT1:6

for n being Nat
for CNS being ComplexNormSpace
for RNS being RealNormSpace
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 Th7: :: NCFCONT1:7

for n being Nat
for CNS being ComplexNormSpace
for RNS being RealNormSpace
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 Th8: :: NCFCONT1:8

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 )

proof end;

theorem Th9: :: NCFCONT1:9

for CNS being ComplexNormSpace
for seq, seq1 being sequence of CNS st seq1 is subsequence of seq holds
rng seq1 c= rng seq

proof end;

theorem Th10: :: NCFCONT1:10

for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for CSeq being sequence of CNS1 st rng CSeq c= dom f holds
for n being Nat holds (f * CSeq) . n = f /. (CSeq . n)

proof end;

theorem Th11: :: NCFCONT1:11

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for CSeq being sequence of CNS st rng CSeq c= dom f holds
for n being Nat holds (f * CSeq) . n = f /. (CSeq . n)

proof end;

theorem Th12: :: NCFCONT1:12

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for f being PartFunc of RNS,CNS
for RSeq being sequence of RNS st rng RSeq c= dom f holds
for n being Nat holds (f * RSeq) . n = f /. (RSeq . n)

proof end;

theorem Th13: :: NCFCONT1:13

for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS, COMPLEX
for CSeq being sequence of CNS st rng CSeq c= dom f holds
for n being Nat holds (f * CSeq) . n = f /. (CSeq . n)

proof end;

theorem Th14: :: NCFCONT1:14

for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS, REAL
for CSeq being sequence of CNS st rng CSeq c= dom f holds
for n being Nat holds (f * CSeq) . n = f /. (CSeq . n)

proof end;

theorem Th15: :: NCFCONT1:15

for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS, COMPLEX
for RSeq being sequence of RNS st rng RSeq c= dom f holds
for n being Nat holds (f * RSeq) . n = f /. (RSeq . n)

proof end;

theorem Th16: :: NCFCONT1:16

for CNS1, CNS2 being ComplexNormSpace
for h being PartFunc of CNS1,CNS2
for CSeq being sequence of CNS1
for Ns being increasing Seq_of_Nat st rng CSeq c= dom h holds
(h * CSeq) * Ns = h * (CSeq * Ns)

proof end;

theorem Th17: :: NCFCONT1:17

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of CNS,RNS
for Cseq being sequence of CNS
for Ns being increasing Seq_of_Nat st rng Cseq c= dom h holds
(h * Cseq) * Ns = h * (Cseq * Ns)

proof end;

theorem Th18: :: NCFCONT1:18

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of RNS,CNS
for Rseq being sequence of RNS
for Ns being increasing Seq_of_Nat st rng Rseq c= dom h holds
(h * Rseq) * Ns = h * (Rseq * Ns)

proof end;

theorem Th19: :: NCFCONT1:19

for CNS being ComplexNormSpace
for h being PartFunc of the carrier of CNS, COMPLEX
for Cseq being sequence of CNS
for Ns being increasing Seq_of_Nat st rng Cseq c= dom h holds
(h * Cseq) * Ns = h * (Cseq * Ns)

proof end;

theorem Th20: :: NCFCONT1:20

for CNS being ComplexNormSpace
for h being PartFunc of the carrier of CNS, REAL
for Cseq being sequence of CNS
for Ns being increasing Seq_of_Nat st rng Cseq c= dom h holds
(h * Cseq) * Ns = h * (Cseq * Ns)

proof end;

theorem Th21: :: NCFCONT1:21

for RNS being RealNormSpace
for h being PartFunc of the carrier of RNS, COMPLEX
for Rseq being sequence of RNS
for Ns being increasing Seq_of_Nat st rng Rseq c= dom h holds
(h * Rseq) * Ns = h * (Rseq * Ns)

proof end;

theorem Th22: :: NCFCONT1:22

for CNS1, CNS2 being ComplexNormSpace
for h being PartFunc of CNS1,CNS2
for Cseq1, Cseq2 being sequence of CNS1 st rng Cseq1 c= dom h & Cseq2 is subsequence of Cseq1 holds
h * Cseq2 is subsequence of h * Cseq1

proof end;

theorem Th23: :: NCFCONT1:23

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of CNS,RNS
for Cseq1, Cseq2 being sequence of CNS st rng Cseq1 c= dom h & Cseq2 is subsequence of Cseq1 holds
h * Cseq2 is subsequence of h * Cseq1

proof end;

theorem Th24: :: NCFCONT1:24

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h being PartFunc of RNS,CNS
for Rseq1, Rseq2 being sequence of RNS st rng Rseq1 c= dom h & Rseq2 is subsequence of Rseq1 holds
h * Rseq2 is subsequence of h * Rseq1

proof end;

theorem :: NCFCONT1:25

for seq being Complex_Sequence
for n being Nat
for Nseq being increasing Seq_of_Nat holds (seq * Nseq) . n = seq . (Nseq . n)

proof end;

theorem Th26: :: NCFCONT1:26

for CNS being ComplexNormSpace
for h being PartFunc of the carrier of CNS, COMPLEX
for Cseq1, Cseq2 being sequence of CNS st rng Cseq1 c= dom h & Cseq2 is subsequence of Cseq1 holds
h * Cseq2 is subsequence of h * Cseq1

proof end;

theorem Th27: :: NCFCONT1:27

for CNS being ComplexNormSpace
for h being PartFunc of the carrier of CNS, REAL
for Cseq1, Cseq2 being sequence of CNS st rng Cseq1 c= dom h & Cseq2 is subsequence of Cseq1 holds
h * Cseq2 is subsequence of h * Cseq1

proof end;

theorem Th28: :: NCFCONT1:28

for RNS being RealNormSpace
for h being PartFunc of the carrier of RNS, COMPLEX
for Rseq1, Rseq2 being sequence of RNS st rng Rseq1 c= dom h & Rseq2 is subsequence of Rseq1 holds
h * Rseq2 is subsequence of h * Rseq1

proof end;

theorem Th29: :: NCFCONT1:29

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 ) ) ) ) )

proof end;

theorem Th30: :: NCFCONT1:30

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 ) ) ) ) )

proof end;

theorem Th31: :: NCFCONT1:31

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 ) ) ) ) )

proof end;

theorem Th32: :: NCFCONT1:32

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
abs ((f /. x1) - (f /. x0)) < r ) ) ) ) )

proof end;

theorem Th33: :: NCFCONT1:33

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 ) ) ) ) )

proof end;

theorem Th34: :: NCFCONT1:34

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 ) ) ) ) )

proof end;

theorem Th35: :: NCFCONT1:35

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 ) ) )

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 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 Th37: :: NCFCONT1:37

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 ) ) )

proof end;

theorem Th38: :: NCFCONT1:38

proof end;

theorem Th39: :: NCFCONT1:39

proof end;

theorem Th40: :: NCFCONT1:40

proof end;

theorem :: NCFCONT1:41

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

proof end;

theorem :: NCFCONT1:42

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

proof end;

theorem :: NCFCONT1:43

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

proof end;

theorem Th44: :: NCFCONT1:44

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) )

proof end;

theorem Th45: :: NCFCONT1:45

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) )

proof end;

theorem Th46: :: NCFCONT1:46

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) )

proof end;

theorem Th47: :: NCFCONT1:47

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)

proof end;

theorem Th48: :: NCFCONT1:48

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)

proof end;

theorem Th49: :: NCFCONT1:49

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)

proof end;

theorem Th50: :: NCFCONT1:50

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 )

proof end;

theorem Th51: :: NCFCONT1:51

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 )

proof end;

theorem Th52: :: NCFCONT1:52

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 )

proof end;

theorem :: NCFCONT1:53

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 )

proof end;

theorem :: NCFCONT1:54

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 )

proof end;

theorem :: NCFCONT1:55

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 )

proof end;

theorem Th56: :: NCFCONT1:56

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

proof end;

theorem Th57: :: NCFCONT1:57

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

proof end;

theorem Th58: :: NCFCONT1:58

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

proof end;

theorem :: NCFCONT1:59

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 )

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 f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 & - f is_continuous_in 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 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 ;
pred f is_continuous_on X means :Def21: :: NCFCONT1:def 21
( X c= dom f & ( for x0 being Point of CNS1 st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def21 defines is_continuous_on NCFCONT1:def 21 :

definition

let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let f be PartFunc of CNS,RNS;
let X be set ;
pred f is_continuous_on X means :Def22: :: NCFCONT1:def 22
( X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def22 defines is_continuous_on NCFCONT1:def 22 :

definition

let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let g be PartFunc of RNS,CNS;
let X be set ;
pred g is_continuous_on X means :Def23: :: NCFCONT1:def 23
( X c= dom g & ( for x0 being Point of RNS st x0 in X holds
g | X is_continuous_in x0 ) );

end;

:: deftheorem Def23 defines is_continuous_on NCFCONT1:def 23 :

definition

let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, COMPLEX ;
let X be set ;
pred f is_continuous_on X means :Def24: :: NCFCONT1:def 24
( X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def24 defines is_continuous_on NCFCONT1:def 24 :

definition

let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS, REAL ;
let X be set ;
pred f is_continuous_on X means :Def25: :: NCFCONT1:def 25
( X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def25 defines is_continuous_on NCFCONT1:def 25 :

definition

let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS, COMPLEX ;
let X be set ;
pred f is_continuous_on X means :Def26: :: NCFCONT1:def 26
( X c= dom f & ( for x0 being Point of RNS st x0 in X holds
f | X is_continuous_in x0 ) );

end;

:: deftheorem Def26 defines is_continuous_on NCFCONT1:def 26 :

theorem Th62: :: NCFCONT1:62

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) ) ) ) )

proof end;

theorem Th63: :: NCFCONT1:63

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) ) ) ) )

proof end;

theorem Th64: :: NCFCONT1:64

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) ) ) ) )

proof end;

theorem Th65: :: NCFCONT1:65

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 ) ) ) ) )

proof end;

theorem Th66: :: NCFCONT1:66

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 ) ) ) ) )

proof end;

theorem Th67: :: NCFCONT1:67

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 ) ) ) ) )

proof end;

theorem :: NCFCONT1:68

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 ) ) ) ) )

proof end;

theorem :: NCFCONT1:69

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
abs ((f /. x1) - (f /. x0)) < r ) ) ) ) )

proof end;

theorem :: NCFCONT1:70

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 ) ) ) ) )

proof end;

theorem :: NCFCONT1:71

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 )

proof end;

theorem :: NCFCONT1:72

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 )

proof end;

theorem :: NCFCONT1:73

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 )

proof end;

theorem :: NCFCONT1:74

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 )

proof end;

theorem Th75: :: NCFCONT1:75

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 )

proof end;

theorem :: NCFCONT1:76

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 )

proof end;

theorem Th77: :: NCFCONT1:77

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

proof end;

theorem Th78: :: NCFCONT1:78

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

proof end;

theorem Th79: :: NCFCONT1:79

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

proof end;

theorem :: NCFCONT1:80

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}

proof end;

theorem :: NCFCONT1:81

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}

proof end;

theorem :: NCFCONT1:82

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}

proof end;

theorem Th83: :: NCFCONT1:83

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 )

proof end;

theorem Th84: :: NCFCONT1:84

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 )

proof end;

theorem Th85: :: NCFCONT1:85

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 )

proof end;

theorem :: NCFCONT1:86

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 )

proof end;

theorem :: NCFCONT1:87

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 )

proof end;

theorem :: NCFCONT1:88

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 )

proof end;

theorem Th89: :: NCFCONT1:89

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

proof end;

theorem Th90: :: NCFCONT1:90

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

proof end;

theorem Th91: :: NCFCONT1:91

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

proof end;

theorem Th92: :: NCFCONT1:92

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 )

proof end;

theorem Th93: :: NCFCONT1:93

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 )

proof end;

theorem Th94: :: NCFCONT1:94

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 )

proof end;

theorem :: NCFCONT1:95

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

proof end;

theorem :: NCFCONT1:96

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

proof end;

theorem :: NCFCONT1:97

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

proof end;

theorem Th98: :: NCFCONT1:98

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

proof end;

theorem Th99: :: NCFCONT1:99

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

proof end;

theorem Th100: :: NCFCONT1:100

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

proof end;

theorem :: NCFCONT1:101

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

proof end;

theorem Th102: :: NCFCONT1:102

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

proof end;

theorem :: NCFCONT1:103

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

proof end;

theorem :: NCFCONT1:104

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

proof end;

theorem :: NCFCONT1:105

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

proof end;

theorem :: NCFCONT1:106

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

proof end;

theorem Th107: :: NCFCONT1:107

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) )

proof end;

theorem Th108: :: NCFCONT1:108

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.||) )

proof end;

theorem Th109: :: NCFCONT1:109

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.||) )

proof end;

theorem Th110: :: NCFCONT1:110

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.||) )

proof end;

theorem Th111: :: NCFCONT1:111

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

proof end;

theorem Th112: :: NCFCONT1:112

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

proof end;

theorem Th113: :: NCFCONT1:113

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

proof end;

theorem :: NCFCONT1:114

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) )

proof end;

theorem :: NCFCONT1:115

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) )

proof end;

theorem :: NCFCONT1:116

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) )

proof end;

theorem :: NCFCONT1:117

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) )

proof end;

definition

let CNS1, CNS2 be ComplexNormSpace;
let X be set ;
let f be PartFunc of CNS1,CNS2;
pred f is_Lipschitzian_on X means :Def27: :: NCFCONT1:def 27
( 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).|| ) ) );

end;

:: deftheorem Def27 defines is_Lipschitzian_on NCFCONT1:def 27 :

definition

let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let X be set ;
let f be PartFunc of CNS,RNS;
pred f is_Lipschitzian_on X means :Def28: :: NCFCONT1:def 28
( 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).|| ) ) );

end;

:: deftheorem Def28 defines is_Lipschitzian_on NCFCONT1:def 28 :

definition

let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let X be set ;
let f be PartFunc of RNS,CNS;
pred f is_Lipschitzian_on X means :Def29: :: NCFCONT1:def 29
( 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).|| ) ) );

end;

:: deftheorem Def29 defines is_Lipschitzian_on NCFCONT1:def 29 :

definition

let CNS be ComplexNormSpace;
let X be set ;
let f be PartFunc of the carrier of CNS, COMPLEX ;
pred f is_Lipschitzian_on X means :Def30: :: NCFCONT1:def 30
( 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).|| ) ) );

end;

:: deftheorem Def30 defines is_Lipschitzian_on NCFCONT1:def 30 :

definition

let CNS be ComplexNormSpace;
let X be set ;
let f be PartFunc of the carrier of CNS, REAL ;
pred f is_Lipschitzian_on X means :Def31: :: NCFCONT1:def 31
( 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
abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) );

end;

:: deftheorem Def31 defines is_Lipschitzian_on NCFCONT1:def 31 :

definition

let RNS be RealNormSpace;
let X be set ;
let f be PartFunc of the carrier of RNS, COMPLEX ;
pred f is_Lipschitzian_on X means :Def32: :: NCFCONT1:def 32
( 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).|| ) ) );

end;

:: deftheorem Def32 defines is_Lipschitzian_on NCFCONT1:def 32 :

theorem Th118: :: NCFCONT1:118

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

proof end;

theorem Th119: :: NCFCONT1:119

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

proof end;

theorem Th120: :: NCFCONT1:120

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

proof end;

theorem :: NCFCONT1:121

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

proof end;

theorem :: NCFCONT1:122

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

proof end;

theorem :: NCFCONT1:123

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

proof end;

theorem :: NCFCONT1:124

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

proof end;

theorem :: NCFCONT1:125

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

proof end;

theorem :: NCFCONT1:126

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

proof end;

theorem Th127: :: NCFCONT1:127

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

proof end;

theorem Th128: :: NCFCONT1:128

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

proof end;

theorem Th129: :: NCFCONT1:129

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

proof end;

theorem :: NCFCONT1:130

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 )

proof end;

theorem :: NCFCONT1:131

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 )

proof end;

theorem :: NCFCONT1:132

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 )

proof end;

theorem Th133: :: NCFCONT1:133

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

proof end;

theorem Th134: :: NCFCONT1:134

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 is_constant_on X holds
f is_Lipschitzian_on X

proof end;

theorem Th135: :: NCFCONT1:135

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 is_constant_on X holds
f is_Lipschitzian_on X

proof end;

theorem :: NCFCONT1:136

for CNS being ComplexNormSpace
for Y being Subset of CNS holds id Y is_Lipschitzian_on Y

proof end;

theorem Th137: :: NCFCONT1:137

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

proof end;

theorem Th138: :: NCFCONT1:138

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

proof end;

theorem Th139: :: NCFCONT1:139

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

proof end;

theorem :: NCFCONT1:140

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

proof end;

theorem Th141: :: NCFCONT1:141

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

proof end;

theorem :: NCFCONT1:142

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

proof end;

theorem :: NCFCONT1:143

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

proof end;

theorem :: NCFCONT1:144

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

proof end;

theorem :: NCFCONT1:145

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

proof end;

theorem :: NCFCONT1:146

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

proof end;

theorem :: NCFCONT1:147

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 is_constant_on X holds
f is_continuous_on X

proof end;

theorem :: NCFCONT1:148

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 is_constant_on X holds
f is_continuous_on X

proof end;

theorem Th149: :: NCFCONT1:149

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

proof end;

theorem :: NCFCONT1:150

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

proof end;

theorem :: NCFCONT1:151

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

proof end;

theorem :: NCFCONT1:152

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

proof end;

theorem Th153: :: NCFCONT1:153

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

proof end;

theorem :: NCFCONT1:154

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

proof end;