PSCOMP_1: Bounding boxes for compact sets in ${\calE}^2$

:: 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

begin

notation

let X be set ;
synonym without_zero X for with_non-empty_elements ;
antonym with_zero X for with_non-empty_elements ;

end;

definition

let X be set ;
redefine attr X is with_non-empty_elements means :Def1: :: PSCOMP_1:def 1
not 0 in X;
compatibility by SETFAM_1:def 9;

end;

:: deftheorem Def1 defines without_zero PSCOMP_1:def 1 :

registration

cluster REAL -> with_zero ;
coherence by Def1;
cluster omega -> with_zero ;
coherence by Def1;

end;

registration

cluster non empty without_zero set ;
existence

proof end;

cluster non empty with_zero set ;
existence by Def1;

end;

registration

cluster non empty without_zero Element of K18(REAL );
existence

proof end;

cluster non empty with_zero Element of K18(REAL );
existence by Def1;

end;

theorem Th1: :: PSCOMP_1:1

for F being set st not F is empty & F is without_zero & F is c=-linear holds
F is centered

proof end;

registration

let F be set ;
cluster non empty c=-linear with_non-empty_elements -> centered Element of K18(K18(F));
coherence by Th1;

end;

registration

let X, Y be non empty set ;
let f be Function of X,Y;
cluster f .: X -> non empty ;
coherence

proof end;

end;

definition

let X, Y be set ;
let f be Function of X,Y;
func " f -> Function of (bool Y),(bool X) means :Def2: :: PSCOMP_1:def 2
for y being Subset of Y holds it . y = f " y;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines " PSCOMP_1:def 2 :

theorem Th2: :: PSCOMP_1:2

for X, Y, x being set
for S being Subset-Family of Y
for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S

proof end;

theorem Th3: :: PSCOMP_1:3

for r, s being real number st (abs r) + (abs s) = 0 holds
r = 0

proof end;

theorem Th4: :: PSCOMP_1:4

for r, s, t being real number st r < s & s < t holds
abs s < (abs r) + (abs t)

proof end;

theorem :: PSCOMP_1:5

canceled;

theorem Th6: :: PSCOMP_1:6

for seq being Real_Sequence st seq is convergent & seq is non-empty & lim seq = 0 holds
not seq " is bounded

proof end;

theorem Th7: :: PSCOMP_1:7

for seq being Real_Sequence holds
( rng seq is bounded iff seq is bounded )

proof end;

notation

let X be real-membered set ;
synonym sup X for upper_bound X;
synonym inf X for lower_bound X;

end;

definition

let X be real-membered set ;
attr X is with_max means :Def3: :: PSCOMP_1:def 3
( X is bounded_above & sup X in X );
attr X is with_min means :Def4: :: PSCOMP_1:def 4
( X is bounded_below & inf X in X );

end;

:: deftheorem Def3 defines with_max PSCOMP_1:def 3 :

:: deftheorem Def4 defines with_min PSCOMP_1:def 4 :

registration

cluster non empty bounded closed Element of K18(REAL );
existence

proof end;

end;

definition

let R be Subset-Family of REAL ;
attr R is open means :Def5: :: PSCOMP_1:def 5
for X being Subset of REAL st X in R holds
X is open ;
attr R is closed means :Def6: :: PSCOMP_1:def 6
for X being Subset of REAL st X in R holds
X is closed ;

end;

:: deftheorem Def5 defines open PSCOMP_1:def 5 :

:: deftheorem Def6 defines closed PSCOMP_1:def 6 :

definition

let X be Subset of REAL ;
func - X -> Subset of REAL equals :: PSCOMP_1:def 7
{ (- r3) where r3 is Real : r3 in X } ;
coherence

proof end;

involutiveness

proof end;

end;

:: 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

for r being real number
for X being Subset of REAL holds
( r in X iff - r in - X )

proof end;

registration

let X be non empty Subset of REAL ;
cluster - X -> non empty ;
coherence

proof end;

end;

Lm1: for X being Subset of REAL st X is bounded_above holds
- X is bounded_below

proof end;

