:: Bounding boxes for compact sets in ${\calE}^2$
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997 Association of Mizar Users
:: deftheorem Def1 defines without_zero PSCOMP_1:def 1 :
theorem Th1: :: PSCOMP_1:1
:: deftheorem Def2 defines " PSCOMP_1:def 2 :
theorem Th2: :: PSCOMP_1:2
theorem Th3: :: PSCOMP_1:3
theorem Th4: :: PSCOMP_1:4
theorem :: PSCOMP_1:5
canceled;
theorem Th6: :: PSCOMP_1:6
theorem Th7: :: PSCOMP_1:7
:: deftheorem Def3 defines with_max PSCOMP_1:def 3 :
:: deftheorem Def4 defines with_min PSCOMP_1:def 4 :
:: deftheorem Def5 defines open PSCOMP_1:def 5 :
:: deftheorem Def6 defines closed PSCOMP_1:def 6 :
:: deftheorem defines - PSCOMP_1:def 7 :
theorem :: PSCOMP_1:8
canceled;
theorem :: PSCOMP_1:9
canceled;
theorem :: PSCOMP_1:10
canceled;
theorem :: PSCOMP_1:11
canceled;
theorem :: PSCOMP_1:12
canceled;
theorem :: PSCOMP_1:13
canceled;
theorem Th14: :: PSCOMP_1:14
Lm1:
for X being Subset of REAL st X is bounded_above holds
- X is bounded_below
Lm2:
for X being Subset of REAL st X is bounded_below holds
- X is bounded_above
theorem Th15: :: PSCOMP_1:15
theorem :: PSCOMP_1:16
theorem Th17: :: PSCOMP_1:17
theorem Th18: :: PSCOMP_1:18
Lm3:
for X being Subset of REAL st X is closed holds
- X is closed
theorem Th19: :: PSCOMP_1:19
:: deftheorem defines ++ PSCOMP_1:def 8 :
theorem Th20: :: PSCOMP_1:20
theorem Th21: :: PSCOMP_1:21
theorem Th22: :: PSCOMP_1:22
Lm4:
for X being Subset of REAL
for s being Real st X is bounded_above holds
s ++ X is bounded_above
theorem :: PSCOMP_1:23
Lm5:
for X being Subset of REAL
for p being Real st X is bounded_below holds
p ++ X is bounded_below
theorem :: PSCOMP_1:24
theorem :: PSCOMP_1:25
theorem :: PSCOMP_1:26
Lm6:
for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed
theorem Th27: :: PSCOMP_1:27
:: deftheorem defines Inv PSCOMP_1:def 9 :
theorem Th28: :: PSCOMP_1:28
theorem :: PSCOMP_1:29
canceled;
theorem :: PSCOMP_1:30
theorem Th31: :: PSCOMP_1:31
:: deftheorem defines Cl PSCOMP_1:def 10 :
theorem Th32: :: PSCOMP_1:32
theorem Th33: :: PSCOMP_1:33
theorem Th34: :: PSCOMP_1:34
theorem :: PSCOMP_1:35
theorem :: PSCOMP_1:36
theorem :: PSCOMP_1:37
theorem Th38: :: PSCOMP_1:38
theorem Th39: :: PSCOMP_1:39
:: deftheorem Def11 defines bounded_below PSCOMP_1:def 11 :
:: deftheorem Def12 defines bounded_above PSCOMP_1:def 12 :
:: deftheorem PSCOMP_1:def 13 :
canceled;
:: deftheorem Def14 defines with_max PSCOMP_1:def 14 :
:: deftheorem Def15 defines with_min PSCOMP_1:def 15 :
theorem Th40: :: PSCOMP_1:40
Lm7:
for X being non empty set
for f being Function of X, REAL st f is with_max holds
- f is with_min
Lm8:
for X being non empty set
for f being Function of X, REAL st f is with_min holds
- f is with_max
theorem Th41: :: PSCOMP_1:41
theorem :: PSCOMP_1:42
theorem Th43: :: PSCOMP_1:43
theorem :: PSCOMP_1:44
theorem Th45: :: PSCOMP_1:45
theorem Th46: :: PSCOMP_1:46
:: deftheorem PSCOMP_1:def 16 :
canceled;
:: deftheorem PSCOMP_1:def 17 :
canceled;
:: deftheorem PSCOMP_1:def 18 :
canceled;
:: deftheorem PSCOMP_1:def 19 :
canceled;
:: deftheorem defines inf PSCOMP_1:def 20 :
:: deftheorem defines sup PSCOMP_1:def 21 :
theorem Th47: :: PSCOMP_1:47
theorem :: PSCOMP_1:48
theorem :: PSCOMP_1:49
theorem Th50: :: PSCOMP_1:50
theorem :: PSCOMP_1:51
theorem :: PSCOMP_1:52
theorem Th53: :: PSCOMP_1:53
:: deftheorem PSCOMP_1:def 22 :
canceled;
:: deftheorem PSCOMP_1:def 23 :
canceled;
:: deftheorem PSCOMP_1:def 24 :
canceled;
:: deftheorem Def25 defines continuous PSCOMP_1:def 25 :
theorem Th54: :: PSCOMP_1:54
theorem Th55: :: PSCOMP_1:55
theorem Th56: :: PSCOMP_1:56
theorem Th57: :: PSCOMP_1:57
theorem :: PSCOMP_1:58
theorem Th59: :: PSCOMP_1:59
theorem Th60: :: PSCOMP_1:60
theorem Th61: :: PSCOMP_1:61
:: deftheorem PSCOMP_1:def 26 :
canceled;
:: deftheorem Def27 defines pseudocompact PSCOMP_1:def 27 :
theorem Th62: :: PSCOMP_1:62
theorem Th63: :: PSCOMP_1:63
theorem Th64: :: PSCOMP_1:64
:: deftheorem Def28 defines proj1 PSCOMP_1:def 28 :
:: deftheorem Def29 defines proj2 PSCOMP_1:def 29 :
theorem Th65: :: PSCOMP_1:65
theorem Th66: :: PSCOMP_1:66
theorem Th67: :: PSCOMP_1:67
theorem Th68: :: PSCOMP_1:68
theorem Th69: :: PSCOMP_1:69
theorem Th70: :: PSCOMP_1:70
:: deftheorem defines W-bound PSCOMP_1:def 30 :
:: deftheorem defines N-bound PSCOMP_1:def 31 :
:: deftheorem defines E-bound PSCOMP_1:def 32 :
:: deftheorem defines S-bound PSCOMP_1:def 33 :
Lm9:
for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( inf (proj1 | X) <= p `1 & p `1 <= sup (proj1 | X) & inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) )
theorem :: PSCOMP_1:71
:: deftheorem defines SW-corner PSCOMP_1:def 34 :
:: deftheorem defines NW-corner PSCOMP_1:def 35 :
:: deftheorem defines NE-corner PSCOMP_1:def 36 :
:: deftheorem defines SE-corner PSCOMP_1:def 37 :
theorem :: PSCOMP_1:72
canceled;
theorem :: PSCOMP_1:73
canceled;
theorem :: PSCOMP_1:74
canceled;
theorem :: PSCOMP_1:75
canceled;
theorem :: PSCOMP_1:76
canceled;
theorem :: PSCOMP_1:77
canceled;
theorem :: PSCOMP_1:78
canceled;
theorem :: PSCOMP_1:79
canceled;
theorem :: PSCOMP_1:80
theorem :: PSCOMP_1:81
theorem :: PSCOMP_1:82
theorem :: PSCOMP_1:83
:: deftheorem defines W-most PSCOMP_1:def 38 :
:: deftheorem defines N-most PSCOMP_1:def 39 :
:: deftheorem defines E-most PSCOMP_1:def 40 :
:: deftheorem defines S-most PSCOMP_1:def 41 :
definition
let X be
Subset of
(TOP-REAL 2);
func W-min X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 42
|[(W-bound X),(inf (proj2 | (W-most X)))]|;
coherence
|[(W-bound X),(inf (proj2 | (W-most X)))]| is Point of (TOP-REAL 2)
;
func W-max X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 43
|[(W-bound X),(sup (proj2 | (W-most X)))]|;
coherence
|[(W-bound X),(sup (proj2 | (W-most X)))]| is Point of (TOP-REAL 2)
;
func N-min X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 44
|[(inf (proj1 | (N-most X))),(N-bound X)]|;
coherence
|[(inf (proj1 | (N-most X))),(N-bound X)]| is Point of (TOP-REAL 2)
;
func N-max X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 45
|[(sup (proj1 | (N-most X))),(N-bound X)]|;
coherence
|[(sup (proj1 | (N-most X))),(N-bound X)]| is Point of (TOP-REAL 2)
;
func E-max X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 46
|[(E-bound X),(sup (proj2 | (E-most X)))]|;
coherence
|[(E-bound X),(sup (proj2 | (E-most X)))]| is Point of (TOP-REAL 2)
;
func E-min X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 47
|[(E-bound X),(inf (proj2 | (E-most X)))]|;
coherence
|[(E-bound X),(inf (proj2 | (E-most X)))]| is Point of (TOP-REAL 2)
;
func S-max X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 48
|[(sup (proj1 | (S-most X))),(S-bound X)]|;
coherence
|[(sup (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2)
;
func S-min X -> Point of
(TOP-REAL 2) equals :: PSCOMP_1:def 49
|[(inf (proj1 | (S-most X))),(S-bound X)]|;
coherence
|[(inf (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2)
;
end;
:: deftheorem defines W-min PSCOMP_1:def 42 :
:: deftheorem defines W-max PSCOMP_1:def 43 :
:: deftheorem defines N-min PSCOMP_1:def 44 :
:: deftheorem defines N-max PSCOMP_1:def 45 :
:: deftheorem defines E-max PSCOMP_1:def 46 :
:: deftheorem defines E-min PSCOMP_1:def 47 :
:: deftheorem defines S-max PSCOMP_1:def 48 :
:: deftheorem defines S-min PSCOMP_1:def 49 :
theorem :: PSCOMP_1:84
canceled;
theorem Th85: :: PSCOMP_1:85
theorem :: PSCOMP_1:86
canceled;
theorem Th87: :: PSCOMP_1:87
theorem Th88: :: PSCOMP_1:88
theorem Th89: :: PSCOMP_1:89
theorem :: PSCOMP_1:90
theorem Th91: :: PSCOMP_1:91
theorem :: PSCOMP_1:92
theorem :: PSCOMP_1:93
theorem :: PSCOMP_1:94
canceled;
theorem Th95: :: PSCOMP_1:95
theorem :: PSCOMP_1:96
canceled;
theorem Th97: :: PSCOMP_1:97
theorem Th98: :: PSCOMP_1:98
theorem Th99: :: PSCOMP_1:99
theorem :: PSCOMP_1:100
theorem Th101: :: PSCOMP_1:101
theorem :: PSCOMP_1:102
theorem :: PSCOMP_1:103
theorem :: PSCOMP_1:104
canceled;
theorem Th105: :: PSCOMP_1:105
theorem :: PSCOMP_1:106
canceled;
theorem Th107: :: PSCOMP_1:107
theorem Th108: :: PSCOMP_1:108
theorem Th109: :: PSCOMP_1:109
theorem :: PSCOMP_1:110
theorem Th111: :: PSCOMP_1:111
theorem :: PSCOMP_1:112
theorem :: PSCOMP_1:113
theorem :: PSCOMP_1:114
canceled;
theorem Th115: :: PSCOMP_1:115
theorem :: PSCOMP_1:116
canceled;
theorem Th117: :: PSCOMP_1:117
theorem Th118: :: PSCOMP_1:118
theorem Th119: :: PSCOMP_1:119
theorem :: PSCOMP_1:120
theorem Th121: :: PSCOMP_1:121
theorem :: PSCOMP_1:122
theorem :: PSCOMP_1:123
theorem :: PSCOMP_1:124
theorem :: PSCOMP_1:125
theorem :: PSCOMP_1:126
theorem :: PSCOMP_1:127
theorem :: PSCOMP_1:128
theorem :: PSCOMP_1:129
theorem :: PSCOMP_1:130
theorem :: PSCOMP_1:131
theorem :: PSCOMP_1:132