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

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

proof end;

Lm2: 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 :: PSCOMP_1:1

canceled;

theorem :: PSCOMP_1:2

canceled;

theorem :: PSCOMP_1:3

canceled;

theorem :: PSCOMP_1:4

canceled;

theorem :: PSCOMP_1:5

canceled;

theorem :: PSCOMP_1:6

canceled;

theorem :: PSCOMP_1:7

canceled;

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

canceled;

theorem :: PSCOMP_1:15

canceled;

theorem :: PSCOMP_1:16

canceled;

theorem :: PSCOMP_1:17

canceled;

theorem :: PSCOMP_1:18

canceled;

theorem :: PSCOMP_1:19

canceled;

theorem :: PSCOMP_1:20

canceled;

theorem :: PSCOMP_1:21

canceled;

theorem :: PSCOMP_1:22

canceled;

theorem :: PSCOMP_1:23

canceled;

theorem :: PSCOMP_1:24

canceled;

theorem :: PSCOMP_1:25

canceled;

theorem :: PSCOMP_1:26

canceled;

theorem :: PSCOMP_1:27

canceled;

theorem :: PSCOMP_1:28

canceled;

theorem :: PSCOMP_1:29

canceled;

theorem :: PSCOMP_1:30

canceled;

theorem :: PSCOMP_1:31

canceled;

theorem :: PSCOMP_1:32

canceled;

theorem :: PSCOMP_1:33

canceled;

theorem :: PSCOMP_1:34

canceled;

theorem :: PSCOMP_1:35

canceled;

theorem :: PSCOMP_1:36

canceled;

theorem :: PSCOMP_1:37

canceled;

theorem :: PSCOMP_1:38

canceled;

theorem :: PSCOMP_1:39

canceled;

theorem :: PSCOMP_1:40

canceled;

theorem :: PSCOMP_1:41

canceled;

theorem :: PSCOMP_1:42

canceled;

theorem :: PSCOMP_1:43

canceled;

theorem :: PSCOMP_1:44

canceled;

theorem :: PSCOMP_1:45

canceled;

theorem :: PSCOMP_1:46

canceled;

begin

definition

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

end;

registration

let T be non empty 1-sorted ;
cluster non empty Relation-like Function-like V23( the carrier of T) V24( the carrier of T, REAL ) complex-valued ext-real-valued real-valued bounded Element of K18(K19( the carrier of T,REAL));
existence
ex b₁ being RealMap of T st b₁ is bounded

proof end;

end;

definition

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

end;

:: 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 lower_bound PSCOMP_1:def 20 :
for T being 1-sorted
for f being RealMap of T holds lower_bound f = lower_bound (f .: the carrier of T);

:: deftheorem defines upper_bound PSCOMP_1:def 21 :
for T being 1-sorted
for f being RealMap of T holds upper_bound f = upper_bound (f .: the carrier of T);

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 >= lower_bound 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
lower_bound 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 = lower_bound 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 <= upper_bound 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
upper_bound 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 = upper_bound f

proof end;

theorem Th53: :: PSCOMP_1:53

for T being non empty 1-sorted
for f being bounded RealMap of T holds lower_bound f <= upper_bound 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 :
canceled;

:: deftheorem PSCOMP_1:def 23 :
canceled;

:: deftheorem PSCOMP_1:def 24 :
canceled;

