begin
:: deftheorem CFCONT_1:def 1 :
canceled;
:: deftheorem Def2 defines is_continuous_in CFCONT_1:def 2 :
for f being PartFunc of COMPLEX,COMPLEX
for x0 being Element of COMPLEX holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) );
theorem
canceled;
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem
theorem Th44:
theorem
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem
theorem
theorem
begin
theorem
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem Th58:
theorem
:: deftheorem CFCONT_1:def 3 :
canceled;
:: deftheorem CFCONT_1:def 4 :
canceled;
:: deftheorem Def5 defines is_continuous_on CFCONT_1:def 5 :
for f being PartFunc of COMPLEX,COMPLEX
for X being set holds
( f is_continuous_on X iff ( X c= dom f & ( for x0 being Element of COMPLEX st x0 in X holds
f | X is_continuous_in x0 ) ) );
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem
theorem Th65:
theorem
theorem Th67:
theorem
theorem Th69:
theorem
theorem
theorem
:: deftheorem Def6 defines compact CFCONT_1:def 6 :
for X being set holds
( X is compact iff for s1 being Complex_Sequence st rng s1 c= X holds
ex s2 being Complex_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) );
theorem Th73:
theorem