begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem
canceled;
theorem Th5:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th13:
begin
theorem Th14:
theorem
theorem
:: deftheorem WEIERSTR:def 1 :
canceled;
:: deftheorem WEIERSTR:def 2 :
canceled;
:: deftheorem defines [#] WEIERSTR:def 3 :
theorem Th17:
theorem Th18:
theorem Th19:
Lm1:
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
:: deftheorem defines upper_bound WEIERSTR:def 4 :
:: deftheorem defines lower_bound WEIERSTR:def 5 :
theorem Th20:
theorem Th21:
begin
:: deftheorem Def6 defines dist WEIERSTR:def 6 :
theorem Th22:
theorem
theorem
:: deftheorem Def7 defines dist_max WEIERSTR:def 7 :
:: deftheorem Def8 defines dist_min WEIERSTR:def 8 :
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem
Lm2:
[#] R^1 <> {}
;
theorem Th30:
theorem
theorem
theorem Th33:
theorem
theorem
:: deftheorem defines min_dist_min WEIERSTR:def 9 :
:: deftheorem defines max_dist_min WEIERSTR:def 10 :
:: deftheorem defines min_dist_max WEIERSTR:def 11 :
:: deftheorem defines max_dist_max WEIERSTR:def 12 :
theorem
theorem
theorem
theorem
theorem