begin
:: deftheorem Def1 defines without_zero PSCOMP_1:def 1 :
theorem Th1:
:: deftheorem Def2 defines " PSCOMP_1:def 2 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th14:
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:
theorem
theorem Th17:
theorem Th18:
Lm3:
for X being Subset of REAL st X is closed holds
- X is closed
theorem Th19:
:: deftheorem defines ++ PSCOMP_1:def 8 :
theorem Th20:
theorem Th21:
theorem Th22:
Lm4:
for X being Subset of REAL
for s being Real st X is bounded_above holds
s ++ X is bounded_above
theorem
Lm5:
for X being Subset of REAL
for p being Real st X is bounded_below holds
p ++ X is bounded_below
theorem
theorem
theorem
Lm6:
for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed
theorem Th27:
:: deftheorem defines Inv PSCOMP_1:def 9 :
theorem Th28:
theorem
canceled;
theorem
theorem Th31:
:: deftheorem defines Cl PSCOMP_1:def 10 :
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem
theorem
theorem Th38:
theorem Th39:
begin
:: 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:
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:
theorem
theorem Th43:
theorem
theorem Th45:
theorem Th46:
begin
:: 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