:: deftheorem Def25 defines continuous PSCOMP_1:def 25 :
for T being TopStruct
for f being RealMap of T holds
( f is continuous iff for Y being Subset of REAL st Y is closed holds
f " Y is closed );

registration

let T be non empty TopSpace;
cluster non empty Relation-like Function-like V23( the carrier of T) V24( the carrier of T, REAL ) complex-valued ext-real-valued real-valued continuous Element of K18(K19( the carrier of T,REAL));
existence
ex b₁ being RealMap of T st b₁ is continuous

proof end;

end;

registration

let T be non empty TopSpace;
let S be non empty SubSpace of T;
cluster non empty Relation-like Function-like V23( the carrier of S) V24( the carrier of S, REAL ) complex-valued ext-real-valued real-valued continuous Element of K18(K19( the carrier of S,REAL));
existence
ex b₁ being RealMap of S st b₁ is continuous

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
f | X is RealMap of (T | X)

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
for b₁ being RealMap of (T | X) st b₁ = f | X holds
b₁ is continuous

proof end;

end;

registration

let T be non empty TopSpace;
let P be non empty compact Subset of T;
cluster T | P -> compact ;
coherence
T | P is compact 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 :
canceled;

:: deftheorem Def27 defines pseudocompact PSCOMP_1:def 27 :
for T being TopStruct holds
( T is pseudocompact iff for f being RealMap of T st f is continuous holds
f is bounded );

registration

cluster non empty TopSpace-like compact -> non empty pseudocompact TopStruct ;
coherence
for b₁ being non empty TopSpace st b₁ is compact holds
b₁ is pseudocompact

proof end;

end;

registration

cluster non empty TopSpace-like compact TopStruct ;
existence
ex b₁ being TopSpace st
( not b₁ is empty & b₁ is compact )

proof end;

end;

registration

let T be non empty pseudocompact TopSpace;
cluster Function-like V24( the carrier of T, REAL ) continuous -> bounded with_max with_min Element of K18(K19( the carrier of T,REAL));
coherence
for b₁ being RealMap of T st b₁ is continuous holds
( b₁ is bounded & b₁ is with_max & b₁ is with_min )

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
lower_bound (f | Y) <= lower_bound (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
upper_bound (f | X) <= upper_bound (f | Y)

proof end;

begin

theorem :: PSCOMP_1:64

canceled;

registration

let n be Element of NAT ;
let X, Y be compact Subset of (TOP-REAL n);
cluster X /\ Y -> compact Subset of (TOP-REAL n);
coherence
for b₁ being Subset of (TOP-REAL n) st b₁ = X /\ Y holds
b₁ is compact by COMPTS_1:20;

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
ex b<sub>1</sub> being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds b<sub>1</sub> . p = p `1

proof end;

uniqueness
for b₁, b₂ being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b₁ . p = p `1 ) & ( for p being Point of (TOP-REAL 2) holds b<sub>2</sub> . p = p `1 ) holds
b₁ = b₂

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
ex b<sub>1</sub> being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds b<sub>1</sub> . p = p `2

proof end;

uniqueness
for b₁, b₂ being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b₁ . p = p `2 ) & ( for p being Point of (TOP-REAL 2) holds b<sub>2</sub> . p = p `2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def28 defines proj1 PSCOMP_1:def 28 :
for b₁ being RealMap of (TOP-REAL 2) holds
( b₁ = proj1 iff for p being Point of (TOP-REAL 2) holds b₁ . p = p `1 );

:: deftheorem Def29 defines proj2 PSCOMP_1:def 29 :
for b₁ being RealMap of (TOP-REAL 2) holds
( b₁ = proj2 iff for p being Point of (TOP-REAL 2) holds b₁ . p = p `2 );

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
proj1 is continuous

proof end;

cluster proj2 -> continuous ;
coherence
proj2 is continuous

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
lower_bound (proj1 | X);
coherence
lower_bound (proj1 | X) is Real ;
func N-bound X -> Real equals :: PSCOMP_1:def 31
upper_bound (proj2 | X);
coherence
upper_bound (proj2 | X) is Real ;
func E-bound X -> Real equals :: PSCOMP_1:def 32
upper_bound (proj1 | X);
coherence
upper_bound (proj1 | X) is Real ;
func S-bound X -> Real equals :: PSCOMP_1:def 33
lower_bound (proj2 | X);
coherence
lower_bound (proj2 | X) is Real ;

end;

:: deftheorem defines W-bound PSCOMP_1:def 30 :
for X being Subset of (TOP-REAL 2) holds W-bound X = lower_bound (proj1 | X);

:: deftheorem defines N-bound PSCOMP_1:def 31 :
for X being Subset of (TOP-REAL 2) holds N-bound X = upper_bound (proj2 | X);

:: deftheorem defines E-bound PSCOMP_1:def 32 :
for X being Subset of (TOP-REAL 2) holds E-bound X = upper_bound (proj1 | X);

:: deftheorem defines S-bound PSCOMP_1:def 33 :
for X being Subset of (TOP-REAL 2) holds S-bound X = lower_bound (proj2 | X);

Lm3: for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (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 Lm3;

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
|[(W-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;
func NW-corner X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 35
|[(W-bound X),(N-bound X)]|;
coherence
|[(W-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;
func NE-corner X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 36
|[(E-bound X),(N-bound X)]|;
coherence
|[(E-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;
func SE-corner X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 37
|[(E-bound X),(S-bound X)]|;
coherence
|[(E-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;

end;

:: deftheorem defines SW-corner PSCOMP_1:def 34 :
for X being Subset of (TOP-REAL 2) holds SW-corner X = |[(W-bound X),(S-bound X)]|;

:: deftheorem defines NW-corner PSCOMP_1:def 35 :
for X being Subset of (TOP-REAL 2) holds NW-corner X = |[(W-bound X),(N-bound X)]|;

:: deftheorem defines NE-corner PSCOMP_1:def 36 :
for X being Subset of (TOP-REAL 2) holds NE-corner X = |[(E-bound X),(N-bound X)]|;

:: deftheorem defines SE-corner PSCOMP_1:def 37 :
for X being Subset of (TOP-REAL 2) holds SE-corner X = |[(E-bound X),(S-bound X)]|;

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
(LSeg ((SW-corner X),(NW-corner X))) /\ X is Subset of (TOP-REAL 2) ;
func N-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 39
(LSeg ((NW-corner X),(NE-corner X))) /\ X;
coherence
(LSeg ((NW-corner X),(NE-corner X))) /\ X is Subset of (TOP-REAL 2) ;
func E-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 40
(LSeg ((SE-corner X),(NE-corner X))) /\ X;
coherence
(LSeg ((SE-corner X),(NE-corner X))) /\ X is Subset of (TOP-REAL 2) ;
func S-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 41
(LSeg ((SW-corner X),(SE-corner X))) /\ X;
coherence
(LSeg ((SW-corner X),(SE-corner X))) /\ X is Subset of (TOP-REAL 2) ;

end;

:: deftheorem defines W-most PSCOMP_1:def 38 :
for X being Subset of (TOP-REAL 2) holds W-most X = (LSeg ((SW-corner X),(NW-corner X))) /\ X;

:: deftheorem defines N-most PSCOMP_1:def 39 :
for X being Subset of (TOP-REAL 2) holds N-most X = (LSeg ((NW-corner X),(NE-corner X))) /\ X;

:: deftheorem defines E-most PSCOMP_1:def 40 :
for X being Subset of (TOP-REAL 2) holds E-most X = (LSeg ((SE-corner X),(NE-corner X))) /\ X;

:: deftheorem defines S-most PSCOMP_1:def 41 :
for X being Subset of (TOP-REAL 2) holds S-most X = (LSeg ((SW-corner X),(SE-corner X))) /\ X;

registration

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

proof end;

cluster N-most X -> non empty compact ;
coherence
( not N-most X is empty & N-most X is compact )

proof end;

cluster E-most X -> non empty compact ;
coherence
( not E-most X is empty & E-most X is compact )

proof end;

cluster S-most X -> non empty compact ;
coherence
( not S-most X is empty & S-most X is compact )

proof end;

end;

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),(lower_bound (proj2 | (W-most X)))]|;
coherence
|[(W-bound X),(lower_bound (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),(upper_bound (proj2 | (W-most X)))]|;
coherence
|[(W-bound X),(upper_bound (proj2 | (W-most X)))]| is Point of (TOP-REAL 2) ;
func N-min X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 44
|[(lower_bound (proj1 | (N-most X))),(N-bound X)]|;
coherence
|[(lower_bound (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
|[(upper_bound (proj1 | (N-most X))),(N-bound X)]|;
coherence
|[(upper_bound (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),(upper_bound (proj2 | (E-most X)))]|;
coherence
|[(E-bound X),(upper_bound (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),(lower_bound (proj2 | (E-most X)))]|;
coherence
|[(E-bound X),(lower_bound (proj2 | (E-most X)))]| is Point of (TOP-REAL 2) ;
func S-max X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 48
|[(upper_bound (proj1 | (S-most X))),(S-bound X)]|;
coherence
|[(upper_bound (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
|[(lower_bound (proj1 | (S-most X))),(S-bound X)]|;
coherence
|[(lower_bound (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2) ;

end;

:: deftheorem defines W-min PSCOMP_1:def 42 :
for X being Subset of (TOP-REAL 2) holds W-min X = |[(W-bound X),(lower_bound (proj2 | (W-most X)))]|;

:: deftheorem defines W-max PSCOMP_1:def 43 :
for X being Subset of (TOP-REAL 2) holds W-max X = |[(W-bound X),(upper_bound (proj2 | (W-most X)))]|;

:: deftheorem defines N-min PSCOMP_1:def 44 :
for X being Subset of (TOP-REAL 2) holds N-min X = |[(lower_bound (proj1 | (N-most X))),(N-bound X)]|;

:: deftheorem defines N-max PSCOMP_1:def 45 :
for X being Subset of (TOP-REAL 2) holds N-max X = |[(upper_bound (proj1 | (N-most X))),(N-bound X)]|;

:: deftheorem defines E-max PSCOMP_1:def 46 :
for X being Subset of (TOP-REAL 2) holds E-max X = |[(E-bound X),(upper_bound (proj2 | (E-most X)))]|;

:: deftheorem defines E-min PSCOMP_1:def 47 :
for X being Subset of (TOP-REAL 2) holds E-min X = |[(E-bound X),(lower_bound (proj2 | (E-most X)))]|;

:: deftheorem defines S-max PSCOMP_1:def 48 :
for X being Subset of (TOP-REAL 2) holds S-max X = |[(upper_bound (proj1 | (S-most X))),(S-bound X)]|;

:: deftheorem defines S-min PSCOMP_1:def 49 :
for X being Subset of (TOP-REAL 2) holds S-min X = |[(lower_bound (proj1 | (S-most X))),(S-bound X)]|;

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;