begin
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
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
begin
:: deftheorem PSCOMP_1:def 1 :
canceled;
:: deftheorem PSCOMP_1:def 2 :
canceled;
:: deftheorem PSCOMP_1:def 3 :
canceled;
:: deftheorem PSCOMP_1:def 4 :
canceled;
:: deftheorem PSCOMP_1:def 5 :
canceled;
:: deftheorem PSCOMP_1:def 6 :
canceled;
:: deftheorem PSCOMP_1:def 7 :
canceled;
:: deftheorem PSCOMP_1:def 8 :
canceled;
:: deftheorem PSCOMP_1:def 9 :
canceled;
:: deftheorem PSCOMP_1:def 10 :
canceled;
:: deftheorem PSCOMP_1:def 11 :
canceled;
:: deftheorem PSCOMP_1:def 12 :
canceled;
:: deftheorem PSCOMP_1:def 13 :
canceled;
:: deftheorem PSCOMP_1:def 14 :
canceled;
:: deftheorem PSCOMP_1:def 15 :
canceled;
:: 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:
theorem
theorem
theorem Th50:
theorem
theorem
theorem Th53:
:: 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:
theorem Th55:
theorem Th56:
theorem Th57:
theorem
theorem Th59:
begin
theorem Th60:
theorem Th61:
:: deftheorem PSCOMP_1:def 26 :
canceled;
:: deftheorem Def27 defines pseudocompact PSCOMP_1:def 27 :
theorem Th62:
theorem Th63:
begin
theorem Th64:
:: deftheorem Def28 defines proj1 PSCOMP_1:def 28 :
:: deftheorem Def29 defines proj2 PSCOMP_1:def 29 :
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
:: 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
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
:: 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
|[(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
|[(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
|[(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
|[(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
|[(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
|[(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
|[(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
|[(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
canceled;
theorem Th85:
theorem
canceled;
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem Th91:
theorem
theorem
theorem
canceled;
theorem Th95:
theorem
canceled;
theorem Th97:
theorem Th98:
theorem Th99:
theorem
theorem Th101:
theorem
theorem
theorem
canceled;
theorem Th105:
theorem
canceled;
theorem Th107:
theorem Th108:
theorem Th109:
theorem
theorem Th111:
theorem
theorem
theorem
canceled;
theorem Th115:
theorem
canceled;
theorem Th117:
theorem Th118:
theorem Th119:
theorem
theorem Th121:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem