:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki

::

:: Received July 29, 1997

:: Copyright (c) 1997-2018 Association of Mizar Users

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;

registration

let T be non empty 1-sorted ;

ex b_{1} being RealMap of T st b_{1} is bounded

end;
cluster non empty Relation-like the carrier of T -defined REAL -valued Function-like V31( the carrier of T) V32( the carrier of T, REAL ) complex-valued ext-real-valued real-valued bounded for RealMap of ;

existence ex b

proof end;

definition

let T be 1-sorted ;

let f be RealMap of T;

coherence

lower_bound (f .: the carrier of T) is Real ;

coherence

upper_bound (f .: the carrier of T) is Real ;

end;
let f be RealMap of T;

coherence

lower_bound (f .: the carrier of T) is Real ;

coherence

upper_bound (f .: the carrier of T) is Real ;

:: deftheorem defines lower_bound PSCOMP_1:def 1 :

for T being 1-sorted

for f being RealMap of T holds lower_bound f = lower_bound (f .: the carrier of T);

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

for T being 1-sorted

for f being RealMap of T holds upper_bound f = upper_bound (f .: the carrier of T);

for T being 1-sorted

for f being RealMap of T holds upper_bound f = upper_bound (f .: the carrier of T);

theorem Th1: :: PSCOMP_1:1

for T being non empty TopSpace

for f being V50() RealMap of T

for p being Point of T holds f . p >= lower_bound f

for f being V50() RealMap of T

for p being Point of T holds f . p >= lower_bound f

proof end;

theorem :: PSCOMP_1:2

for T being non empty TopSpace

for f being V50() RealMap of T

for s being Real st ( for t being Point of T holds f . t >= s ) holds

lower_bound f >= s

for f being V50() 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:3

for r being Real

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 st ( for p being Point of T holds f . p >= t ) holds

r >= t ) holds

r = lower_bound f

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 st ( for p being Point of T holds f . p >= t ) holds

r >= t ) holds

r = lower_bound f

proof end;

theorem Th4: :: PSCOMP_1:4

for T being non empty TopSpace

for f being V49() RealMap of T

for p being Point of T holds f . p <= upper_bound f

for f being V49() RealMap of T

for p being Point of T holds f . p <= upper_bound f

proof end;

theorem :: PSCOMP_1:5

for T being non empty TopSpace

for f being V49() RealMap of T

for t being Real st ( for p being Point of T holds f . p <= t ) holds

upper_bound f <= t

for f being V49() RealMap of T

for t being Real st ( for p being Point of T holds f . p <= t ) holds

upper_bound f <= t

proof end;

theorem :: PSCOMP_1:6

for r being Real

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 st ( for p being Point of T holds f . p <= t ) holds

r <= t ) holds

r = upper_bound f

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 st ( for p being Point of T holds f . p <= t ) holds

r <= t ) holds

r = upper_bound f

proof end;

theorem Th7: :: PSCOMP_1:7

for T being non empty 1-sorted

for f being bounded RealMap of T holds lower_bound f <= upper_bound f

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;

end;
let f be RealMap of T;

attr f is continuous means :: PSCOMP_1:def 3

for Y being Subset of REAL st Y is closed holds

f " Y is closed ;

for Y being Subset of REAL st Y is closed holds

f " Y is closed ;

:: deftheorem defines continuous PSCOMP_1:def 3 :

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

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;

ex b_{1} being RealMap of T st b_{1} is continuous

end;
cluster non empty Relation-like the carrier of T -defined REAL -valued Function-like V31( the carrier of T) V32( the carrier of T, REAL ) complex-valued ext-real-valued real-valued continuous for RealMap of ;

existence ex b

proof end;

registration

let T be non empty TopSpace;

let S be non empty SubSpace of T;

ex b_{1} being RealMap of S st b_{1} is continuous

end;
let S be non empty SubSpace of T;

cluster non empty Relation-like the carrier of S -defined REAL -valued Function-like V31( the carrier of S) V32( the carrier of S, REAL ) complex-valued ext-real-valued real-valued continuous for RealMap of ;

existence ex b

proof end;

theorem Th8: :: PSCOMP_1:8

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 )

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 Th10: :: PSCOMP_1:10

for r3 being Real

for T being TopStruct

for f being RealMap of T st f is continuous holds

r3 + f is continuous

for T being TopStruct

for f being RealMap of T st f is continuous holds

r3 + f is continuous

proof end;

theorem Th11: :: PSCOMP_1:11

for T being TopStruct

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

Inv f is continuous

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

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

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 Th13: :: PSCOMP_1:13

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

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)

end;
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;

registration

let T be non empty TopSpace;