Lm2: for X being Subset of REAL st X is bounded_below holds
- X is bounded_above

proof end;

theorem Th15: :: PSCOMP_1:15

for X being Subset of REAL holds
( X is bounded_above iff - X is bounded_below )

proof end;

theorem :: PSCOMP_1:16

for X being Subset of REAL holds
( X is bounded_below iff - X is bounded_above )

proof end;

theorem Th17: :: PSCOMP_1:17

for X being non empty Subset of REAL st X is bounded_below holds
inf X = - (sup (- X))

proof end;

theorem Th18: :: PSCOMP_1:18

for X being non empty Subset of REAL st X is bounded_above holds
sup X = - (inf (- X))

proof end;

Lm3: for X being Subset of REAL st X is closed holds
- X is closed

proof end;

theorem Th19: :: PSCOMP_1:19

for X being Subset of REAL holds
( X is closed iff - X is closed )

proof end;

definition

let X be Subset of REAL ;
let p be Real;
redefine func p ++ X equals :: PSCOMP_1:def 8
{ (p + r3) where r3 is Real : r3 in X } ;
compatibility

proof end;

end;

:: deftheorem defines ++ PSCOMP_1:def 8 :

theorem Th20: :: PSCOMP_1:20

for r being real number
for X being Subset of REAL
for q3 being Real holds
( r in X iff q3 + r in q3 ++ X )

proof end;

registration

let X be non empty Subset of REAL ;
let s be Real;
cluster s ++ X -> non empty ;
coherence

proof end;

end;

theorem Th21: :: PSCOMP_1:21

for X being Subset of REAL holds X = 0 ++ X

proof end;

theorem Th22: :: PSCOMP_1:22

for X being Subset of REAL
for q3, p3 being Real holds q3 ++ (p3 ++ X) = (q3 + p3) ++ X

proof end;

Lm4: for X being Subset of REAL
for s being Real st X is bounded_above holds
s ++ X is bounded_above

proof end;

theorem :: PSCOMP_1:23

for X being Subset of REAL
for q3 being Real holds
( X is bounded_above iff q3 ++ X is bounded_above )

proof end;

Lm5: for X being Subset of REAL
for p being Real st X is bounded_below holds
p ++ X is bounded_below

proof end;

theorem :: PSCOMP_1:24

for X being Subset of REAL
for q3 being Real holds
( X is bounded_below iff q3 ++ X is bounded_below )

proof end;

theorem :: PSCOMP_1:25

for q3 being Real
for X being non empty Subset of REAL st X is bounded_below holds
inf (q3 ++ X) = q3 + (inf X)

proof end;

theorem :: PSCOMP_1:26

for q3 being Real
for X being non empty Subset of REAL st X is bounded_above holds
sup (q3 ++ X) = q3 + (sup X)

proof end;

Lm6: for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed

proof end;

theorem Th27: :: PSCOMP_1:27

for X being Subset of REAL
for q3 being Real holds
( X is closed iff q3 ++ X is closed )

proof end;

definition

let X be Subset of REAL ;
func Inv X -> Subset of REAL equals :: PSCOMP_1:def 9
{ (1 / r3) where r3 is Real : r3 in X } ;
coherence

proof end;

involutiveness

proof end;

end;

:: deftheorem defines Inv PSCOMP_1:def 9 :

theorem Th28: :: PSCOMP_1:28

for r being real number
for X being Subset of REAL holds
( r in X iff 1 / r in Inv X )

proof end;

registration

let X be non empty Subset of REAL ;
cluster Inv X -> non empty ;
coherence

proof end;

end;

registration

let X be without_zero Subset of REAL ;
cluster Inv X -> without_zero ;
coherence

proof end;

end;

theorem :: PSCOMP_1:29

canceled;

theorem :: PSCOMP_1:30

for X being without_zero Subset of REAL st X is closed & X is bounded holds
Inv X is closed

proof end;

theorem Th31: :: PSCOMP_1:31

for Z being Subset-Family of REAL st Z is closed holds
meet Z is closed

proof end;

definition

