:: The Theorem of Weierstrass
:: by J\'ozef Bia\las and Yatsuka Nakamura
::
:: Received July 10, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: WEIERSTR:1
theorem Th2: :: WEIERSTR:2
theorem Th3: :: WEIERSTR:3
theorem :: WEIERSTR:4
canceled;
theorem Th5: :: WEIERSTR:5
theorem :: WEIERSTR:6
canceled;
theorem :: WEIERSTR:7
canceled;
theorem :: WEIERSTR:8
canceled;
theorem :: WEIERSTR:9
canceled;
theorem :: WEIERSTR:10
canceled;
theorem :: WEIERSTR:11
theorem :: WEIERSTR:12
theorem Th13: :: WEIERSTR:13
theorem Th14: :: WEIERSTR:14
theorem :: WEIERSTR:15
theorem :: WEIERSTR:16
:: deftheorem WEIERSTR:def 1 :
canceled;
:: deftheorem WEIERSTR:def 2 :
canceled;
:: deftheorem defines [#] WEIERSTR:def 3 :
theorem Th17: :: WEIERSTR:17
theorem Th18: :: WEIERSTR:18
theorem Th19: :: WEIERSTR:19
Lm1:
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T 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: :: WEIERSTR:20
theorem Th21: :: WEIERSTR:21
:: deftheorem Def6 defines dist WEIERSTR:def 6 :
theorem Th22: :: WEIERSTR:22
theorem :: WEIERSTR:23
theorem :: WEIERSTR:24
:: deftheorem Def7 defines dist_max WEIERSTR:def 7 :
:: deftheorem Def8 defines dist_min WEIERSTR:def 8 :
theorem Th25: :: WEIERSTR:25
theorem Th26: :: WEIERSTR:26
theorem :: WEIERSTR:27
theorem Th28: :: WEIERSTR:28
theorem :: WEIERSTR:29
Lm2:
[#] R^1 <> {}
;
theorem Th30: :: WEIERSTR:30
theorem :: WEIERSTR:31
theorem :: WEIERSTR:32
theorem Th33: :: WEIERSTR:33
theorem :: WEIERSTR:34
theorem :: WEIERSTR:35
:: 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 :: WEIERSTR:36
theorem :: WEIERSTR:37
theorem :: WEIERSTR:38
theorem :: WEIERSTR:39
theorem :: WEIERSTR:40