let f be continuous RealMap of T;

let X be Subset of T;

coherence

for b_{1} being RealMap of (T | X) st b_{1} = f | X holds

b_{1} is continuous

end;
let f be continuous RealMap of T;

let X be Subset of T;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let P be non empty compact Subset of T;

coherence

T | P is compact by COMPTS_1:3;

end;
let P be non empty compact Subset of T;

coherence

T | P is compact by COMPTS_1:3;

theorem Th14: :: PSCOMP_1:14

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 )

( ( 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 Th15: :: PSCOMP_1:15

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 )

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

let T be TopStruct ;

end;
attr T is pseudocompact means :Def4: :: PSCOMP_1:def 4

for f being RealMap of T st f is continuous holds

f is bounded ;

for f being RealMap of T st f is continuous holds

f is bounded ;

:: deftheorem Def4 defines pseudocompact PSCOMP_1:def 4 :

for T being TopStruct holds

( T is pseudocompact iff for f being RealMap of T st f is continuous holds

f is bounded );

for T being TopStruct holds

( T is pseudocompact iff for f being RealMap of T st f is continuous holds

f is bounded );

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is compact holds

b_{1} is pseudocompact

end;
for b

b

proof end;

registration
end;

registration

let T be non empty pseudocompact TopSpace;

for b_{1} being RealMap of T st b_{1} is continuous holds

( b_{1} is bounded & b_{1} is with_max & b_{1} is with_min )

end;
cluster Function-like V32( the carrier of T, REAL ) continuous -> with_max with_min bounded for RealMap of ;

coherence for b

( b

proof end;

theorem Th16: :: PSCOMP_1:16

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)

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 Th17: :: PSCOMP_1:17

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)

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;

registration

let n be Element of NAT ;

let X, Y be compact Subset of (TOP-REAL n);

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} = X /\ Y holds

b_{1} is compact
by COMPTS_1:11;

end;
let X, Y be compact Subset of (TOP-REAL n);

coherence

for b

b

definition

ex b_{1} being RealMap of (TOP-REAL 2) st

for p being Point of (TOP-REAL 2) holds b_{1} . p = p `1

for b_{1}, b_{2} being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b_{1} . p = p `1 ) & ( for p being Point of (TOP-REAL 2) holds b_{2} . p = p `1 ) holds

b_{1} = b_{2}

ex b_{1} being RealMap of (TOP-REAL 2) st

for p being Point of (TOP-REAL 2) holds b_{1} . p = p `2

for b_{1}, b_{2} being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b_{1} . p = p `2 ) & ( for p being Point of (TOP-REAL 2) holds b_{2} . p = p `2 ) holds

b_{1} = b_{2}
end;

func proj1 -> RealMap of (TOP-REAL 2) means :Def5: :: PSCOMP_1:def 5

for p being Point of (TOP-REAL 2) holds it . p = p `1 ;

existence for p being Point of (TOP-REAL 2) holds it . p = p `1 ;

ex b

for p being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

func proj2 -> RealMap of (TOP-REAL 2) means :Def6: :: PSCOMP_1:def 6

for p being Point of (TOP-REAL 2) holds it . p = p `2 ;

existence for p being Point of (TOP-REAL 2) holds it . p = p `2 ;

ex b

for p being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines proj1 PSCOMP_1:def 5 :

for b_{1} being RealMap of (TOP-REAL 2) holds

( b_{1} = proj1 iff for p being Point of (TOP-REAL 2) holds b_{1} . p = p `1 );

for b

( b

:: deftheorem Def6 defines proj2 PSCOMP_1:def 6 :

for b_{1} being RealMap of (TOP-REAL 2) holds

( b_{1} = proj2 iff for p being Point of (TOP-REAL 2) holds b_{1} . p = p `2 );

for b

( b

theorem Th18: :: PSCOMP_1:18

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

proof end;

theorem Th19: :: PSCOMP_1:19

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

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 Th20: :: PSCOMP_1:20

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

proof end;

theorem Th21: :: PSCOMP_1:21

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

for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } holds

P is open

proof end;

theorem Th22: :: PSCOMP_1:22

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

for p being Point of (TOP-REAL 2) st p in X holds