let X be Subset of REAL ;
func Cl X -> Subset of REAL equals :: PSCOMP_1:def 10
meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
coherence

proof end;

projectivity

proof end;

end;

:: deftheorem defines Cl PSCOMP_1:def 10 :

registration

let X be Subset of REAL ;
cluster Cl X -> closed ;
coherence

proof end;

end;

theorem Th32: :: PSCOMP_1:32

for X being Subset of REAL
for Y being closed Subset of REAL st X c= Y holds
Cl X c= Y

proof end;

theorem Th33: :: PSCOMP_1:33

for X being Subset of REAL holds X c= Cl X

proof end;

theorem Th34: :: PSCOMP_1:34

for X being Subset of REAL holds
( X is closed iff X = Cl X )

proof end;

theorem :: PSCOMP_1:35

Cl ({} REAL ) = {} by Th34;

theorem :: PSCOMP_1:36

Cl ([#] REAL ) = REAL by Th34;

theorem :: PSCOMP_1:37

for X, Y being Subset of REAL st X c= Y holds
Cl X c= Cl Y

proof end;

theorem Th38: :: PSCOMP_1:38

for X being Subset of REAL
for r3 being Real holds
( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds
not O /\ X is empty )

proof end;

theorem Th39: :: PSCOMP_1:39

for X being Subset of REAL
for r3 being Real st r3 in Cl X holds
ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )

proof end;

begin

definition

let X be set ;
let f be Function of X,REAL ;
:: original: bounded_below
redefine attr f is bounded_below means :Def11: :: PSCOMP_1:def 11
f .: X is bounded_below ;
compatibility

proof end;

:: original: bounded_above
redefine attr f is bounded_above means :Def12: :: PSCOMP_1:def 12
f .: X is bounded_above ;
compatibility

proof end;

end;

:: deftheorem Def11 defines bounded_below PSCOMP_1:def 11 :

:: deftheorem Def12 defines bounded_above PSCOMP_1:def 12 :

definition

let X be set ;
let f be Function of X,REAL ;
canceled;
attr f is with_max means :Def14: :: PSCOMP_1:def 14
f .: X is with_max ;
attr f is with_min means :Def15: :: PSCOMP_1:def 15
f .: X is with_min ;

end;

:: deftheorem PSCOMP_1:def 13 :

:: deftheorem Def14 defines with_max PSCOMP_1:def 14 :

:: deftheorem Def15 defines with_min PSCOMP_1:def 15 :

theorem Th40: :: PSCOMP_1:40

for X, A being set
for f being Function of X,REAL holds (- f) .: A = - (f .: A)

proof end;

Lm7: for X being non empty set
for f being Function of X,REAL st f is with_max holds
- f is with_min

proof end;

Lm8: for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max

proof end;

theorem Th41: :: PSCOMP_1:41

for X being non empty set
for f being Function of X,REAL holds
( f is with_min iff - f is with_max )

proof end;

theorem :: PSCOMP_1:42

for X being non empty set
for f being Function of X,REAL holds
( f is with_max iff - f is with_min )

proof end;

theorem Th43: :: PSCOMP_1:43

for X being set
for A being Subset of REAL
for f being Function of X,REAL holds (- f) " A = f " (- A)

proof end;

theorem :: PSCOMP_1:44

for X, A being set
for f being Function of X,REAL
for s being Real holds (s + f) .: A = s ++ (f .: A)

proof end;

theorem Th45: :: PSCOMP_1:45

for X being set
for A being Subset of REAL
for f being Function of X,REAL
for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)

proof end;

notation

let f be real-valued Function;
synonym Inv f for f " ;

end;

definition

let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: Inv
redefine func Inv f -> PartFunc of C,REAL ;
coherence

proof end;

end;

theorem Th46: :: PSCOMP_1:46

for X being set
for A being without_zero Subset of REAL
for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)

proof end;

begin

definition

let T be 1-sorted ;
canceled;
canceled;
canceled;
mode RealMap of T is Function of the carrier of T,REAL ;

end;

:: deftheorem PSCOMP_1:def 16 :

:: deftheorem PSCOMP_1:def 17 :

:: deftheorem PSCOMP_1:def 18 :

registration

let T be non empty 1-sorted ;
cluster bounded Element of K18(K19(the carrier of T,REAL ));
existence

proof end;

end;

definition

let T be 1-sorted ;
let f be RealMap of T;
canceled;
func inf f -> Real equals :: PSCOMP_1:def 20
lower_bound (f .: the carrier of T);
coherence ;
func sup f -> Real equals :: PSCOMP_1:def 21
upper_bound (f .: the carrier of T);
coherence ;

end;

:: deftheorem PSCOMP_1:def 19 :

:: deftheorem defines inf PSCOMP_1:def 20 :

:: deftheorem defines sup PSCOMP_1:def 21 :

theorem Th47: :: PSCOMP_1:47

for T being non empty TopSpace
for f being V40() RealMap of T
for p being Point of T holds f . p >= inf f

proof end;

theorem :: PSCOMP_1:48

for T being non empty TopSpace
for f being V40() RealMap of T
for s being Real st ( for t being Point of T holds f . t >= s ) holds
inf f >= s

proof end;

theorem :: PSCOMP_1:49

for r being real number
for T being non empty TopSpace
for f being RealMap of T st ( for p being Point of T holds f . p >= r ) & ( for t being real number st ( for p being Point of T holds f . p >= t ) holds
r >= t ) holds
r = inf f

proof end;

theorem Th50: :: PSCOMP_1:50

for T being non empty TopSpace
for f being V39() RealMap of T
for p being Point of T holds f . p <= sup f

proof end;

theorem :: PSCOMP_1:51

for T being non empty TopSpace
for f being V39() RealMap of T
for t being real number st ( for p being Point of T holds f . p <= t ) holds
sup f <= t

proof end;

theorem :: PSCOMP_1:52

for r being real number
for T being non empty TopSpace
for f being RealMap of T st ( for p being Point of T holds f . p <= r ) & ( for t being real number st ( for p being Point of T holds f . p <= t ) holds
r <= t ) holds
r = sup f

proof end;

theorem Th53: :: PSCOMP_1:53

for T being non empty 1-sorted
for f being bounded RealMap of T holds inf f <= sup f

proof end;

definition

let T be TopStruct ;
let f be RealMap of T;
canceled;
canceled;
canceled;
attr f is continuous means :Def25: :: PSCOMP_1:def 25
for Y being Subset of REAL st Y is closed holds
f " Y is closed ;

end;

:: deftheorem PSCOMP_1:def 22 :

:: deftheorem PSCOMP_1:def 23 :

:: deftheorem PSCOMP_1:def 24 :

:: deftheorem Def25 defines continuous PSCOMP_1:def 25 :

registration

let T be non empty TopSpace;
cluster continuous Element of K18(K19(the carrier of T,REAL ));
existence

proof end;

end;

registration

let T be non empty TopSpace;
let S be non empty SubSpace of T;
cluster continuous Element of K18(K19(the carrier of S,REAL ));
existence

proof end;

end;

theorem Th54: :: PSCOMP_1:54