(proj1 | X) . p = p `1

proof end;

theorem Th23: :: PSCOMP_1:23

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

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

coherence

lower_bound (proj1 | X) is Real ;

coherence

upper_bound (proj2 | X) is Real ;

coherence

upper_bound (proj1 | X) is Real ;

coherence

lower_bound (proj2 | X) is Real ;

end;
coherence

lower_bound (proj1 | X) is Real ;

coherence

upper_bound (proj2 | X) is Real ;

coherence

upper_bound (proj1 | X) is Real ;

coherence

lower_bound (proj2 | X) is Real ;

:: deftheorem defines W-bound PSCOMP_1:def 7 :

for X being Subset of (TOP-REAL 2) holds W-bound X = lower_bound (proj1 | X);

for X being Subset of (TOP-REAL 2) holds W-bound X = lower_bound (proj1 | X);

:: deftheorem defines N-bound PSCOMP_1:def 8 :

for X being Subset of (TOP-REAL 2) holds N-bound X = upper_bound (proj2 | X);

for X being Subset of (TOP-REAL 2) holds N-bound X = upper_bound (proj2 | X);

:: deftheorem defines E-bound PSCOMP_1:def 9 :

for X being Subset of (TOP-REAL 2) holds E-bound X = upper_bound (proj1 | X);

for X being Subset of (TOP-REAL 2) holds E-bound X = upper_bound (proj1 | X);

:: deftheorem defines S-bound PSCOMP_1:def 10 :

for X being Subset of (TOP-REAL 2) holds S-bound X = lower_bound (proj2 | X);

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

definition

let X be Subset of (TOP-REAL 2);

coherence

|[(W-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;

coherence

|[(W-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;

coherence

|[(E-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;

coherence

|[(E-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;

end;
coherence

|[(W-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;

coherence

|[(W-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;

coherence

|[(E-bound X),(N-bound X)]| is Point of (TOP-REAL 2) ;

coherence

|[(E-bound X),(S-bound X)]| is Point of (TOP-REAL 2) ;

:: deftheorem defines SW-corner PSCOMP_1:def 11 :

for X being Subset of (TOP-REAL 2) holds SW-corner X = |[(W-bound X),(S-bound X)]|;

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

for X being Subset of (TOP-REAL 2) holds NW-corner X = |[(W-bound X),(N-bound X)]|;

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

for X being Subset of (TOP-REAL 2) holds NE-corner X = |[(E-bound X),(N-bound X)]|;

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

for X being Subset of (TOP-REAL 2) holds SE-corner X = |[(E-bound X),(S-bound X)]|;

for X being Subset of (TOP-REAL 2) holds SE-corner X = |[(E-bound X),(S-bound X)]|;

definition

let X be Subset of (TOP-REAL 2);

(LSeg ((SW-corner X),(NW-corner X))) /\ X is Subset of (TOP-REAL 2) ;

(LSeg ((NW-corner X),(NE-corner X))) /\ X is Subset of (TOP-REAL 2) ;

(LSeg ((SE-corner X),(NE-corner X))) /\ X is Subset of (TOP-REAL 2) ;

(LSeg ((SW-corner X),(SE-corner X))) /\ X is Subset of (TOP-REAL 2) ;

end;
func W-most X -> Subset of (TOP-REAL 2) equals :: PSCOMP_1:def 15

(LSeg ((SW-corner X),(NW-corner X))) /\ X;

coherence (LSeg ((SW-corner X),(NW-corner X))) /\ X;

(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 16

(LSeg ((NW-corner X),(NE-corner X))) /\ X;

coherence (LSeg ((NW-corner X),(NE-corner X))) /\ X;

(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 17

(LSeg ((SE-corner X),(NE-corner X))) /\ X;

coherence (LSeg ((SE-corner X),(NE-corner X))) /\ X;

(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 18

(LSeg ((SW-corner X),(SE-corner X))) /\ X;

coherence (LSeg ((SW-corner X),(SE-corner X))) /\ X;

(LSeg ((SW-corner X),(SE-corner X))) /\ X is Subset of (TOP-REAL 2) ;

:: deftheorem defines W-most PSCOMP_1:def 15 :

for X being Subset of (TOP-REAL 2) holds W-most X = (LSeg ((SW-corner X),(NW-corner X))) /\ X;

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

for X being Subset of (TOP-REAL 2) holds N-most X = (LSeg ((NW-corner X),(NE-corner X))) /\ X;

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

for X being Subset of (TOP-REAL 2) holds E-most X = (LSeg ((SE-corner X),(NE-corner X))) /\ X;

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

for X being Subset of (TOP-REAL 2) holds S-most X = (LSeg ((SW-corner X),(SE-corner X))) /\ X;

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

coherence

( not W-most X is empty & W-most X is compact )

( not N-most X is empty & N-most X is compact )

( not E-most X is empty & E-most X is compact )

( not S-most X is empty & S-most X is compact )

end;
coherence

( not W-most X is empty & W-most X is compact )

proof end;

coherence ( not N-most X is empty & N-most X is compact )

proof end;

coherence ( not E-most X is empty & E-most X is compact )

proof end;

coherence ( not S-most X is empty & S-most X is compact )

proof end;

definition

let X be Subset of (TOP-REAL 2);

|[(W-bound X),(lower_bound (proj2 | (W-most X)))]| is Point of (TOP-REAL 2) ;

|[(W-bound X),(upper_bound (proj2 | (W-most X)))]| is Point of (TOP-REAL 2) ;

|[(lower_bound (proj1 | (N-most X))),(N-bound X)]| is Point of (TOP-REAL 2) ;

|[(upper_bound (proj1 | (N-most X))),(N-bound X)]| is Point of (TOP-REAL 2) ;

|[(E-bound X),(upper_bound (proj2 | (E-most X)))]| is Point of (TOP-REAL 2) ;

|[(E-bound X),(lower_bound (proj2 | (E-most X)))]| is Point of (TOP-REAL 2) ;

|[(upper_bound (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2) ;

|[(lower_bound (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2) ;

end;
func W-min X -> Point of (TOP-REAL 2) equals :: PSCOMP_1:def 19

|[(W-bound X),(lower_bound (proj2 | (W-most X)))]|;

coherence |[(W-bound X),(lower_bound (proj2 | (W-most X)))]|;

|[(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 20

|[(W-bound X),(upper_bound (proj2 | (W-most X)))]|;

coherence |[(W-bound X),(upper_bound (proj2 | (W-most X)))]|;

|[(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 21

|[(lower_bound (proj1 | (N-most X))),(N-bound X)]|;

coherence |[(lower_bound (proj1 | (N-most X))),(N-bound X)]|;

|[(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 22

|[(upper_bound (proj1 | (N-most X))),(N-bound X)]|;

coherence |[(upper_bound (proj1 | (N-most X))),(N-bound X)]|;

|[(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 23

|[(E-bound X),(upper_bound (proj2 | (E-most X)))]|;

coherence |[(E-bound X),(upper_bound (proj2 | (E-most X)))]|;

|[(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 24

|[(E-bound X),(lower_bound (proj2 | (E-most X)))]|;

coherence |[(E-bound X),(lower_bound (proj2 | (E-most X)))]|;

|[(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 25

|[(upper_bound (proj1 | (S-most X))),(S-bound X)]|;

coherence |[(upper_bound (proj1 | (S-most X))),(S-bound X)]|;

|[(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 26

|[(lower_bound (proj1 | (S-most X))),(S-bound X)]|;

coherence |[(lower_bound (proj1 | (S-most X))),(S-bound X)]|;

|[(lower_bound (proj1 | (S-most X))),(S-bound X)]| is Point of (TOP-REAL 2) ;

:: deftheorem defines W-min PSCOMP_1:def 19 :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Th29: :: PSCOMP_1:29

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 )

( (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 Th30: :: PSCOMP_1:30

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 )

( (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 Th31: :: PSCOMP_1:31

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

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

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 Th34: :: PSCOMP_1:34

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 )

( W-min X in W-most X & W-max X in W-most X )

proof end;

theorem :: PSCOMP_1:35

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

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

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

W-most X = {(W-min X)}

proof end;

theorem Th37: :: PSCOMP_1:37

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 )

( (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 Th38: :: PSCOMP_1:38

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 )

( (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 Th39: :: PSCOMP_1:39

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

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

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 Th42: :: PSCOMP_1:42

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 )

( N-min X in N-most X & N-max X in N-most X )

proof end;

theorem :: PSCOMP_1:43

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

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

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

N-most X = {(N-min X)}

proof end;

theorem Th45: :: PSCOMP_1:45

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 )

( (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 Th46: :: PSCOMP_1:46

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 )

( (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 Th47: :: PSCOMP_1:47

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

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

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 Th50: :: PSCOMP_1:50

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 )

( E-min X in E-most X & E-max X in E-most X )

proof end;

theorem :: PSCOMP_1:51

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

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

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

E-most X = {(E-min X)}

proof end;

theorem Th53: :: PSCOMP_1:53

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 )

( (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 Th54: :: PSCOMP_1:54

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 )

( (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 Th55: :: PSCOMP_1:55

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

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

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 Th58: :: PSCOMP_1:58

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 )

( S-min X in S-most X & S-max X in S-most X )

proof end;

theorem :: PSCOMP_1:59

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

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

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

S-most X = {(S-min X)}

proof end;

:: Degenerate cases

:: Moved from JORDAN1E, AK, 23.02.2006

theorem :: PSCOMP_1:66

theorem :: PSCOMP_1:67

theorem :: PSCOMP_1:68

theorem :: PSCOMP_1:69