for T being TopStruct
for f being RealMap of T holds
( f is continuous iff for Y being Subset of REAL st Y is open holds
f " Y is open )

proof end;

theorem Th55: :: PSCOMP_1:55

for T being TopStruct
for f being RealMap of T st f is continuous holds
- f is continuous

proof end;

theorem Th56: :: PSCOMP_1:56

for r3 being Real
for T being TopStruct
for f being RealMap of T st f is continuous holds
r3 + f is continuous

proof end;

theorem Th57: :: PSCOMP_1:57

for T being TopStruct
for f being RealMap of T st f is continuous & not 0 in rng f holds
Inv f is continuous

proof end;

theorem :: PSCOMP_1:58

for T being TopStruct
for f being RealMap of T
for R being Subset-Family of REAL st f is continuous & R is open holds
(" f) .: R is open

proof end;

theorem Th59: :: PSCOMP_1:59

for T being TopStruct
for f being RealMap of T
for R being Subset-Family of REAL st f is continuous & R is closed holds
(" f) .: R is closed

proof end;

definition

let T be non empty TopStruct ;
let f be RealMap of T;
let X be Subset of T;
:: original: |
redefine func f | X -> RealMap of (T | X);
coherence

proof end;

end;

registration

let T be non empty TopSpace;
let f be continuous RealMap of T;
let X be Subset of T;
cluster f | X -> continuous RealMap of (T | X);
coherence

proof end;

end;

registration

let T be non empty TopSpace;
let P be non empty compact Subset of T;
cluster T | P -> compact ;
coherence by COMPTS_1:12;

end;

begin

theorem Th60: :: PSCOMP_1:60

for T being non empty TopSpace holds
( ( for f being RealMap of T st f is continuous holds
f is with_max ) iff for f being RealMap of T st f is continuous holds
f is with_min )

proof end;

theorem Th61: :: PSCOMP_1:61

for T being non empty TopSpace holds
( ( for f being RealMap of T st f is continuous holds
f is bounded ) iff for f being RealMap of T st f is continuous holds
f is with_max )

proof end;

definition

canceled;
let T be TopStruct ;
attr T is pseudocompact means :Def27: :: PSCOMP_1:def 27
for f being RealMap of T st f is continuous holds
f is bounded ;

end;

:: deftheorem PSCOMP_1:def 26 :

:: deftheorem Def27 defines pseudocompact PSCOMP_1:def 27 :

registration

cluster non empty compact -> non empty pseudocompact TopStruct ;
coherence

proof end;

end;

registration

cluster non empty compact TopStruct ;
existence

proof end;

end;

registration

let T be non empty pseudocompact TopSpace;
cluster continuous -> bounded with_max with_min Element of K18(K19(the carrier of T,REAL ));
coherence

proof end;

end;

theorem Th62: :: PSCOMP_1:62

for T being non empty TopSpace
for X being non empty Subset of T
for Y being compact Subset of T
for f being continuous RealMap of T st X c= Y holds
inf (f | Y) <= inf (f | X)

proof end;

theorem Th63: :: PSCOMP_1:63

for T being non empty TopSpace
for X being non empty Subset of T
for Y being compact Subset of T
for f being continuous RealMap of T st X c= Y holds
sup (f | X) <= sup (f | Y)

proof end;

begin

theorem Th64: :: PSCOMP_1:64

for n being Element of NAT
for X, Y being compact Subset of (TOP-REAL n) holds X /\ Y is compact

proof end;

definition

func proj1 -> RealMap of (TOP-REAL 2) means :Def28: :: PSCOMP_1:def 28
for p being Point of (TOP-REAL 2) holds it . p = p `1 ;
existence

proof end;

uniqueness

proof end;

func proj2 -> RealMap of (TOP-REAL 2) means :Def29: :: PSCOMP_1:def 29
for p being Point of (TOP-REAL 2) holds it . p = p `2 ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines proj1 PSCOMP_1:def 28 :

:: deftheorem Def29 defines proj2 PSCOMP_1:def 29 :

theorem Th65: :: PSCOMP_1:65

for r, s being real number holds proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }

proof end;

theorem Th66: :: PSCOMP_1:66

for P being Subset of (TOP-REAL 2)
for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } holds
P is open

proof end;

theorem Th67: :: PSCOMP_1:67

for r, s being real number holds proj2 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) }

proof end;

theorem Th68: :: PSCOMP_1:68

for P being Subset of (TOP-REAL 2)
for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } holds
P is open

proof end;

registration

cluster proj1 -> continuous ;
coherence

proof end;

cluster proj2 -> continuous ;
coherence

proof end;

end;

theorem Th69: :: PSCOMP_1:69

for X being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in X holds
(proj1 | X) . p = p `1

proof end;

theorem Th70: :: PSCOMP_1:70

for X being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in X holds
(proj2 | X) . p = p `2

proof end;

definition

let X be Subset of (TOP-REAL 2);
func W-bound X -> Real equals :: PSCOMP_1:def 30
inf (proj1 | X);
coherence ;
func N-bound X -> Real equals :: PSCOMP_1:def 31
sup (proj2 | X);
coherence ;
func E-bound X -> Real equals :: PSCOMP_1:def 32
sup (proj1 | X);
coherence ;
func S-bound X -> Real equals :: PSCOMP_1:def 33
inf (proj2 | X);
coherence ;

end;

:: 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) )

proof end;

theorem :: PSCOMP_1:71

for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X ) by Lm9;

definition

let X be Subset of (TOP-REAL 2);
func SW-corner X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 34
|[(W-bound X),(S-bound X)]|;
coherence ;
func NW-corner X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 35
|[(W-bound X),(N-bound X)]|;
coherence ;
func NE-corner X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 36
|[(E-bound X),(N-bound X)]|;
coherence ;
func SE-corner X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 37
|[(E-bound X),(S-bound X)]|;
coherence ;

end;

:: 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

for P being Subset of (TOP-REAL 2) holds (SW-corner P) `1 = (NW-corner P) `1

proof end;

theorem :: PSCOMP_1:81

for P being Subset of (TOP-REAL 2) holds (SE-corner P) `1 = (NE-corner P) `1

proof end;

theorem :: PSCOMP_1:82

for P being Subset of (TOP-REAL 2) holds (NW-corner P) `2 = (NE-corner P) `2

proof end;

theorem :: PSCOMP_1:83

for P being Subset of (TOP-REAL 2) holds (SW-corner P) `2 = (SE-corner P) `2

proof end;

definition

let X be Subset of (TOP-REAL 2);
func W-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 38
(LSeg (SW-corner X),(NW-corner X)) /\ X;
coherence ;
func N-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 39
(LSeg (NW-corner X),(NE-corner X)) /\ X;
coherence ;
func E-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 40
(LSeg (SE-corner X),(NE-corner X)) /\ X;
coherence ;
func S-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 41
(LSeg (SW-corner X),(SE-corner X)) /\ X;
coherence ;

end;

:: 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 :

registration

let X be non empty compact Subset of (TOP-REAL 2);
cluster W-most X -> non empty compact ;
coherence

proof end;

cluster N-most X -> non empty compact ;
coherence

proof end;

cluster E-most X -> non empty compact ;
coherence

proof end;

cluster S-most X -> non empty compact ;
coherence

proof end;

end;

definition

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

for P being Subset of (TOP-REAL 2) holds
( (SW-corner P) `1 = (W-min P) `1 & (SW-corner P) `1 = (W-max P) `1 & (W-min P) `1 = (W-max P) `1 & (W-min P) `1 = (NW-corner P) `1 & (W-max P) `1 = (NW-corner P) `1 )

proof end;

theorem :: PSCOMP_1:86

canceled;

theorem Th87: :: PSCOMP_1:87

for X being non empty compact Subset of (TOP-REAL 2) holds
( (SW-corner X) `2 <= (W-min X) `2 & (SW-corner X) `2 <= (W-max X) `2 & (SW-corner X) `2 <= (NW-corner X) `2 & (W-min X) `2 <= (W-max X) `2 & (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )

proof end;

theorem Th88: :: PSCOMP_1:88

for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in W-most Z holds
( p `1 = (W-min Z) `1 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) )

proof end;

theorem Th89: :: PSCOMP_1:89

for X being non empty compact Subset of (TOP-REAL 2) holds W-most X c= LSeg (W-min X),(W-max X)

proof end;

theorem :: PSCOMP_1:90

for X being non empty compact Subset of (TOP-REAL 2) holds LSeg (W-min X),(W-max X) c= LSeg (SW-corner X),(NW-corner X)

proof end;

theorem Th91: :: PSCOMP_1:91

for X being non empty compact Subset of (TOP-REAL 2) holds
( W-min X in W-most X & W-max X in W-most X )

proof end;

theorem :: PSCOMP_1:92

for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SW-corner X),(W-min X)) /\ X = {(W-min X)} & (LSeg (W-max X),(NW-corner X)) /\ X = {(W-max X)} )

proof end;

theorem :: PSCOMP_1:93

for X being non empty compact Subset of (TOP-REAL 2) st W-min X = W-max X holds
W-most X = {(W-min X)}

proof end;

theorem :: PSCOMP_1:94

canceled;

theorem Th95: :: PSCOMP_1:95

for P being Subset of (TOP-REAL 2) holds
( (NW-corner P) `2 = (N-min P) `2 & (NW-corner P) `2 = (N-max P) `2 & (N-min P) `2 = (N-max P) `2 & (N-min P) `2 = (NE-corner P) `2 & (N-max P) `2 = (NE-corner P) `2 )

proof end;

theorem :: PSCOMP_1:96

canceled;

theorem Th97: :: PSCOMP_1:97

for X being non empty compact Subset of (TOP-REAL 2) holds
( (NW-corner X) `1 <= (N-min X) `1 & (NW-corner X) `1 <= (N-max X) `1 & (NW-corner X) `1 <= (NE-corner X) `1 & (N-min X) `1 <= (N-max X) `1 & (N-min X) `1 <= (NE-corner X) `1 & (N-max X) `1 <= (NE-corner X) `1 )

proof end;

theorem Th98: :: PSCOMP_1:98

for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in N-most Z holds
( p `2 = (N-min Z) `2 & ( Z is compact implies ( (N-min Z) `1 <= p `1 & p `1 <= (N-max Z) `1 ) ) )

proof end;

theorem Th99: :: PSCOMP_1:99

for X being non empty compact Subset of (TOP-REAL 2) holds N-most X c= LSeg (N-min X),(N-max X)

proof end;

theorem :: PSCOMP_1:100

for X being non empty compact Subset of (TOP-REAL 2) holds LSeg (N-min X),(N-max X) c= LSeg (NW-corner X),(NE-corner X)

proof end;

theorem Th101: :: PSCOMP_1:101

for X being non empty compact Subset of (TOP-REAL 2) holds
( N-min X in N-most X & N-max X in N-most X )

proof end;

theorem :: PSCOMP_1:102

for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (NW-corner X),(N-min X)) /\ X = {(N-min X)} & (LSeg (N-max X),(NE-corner X)) /\ X = {(N-max X)} )

proof end;

theorem :: PSCOMP_1:103

for X being non empty compact Subset of (TOP-REAL 2) st N-min X = N-max X holds
N-most X = {(N-min X)}

proof end;

theorem :: PSCOMP_1:104

canceled;

theorem Th105: :: PSCOMP_1:105

for P being Subset of (TOP-REAL 2) holds
( (SE-corner P) `1 = (E-min P) `1 & (SE-corner P) `1 = (E-max P) `1 & (E-min P) `1 = (E-max P) `1 & (E-min P) `1 = (NE-corner P) `1 & (E-max P) `1 = (NE-corner P) `1 )

proof end;

theorem :: PSCOMP_1:106

canceled;

theorem Th107: :: PSCOMP_1:107

for X being non empty compact Subset of (TOP-REAL 2) holds
( (SE-corner X) `2 <= (E-min X) `2 & (SE-corner X) `2 <= (E-max X) `2 & (SE-corner X) `2 <= (NE-corner X) `2 & (E-min X) `2 <= (E-max X) `2 & (E-min X) `2 <= (NE-corner X) `2 & (E-max X) `2 <= (NE-corner X) `2 )

proof end;

theorem Th108: :: PSCOMP_1:108

for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in E-most Z holds
( p `1 = (E-min Z) `1 & ( Z is compact implies ( (E-min Z) `2 <= p `2 & p `2 <= (E-max Z) `2 ) ) )

proof end;

theorem Th109: :: PSCOMP_1:109

for X being non empty compact Subset of (TOP-REAL 2) holds E-most X c= LSeg (E-min X),(E-max X)

proof end;

theorem :: PSCOMP_1:110

for X being non empty compact Subset of (TOP-REAL 2) holds LSeg (E-min X),(E-max X) c= LSeg (SE-corner X),(NE-corner X)

proof end;

theorem Th111: :: PSCOMP_1:111

for X being non empty compact Subset of (TOP-REAL 2) holds
( E-min X in E-most X & E-max X in E-most X )

proof end;

theorem :: PSCOMP_1:112

for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SE-corner X),(E-min X)) /\ X = {(E-min X)} & (LSeg (E-max X),(NE-corner X)) /\ X = {(E-max X)} )

proof end;

theorem :: PSCOMP_1:113

for X being non empty compact Subset of (TOP-REAL 2) st E-min X = E-max X holds
E-most X = {(E-min X)}

proof end;

theorem :: PSCOMP_1:114

canceled;

theorem Th115: :: PSCOMP_1:115

for P being Subset of (TOP-REAL 2) holds
( (SW-corner P) `2 = (S-min P) `2 & (SW-corner P) `2 = (S-max P) `2 & (S-min P) `2 = (S-max P) `2 & (S-min P) `2 = (SE-corner P) `2 & (S-max P) `2 = (SE-corner P) `2 )

proof end;

theorem :: PSCOMP_1:116

canceled;

theorem Th117: :: PSCOMP_1:117

for X being non empty compact Subset of (TOP-REAL 2) holds
( (SW-corner X) `1 <= (S-min X) `1 & (SW-corner X) `1 <= (S-max X) `1 & (SW-corner X) `1 <= (SE-corner X) `1 & (S-min X) `1 <= (S-max X) `1 & (S-min X) `1 <= (SE-corner X) `1 & (S-max X) `1 <= (SE-corner X) `1 )

proof end;

theorem Th118: :: PSCOMP_1:118

for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in S-most Z holds
( p `2 = (S-min Z) `2 & ( Z is compact implies ( (S-min Z) `1 <= p `1 & p `1 <= (S-max Z) `1 ) ) )

proof end;

theorem Th119: :: PSCOMP_1:119

for X being non empty compact Subset of (TOP-REAL 2) holds S-most X c= LSeg (S-min X),(S-max X)

proof end;

theorem :: PSCOMP_1:120

for X being non empty compact Subset of (TOP-REAL 2) holds LSeg (S-min X),(S-max X) c= LSeg (SW-corner X),(SE-corner X)

proof end;

theorem Th121: :: PSCOMP_1:121

for X being non empty compact Subset of (TOP-REAL 2) holds
( S-min X in S-most X & S-max X in S-most X )

proof end;

theorem :: PSCOMP_1:122

for X being non empty compact Subset of (TOP-REAL 2) holds
( (LSeg (SW-corner X),(S-min X)) /\ X = {(S-min X)} & (LSeg (S-max X),(SE-corner X)) /\ X = {(S-max X)} )

proof end;

theorem :: PSCOMP_1:123

for X being non empty compact Subset of (TOP-REAL 2) st S-min X = S-max X holds
S-most X = {(S-min X)}

proof end;

theorem :: PSCOMP_1:124

for P being Subset of (TOP-REAL 2) st W-max P = N-min P holds
W-max P = NW-corner P

proof end;

theorem :: PSCOMP_1:125

for P being Subset of (TOP-REAL 2) st N-max P = E-max P holds
N-max P = NE-corner P

proof end;

theorem :: PSCOMP_1:126

for P being Subset of (TOP-REAL 2) st E-min P = S-max P holds
E-min P = SE-corner P

proof end;

theorem :: PSCOMP_1:127

for P being Subset of (TOP-REAL 2) st S-min P = W-min P holds
S-min P = SW-corner P

proof end;

theorem :: PSCOMP_1:128

for r, s being real number holds
( proj2 . |[r,s]| = s & proj1 . |[r,s]| = r )

proof end;

theorem :: PSCOMP_1:129

for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
N-bound X <= N-bound Y by Th63;

theorem :: PSCOMP_1:130

for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
E-bound X <= E-bound Y by Th63;

theorem :: PSCOMP_1:131

for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
S-bound X >= S-bound Y by Th62;

theorem :: PSCOMP_1:132

for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
W-bound X >= W-bound Y by Th62;