:: PSCOMP_1 semantic presentation
begin
Lm1: for X being Subset of REAL st X is bounded_below holds
-- X is bounded_above
proof
let X be Subset of REAL; ::_thesis: ( X is bounded_below implies -- X is bounded_above )
given s being real number such that A1: s is LowerBound of X ; :: according to XXREAL_2:def_9 ::_thesis: -- X is bounded_above
take - s ; :: according to XXREAL_2:def_10 ::_thesis: - s is UpperBound of -- X
let t be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not t in -- X or t <= - s )
assume t in -- X ; ::_thesis: t <= - s
then t in { (- r2) where r2 is Element of COMPLEX : r2 in X } by MEMBER_1:def_2;
then consider r2 being Element of COMPLEX such that
A2: t = - r2 and
A3: r2 in X ;
reconsider r3 = r2 as Real by A3;
r3 >= s by A1, A3, XXREAL_2:def_2;
hence t <= - s by A2, XREAL_1:24; ::_thesis: verum
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
let X be non empty set ; ::_thesis: for f being Function of X,REAL st f is with_min holds
- f is with_max
let f be Function of X,REAL; ::_thesis: ( f is with_min implies - f is with_max )
assume that
A1: f .: X is bounded_below and
A2: lower_bound (f .: X) in f .: X ; :: according to MEASURE6:def_5,MEASURE6:def_13 ::_thesis: - f is with_max
A3: -- (f .: X) = (- f) .: X by MEASURE6:65;
hence (- f) .: X is bounded_above by A1, Lm1; :: according to MEASURE6:def_4,MEASURE6:def_12 ::_thesis: upper_bound ((- f) .: X) in (- f) .: X
then A4: upper_bound ((- f) .: X) = - (lower_bound (-- (-- (f .: X)))) by A3, MEASURE6:44
.= - (lower_bound (f .: X)) ;
- (lower_bound (f .: X)) in -- (f .: X) by A2, MEMBER_1:11;
hence upper_bound ((- f) .: X) in (- f) .: X by A4, MEASURE6:65; ::_thesis: verum
end;
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 the carrier of T -defined REAL -valued Function-like V29( the carrier of T) V30( the carrier of T, REAL ) complex-valued ext-real-valued real-valued bounded for Element of K32(K33( the carrier of T,REAL));
existence
ex b1 being RealMap of T st b1 is bounded
proof
set c = the carrier of T;
reconsider f = the carrier of T --> 0 as RealMap of T ;
take f ; ::_thesis: f is bounded
( dom f = the carrier of T & rng f = {0} ) by FUNCOP_1:8, FUNCT_2:def_1;
hence f .: the carrier of T is bounded_above by RELAT_1:113; :: according to SEQ_2:def_8,MEASURE6:def_11 ::_thesis: f is bounded_below
thus f .: the carrier of T is bounded_below ; :: according to MEASURE6:def_10 ::_thesis: verum
end;
end;
definition
let T be 1-sorted ;
let f be RealMap of T;
func lower_bound f -> Real equals :: PSCOMP_1:def 1
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 2
upper_bound (f .: the carrier of T);
coherence
upper_bound (f .: the carrier of T) is Real ;
end;
:: 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);
:: 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);
theorem Th1: :: PSCOMP_1:1
for T being non empty TopSpace
for f being V44() RealMap of T
for p being Point of T holds f . p >= lower_bound f
proof
let T be non empty TopSpace; ::_thesis: for f being V44() RealMap of T
for p being Point of T holds f . p >= lower_bound f
let f be V44() RealMap of T; ::_thesis: for p being Point of T holds f . p >= lower_bound f
set fc = f .: the carrier of T;
let p be Point of T; ::_thesis: f . p >= lower_bound f
( f .: the carrier of T is bounded_below & f . p in f .: the carrier of T ) by FUNCT_2:35, MEASURE6:def_10;
hence f . p >= lower_bound f by SEQ_4:def_2; ::_thesis: verum
end;
theorem :: PSCOMP_1:2
for T being non empty TopSpace
for f being V44() RealMap of T
for s being Real st ( for t being Point of T holds f . t >= s ) holds
lower_bound f >= s
proof
let T be non empty TopSpace; ::_thesis: for f being V44() RealMap of T
for s being Real st ( for t being Point of T holds f . t >= s ) holds
lower_bound f >= s
let f be V44() RealMap of T; ::_thesis: for s being Real st ( for t being Point of T holds f . t >= s ) holds
lower_bound f >= s
set c = the carrier of T;
set fc = f .: the carrier of T;
let s be Real; ::_thesis: ( ( for t being Point of T holds f . t >= s ) implies lower_bound f >= s )
assume A1: for t being Point of T holds f . t >= s ; ::_thesis: lower_bound f >= s
now__::_thesis:_for_p1_being_real_number_st_p1_in_f_.:_the_carrier_of_T_holds_
p1_>=_s
let p1 be real number ; ::_thesis: ( p1 in f .: the carrier of T implies p1 >= s )
assume p1 in f .: the carrier of T ; ::_thesis: p1 >= s
then ex x being set st
( x in the carrier of T & x in the carrier of T & p1 = f . x ) by FUNCT_2:64;
hence p1 >= s by A1; ::_thesis: verum
end;
hence lower_bound f >= s by SEQ_4:43; ::_thesis: verum
end;
theorem :: PSCOMP_1:3
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
let r be real number ; ::_thesis: 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
let T be non empty TopSpace; ::_thesis: 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
let f be RealMap of T; ::_thesis: ( ( 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 ) implies r = lower_bound f )
set c = the carrier of T;
set fc = f .: the carrier of T;
assume that
A1: for p being Point of T holds f . p >= r and
A2: for t being real number st ( for p being Point of T holds f . p >= t ) holds
r >= t ; ::_thesis: r = lower_bound f
A3: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_f_.:_the_carrier_of_T_holds_
s_>=_t_)_holds_
r_>=_t
let t be real number ; ::_thesis: ( ( for s being real number st s in f .: the carrier of T holds
s >= t ) implies r >= t )
assume for s being real number st s in f .: the carrier of T holds
s >= t ; ::_thesis: r >= t
then for s being Point of T holds f . s >= t by FUNCT_2:35;
hence r >= t by A2; ::_thesis: verum
end;
now__::_thesis:_for_s_being_real_number_st_s_in_f_.:_the_carrier_of_T_holds_
s_>=_r
let s be real number ; ::_thesis: ( s in f .: the carrier of T implies s >= r )
assume s in f .: the carrier of T ; ::_thesis: s >= r
then ex x being set st
( x in the carrier of T & x in the carrier of T & s = f . x ) by FUNCT_2:64;
hence s >= r by A1; ::_thesis: verum
end;
hence r = lower_bound f by A3, SEQ_4:44; ::_thesis: verum
end;
theorem Th4: :: PSCOMP_1:4
for T being non empty TopSpace
for f being V43() RealMap of T
for p being Point of T holds f . p <= upper_bound f
proof
let T be non empty TopSpace; ::_thesis: for f being V43() RealMap of T
for p being Point of T holds f . p <= upper_bound f
let f be V43() RealMap of T; ::_thesis: for p being Point of T holds f . p <= upper_bound f
set fc = f .: the carrier of T;
let p be Point of T; ::_thesis: f . p <= upper_bound f
( f .: the carrier of T is bounded_above & f . p in f .: the carrier of T ) by FUNCT_2:35, MEASURE6:def_11;
hence f . p <= upper_bound f by SEQ_4:def_1; ::_thesis: verum
end;
theorem :: PSCOMP_1:5
for T being non empty TopSpace
for f being V43() 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
let T be non empty TopSpace; ::_thesis: for f being V43() RealMap of T
for t being real number st ( for p being Point of T holds f . p <= t ) holds
upper_bound f <= t
let f be V43() RealMap of T; ::_thesis: for t being real number st ( for p being Point of T holds f . p <= t ) holds
upper_bound f <= t
set c = the carrier of T;
set fc = f .: the carrier of T;
let t be real number ; ::_thesis: ( ( for p being Point of T holds f . p <= t ) implies upper_bound f <= t )
assume A1: for p being Point of T holds f . p <= t ; ::_thesis: upper_bound f <= t
now__::_thesis:_for_s_being_real_number_st_s_in_f_.:_the_carrier_of_T_holds_
s_<=_t
let s be real number ; ::_thesis: ( s in f .: the carrier of T implies s <= t )
assume s in f .: the carrier of T ; ::_thesis: s <= t
then ex x being set st
( x in the carrier of T & x in the carrier of T & s = f . x ) by FUNCT_2:64;
hence s <= t by A1; ::_thesis: verum
end;
hence upper_bound f <= t by SEQ_4:45; ::_thesis: verum
end;
theorem :: PSCOMP_1:6
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
let r be real number ; ::_thesis: 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
let T be non empty TopSpace; ::_thesis: 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
let f be RealMap of T; ::_thesis: ( ( 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 ) implies r = upper_bound f )
set c = the carrier of T;
set fc = f .: the carrier of T;
assume that
A1: for p being Point of T holds f . p <= r and
A2: for t being real number st ( for p being Point of T holds f . p <= t ) holds
r <= t ; ::_thesis: r = upper_bound f
A3: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_f_.:_the_carrier_of_T_holds_
s_<=_t_)_holds_
r_<=_t
let t be real number ; ::_thesis: ( ( for s being real number st s in f .: the carrier of T holds
s <= t ) implies r <= t )
assume for s being real number st s in f .: the carrier of T holds
s <= t ; ::_thesis: r <= t
then for s being Point of T holds f . s <= t by FUNCT_2:35;
hence r <= t by A2; ::_thesis: verum
end;
now__::_thesis:_for_s_being_real_number_st_s_in_f_.:_the_carrier_of_T_holds_
s_<=_r
let s be real number ; ::_thesis: ( s in f .: the carrier of T implies s <= r )
assume s in f .: the carrier of T ; ::_thesis: s <= r
then ex x being set st
( x in the carrier of T & x in the carrier of T & s = f . x ) by FUNCT_2:64;
hence s <= r by A1; ::_thesis: verum
end;
hence r = upper_bound f by A3, SEQ_4:46; ::_thesis: verum
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
proof
let T be non empty 1-sorted ; ::_thesis: for f being bounded RealMap of T holds lower_bound f <= upper_bound f
let f be bounded RealMap of T; ::_thesis: lower_bound f <= upper_bound f
( f .: the carrier of T is bounded_below & f .: the carrier of T is bounded_above ) by MEASURE6:def_10, MEASURE6:def_11;
hence lower_bound f <= upper_bound f by SEQ_4:11; ::_thesis: verum
end;
definition
let T be TopStruct ;
let f be RealMap of T;
attrf is continuous means :Def3: :: PSCOMP_1:def 3
for Y being Subset of REAL st Y is closed holds
f " Y is closed ;
end;
:: deftheorem Def3 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 );
registration
let T be non empty TopSpace;
cluster non empty Relation-like the carrier of T -defined REAL -valued Function-like V29( the carrier of T) V30( the carrier of T, REAL ) complex-valued ext-real-valued real-valued continuous for Element of K32(K33( the carrier of T,REAL));
existence
ex b1 being RealMap of T st b1 is continuous
proof
set c = the carrier of T;
reconsider f = the carrier of T --> 0 as RealMap of T ;
take f ; ::_thesis: f is continuous
A1: dom f = the carrier of T by FUNCT_2:def_1;
let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( Y is closed implies f " Y is closed )
A2: rng f = {0} by FUNCOP_1:8;
assume Y is closed ; ::_thesis: f " Y is closed
percases ( 0 in Y or not 0 in Y ) ;
suppose 0 in Y ; ::_thesis: f " Y is closed
then A3: rng f c= Y by A2, ZFMISC_1:31;
f " Y = f " ((rng f) /\ Y) by RELAT_1:133
.= f " (rng f) by A3, XBOOLE_1:28
.= [#] T by A1, RELAT_1:134 ;
hence f " Y is closed ; ::_thesis: verum
end;
suppose not 0 in Y ; ::_thesis: f " Y is closed
then A4: rng f misses Y by A2, ZFMISC_1:50;
f " Y = f " ((rng f) /\ Y) by RELAT_1:133
.= f " {} by A4, XBOOLE_0:def_7
.= {} T ;
hence f " Y is closed ; ::_thesis: verum
end;
end;
end;
end;
registration
let T be non empty TopSpace;
let S be non empty SubSpace of T;
cluster non empty Relation-like the carrier of S -defined REAL -valued Function-like V29( the carrier of S) V30( the carrier of S, REAL ) complex-valued ext-real-valued real-valued continuous for Element of K32(K33( the carrier of S,REAL));
existence
ex b1 being RealMap of S st b1 is continuous
proof
set c = the carrier of S;
reconsider f = the carrier of S --> 0 as RealMap of S ;
take f ; ::_thesis: f is continuous
A1: dom f = the carrier of S by FUNCT_2:def_1;
let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( Y is closed implies f " Y is closed )
A2: rng f = {0} by FUNCOP_1:8;
assume Y is closed ; ::_thesis: f " Y is closed
percases ( 0 in Y or not 0 in Y ) ;
suppose 0 in Y ; ::_thesis: f " Y is closed
then A3: rng f c= Y by A2, ZFMISC_1:31;
f " Y = f " ((rng f) /\ Y) by RELAT_1:133
.= f " (rng f) by A3, XBOOLE_1:28
.= [#] S by A1, RELAT_1:134 ;
hence f " Y is closed ; ::_thesis: verum
end;
suppose not 0 in Y ; ::_thesis: f " Y is closed
then A4: rng f misses Y by A2, ZFMISC_1:50;
f " Y = f " ((rng f) /\ Y) by RELAT_1:133
.= f " {} by A4, XBOOLE_0:def_7
.= {} S ;
hence f " Y is closed ; ::_thesis: verum
end;
end;
end;
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 )
proof
let T be TopStruct ; ::_thesis: 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 )
let f be RealMap of T; ::_thesis: ( f is continuous iff for Y being Subset of REAL st Y is open holds
f " Y is open )
hereby ::_thesis: ( ( for Y being Subset of REAL st Y is open holds
f " Y is open ) implies f is continuous )
assume A1: f is continuous ; ::_thesis: for Y being Subset of REAL st Y is open holds
f " Y is open
let Y be Subset of REAL; ::_thesis: ( Y is open implies f " Y is open )
assume Y is open ; ::_thesis: f " Y is open
then Y ` is closed by RCOMP_1:def_5;
then A2: f " (Y `) is closed by A1, Def3;
f " (Y `) = (f " REAL) \ (f " Y) by FUNCT_1:69
.= ([#] T) \ (f " Y) by FUNCT_2:40 ;
then ([#] T) \ (([#] T) \ (f " Y)) is open by A2, PRE_TOPC:def_3;
hence f " Y is open by PRE_TOPC:3; ::_thesis: verum
end;
assume A3: for Y being Subset of REAL st Y is open holds
f " Y is open ; ::_thesis: f is continuous
let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( Y is closed implies f " Y is closed )
A4: Y = (Y `) ` ;
assume Y is closed ; ::_thesis: f " Y is closed
then Y ` is open by A4, RCOMP_1:def_5;
then A5: f " (Y `) is open by A3;
f " (Y `) = (f " REAL) \ (f " Y) by FUNCT_1:69
.= ([#] T) \ (f " Y) by FUNCT_2:40 ;
hence f " Y is closed by A5, PRE_TOPC:def_3; ::_thesis: verum
end;
theorem Th9: :: PSCOMP_1:9
for T being TopStruct
for f being RealMap of T st f is continuous holds
- f is continuous
proof
let T be TopStruct ; ::_thesis: for f being RealMap of T st f is continuous holds
- f is continuous
let f be RealMap of T; ::_thesis: ( f is continuous implies - f is continuous )
assume A1: f is continuous ; ::_thesis: - f is continuous
let X be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( X is closed implies (- f) " X is closed )
assume X is closed ; ::_thesis: (- f) " X is closed
then A2: -- X is closed by MEASURE6:45;
(- f) " X = f " (-- X) by MEASURE6:68;
hence (- f) " X is closed by A1, A2, Def3; ::_thesis: verum
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
proof
let r3 be Real; ::_thesis: for T being TopStruct
for f being RealMap of T st f is continuous holds
r3 + f is continuous
let T be TopStruct ; ::_thesis: for f being RealMap of T st f is continuous holds
r3 + f is continuous
let f be RealMap of T; ::_thesis: ( f is continuous implies r3 + f is continuous )
assume A1: f is continuous ; ::_thesis: r3 + f is continuous
let X be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( X is closed implies (r3 + f) " X is closed )
assume X is closed ; ::_thesis: (r3 + f) " X is closed
then A2: (- r3) ++ X is closed by MEASURE6:53;
(r3 + f) " X = f " ((- r3) ++ X) by MEASURE6:70;
hence (r3 + f) " X is closed by A1, A2, Def3; ::_thesis: verum
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
proof
let T be TopStruct ; ::_thesis: for f being RealMap of T st f is continuous & not 0 in rng f holds
Inv f is continuous
let f be RealMap of T; ::_thesis: ( f is continuous & not 0 in rng f implies Inv f is continuous )
assume that
A1: f is continuous and
A2: not 0 in rng f ; ::_thesis: Inv f is continuous
let X0 be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( X0 is closed implies (Inv f) " X0 is closed )
0 in {0} by TARSKI:def_1;
then not 0 in X0 \ {0} by XBOOLE_0:def_5;
then reconsider X = X0 \ {0} as without_zero Subset of REAL by MEASURE6:def_2;
set X9 = Inv X;
A3: X0 \ {0} c= X0 by XBOOLE_1:36;
set X9r = (Inv X) /\ (rng f);
assume A4: X0 is closed ; ::_thesis: (Inv f) " X0 is closed
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(Inv_X)_/\_(rng_f)_implies_x_in_(Cl_((Inv_X)_/\_(rng_f)))_/\_(rng_f)_)_&_(_x_in_(Cl_((Inv_X)_/\_(rng_f)))_/\_(rng_f)_implies_x_in_(Inv_X)_/\_(rng_f)_)_)
let x be set ; ::_thesis: ( ( x in (Inv X) /\ (rng f) implies x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) ) & ( x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) implies x in (Inv X) /\ (rng f) ) )
hereby ::_thesis: ( x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) implies x in (Inv X) /\ (rng f) )
A5: (Inv X) /\ (rng f) c= Cl ((Inv X) /\ (rng f)) by MEASURE6:58;
assume A6: x in (Inv X) /\ (rng f) ; ::_thesis: x in (Cl ((Inv X) /\ (rng f))) /\ (rng f)
then x in rng f by XBOOLE_0:def_4;
hence x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) by A6, A5, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A7: x in (Cl ((Inv X) /\ (rng f))) /\ (rng f) ; ::_thesis: x in (Inv X) /\ (rng f)
then reconsider s = x as Real ;
x in Cl ((Inv X) /\ (rng f)) by A7, XBOOLE_0:def_4;
then consider seq being Real_Sequence such that
A8: rng seq c= (Inv X) /\ (rng f) and
A9: seq is convergent and
A10: lim seq = s by MEASURE6:64;
assume A11: not x in (Inv X) /\ (rng f) ; ::_thesis: contradiction
A12: x in rng f by A7, XBOOLE_0:def_4;
now__::_thesis:_not_lim_seq_<>_0
rng (seq ") c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (seq ") or y in X )
assume y in rng (seq ") ; ::_thesis: y in X
then consider n being set such that
A13: n in dom (seq ") and
A14: y = (seq ") . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A13;
seq . n in rng seq by FUNCT_2:4;
then A15: 1 / (1 / (seq . n)) in Inv X by A8, XBOOLE_0:def_4;
(seq ") . n = (seq . n) " by VALUED_1:10
.= 1 / (seq . n) ;
hence y in X by A14, A15, MEASURE6:54; ::_thesis: verum
end;
then A16: rng (seq ") c= X0 by A3, XBOOLE_1:1;
assume A17: lim seq <> 0 ; ::_thesis: contradiction
now__::_thesis:_for_n_being_Element_of_NAT_holds_not_seq_._n_=_0
let n be Element of NAT ; ::_thesis: not seq . n = 0
assume seq . n = 0 ; ::_thesis: contradiction
then 0 in rng seq by FUNCT_2:4;
hence contradiction by A2, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
then A18: seq is non-zero by SEQ_1:5;
then seq " is convergent by A9, A17, SEQ_2:21;
then A19: lim (seq ") in X0 by A4, A16, RCOMP_1:def_4;
A20: lim (seq ") = (lim seq) " by A9, A17, A18, SEQ_2:22;
then lim (seq ") <> 0 by A17, XCMPLX_1:202;
then not lim (seq ") in {0} by TARSKI:def_1;
then lim (seq ") in X by A19, XBOOLE_0:def_5;
then 1 / (lim (seq ")) in Inv X ;
hence contradiction by A12, A10, A11, A20, XBOOLE_0:def_4; ::_thesis: verum
end;
hence contradiction by A2, A7, A10, XBOOLE_0:def_4; ::_thesis: verum
end;
then A21: (Inv X) /\ (rng f) = (Cl ((Inv X) /\ (rng f))) /\ (rng f) by TARSKI:1;
f " (Cl ((Inv X) /\ (rng f))) is closed by A1, Def3;
then A22: f " ((Inv X) /\ (rng f)) is closed by A21, RELAT_1:133;
A23: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(Inv_f)_"_X0_implies_x_in_(Inv_f)_"_X_)_&_(_x_in_(Inv_f)_"_X_implies_x_in_(Inv_f)_"_X0_)_)
let x be set ; ::_thesis: ( ( x in (Inv f) " X0 implies x in (Inv f) " X ) & ( x in (Inv f) " X implies x in (Inv f) " X0 ) )
hereby ::_thesis: ( x in (Inv f) " X implies x in (Inv f) " X0 )
assume A24: x in (Inv f) " X0 ; ::_thesis: x in (Inv f) " X
then A25: (Inv f) . x in X0 by FUNCT_2:38;
now__::_thesis:_(Inv_f)_._x_in_X
assume not (Inv f) . x in X ; ::_thesis: contradiction
then (Inv f) . x in {0} by A25, XBOOLE_0:def_5;
then (Inv f) . x = 0 by TARSKI:def_1;
then 0 = (f . x) " by VALUED_1:10;
hence contradiction by A2, A24, FUNCT_2:4, XCMPLX_1:202; ::_thesis: verum
end;
hence x in (Inv f) " X by A24, FUNCT_2:38; ::_thesis: verum
end;
(Inv f) " X c= (Inv f) " X0 by RELAT_1:143, XBOOLE_1:36;
hence ( x in (Inv f) " X implies x in (Inv f) " X0 ) ; ::_thesis: verum
end;
( f " (Inv X) = f " ((Inv X) /\ (rng f)) & (Inv f) " X = f " (Inv X) ) by MEASURE6:71, RELAT_1:133;
hence (Inv f) " X0 is closed by A22, A23, TARSKI:1; ::_thesis: verum
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
proof
let T be TopStruct ; ::_thesis: 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
let f be RealMap of T; ::_thesis: for R being Subset-Family of REAL st f is continuous & R is open holds
(" f) .: R is open
let R be Subset-Family of REAL; ::_thesis: ( f is continuous & R is open implies (" f) .: R is open )
assume A1: f is continuous ; ::_thesis: ( not R is open or (" f) .: R is open )
assume A2: R is open ; ::_thesis: (" f) .: R is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in (" f) .: R or P is open )
assume P in (" f) .: R ; ::_thesis: P is open
then consider eR being set such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = (" f) . eR by FUNCT_2:64;
A6: P = f " eR by A3, A5, MEASURE6:def_3;
reconsider eR = eR as Subset of REAL by A3;
eR is open by A2, A4, MEASURE6:def_6;
hence P is open by A1, A6, Th8; ::_thesis: verum
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
proof
let T be TopStruct ; ::_thesis: 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
let f be RealMap of T; ::_thesis: for R being Subset-Family of REAL st f is continuous & R is closed holds
(" f) .: R is closed
let R be Subset-Family of REAL; ::_thesis: ( f is continuous & R is closed implies (" f) .: R is closed )
assume A1: f is continuous ; ::_thesis: ( not R is closed or (" f) .: R is closed )
assume A2: R is closed ; ::_thesis: (" f) .: R is closed
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in (" f) .: R or P is closed )
assume P in (" f) .: R ; ::_thesis: P is closed
then consider eR being set such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = (" f) . eR by FUNCT_2:64;
A6: P = f " eR by A3, A5, MEASURE6:def_3;
reconsider eR = eR as Subset of REAL by A3;
eR is closed by A2, A4, MEASURE6:def_7;
hence P is closed by A1, A6, Def3; ::_thesis: verum
end;
definition
let T be non empty TopStruct ;
let f be RealMap of T;
let X be Subset of T;
:: original: |
redefine funcf | X -> RealMap of (T | X);
coherence
f | X is RealMap of (T | X)
proof
the carrier of (T | X) = X by PRE_TOPC:8;
hence f | X is RealMap of (T | X) by FUNCT_2:32; ::_thesis: verum
end;
end;
registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let X be Subset of T;
clusterf | X -> continuous for RealMap of (T | X);
coherence
for b1 being RealMap of (T | X) st b1 = f | X holds
b1 is continuous
proof
now__::_thesis:_for_Y_being_Subset_of_REAL_st_Y_is_open_holds_
(f_|_X)_"_Y_is_open
let Y be Subset of REAL; ::_thesis: ( Y is open implies (f | X) " Y is open )
assume Y is open ; ::_thesis: (f | X) " Y is open
then A1: f " Y is open by Th8;
( the carrier of (T | X) = X & (f | X) " Y = X /\ (f " Y) ) by FUNCT_1:70, PRE_TOPC:8;
hence (f | X) " Y is open by A1, TSP_1:def_1; ::_thesis: verum
end;
hence for b1 being RealMap of (T | X) st b1 = f | X holds
b1 is continuous by Th8; ::_thesis: verum
end;
end;
registration
let T be non empty TopSpace;
let P be non empty compact Subset of T;
clusterT | P -> compact ;
coherence
T | P is compact by COMPTS_1:3;
end;
begin
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 )
proof
let T be non empty TopSpace; ::_thesis: ( ( 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 )
hereby ::_thesis: ( ( for f being RealMap of T st f is continuous holds
f is with_min ) implies for f being RealMap of T st f is continuous holds
f is with_max )
assume A1: for f being RealMap of T st f is continuous holds
f is with_max ; ::_thesis: for f being RealMap of T st f is continuous holds
f is with_min
let f be RealMap of T; ::_thesis: ( f is continuous implies f is with_min )
assume f is continuous ; ::_thesis: f is with_min
then - f is continuous by Th9;
then - f is with_max by A1;
hence f is with_min by MEASURE6:66; ::_thesis: verum
end;
assume A2: for f being RealMap of T st f is continuous holds
f is with_min ; ::_thesis: for f being RealMap of T st f is continuous holds
f is with_max
let f be RealMap of T; ::_thesis: ( f is continuous implies f is with_max )
assume f is continuous ; ::_thesis: f is with_max
then - f is continuous by Th9;
then - (- f) is with_max by A2, Lm2;
hence f is with_max ; ::_thesis: verum
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 )
proof
let T be non empty TopSpace; ::_thesis: ( ( 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 )
set cT = the carrier of T;
hereby ::_thesis: ( ( for f being RealMap of T st f is continuous holds
f is with_max ) implies for f being RealMap of T st f is continuous holds
f is bounded )
assume A1: for f being RealMap of T st f is continuous holds
f is bounded ; ::_thesis: for f being RealMap of T st f is continuous holds
f is with_max
let f be RealMap of T; ::_thesis: ( f is continuous implies f is with_max )
assume A2: f is continuous ; ::_thesis: f is with_max
set fcT = f .: the carrier of T;
f is bounded by A1, A2;
then A3: f .: the carrier of T is bounded_above by MEASURE6:def_11;
set b = upper_bound (f .: the carrier of T);
set bf = (upper_bound (f .: the carrier of T)) + (- f);
- f is continuous by A2, Th9;
then A4: (upper_bound (f .: the carrier of T)) + (- f) is continuous by Th10;
reconsider bf9 = (upper_bound (f .: the carrier of T)) + (- f) as Function of the carrier of T,REAL ;
reconsider f9 = f as Function of the carrier of T,REAL ;
set g = Inv ((upper_bound (f .: the carrier of T)) + (- f));
set gcT = (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T;
assume not f is with_max ; ::_thesis: contradiction
then A5: not f .: the carrier of T is with_max by MEASURE6:def_12;
then A6: not upper_bound (f .: the carrier of T) in f .: the carrier of T by A3, MEASURE6:def_4;
now__::_thesis:_not_0_in_rng_((upper_bound_(f_.:_the_carrier_of_T))_+_(-_f))
assume 0 in rng ((upper_bound (f .: the carrier of T)) + (- f)) ; ::_thesis: contradiction
then consider x being set such that
A7: x in dom ((upper_bound (f .: the carrier of T)) + (- f)) and
A8: ((upper_bound (f .: the carrier of T)) + (- f)) . x = 0 by FUNCT_1:def_3;
reconsider x = x as Element of the carrier of T by A7;
bf9 . x = (upper_bound (f .: the carrier of T)) + ((- f9) . x) by VALUED_1:2
.= (upper_bound (f .: the carrier of T)) + (- (f . x)) by VALUED_1:8
.= (upper_bound (f .: the carrier of T)) - (f . x) ;
hence contradiction by A6, A8, FUNCT_2:35; ::_thesis: verum
end;
then A9: Inv ((upper_bound (f .: the carrier of T)) + (- f)) is continuous by A4, Th11;
now__::_thesis:_ex_a19_being_real_number_st_
(_a19_>_0_&_(_for_r_being_real_number_st_r_in_(Inv_((upper_bound_(f_.:_the_carrier_of_T))_+_(-_f)))_.:_the_carrier_of_T_holds_
r_<=_a19_)_)
Inv ((upper_bound (f .: the carrier of T)) + (- f)) is bounded by A1, A9;
then (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T is bounded_above by MEASURE6:def_11;
then consider p being real number such that
A10: p is UpperBound of (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T by XXREAL_2:def_10;
A11: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by A10, XXREAL_2:def_1;
percases ( p <= 0 or p > 0 ) ;
supposeA12: p <= 0 ; ::_thesis: ex a19 being real number st
( a19 > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19 ) )
reconsider a19 = 1 as real number ;
take a19 = a19; ::_thesis: ( a19 > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19 ) )
thus a19 > 0 ; ::_thesis: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19
let r be real number ; ::_thesis: ( r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T implies r <= a19 )
assume r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T ; ::_thesis: r <= a19
hence r <= a19 by A11, A12; ::_thesis: verum
end;
supposeA13: p > 0 ; ::_thesis: ex p being real number st
( p > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )
take p = p; ::_thesis: ( p > 0 & ( for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )
thus p > 0 by A13; ::_thesis: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p
thus for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by A11; ::_thesis: verum
end;
end;
end;
then consider p being real number such that
A14: p > 0 and
A15: for r being real number st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ;
consider r being real number such that
A16: r in f .: the carrier of T and
A17: (upper_bound (f .: the carrier of T)) - (1 / p) < r by A3, A14, SEQ_4:def_1;
consider x being set such that
A18: x in the carrier of T and
x in the carrier of T and
A19: r = f . x by A16, FUNCT_2:64;
reconsider x = x as Element of T by A18;
A20: f . x <= upper_bound (f .: the carrier of T) by A3, A16, A19, SEQ_4:def_1;
f . x <> upper_bound (f .: the carrier of T) by A3, A5, A16, A19, MEASURE6:def_4;
then (f . x) + 0 < upper_bound (f .: the carrier of T) by A20, XXREAL_0:1;
then A21: (upper_bound (f .: the carrier of T)) - (f . x) > 0 by XREAL_1:20;
(Inv ((upper_bound (f .: the carrier of T)) + (- f))) . x = (bf9 . x) " by VALUED_1:10
.= ((upper_bound (f .: the carrier of T)) + ((- f9) . x)) " by VALUED_1:2
.= 1 / ((upper_bound (f .: the carrier of T)) + ((- f9) . x))
.= 1 / ((upper_bound (f .: the carrier of T)) + (- (f . x))) by VALUED_1:8
.= 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) ;
then 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) <= p by A15, FUNCT_2:35;
then 1 <= p * ((upper_bound (f .: the carrier of T)) - (f . x)) by A21, XREAL_1:81;
then 1 / p <= (upper_bound (f .: the carrier of T)) - (f . x) by A14, XREAL_1:79;
then (f . x) + (1 / p) <= upper_bound (f .: the carrier of T) by XREAL_1:19;
hence contradiction by A17, A19, XREAL_1:19; ::_thesis: verum
end;
assume A22: for f being RealMap of T st f is continuous holds
f is with_max ; ::_thesis: for f being RealMap of T st f is continuous holds
f is bounded
let f be RealMap of T; ::_thesis: ( f is continuous implies f is bounded )
assume A23: f is continuous ; ::_thesis: f is bounded
then f is with_max by A22;
then f .: the carrier of T is with_max by MEASURE6:def_12;
then f .: the carrier of T is bounded_above ;
hence f is V43() by MEASURE6:def_11; :: according to SEQ_2:def_8 ::_thesis: f is bounded_below
f is with_min by A22, A23, Th14;
then f .: the carrier of T is with_min by MEASURE6:def_13;
then f .: the carrier of T is bounded_below ;
hence f is bounded_below by MEASURE6:def_10; ::_thesis: verum
end;
definition
let T be TopStruct ;
attrT is pseudocompact means :Def4: :: PSCOMP_1:def 4
for f being RealMap of T st f is continuous holds
f is bounded ;
end;
:: 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 );
registration
cluster non empty TopSpace-like compact -> non empty pseudocompact for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is compact holds
b1 is pseudocompact
proof
let T be non empty TopSpace; ::_thesis: ( T is compact implies T is pseudocompact )
assume A1: T is compact ; ::_thesis: T is pseudocompact
let f be RealMap of T; :: according to PSCOMP_1:def_4 ::_thesis: ( f is continuous implies f is bounded )
assume A2: f is continuous ; ::_thesis: f is bounded
thus f is V43() :: according to SEQ_2:def_8 ::_thesis: f is bounded_below
proof
set p = the Element of T;
defpred S1[ Real] means c1 >= f . the Element of T;
set R = { (right_closed_halfline r3) where r3 is Real : S1[r3] } ;
A3: { (right_closed_halfline r3) where r3 is Real : S1[r3] } is Subset-Family of REAL from DOMAIN_1:sch_8();
A4: right_closed_halfline (f . the Element of T) in { (right_closed_halfline r3) where r3 is Real : S1[r3] } ;
then reconsider R = { (right_closed_halfline r3) where r3 is Real : S1[r3] } as non empty Subset-Family of REAL by A3;
reconsider F = (" f) .: R as Subset-Family of T ;
A5: F is c=-linear
proof
let X, Y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not X in F or not Y in F or X,Y are_c=-comparable )
assume X in F ; ::_thesis: ( not Y in F or X,Y are_c=-comparable )
then consider A being set such that
A6: A in bool REAL and
A7: A in R and
A8: X = (" f) . A by FUNCT_2:64;
A9: X = f " A by A6, A8, MEASURE6:def_3;
consider r1 being Real such that
A10: A = right_closed_halfline r1 and
r1 >= f . the Element of T by A7;
assume Y in F ; ::_thesis: X,Y are_c=-comparable
then consider B being set such that
A11: B in bool REAL and
A12: B in R and
A13: Y = (" f) . B by FUNCT_2:64;
A14: Y = f " B by A11, A13, MEASURE6:def_3;
consider r2 being Real such that
A15: B = right_closed_halfline r2 and
r2 >= f . the Element of T by A12;
( r1 >= r2 or r2 >= r1 ) ;
then ( X c= Y or Y c= X ) by A10, A15, A9, A14, RELAT_1:143, XXREAL_1:38;
hence X,Y are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
assume A16: for s being real number holds s is not UpperBound of f .: the carrier of T ; :: according to XXREAL_2:def_10,MEASURE6:def_11 ::_thesis: contradiction
now__::_thesis:_not_{}_in_F
assume {} in F ; ::_thesis: contradiction
then consider rchx being set such that
A17: rchx in bool REAL and
A18: rchx in R and
A19: {} = (" f) . rchx by FUNCT_2:64;
consider r3 being Real such that
A20: rchx = right_closed_halfline r3 and
r3 >= f . the Element of T by A18;
r3 is not UpperBound of f .: the carrier of T by A16;
then consider r1 being ext-real number such that
A21: r1 in f .: the carrier of T and
A22: r1 > r3 by XXREAL_2:def_1;
rchx = { g where g is Real : g >= r3 } by A20, XXREAL_1:232;
then A23: r1 in rchx by A21, A22;
A24: ex c being set st
( c in the carrier of T & c in the carrier of T & r1 = f . c ) by A21, FUNCT_2:64;
{} = f " rchx by A17, A19, MEASURE6:def_3;
hence contradiction by A24, A23, FUNCT_2:38; ::_thesis: verum
end;
then A25: F is with_non-empty_elements by SETFAM_1:def_8;
R is closed
proof
let X be Subset of REAL; :: according to MEASURE6:def_7 ::_thesis: ( not X in R or X is closed )
assume X in R ; ::_thesis: X is closed
then ex r3 being Real st
( X = right_closed_halfline r3 & r3 >= f . the Element of T ) ;
hence X is closed ; ::_thesis: verum
end;
then A26: F is closed by A2, Th13;
(" f) . (right_closed_halfline (f . the Element of T)) in F by A4, FUNCT_2:35;
then meet F <> {} by A1, A25, A5, A26, COMPTS_1:4;
then consider x being set such that
A27: x in meet F by XBOOLE_0:def_1;
set eR = the Element of R;
the Element of R in R ;
then consider er being Real such that
A28: the Element of R = right_closed_halfline er and
A29: er >= f . the Element of T ;
reconsider x = x as Element of T by A27;
A30: f . x in meet R by A27, MEASURE6:35;
then A31: f . x in the Element of R by SETFAM_1:def_1;
consider fx9 being real number such that
A32: fx9 > f . x by XREAL_1:1;
reconsider fx9 = fx9 as Real by XREAL_0:def_1;
right_closed_halfline er = { r3 where r3 is Real : r3 >= er } by XXREAL_1:232;
then ex r1 being Real st
( f . x = r1 & r1 >= er ) by A31, A28;
then f . x >= f . the Element of T by A29, XXREAL_0:2;
then fx9 >= f . the Element of T by A32, XXREAL_0:2;
then right_closed_halfline fx9 in R ;
then A33: f . x in right_closed_halfline fx9 by A30, SETFAM_1:def_1;
right_closed_halfline fx9 = { r3 where r3 is Real : r3 >= fx9 } by XXREAL_1:232;
then ex r3 being Real st
( f . x = r3 & r3 >= fx9 ) by A33;
hence contradiction by A32; ::_thesis: verum
end;
set p = the Element of T;
defpred S1[ Real] means c1 <= f . the Element of T;
set R = { (left_closed_halfline r3) where r3 is Real : S1[r3] } ;
A34: { (left_closed_halfline r3) where r3 is Real : S1[r3] } is Subset-Family of REAL from DOMAIN_1:sch_8();
A35: left_closed_halfline (f . the Element of T) in { (left_closed_halfline r3) where r3 is Real : S1[r3] } ;
then reconsider R = { (left_closed_halfline r3) where r3 is Real : S1[r3] } as non empty Subset-Family of REAL by A34;
reconsider F = (" f) .: R as Subset-Family of T ;
R is closed
proof
let X be Subset of REAL; :: according to MEASURE6:def_7 ::_thesis: ( not X in R or X is closed )
assume X in R ; ::_thesis: X is closed
then ex r3 being Real st
( X = left_closed_halfline r3 & r3 <= f . the Element of T ) ;
hence X is closed ; ::_thesis: verum
end;
then A36: F is closed by A2, Th13;
A37: F is c=-linear
proof
let X, Y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not X in F or not Y in F or X,Y are_c=-comparable )
assume X in F ; ::_thesis: ( not Y in F or X,Y are_c=-comparable )
then consider A being set such that
A38: A in bool REAL and
A39: A in R and
A40: X = (" f) . A by FUNCT_2:64;
A41: X = f " A by A38, A40, MEASURE6:def_3;
consider r1 being Real such that
A42: A = left_closed_halfline r1 and
r1 <= f . the Element of T by A39;
assume Y in F ; ::_thesis: X,Y are_c=-comparable
then consider B being set such that
A43: B in bool REAL and
A44: B in R and
A45: Y = (" f) . B by FUNCT_2:64;
A46: Y = f " B by A43, A45, MEASURE6:def_3;
consider r2 being Real such that
A47: B = left_closed_halfline r2 and
r2 <= f . the Element of T by A44;
( r1 <= r2 or r2 <= r1 ) ;
then ( X c= Y or Y c= X ) by A42, A47, A41, A46, RELAT_1:143, XXREAL_1:42;
hence X,Y are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum
end;
assume A48: for s being real number holds s is not LowerBound of f .: the carrier of T ; :: according to XXREAL_2:def_9,MEASURE6:def_10 ::_thesis: contradiction
now__::_thesis:_not_{}_in_F
assume {} in F ; ::_thesis: contradiction
then consider rchx being set such that
A49: rchx in bool REAL and
A50: rchx in R and
A51: {} = (" f) . rchx by FUNCT_2:64;
consider r3 being Real such that
A52: rchx = left_closed_halfline r3 and
r3 <= f . the Element of T by A50;
r3 is not LowerBound of f .: the carrier of T by A48;
then consider r1 being ext-real number such that
A53: r1 in f .: the carrier of T and
A54: r1 < r3 by XXREAL_2:def_2;
rchx = { g where g is Real : g <= r3 } by A52, XXREAL_1:231;
then A55: r1 in rchx by A53, A54;
A56: ex c being set st
( c in the carrier of T & c in the carrier of T & r1 = f . c ) by A53, FUNCT_2:64;
{} = f " rchx by A49, A51, MEASURE6:def_3;
hence contradiction by A56, A55, FUNCT_2:38; ::_thesis: verum
end;
then A57: F is with_non-empty_elements by SETFAM_1:def_8;
(" f) . (left_closed_halfline (f . the Element of T)) in F by A35, FUNCT_2:35;
then meet F <> {} by A1, A57, A37, A36, COMPTS_1:4;
then consider x being set such that
A58: x in meet F by XBOOLE_0:def_1;
set eR = the Element of R;
the Element of R in R ;
then consider er being Real such that
A59: the Element of R = left_closed_halfline er and
A60: er <= f . the Element of T ;
reconsider x = x as Element of T by A58;
A61: f . x in meet R by A58, MEASURE6:35;
then A62: f . x in the Element of R by SETFAM_1:def_1;
consider fx9 being real number such that
A63: fx9 < f . x by XREAL_1:2;
reconsider fx9 = fx9 as Real by XREAL_0:def_1;
left_closed_halfline er = { r3 where r3 is Real : r3 <= er } by XXREAL_1:231;
then ex r1 being Real st
( f . x = r1 & r1 <= er ) by A62, A59;
then f . x <= f . the Element of T by A60, XXREAL_0:2;
then fx9 <= f . the Element of T by A63, XXREAL_0:2;
then left_closed_halfline fx9 in R ;
then A64: f . x in left_closed_halfline fx9 by A61, SETFAM_1:def_1;
left_closed_halfline fx9 = { r3 where r3 is Real : r3 <= fx9 } by XXREAL_1:231;
then ex r3 being Real st
( f . x = r3 & r3 <= fx9 ) by A64;
hence contradiction by A63; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like compact for TopStruct ;
existence
ex b1 being TopSpace st
( not b1 is empty & b1 is compact )
proof
set T = the non empty compact TopSpace;
take the non empty compact TopSpace ; ::_thesis: ( not the non empty compact TopSpace is empty & the non empty compact TopSpace is compact )
thus ( not the non empty compact TopSpace is empty & the non empty compact TopSpace is compact ) ; ::_thesis: verum
end;
end;
registration
let T be non empty pseudocompact TopSpace;
cluster Function-like V30( the carrier of T, REAL ) continuous -> with_max with_min bounded for Element of K32(K33( the carrier of T,REAL));
coherence
for b1 being RealMap of T st b1 is continuous holds
( b1 is bounded & b1 is with_max & b1 is with_min )
proof
let f be RealMap of T; ::_thesis: ( f is continuous implies ( f is bounded & f is with_max & f is with_min ) )
assume A1: f is continuous ; ::_thesis: ( f is bounded & f is with_max & f is with_min )
hence f is bounded by Def4; ::_thesis: ( f is with_max & f is with_min )
A2: for f being RealMap of T st f is continuous holds
f is bounded by Def4;
hence f is with_max by A1, Th15; ::_thesis: f is with_min
for f being RealMap of T st f is continuous holds
f is with_max by A2, Th15;
hence f is with_min by A1, Th14; ::_thesis: verum
end;
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)
proof
let T be non empty TopSpace; ::_thesis: 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)
let X be non empty Subset of T; ::_thesis: 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)
let Y be compact Subset of T; ::_thesis: for f being continuous RealMap of T st X c= Y holds
lower_bound (f | Y) <= lower_bound (f | X)
let f be continuous RealMap of T; ::_thesis: ( X c= Y implies lower_bound (f | Y) <= lower_bound (f | X) )
A1: (f | Y) .: the carrier of (T | Y) = (f | Y) .: Y by PRE_TOPC:8
.= f .: Y by RELAT_1:129 ;
assume A2: X c= Y ; ::_thesis: lower_bound (f | Y) <= lower_bound (f | X)
then reconsider Y1 = Y as non empty compact Subset of T ;
A3: (f | X) .: the carrier of (T | X) = (f | X) .: X by PRE_TOPC:8
.= f .: X by RELAT_1:129 ;
(f | Y1) .: the carrier of (T | Y1) is bounded_below by MEASURE6:def_10;
hence lower_bound (f | Y) <= lower_bound (f | X) by A2, A1, A3, RELAT_1:123, SEQ_4:47; ::_thesis: verum
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)
proof
let T be non empty TopSpace; ::_thesis: 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)
let X be non empty Subset of T; ::_thesis: 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)
let Y be compact Subset of T; ::_thesis: for f being continuous RealMap of T st X c= Y holds
upper_bound (f | X) <= upper_bound (f | Y)
let f be continuous RealMap of T; ::_thesis: ( X c= Y implies upper_bound (f | X) <= upper_bound (f | Y) )
A1: (f | Y) .: the carrier of (T | Y) = (f | Y) .: Y by PRE_TOPC:8
.= f .: Y by RELAT_1:129 ;
assume A2: X c= Y ; ::_thesis: upper_bound (f | X) <= upper_bound (f | Y)
then reconsider Y1 = Y as non empty compact Subset of T ;
A3: (f | X) .: the carrier of (T | X) = (f | X) .: X by PRE_TOPC:8
.= f .: X by RELAT_1:129 ;
(f | Y1) .: the carrier of (T | Y1) is bounded_above by MEASURE6:def_11;
hence upper_bound (f | X) <= upper_bound (f | Y) by A2, A1, A3, RELAT_1:123, SEQ_4:48; ::_thesis: verum
end;
begin
registration
let n be Element of NAT ;
let X, Y be compact Subset of (TOP-REAL n);
clusterX /\ Y -> compact for Subset of (TOP-REAL n);
coherence
for b1 being Subset of (TOP-REAL n) st b1 = X /\ Y holds
b1 is compact by COMPTS_1:11;
end;
definition
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
ex b1 being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds b1 . p = p `1
proof
deffunc H1( Point of (TOP-REAL 2)) -> Element of REAL = $1 `1 ;
thus ex f being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds f . p = H1(p) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = p `1 ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = p `1 ) holds
b1 = b2
proof
let it1, it2 be RealMap of (TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) holds it1 . p = p `1 ) & ( for p being Point of (TOP-REAL 2) holds it2 . p = p `1 ) implies it1 = it2 )
assume that
A1: for p being Point of (TOP-REAL 2) holds it1 . p = p `1 and
A2: for p being Point of (TOP-REAL 2) holds it2 . p = p `1 ; ::_thesis: it1 = it2
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_it1_._p_=_it2_._p
let p be Point of (TOP-REAL 2); ::_thesis: it1 . p = it2 . p
thus it1 . p = p `1 by A1
.= it2 . p by A2 ; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:63; ::_thesis: verum
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
ex b1 being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds b1 . p = p `2
proof
deffunc H1( Point of (TOP-REAL 2)) -> Element of REAL = $1 `2 ;
thus ex f being RealMap of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds f . p = H1(p) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being RealMap of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = p `2 ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = p `2 ) holds
b1 = b2
proof
let it1, it2 be RealMap of (TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) holds it1 . p = p `2 ) & ( for p being Point of (TOP-REAL 2) holds it2 . p = p `2 ) implies it1 = it2 )
assume that
A3: for p being Point of (TOP-REAL 2) holds it1 . p = p `2 and
A4: for p being Point of (TOP-REAL 2) holds it2 . p = p `2 ; ::_thesis: it1 = it2
now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_it1_._p_=_it2_._p
let p be Point of (TOP-REAL 2); ::_thesis: it1 . p = it2 . p
thus it1 . p = p `2 by A3
.= it2 . p by A4 ; ::_thesis: verum
end;
hence it1 = it2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines proj1 PSCOMP_1:def_5_:_
for b1 being RealMap of (TOP-REAL 2) holds
( b1 = proj1 iff for p being Point of (TOP-REAL 2) holds b1 . p = p `1 );
:: deftheorem Def6 defines proj2 PSCOMP_1:def_6_:_
for b1 being RealMap of (TOP-REAL 2) holds
( b1 = proj2 iff for p being Point of (TOP-REAL 2) holds b1 . p = p `2 );
theorem Th18: :: PSCOMP_1:18
for r, s being real number holds proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
proof
let r, s be real number ; ::_thesis: proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
set Q = proj1 " ].r,s.[;
set QQ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } ;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_proj1_"_].r,s.[_implies_z_in__{__|[r1,r2]|_where_r1,_r2_is_Real_:_(_r_<_r1_&_r1_<_s_)__}__)_&_(_z_in__{__|[r1,r2]|_where_r1,_r2_is_Real_:_(_r_<_r1_&_r1_<_s_)__}__implies_z_in_proj1_"_].r,s.[_)_)
let z be set ; ::_thesis: ( ( z in proj1 " ].r,s.[ implies z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } ) & ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } implies z in proj1 " ].r,s.[ ) )
hereby ::_thesis: ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } implies z in proj1 " ].r,s.[ )
assume A1: z in proj1 " ].r,s.[ ; ::_thesis: z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) }
then reconsider p = z as Point of (TOP-REAL 2) ;
proj1 . p in ].r,s.[ by A1, FUNCT_2:38;
then A2: ex t being Real st
( t = proj1 . p & r < t & t < s ) ;
( p `1 = proj1 . p & p = |[(p `1),(p `2)]| ) by Def5, EUCLID:53;
hence z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } by A2; ::_thesis: verum
end;
assume z in { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } ; ::_thesis: z in proj1 " ].r,s.[
then consider r1, r2 being Real such that
A3: z = |[r1,r2]| and
A4: ( r < r1 & r1 < s ) ;
set p = |[r1,r2]|;
A5: r1 in ].r,s.[ by A4;
proj1 . |[r1,r2]| = |[r1,r2]| `1 by Def5
.= r1 by EUCLID:52 ;
hence z in proj1 " ].r,s.[ by A3, A5, FUNCT_2:38; ::_thesis: verum
end;
hence proj1 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r1 & r1 < s ) } by TARSKI:1; ::_thesis: verum
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
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } holds
P is open
deffunc H1( Real, Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,$2]|;
let r3, q3 be Real; ::_thesis: ( P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } implies P is open )
defpred S1[ Real, Real] means r3 < $1;
defpred S2[ Real, Real] means $1 < q3;
A1: { H1(r1,r2) where r1, r2 is Real : S2[r1,r2] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_9();
{ H1(r1,r2) where r1, r2 is Real : S1[r1,r2] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_9();
then reconsider Q1 = { |[r1,r2]| where r1, r2 is Real : r3 < r1 } , Q2 = { |[r1,r2]| where r1, r2 is Real : r1 < q3 } as Subset of (TOP-REAL 2) by A1;
assume A2: P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r1 & r1 < q3 ) } ; ::_thesis: P is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_P_implies_x_in_Q1_/\_Q2_)_&_(_x_in_Q1_/\_Q2_implies_x_in_P_)_)
let x be set ; ::_thesis: ( ( x in P implies x in Q1 /\ Q2 ) & ( x in Q1 /\ Q2 implies x in P ) )
hereby ::_thesis: ( x in Q1 /\ Q2 implies x in P )
assume x in P ; ::_thesis: x in Q1 /\ Q2
then ex r1, r2 being Real st
( x = |[r1,r2]| & r3 < r1 & r1 < q3 ) by A2;
then ( x in Q1 & x in Q2 ) ;
hence x in Q1 /\ Q2 by XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: x in Q1 /\ Q2 ; ::_thesis: x in P
then x in Q1 by XBOOLE_0:def_4;
then consider r1, r2 being Real such that
A4: ( x = |[r1,r2]| & r3 < r1 ) ;
x in Q2 by A3, XBOOLE_0:def_4;
then consider r19, r29 being Real such that
A5: ( x = |[r19,r29]| & r19 < q3 ) ;
( |[r1,r2]| `1 = r1 & |[r19,r29]| `1 = r19 ) by EUCLID:52;
hence x in P by A2, A4, A5; ::_thesis: verum
end;
then A6: P = Q1 /\ Q2 by TARSKI:1;
( Q1 is open & Q2 is open ) by JORDAN1:20, JORDAN1:21;
hence P is open by A6, TOPS_1:11; ::_thesis: verum
end;
theorem Th20: :: PSCOMP_1:20
for r, s being real number holds proj2 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) }
proof
let r, s be real number ; ::_thesis: proj2 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) }
set Q = proj2 " ].r,s.[;
set QQ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } ;
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_proj2_"_].r,s.[_implies_z_in__{__|[r1,r2]|_where_r1,_r2_is_Real_:_(_r_<_r2_&_r2_<_s_)__}__)_&_(_z_in__{__|[r1,r2]|_where_r1,_r2_is_Real_:_(_r_<_r2_&_r2_<_s_)__}__implies_z_in_proj2_"_].r,s.[_)_)
let z be set ; ::_thesis: ( ( z in proj2 " ].r,s.[ implies z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } ) & ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } implies z in proj2 " ].r,s.[ ) )
hereby ::_thesis: ( z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } implies z in proj2 " ].r,s.[ )
assume A1: z in proj2 " ].r,s.[ ; ::_thesis: z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) }
then reconsider p = z as Point of (TOP-REAL 2) ;
proj2 . p in ].r,s.[ by A1, FUNCT_2:38;
then A2: ex t being Real st
( t = proj2 . p & r < t & t < s ) ;
( p `2 = proj2 . p & p = |[(p `1),(p `2)]| ) by Def6, EUCLID:53;
hence z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } by A2; ::_thesis: verum
end;
assume z in { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } ; ::_thesis: z in proj2 " ].r,s.[
then consider r1, r2 being Real such that
A3: z = |[r1,r2]| and
A4: ( r < r2 & r2 < s ) ;
set p = |[r1,r2]|;
A5: r2 in ].r,s.[ by A4;
proj2 . |[r1,r2]| = |[r1,r2]| `2 by Def6
.= r2 by EUCLID:52 ;
hence z in proj2 " ].r,s.[ by A3, A5, FUNCT_2:38; ::_thesis: verum
end;
hence proj2 " ].r,s.[ = { |[r1,r2]| where r1, r2 is Real : ( r < r2 & r2 < s ) } by TARSKI:1; ::_thesis: verum
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
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for r3, q3 being Real st P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } holds
P is open
deffunc H1( Real, Real) -> Element of the carrier of (TOP-REAL 2) = |[$1,$2]|;
let r3, q3 be Real; ::_thesis: ( P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } implies P is open )
defpred S1[ Real, Real] means r3 < $2;
defpred S2[ Real, Real] means $2 < q3;
A1: { H1(r1,r2) where r1, r2 is Real : S2[r1,r2] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_9();
{ H1(r1,r2) where r1, r2 is Real : S1[r1,r2] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_9();
then reconsider Q1 = { |[r1,r2]| where r1, r2 is Real : r3 < r2 } , Q2 = { |[r1,r2]| where r1, r2 is Real : r2 < q3 } as Subset of (TOP-REAL 2) by A1;
assume A2: P = { |[r1,r2]| where r1, r2 is Real : ( r3 < r2 & r2 < q3 ) } ; ::_thesis: P is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_P_implies_x_in_Q1_/\_Q2_)_&_(_x_in_Q1_/\_Q2_implies_x_in_P_)_)
let x be set ; ::_thesis: ( ( x in P implies x in Q1 /\ Q2 ) & ( x in Q1 /\ Q2 implies x in P ) )
hereby ::_thesis: ( x in Q1 /\ Q2 implies x in P )
assume x in P ; ::_thesis: x in Q1 /\ Q2
then ex r1, r2 being Real st
( x = |[r1,r2]| & r3 < r2 & r2 < q3 ) by A2;
then ( x in Q1 & x in Q2 ) ;
hence x in Q1 /\ Q2 by XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: x in Q1 /\ Q2 ; ::_thesis: x in P
then x in Q1 by XBOOLE_0:def_4;
then consider r1, r2 being Real such that
A4: ( x = |[r1,r2]| & r3 < r2 ) ;
x in Q2 by A3, XBOOLE_0:def_4;
then consider r19, r29 being Real such that
A5: ( x = |[r19,r29]| & r29 < q3 ) ;
( |[r1,r2]| `2 = r2 & |[r19,r29]| `2 = r29 ) by EUCLID:52;
hence x in P by A2, A4, A5; ::_thesis: verum
end;
then A6: P = Q1 /\ Q2 by TARSKI:1;
( Q1 is open & Q2 is open ) by JORDAN1:22, JORDAN1:23;
hence P is open by A6, TOPS_1:11; ::_thesis: verum
end;
registration
cluster proj1 -> continuous ;
coherence
proj1 is continuous
proof
now__::_thesis:_for_Y_being_Subset_of_REAL_st_Y_is_open_holds_
proj1_"_Y_is_open
let Y be Subset of REAL; ::_thesis: ( Y is open implies proj1 " Y is open )
set p1Y = proj1 " Y;
assume A1: Y is open ; ::_thesis: proj1 " Y is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_proj1_"_Y_implies_ex_Q_being_Subset_of_(TOP-REAL_2)_st_
(_Q_is_open_&_Q_c=_proj1_"_Y_&_x_in_Q_)_)_&_(_ex_Q_being_Subset_of_(TOP-REAL_2)_st_
(_Q_is_open_&_Q_c=_proj1_"_Y_&_x_in_Q_)_implies_x_in_proj1_"_Y_)_)
let x be set ; ::_thesis: ( ( x in proj1 " Y implies ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj1 " Y & x in Q ) ) & ( ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj1 " Y & x in Q ) implies x in proj1 " Y ) )
hereby ::_thesis: ( ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj1 " Y & x in Q ) implies x in proj1 " Y )
assume A2: x in proj1 " Y ; ::_thesis: ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj1 " Y & x in Q )
then reconsider p = x as Point of (TOP-REAL 2) ;
set p1 = proj1 . p;
proj1 . p in Y by A2, FUNCT_2:38;
then consider g being real number such that
A3: 0 < g and
A4: ].((proj1 . p) - g),((proj1 . p) + g).[ c= Y by A1, RCOMP_1:19;
reconsider g = g as Real by XREAL_0:def_1;
reconsider Q = proj1 " ].((proj1 . p) - g),((proj1 . p) + g).[ as Subset of (TOP-REAL 2) ;
take Q = Q; ::_thesis: ( Q is open & Q c= proj1 " Y & x in Q )
Q = { |[q3,p3]| where q3, p3 is Real : ( (proj1 . p) - g < q3 & q3 < (proj1 . p) + g ) } by Th18;
hence Q is open by Th19; ::_thesis: ( Q c= proj1 " Y & x in Q )
thus Q c= proj1 " Y by A4, RELAT_1:143; ::_thesis: x in Q
A5: proj1 . p < (proj1 . p) + g by A3, XREAL_1:29;
then (proj1 . p) - g < proj1 . p by XREAL_1:19;
then proj1 . p in ].((proj1 . p) - g),((proj1 . p) + g).[ by A5;
hence x in Q by FUNCT_2:38; ::_thesis: verum
end;
assume ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj1 " Y & x in Q ) ; ::_thesis: x in proj1 " Y
hence x in proj1 " Y ; ::_thesis: verum
end;
hence proj1 " Y is open by TOPS_1:25; ::_thesis: verum
end;
hence proj1 is continuous by Th8; ::_thesis: verum
end;
cluster proj2 -> continuous ;
coherence
proj2 is continuous
proof
now__::_thesis:_for_Y_being_Subset_of_REAL_st_Y_is_open_holds_
proj2_"_Y_is_open
let Y be Subset of REAL; ::_thesis: ( Y is open implies proj2 " Y is open )
set p1Y = proj2 " Y;
assume A6: Y is open ; ::_thesis: proj2 " Y is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_proj2_"_Y_implies_ex_Q_being_Subset_of_(TOP-REAL_2)_st_
(_Q_is_open_&_Q_c=_proj2_"_Y_&_x_in_Q_)_)_&_(_ex_Q_being_Subset_of_(TOP-REAL_2)_st_
(_Q_is_open_&_Q_c=_proj2_"_Y_&_x_in_Q_)_implies_x_in_proj2_"_Y_)_)
let x be set ; ::_thesis: ( ( x in proj2 " Y implies ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) ) & ( ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) implies x in proj2 " Y ) )
hereby ::_thesis: ( ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) implies x in proj2 " Y )
assume A7: x in proj2 " Y ; ::_thesis: ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q )
then reconsider p = x as Point of (TOP-REAL 2) ;
set p1 = proj2 . p;
proj2 . p in Y by A7, FUNCT_2:38;
then consider g being real number such that
A8: 0 < g and
A9: ].((proj2 . p) - g),((proj2 . p) + g).[ c= Y by A6, RCOMP_1:19;
reconsider g = g as Real by XREAL_0:def_1;
reconsider Q = proj2 " ].((proj2 . p) - g),((proj2 . p) + g).[ as Subset of (TOP-REAL 2) ;
take Q = Q; ::_thesis: ( Q is open & Q c= proj2 " Y & x in Q )
Q = { |[q3,p3]| where q3, p3 is Real : ( (proj2 . p) - g < p3 & p3 < (proj2 . p) + g ) } by Th20;
hence Q is open by Th21; ::_thesis: ( Q c= proj2 " Y & x in Q )
thus Q c= proj2 " Y by A9, RELAT_1:143; ::_thesis: x in Q
A10: proj2 . p < (proj2 . p) + g by A8, XREAL_1:29;
then (proj2 . p) - g < proj2 . p by XREAL_1:19;
then proj2 . p in ].((proj2 . p) - g),((proj2 . p) + g).[ by A10;
hence x in Q by FUNCT_2:38; ::_thesis: verum
end;
assume ex Q being Subset of (TOP-REAL 2) st
( Q is open & Q c= proj2 " Y & x in Q ) ; ::_thesis: x in proj2 " Y
hence x in proj2 " Y ; ::_thesis: verum
end;
hence proj2 " Y is open by TOPS_1:25; ::_thesis: verum
end;
hence proj2 is continuous by Th8; ::_thesis: verum
end;
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
proof
let X be Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in X holds
(proj1 | X) . p = p `1
let p be Point of (TOP-REAL 2); ::_thesis: ( p in X implies (proj1 | X) . p = p `1 )
assume p in X ; ::_thesis: (proj1 | X) . p = p `1
hence (proj1 | X) . p = proj1 . p by FUNCT_1:49
.= p `1 by Def5 ;
::_thesis: verum
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
proof
let X be Subset of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in X holds
(proj2 | X) . p = p `2
let p be Point of (TOP-REAL 2); ::_thesis: ( p in X implies (proj2 | X) . p = p `2 )
assume p in X ; ::_thesis: (proj2 | X) . p = p `2
hence (proj2 | X) . p = proj2 . p by FUNCT_1:49
.= p `2 by Def6 ;
::_thesis: verum
end;
definition
let X be Subset of (TOP-REAL 2);
func W-bound X -> Real equals :: PSCOMP_1:def 7
lower_bound (proj1 | X);
coherence
lower_bound (proj1 | X) is Real ;
func N-bound X -> Real equals :: PSCOMP_1:def 8
upper_bound (proj2 | X);
coherence
upper_bound (proj2 | X) is Real ;
func E-bound X -> Real equals :: PSCOMP_1:def 9
upper_bound (proj1 | X);
coherence
upper_bound (proj1 | X) is Real ;
func S-bound X -> Real equals :: PSCOMP_1:def 10
lower_bound (proj2 | X);
coherence
lower_bound (proj2 | X) is Real ;
end;
:: deftheorem defines W-bound PSCOMP_1:def_7_:_
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);
:: deftheorem defines E-bound PSCOMP_1:def_9_:_
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);
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
let p be Point of (TOP-REAL 2); ::_thesis: 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) )
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( p in X implies ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) ) )
assume A1: p in X ; ::_thesis: ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
then reconsider p9 = p as Point of ((TOP-REAL 2) | X) by PRE_TOPC:8;
A2: (proj1 | X) . p9 = p `1 by A1, Th22;
hence lower_bound (proj1 | X) <= p `1 by Th1; ::_thesis: ( p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
thus p `1 <= upper_bound (proj1 | X) by A2, Th4; ::_thesis: ( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
A3: (proj2 | X) . p9 = p `2 by A1, Th23;
hence lower_bound (proj2 | X) <= p `2 by Th1; ::_thesis: p `2 <= upper_bound (proj2 | X)
thus p `2 <= upper_bound (proj2 | X) by A3, Th4; ::_thesis: verum
end;
theorem :: PSCOMP_1:24
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 11
|[(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 12
|[(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 13
|[(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 14
|[(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_11_:_
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)]|;
:: 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)]|;
:: 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)]|;
theorem :: PSCOMP_1:25
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `1 = (NW-corner P) `1
proof
let P be Subset of (TOP-REAL 2); ::_thesis: (SW-corner P) `1 = (NW-corner P) `1
thus (SW-corner P) `1 = W-bound P by EUCLID:52
.= (NW-corner P) `1 by EUCLID:52 ; ::_thesis: verum
end;
theorem :: PSCOMP_1:26
for P being Subset of (TOP-REAL 2) holds (SE-corner P) `1 = (NE-corner P) `1
proof
let P be Subset of (TOP-REAL 2); ::_thesis: (SE-corner P) `1 = (NE-corner P) `1
thus (SE-corner P) `1 = E-bound P by EUCLID:52
.= (NE-corner P) `1 by EUCLID:52 ; ::_thesis: verum
end;
theorem :: PSCOMP_1:27
for P being Subset of (TOP-REAL 2) holds (NW-corner P) `2 = (NE-corner P) `2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: (NW-corner P) `2 = (NE-corner P) `2
thus (NW-corner P) `2 = N-bound P by EUCLID:52
.= (NE-corner P) `2 by EUCLID:52 ; ::_thesis: verum
end;
theorem :: PSCOMP_1:28
for P being Subset of (TOP-REAL 2) holds (SW-corner P) `2 = (SE-corner P) `2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: (SW-corner P) `2 = (SE-corner P) `2
thus (SW-corner P) `2 = S-bound P by EUCLID:52
.= (SE-corner P) `2 by EUCLID:52 ; ::_thesis: verum
end;
definition
let X be Subset of (TOP-REAL 2);
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 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 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 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 is Subset of (TOP-REAL 2) ;
end;
:: 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;
:: 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;
:: 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;
:: 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;
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
set p1X = proj1 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A1: ( (SW-corner X) `1 = W-bound X & (NW-corner X) `1 = W-bound X ) by EUCLID:52;
(proj1 | X) .: the carrier of ((TOP-REAL 2) | X) is with_min by MEASURE6:def_13;
then lower_bound ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj1 | X) .: the carrier of ((TOP-REAL 2) | X) by MEASURE6:def_5;
then consider p being set such that
A2: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A3: lower_bound ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj1 | X) . p by FUNCT_2:64;
A4: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
A5: p `2 <= N-bound X by A4, A2, Lm3;
A6: ( (SW-corner X) `2 = S-bound X & (NW-corner X) `2 = N-bound X ) by EUCLID:52;
( (proj1 | X) . p = p `1 & S-bound X <= p `2 ) by A4, A2, Lm3, Th22;
then p in LSeg ((SW-corner X),(NW-corner X)) by A1, A6, A3, A5, GOBOARD7:7;
hence ( not W-most X is empty & W-most X is compact ) by A4, A2, XBOOLE_0:def_4; ::_thesis: verum
end;
cluster N-most X -> non empty compact ;
coherence
( not N-most X is empty & N-most X is compact )
proof
set p2X = proj2 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A7: ( (NW-corner X) `1 = W-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:52;
(proj2 | X) .: the carrier of ((TOP-REAL 2) | X) is with_max by MEASURE6:def_12;
then upper_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj2 | X) .: the carrier of ((TOP-REAL 2) | X) by MEASURE6:def_4;
then consider p being set such that
A8: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A9: upper_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj2 | X) . p by FUNCT_2:64;
A10: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A8;
A11: p `1 <= E-bound X by A10, A8, Lm3;
A12: ( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
( (proj2 | X) . p = p `2 & W-bound X <= p `1 ) by A10, A8, Lm3, Th23;
then p in LSeg ((NW-corner X),(NE-corner X)) by A7, A12, A9, A11, GOBOARD7:8;
hence ( not N-most X is empty & N-most X is compact ) by A10, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
cluster E-most X -> non empty compact ;
coherence
( not E-most X is empty & E-most X is compact )
proof
set p1X = proj1 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A13: ( (SE-corner X) `1 = E-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:52;
(proj1 | X) .: the carrier of ((TOP-REAL 2) | X) is with_max by MEASURE6:def_12;
then upper_bound ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj1 | X) .: the carrier of ((TOP-REAL 2) | X) by MEASURE6:def_4;
then consider p being set such that
A14: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A15: upper_bound ((proj1 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj1 | X) . p by FUNCT_2:64;
A16: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A14;
A17: p `2 <= N-bound X by A16, A14, Lm3;
A18: ( (SE-corner X) `2 = S-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
( (proj1 | X) . p = p `1 & S-bound X <= p `2 ) by A16, A14, Lm3, Th22;
then p in LSeg ((SE-corner X),(NE-corner X)) by A13, A18, A15, A17, GOBOARD7:7;
hence ( not E-most X is empty & E-most X is compact ) by A16, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
cluster S-most X -> non empty compact ;
coherence
( not S-most X is empty & S-most X is compact )
proof
set p2X = proj2 | X;
set c = the carrier of ((TOP-REAL 2) | X);
A19: ( (SW-corner X) `1 = W-bound X & (SE-corner X) `1 = E-bound X ) by EUCLID:52;
(proj2 | X) .: the carrier of ((TOP-REAL 2) | X) is with_min by MEASURE6:def_13;
then lower_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) in (proj2 | X) .: the carrier of ((TOP-REAL 2) | X) by MEASURE6:def_5;
then consider p being set such that
A20: p in the carrier of ((TOP-REAL 2) | X) and
p in the carrier of ((TOP-REAL 2) | X) and
A21: lower_bound ((proj2 | X) .: the carrier of ((TOP-REAL 2) | X)) = (proj2 | X) . p by FUNCT_2:64;
A22: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A20;
A23: p `1 <= E-bound X by A22, A20, Lm3;
A24: ( (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:52;
( (proj2 | X) . p = p `2 & W-bound X <= p `1 ) by A22, A20, Lm3, Th23;
then p in LSeg ((SW-corner X),(SE-corner X)) by A19, A24, A21, A23, GOBOARD7:8;
hence ( not S-most X is empty & S-most X is compact ) by A22, A20, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
definition
let X be Subset of (TOP-REAL 2);
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)))]| 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)))]| 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)]| 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)]| 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)))]| 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)))]| 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)]| 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)]| is Point of (TOP-REAL 2) ;
end;
:: 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)))]|;
:: 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)))]|;
:: 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)]|;
:: 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)]|;
:: 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)))]|;
:: 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)))]|;
:: 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)]|;
:: 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)]|;
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 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( (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 )
( (W-min P) `1 = W-bound P & (W-max P) `1 = W-bound P ) by EUCLID:52;
hence ( (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 ) by EUCLID:52; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (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 )
set LX = W-most X;
A1: (W-min X) `2 = lower_bound (proj2 | (W-most X)) by EUCLID:52;
A2: (SW-corner X) `2 = lower_bound (proj2 | X) by EUCLID:52;
hence (SW-corner X) `2 <= (W-min X) `2 by A1, Th16, XBOOLE_1:17; ::_thesis: ( (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 )
A3: (W-max X) `2 = upper_bound (proj2 | (W-most X)) by EUCLID:52;
then A4: (W-min X) `2 <= (W-max X) `2 by A1, Th7;
(SW-corner X) `2 <= (W-min X) `2 by A2, A1, Th16, XBOOLE_1:17;
hence A5: (SW-corner X) `2 <= (W-max X) `2 by A4, XXREAL_0:2; ::_thesis: ( (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 )
A6: (NW-corner X) `2 = upper_bound (proj2 | X) by EUCLID:52;
then A7: (W-max X) `2 <= (NW-corner X) `2 by A3, Th17, XBOOLE_1:17;
hence (SW-corner X) `2 <= (NW-corner X) `2 by A5, XXREAL_0:2; ::_thesis: ( (W-min X) `2 <= (W-max X) `2 & (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )
thus (W-min X) `2 <= (W-max X) `2 by A1, A3, Th7; ::_thesis: ( (W-min X) `2 <= (NW-corner X) `2 & (W-max X) `2 <= (NW-corner X) `2 )
thus (W-min X) `2 <= (NW-corner X) `2 by A4, A7, XXREAL_0:2; ::_thesis: (W-max X) `2 <= (NW-corner X) `2
thus (W-max X) `2 <= (NW-corner X) `2 by A3, A6, Th17, XBOOLE_1:17; ::_thesis: verum
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 ) ) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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 ) ) )
let Z be non empty Subset of (TOP-REAL 2); ::_thesis: ( p in W-most Z implies ( p `1 = (W-min Z) `1 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) ) )
A1: ( (SW-corner Z) `1 = W-bound Z & (W-min Z) `1 = W-bound Z ) by EUCLID:52;
A2: (NW-corner Z) `1 = W-bound Z by EUCLID:52;
assume A3: p in W-most Z ; ::_thesis: ( p `1 = (W-min Z) `1 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) )
then p in LSeg ((SW-corner Z),(NW-corner Z)) by XBOOLE_0:def_4;
hence p `1 = (W-min Z) `1 by A1, A2, GOBOARD7:5; ::_thesis: ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) )
assume Z is compact ; ::_thesis: ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 )
then reconsider Z = Z as non empty compact Subset of (TOP-REAL 2) ;
( (W-min Z) `2 = lower_bound (proj2 | (W-most Z)) & (W-max Z) `2 = upper_bound (proj2 | (W-most Z)) ) by EUCLID:52;
hence ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) by A3, Lm3; ::_thesis: verum
end;
theorem Th32: :: PSCOMP_1:32
for X being non empty compact Subset of (TOP-REAL 2) holds W-most X c= LSeg ((W-min X),(W-max X))
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: W-most X c= LSeg ((W-min X),(W-max X))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W-most X or x in LSeg ((W-min X),(W-max X)) )
assume A1: x in W-most X ; ::_thesis: x in LSeg ((W-min X),(W-max X))
then reconsider p = x as Point of (TOP-REAL 2) ;
A2: p `2 <= (W-max X) `2 by A1, Th31;
A3: (W-min X) `1 = (W-max X) `1 by Th29;
( p `1 = (W-min X) `1 & (W-min X) `2 <= p `2 ) by A1, Th31;
hence x in LSeg ((W-min X),(W-max X)) by A3, A2, GOBOARD7:7; ::_thesis: verum
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
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: LSeg ((W-min X),(W-max X)) c= LSeg ((SW-corner X),(NW-corner X))
A1: ( (SW-corner X) `1 = W-bound X & (NW-corner X) `1 = W-bound X ) by EUCLID:52;
A2: (W-max X) `2 <= (NW-corner X) `2 by Th30;
( (W-max X) `1 = W-bound X & (SW-corner X) `2 <= (W-max X) `2 ) by Th30, EUCLID:52;
then A3: W-max X in LSeg ((SW-corner X),(NW-corner X)) by A1, A2, GOBOARD7:7;
A4: (W-min X) `2 <= (NW-corner X) `2 by Th30;
( (W-min X) `1 = W-bound X & (SW-corner X) `2 <= (W-min X) `2 ) by Th30, EUCLID:52;
then W-min X in LSeg ((SW-corner X),(NW-corner X)) by A1, A4, GOBOARD7:7;
hence LSeg ((W-min X),(W-max X)) c= LSeg ((SW-corner X),(NW-corner X)) by A3, TOPREAL1:6; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( W-min X in W-most X & W-max X in W-most X )
set p2W = proj2 | (W-most X);
set c = the carrier of ((TOP-REAL 2) | (W-most X));
A1: ( (SW-corner X) `1 = W-bound X & (NW-corner X) `1 = W-bound X ) by EUCLID:52;
(proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X)) is with_min by MEASURE6:def_13;
then lower_bound ((proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X))) in (proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X)) by MEASURE6:def_5;
then consider p being set such that
A2: p in the carrier of ((TOP-REAL 2) | (W-most X)) and
p in the carrier of ((TOP-REAL 2) | (W-most X)) and
A3: lower_bound ((proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X))) = (proj2 | (W-most X)) . p by FUNCT_2:64;
A4: the carrier of ((TOP-REAL 2) | (W-most X)) = W-most X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
p in LSeg ((SW-corner X),(NW-corner X)) by A4, A2, XBOOLE_0:def_4;
then A5: p `1 = W-bound X by A1, GOBOARD7:5;
A6: ( (SW-corner X) `1 = W-bound X & (NW-corner X) `1 = W-bound X ) by EUCLID:52;
(proj2 | (W-most X)) . p = p `2 by A4, A2, Th23;
hence W-min X in W-most X by A4, A2, A3, A5, EUCLID:53; ::_thesis: W-max X in W-most X
(proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X)) is with_max by MEASURE6:def_12;
then upper_bound ((proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X))) in (proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X)) by MEASURE6:def_4;
then consider p being set such that
A7: p in the carrier of ((TOP-REAL 2) | (W-most X)) and
p in the carrier of ((TOP-REAL 2) | (W-most X)) and
A8: upper_bound ((proj2 | (W-most X)) .: the carrier of ((TOP-REAL 2) | (W-most X))) = (proj2 | (W-most X)) . p by FUNCT_2:64;
reconsider p = p as Point of (TOP-REAL 2) by A4, A7;
p in LSeg ((SW-corner X),(NW-corner X)) by A4, A7, XBOOLE_0:def_4;
then A9: p `1 = W-bound X by A6, GOBOARD7:5;
(proj2 | (W-most X)) . p = p `2 by A4, A7, Th23;
hence W-max X in W-most X by A4, A7, A8, A9, EUCLID:53; ::_thesis: verum
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)} )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (LSeg ((SW-corner X),(W-min X))) /\ X = {(W-min X)} & (LSeg ((W-max X),(NW-corner X))) /\ X = {(W-max X)} )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((SW-corner_X),(W-min_X)))_/\_X_implies_x_=_W-min_X_)_&_(_x_=_W-min_X_implies_x_in_(LSeg_((SW-corner_X),(W-min_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((SW-corner X),(W-min X))) /\ X implies x = W-min X ) & ( x = W-min X implies x in (LSeg ((SW-corner X),(W-min X))) /\ X ) )
A1: W-min X in LSeg ((SW-corner X),(W-min X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = W-min X implies x in (LSeg ((SW-corner X),(W-min X))) /\ X )
W-min X in W-most X by Th34;
then ( SW-corner X in LSeg ((SW-corner X),(NW-corner X)) & W-min X in LSeg ((SW-corner X),(NW-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A2: LSeg ((SW-corner X),(W-min X)) c= LSeg ((SW-corner X),(NW-corner X)) by TOPREAL1:6;
assume A3: x in (LSeg ((SW-corner X),(W-min X))) /\ X ; ::_thesis: x = W-min X
then A4: x in LSeg ((SW-corner X),(W-min X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A3;
x in X by A3, XBOOLE_0:def_4;
then p in W-most X by A4, A2, XBOOLE_0:def_4;
then A5: (W-min X) `2 <= p `2 by Th31;
(SW-corner X) `2 <= (W-min X) `2 by Th30;
then p `2 <= (W-min X) `2 by A4, TOPREAL1:4;
then A6: p `2 = (W-min X) `2 by A5, XXREAL_0:1;
(SW-corner X) `1 = (W-min X) `1 by Th29;
then A7: p `1 = (W-min X) `1 by A4, GOBOARD7:5;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = W-min X by A7, A6, EUCLID:53; ::_thesis: verum
end;
W-min X in W-most X by Th34;
then A8: W-min X in X by XBOOLE_0:def_4;
assume x = W-min X ; ::_thesis: x in (LSeg ((SW-corner X),(W-min X))) /\ X
hence x in (LSeg ((SW-corner X),(W-min X))) /\ X by A8, A1, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((SW-corner X),(W-min X))) /\ X = {(W-min X)} by TARSKI:def_1; ::_thesis: (LSeg ((W-max X),(NW-corner X))) /\ X = {(W-max X)}
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((W-max_X),(NW-corner_X)))_/\_X_implies_x_=_W-max_X_)_&_(_x_=_W-max_X_implies_x_in_(LSeg_((W-max_X),(NW-corner_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((W-max X),(NW-corner X))) /\ X implies x = W-max X ) & ( x = W-max X implies x in (LSeg ((W-max X),(NW-corner X))) /\ X ) )
A9: W-max X in LSeg ((W-max X),(NW-corner X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = W-max X implies x in (LSeg ((W-max X),(NW-corner X))) /\ X )
W-max X in W-most X by Th34;
then ( NW-corner X in LSeg ((SW-corner X),(NW-corner X)) & W-max X in LSeg ((SW-corner X),(NW-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A10: LSeg ((W-max X),(NW-corner X)) c= LSeg ((SW-corner X),(NW-corner X)) by TOPREAL1:6;
assume A11: x in (LSeg ((W-max X),(NW-corner X))) /\ X ; ::_thesis: x = W-max X
then A12: x in LSeg ((W-max X),(NW-corner X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A11;
x in X by A11, XBOOLE_0:def_4;
then p in W-most X by A12, A10, XBOOLE_0:def_4;
then A13: p `2 <= (W-max X) `2 by Th31;
(W-max X) `2 <= (NW-corner X) `2 by Th30;
then (W-max X) `2 <= p `2 by A12, TOPREAL1:4;
then A14: p `2 = (W-max X) `2 by A13, XXREAL_0:1;
(NW-corner X) `1 = (W-max X) `1 by Th29;
then A15: p `1 = (W-max X) `1 by A12, GOBOARD7:5;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = W-max X by A15, A14, EUCLID:53; ::_thesis: verum
end;
W-max X in W-most X by Th34;
then A16: W-max X in X by XBOOLE_0:def_4;
assume x = W-max X ; ::_thesis: x in (LSeg ((W-max X),(NW-corner X))) /\ X
hence x in (LSeg ((W-max X),(NW-corner X))) /\ X by A16, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((W-max X),(NW-corner X))) /\ X = {(W-max X)} by TARSKI:def_1; ::_thesis: verum
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)}
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( W-min X = W-max X implies W-most X = {(W-min X)} )
assume W-min X = W-max X ; ::_thesis: W-most X = {(W-min X)}
then W-most X c= LSeg ((W-min X),(W-min X)) by Th32;
then W-most X c= {(W-min X)} by RLTOPSP1:70;
hence W-most X = {(W-min X)} by ZFMISC_1:33; ::_thesis: verum
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 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( (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 )
( (N-min P) `2 = N-bound P & (N-max P) `2 = N-bound P ) by EUCLID:52;
hence ( (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 ) by EUCLID:52; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (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 )
set LX = N-most X;
A1: (N-min X) `1 = lower_bound (proj1 | (N-most X)) by EUCLID:52;
A2: (NW-corner X) `1 = lower_bound (proj1 | X) by EUCLID:52;
hence (NW-corner X) `1 <= (N-min X) `1 by A1, Th16, XBOOLE_1:17; ::_thesis: ( (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 )
A3: (N-max X) `1 = upper_bound (proj1 | (N-most X)) by EUCLID:52;
then A4: (N-min X) `1 <= (N-max X) `1 by A1, Th7;
(NW-corner X) `1 <= (N-min X) `1 by A2, A1, Th16, XBOOLE_1:17;
hence A5: (NW-corner X) `1 <= (N-max X) `1 by A4, XXREAL_0:2; ::_thesis: ( (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 )
A6: (NE-corner X) `1 = upper_bound (proj1 | X) by EUCLID:52;
then A7: (N-max X) `1 <= (NE-corner X) `1 by A3, Th17, XBOOLE_1:17;
hence (NW-corner X) `1 <= (NE-corner X) `1 by A5, XXREAL_0:2; ::_thesis: ( (N-min X) `1 <= (N-max X) `1 & (N-min X) `1 <= (NE-corner X) `1 & (N-max X) `1 <= (NE-corner X) `1 )
thus (N-min X) `1 <= (N-max X) `1 by A1, A3, Th7; ::_thesis: ( (N-min X) `1 <= (NE-corner X) `1 & (N-max X) `1 <= (NE-corner X) `1 )
thus (N-min X) `1 <= (NE-corner X) `1 by A4, A7, XXREAL_0:2; ::_thesis: (N-max X) `1 <= (NE-corner X) `1
thus (N-max X) `1 <= (NE-corner X) `1 by A3, A6, Th17, XBOOLE_1:17; ::_thesis: verum
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 ) ) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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 ) ) )
let Z be non empty Subset of (TOP-REAL 2); ::_thesis: ( p in N-most Z implies ( p `2 = (N-min Z) `2 & ( Z is compact implies ( (N-min Z) `1 <= p `1 & p `1 <= (N-max Z) `1 ) ) ) )
A1: ( (NW-corner Z) `2 = N-bound Z & (N-min Z) `2 = N-bound Z ) by EUCLID:52;
A2: (NE-corner Z) `2 = N-bound Z by EUCLID:52;
assume A3: p in N-most Z ; ::_thesis: ( p `2 = (N-min Z) `2 & ( Z is compact implies ( (N-min Z) `1 <= p `1 & p `1 <= (N-max Z) `1 ) ) )
then p in LSeg ((NW-corner Z),(NE-corner Z)) by XBOOLE_0:def_4;
hence p `2 = (N-min Z) `2 by A1, A2, GOBOARD7:6; ::_thesis: ( Z is compact implies ( (N-min Z) `1 <= p `1 & p `1 <= (N-max Z) `1 ) )
assume Z is compact ; ::_thesis: ( (N-min Z) `1 <= p `1 & p `1 <= (N-max Z) `1 )
then reconsider Z = Z as non empty compact Subset of (TOP-REAL 2) ;
( (N-min Z) `1 = lower_bound (proj1 | (N-most Z)) & (N-max Z) `1 = upper_bound (proj1 | (N-most Z)) ) by EUCLID:52;
hence ( (N-min Z) `1 <= p `1 & p `1 <= (N-max Z) `1 ) by A3, Lm3; ::_thesis: verum
end;
theorem Th40: :: PSCOMP_1:40
for X being non empty compact Subset of (TOP-REAL 2) holds N-most X c= LSeg ((N-min X),(N-max X))
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: N-most X c= LSeg ((N-min X),(N-max X))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N-most X or x in LSeg ((N-min X),(N-max X)) )
assume A1: x in N-most X ; ::_thesis: x in LSeg ((N-min X),(N-max X))
then reconsider p = x as Point of (TOP-REAL 2) ;
A2: p `1 <= (N-max X) `1 by A1, Th39;
A3: (N-min X) `2 = (N-max X) `2 by Th37;
( p `2 = (N-min X) `2 & (N-min X) `1 <= p `1 ) by A1, Th39;
hence x in LSeg ((N-min X),(N-max X)) by A3, A2, GOBOARD7:8; ::_thesis: verum
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
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: LSeg ((N-min X),(N-max X)) c= LSeg ((NW-corner X),(NE-corner X))
A1: ( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
A2: (N-max X) `1 <= (NE-corner X) `1 by Th38;
( (N-max X) `2 = N-bound X & (NW-corner X) `1 <= (N-max X) `1 ) by Th38, EUCLID:52;
then A3: N-max X in LSeg ((NW-corner X),(NE-corner X)) by A1, A2, GOBOARD7:8;
A4: (N-min X) `1 <= (NE-corner X) `1 by Th38;
( (N-min X) `2 = N-bound X & (NW-corner X) `1 <= (N-min X) `1 ) by Th38, EUCLID:52;
then N-min X in LSeg ((NW-corner X),(NE-corner X)) by A1, A4, GOBOARD7:8;
hence LSeg ((N-min X),(N-max X)) c= LSeg ((NW-corner X),(NE-corner X)) by A3, TOPREAL1:6; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( N-min X in N-most X & N-max X in N-most X )
set p2W = proj1 | (N-most X);
set c = the carrier of ((TOP-REAL 2) | (N-most X));
A1: ( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
(proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X)) is with_min by MEASURE6:def_13;
then lower_bound ((proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X))) in (proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X)) by MEASURE6:def_5;
then consider p being set such that
A2: p in the carrier of ((TOP-REAL 2) | (N-most X)) and
p in the carrier of ((TOP-REAL 2) | (N-most X)) and
A3: lower_bound ((proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X))) = (proj1 | (N-most X)) . p by FUNCT_2:64;
A4: the carrier of ((TOP-REAL 2) | (N-most X)) = N-most X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
p in LSeg ((NW-corner X),(NE-corner X)) by A4, A2, XBOOLE_0:def_4;
then A5: p `2 = N-bound X by A1, GOBOARD7:6;
A6: ( (NW-corner X) `2 = N-bound X & (NE-corner X) `2 = N-bound X ) by EUCLID:52;
(proj1 | (N-most X)) . p = p `1 by A4, A2, Th22;
hence N-min X in N-most X by A4, A2, A3, A5, EUCLID:53; ::_thesis: N-max X in N-most X
(proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X)) is with_max by MEASURE6:def_12;
then upper_bound ((proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X))) in (proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X)) by MEASURE6:def_4;
then consider p being set such that
A7: p in the carrier of ((TOP-REAL 2) | (N-most X)) and
p in the carrier of ((TOP-REAL 2) | (N-most X)) and
A8: upper_bound ((proj1 | (N-most X)) .: the carrier of ((TOP-REAL 2) | (N-most X))) = (proj1 | (N-most X)) . p by FUNCT_2:64;
reconsider p = p as Point of (TOP-REAL 2) by A4, A7;
p in LSeg ((NW-corner X),(NE-corner X)) by A4, A7, XBOOLE_0:def_4;
then A9: p `2 = N-bound X by A6, GOBOARD7:6;
(proj1 | (N-most X)) . p = p `1 by A4, A7, Th22;
hence N-max X in N-most X by A4, A7, A8, A9, EUCLID:53; ::_thesis: verum
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)} )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (LSeg ((NW-corner X),(N-min X))) /\ X = {(N-min X)} & (LSeg ((N-max X),(NE-corner X))) /\ X = {(N-max X)} )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((NW-corner_X),(N-min_X)))_/\_X_implies_x_=_N-min_X_)_&_(_x_=_N-min_X_implies_x_in_(LSeg_((NW-corner_X),(N-min_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((NW-corner X),(N-min X))) /\ X implies x = N-min X ) & ( x = N-min X implies x in (LSeg ((NW-corner X),(N-min X))) /\ X ) )
A1: N-min X in LSeg ((NW-corner X),(N-min X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = N-min X implies x in (LSeg ((NW-corner X),(N-min X))) /\ X )
N-min X in N-most X by Th42;
then ( NW-corner X in LSeg ((NW-corner X),(NE-corner X)) & N-min X in LSeg ((NW-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A2: LSeg ((NW-corner X),(N-min X)) c= LSeg ((NW-corner X),(NE-corner X)) by TOPREAL1:6;
assume A3: x in (LSeg ((NW-corner X),(N-min X))) /\ X ; ::_thesis: x = N-min X
then A4: x in LSeg ((NW-corner X),(N-min X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A3;
x in X by A3, XBOOLE_0:def_4;
then p in N-most X by A4, A2, XBOOLE_0:def_4;
then A5: (N-min X) `1 <= p `1 by Th39;
(NW-corner X) `1 <= (N-min X) `1 by Th38;
then p `1 <= (N-min X) `1 by A4, TOPREAL1:3;
then A6: p `1 = (N-min X) `1 by A5, XXREAL_0:1;
(NW-corner X) `2 = (N-min X) `2 by Th37;
then A7: p `2 = (N-min X) `2 by A4, GOBOARD7:6;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = N-min X by A7, A6, EUCLID:53; ::_thesis: verum
end;
N-min X in N-most X by Th42;
then A8: N-min X in X by XBOOLE_0:def_4;
assume x = N-min X ; ::_thesis: x in (LSeg ((NW-corner X),(N-min X))) /\ X
hence x in (LSeg ((NW-corner X),(N-min X))) /\ X by A8, A1, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((NW-corner X),(N-min X))) /\ X = {(N-min X)} by TARSKI:def_1; ::_thesis: (LSeg ((N-max X),(NE-corner X))) /\ X = {(N-max X)}
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((N-max_X),(NE-corner_X)))_/\_X_implies_x_=_N-max_X_)_&_(_x_=_N-max_X_implies_x_in_(LSeg_((N-max_X),(NE-corner_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((N-max X),(NE-corner X))) /\ X implies x = N-max X ) & ( x = N-max X implies x in (LSeg ((N-max X),(NE-corner X))) /\ X ) )
A9: N-max X in LSeg ((N-max X),(NE-corner X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = N-max X implies x in (LSeg ((N-max X),(NE-corner X))) /\ X )
N-max X in N-most X by Th42;
then ( NE-corner X in LSeg ((NW-corner X),(NE-corner X)) & N-max X in LSeg ((NW-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A10: LSeg ((N-max X),(NE-corner X)) c= LSeg ((NW-corner X),(NE-corner X)) by TOPREAL1:6;
assume A11: x in (LSeg ((N-max X),(NE-corner X))) /\ X ; ::_thesis: x = N-max X
then A12: x in LSeg ((N-max X),(NE-corner X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A11;
x in X by A11, XBOOLE_0:def_4;
then p in N-most X by A12, A10, XBOOLE_0:def_4;
then A13: p `1 <= (N-max X) `1 by Th39;
(N-max X) `1 <= (NE-corner X) `1 by Th38;
then (N-max X) `1 <= p `1 by A12, TOPREAL1:3;
then A14: p `1 = (N-max X) `1 by A13, XXREAL_0:1;
(NE-corner X) `2 = (N-max X) `2 by Th37;
then A15: p `2 = (N-max X) `2 by A12, GOBOARD7:6;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = N-max X by A15, A14, EUCLID:53; ::_thesis: verum
end;
N-max X in N-most X by Th42;
then A16: N-max X in X by XBOOLE_0:def_4;
assume x = N-max X ; ::_thesis: x in (LSeg ((N-max X),(NE-corner X))) /\ X
hence x in (LSeg ((N-max X),(NE-corner X))) /\ X by A16, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((N-max X),(NE-corner X))) /\ X = {(N-max X)} by TARSKI:def_1; ::_thesis: verum
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)}
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( N-min X = N-max X implies N-most X = {(N-min X)} )
assume N-min X = N-max X ; ::_thesis: N-most X = {(N-min X)}
then N-most X c= LSeg ((N-min X),(N-min X)) by Th40;
then N-most X c= {(N-min X)} by RLTOPSP1:70;
hence N-most X = {(N-min X)} by ZFMISC_1:33; ::_thesis: verum
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 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( (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 )
( (E-min P) `1 = E-bound P & (E-max P) `1 = E-bound P ) by EUCLID:52;
hence ( (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 ) by EUCLID:52; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (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 )
set LX = E-most X;
A1: (E-min X) `2 = lower_bound (proj2 | (E-most X)) by EUCLID:52;
A2: (SE-corner X) `2 = lower_bound (proj2 | X) by EUCLID:52;
hence (SE-corner X) `2 <= (E-min X) `2 by A1, Th16, XBOOLE_1:17; ::_thesis: ( (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 )
A3: (E-max X) `2 = upper_bound (proj2 | (E-most X)) by EUCLID:52;
then A4: (E-min X) `2 <= (E-max X) `2 by A1, Th7;
(SE-corner X) `2 <= (E-min X) `2 by A2, A1, Th16, XBOOLE_1:17;
hence A5: (SE-corner X) `2 <= (E-max X) `2 by A4, XXREAL_0:2; ::_thesis: ( (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 )
A6: (NE-corner X) `2 = upper_bound (proj2 | X) by EUCLID:52;
then A7: (E-max X) `2 <= (NE-corner X) `2 by A3, Th17, XBOOLE_1:17;
hence (SE-corner X) `2 <= (NE-corner X) `2 by A5, XXREAL_0:2; ::_thesis: ( (E-min X) `2 <= (E-max X) `2 & (E-min X) `2 <= (NE-corner X) `2 & (E-max X) `2 <= (NE-corner X) `2 )
thus (E-min X) `2 <= (E-max X) `2 by A1, A3, Th7; ::_thesis: ( (E-min X) `2 <= (NE-corner X) `2 & (E-max X) `2 <= (NE-corner X) `2 )
thus (E-min X) `2 <= (NE-corner X) `2 by A4, A7, XXREAL_0:2; ::_thesis: (E-max X) `2 <= (NE-corner X) `2
thus (E-max X) `2 <= (NE-corner X) `2 by A3, A6, Th17, XBOOLE_1:17; ::_thesis: verum
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 ) ) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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 ) ) )
let Z be non empty Subset of (TOP-REAL 2); ::_thesis: ( p in E-most Z implies ( p `1 = (E-min Z) `1 & ( Z is compact implies ( (E-min Z) `2 <= p `2 & p `2 <= (E-max Z) `2 ) ) ) )
A1: ( (SE-corner Z) `1 = E-bound Z & (E-min Z) `1 = E-bound Z ) by EUCLID:52;
A2: (NE-corner Z) `1 = E-bound Z by EUCLID:52;
assume A3: p in E-most Z ; ::_thesis: ( p `1 = (E-min Z) `1 & ( Z is compact implies ( (E-min Z) `2 <= p `2 & p `2 <= (E-max Z) `2 ) ) )
then p in LSeg ((SE-corner Z),(NE-corner Z)) by XBOOLE_0:def_4;
hence p `1 = (E-min Z) `1 by A1, A2, GOBOARD7:5; ::_thesis: ( Z is compact implies ( (E-min Z) `2 <= p `2 & p `2 <= (E-max Z) `2 ) )
assume Z is compact ; ::_thesis: ( (E-min Z) `2 <= p `2 & p `2 <= (E-max Z) `2 )
then reconsider Z = Z as non empty compact Subset of (TOP-REAL 2) ;
( (E-min Z) `2 = lower_bound (proj2 | (E-most Z)) & (E-max Z) `2 = upper_bound (proj2 | (E-most Z)) ) by EUCLID:52;
hence ( (E-min Z) `2 <= p `2 & p `2 <= (E-max Z) `2 ) by A3, Lm3; ::_thesis: verum
end;
theorem Th48: :: PSCOMP_1:48
for X being non empty compact Subset of (TOP-REAL 2) holds E-most X c= LSeg ((E-min X),(E-max X))
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: E-most X c= LSeg ((E-min X),(E-max X))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E-most X or x in LSeg ((E-min X),(E-max X)) )
assume A1: x in E-most X ; ::_thesis: x in LSeg ((E-min X),(E-max X))
then reconsider p = x as Point of (TOP-REAL 2) ;
A2: p `2 <= (E-max X) `2 by A1, Th47;
A3: (E-min X) `1 = (E-max X) `1 by Th45;
( p `1 = (E-min X) `1 & (E-min X) `2 <= p `2 ) by A1, Th47;
hence x in LSeg ((E-min X),(E-max X)) by A3, A2, GOBOARD7:7; ::_thesis: verum
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
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: LSeg ((E-min X),(E-max X)) c= LSeg ((SE-corner X),(NE-corner X))
A1: ( (SE-corner X) `1 = E-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:52;
A2: (E-max X) `2 <= (NE-corner X) `2 by Th46;
( (E-max X) `1 = E-bound X & (SE-corner X) `2 <= (E-max X) `2 ) by Th46, EUCLID:52;
then A3: E-max X in LSeg ((SE-corner X),(NE-corner X)) by A1, A2, GOBOARD7:7;
A4: (E-min X) `2 <= (NE-corner X) `2 by Th46;
( (E-min X) `1 = E-bound X & (SE-corner X) `2 <= (E-min X) `2 ) by Th46, EUCLID:52;
then E-min X in LSeg ((SE-corner X),(NE-corner X)) by A1, A4, GOBOARD7:7;
hence LSeg ((E-min X),(E-max X)) c= LSeg ((SE-corner X),(NE-corner X)) by A3, TOPREAL1:6; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( E-min X in E-most X & E-max X in E-most X )
set p2W = proj2 | (E-most X);
set c = the carrier of ((TOP-REAL 2) | (E-most X));
A1: ( (SE-corner X) `1 = E-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:52;
(proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) is with_min by MEASURE6:def_13;
then lower_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) in (proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) by MEASURE6:def_5;
then consider p being set such that
A2: p in the carrier of ((TOP-REAL 2) | (E-most X)) and
p in the carrier of ((TOP-REAL 2) | (E-most X)) and
A3: lower_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) = (proj2 | (E-most X)) . p by FUNCT_2:64;
A4: the carrier of ((TOP-REAL 2) | (E-most X)) = E-most X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
p in LSeg ((SE-corner X),(NE-corner X)) by A4, A2, XBOOLE_0:def_4;
then A5: p `1 = E-bound X by A1, GOBOARD7:5;
A6: ( (SE-corner X) `1 = E-bound X & (NE-corner X) `1 = E-bound X ) by EUCLID:52;
(proj2 | (E-most X)) . p = p `2 by A4, A2, Th23;
hence E-min X in E-most X by A4, A2, A3, A5, EUCLID:53; ::_thesis: E-max X in E-most X
(proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) is with_max by MEASURE6:def_12;
then upper_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) in (proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X)) by MEASURE6:def_4;
then consider p being set such that
A7: p in the carrier of ((TOP-REAL 2) | (E-most X)) and
p in the carrier of ((TOP-REAL 2) | (E-most X)) and
A8: upper_bound ((proj2 | (E-most X)) .: the carrier of ((TOP-REAL 2) | (E-most X))) = (proj2 | (E-most X)) . p by FUNCT_2:64;
reconsider p = p as Point of (TOP-REAL 2) by A4, A7;
p in LSeg ((SE-corner X),(NE-corner X)) by A4, A7, XBOOLE_0:def_4;
then A9: p `1 = E-bound X by A6, GOBOARD7:5;
(proj2 | (E-most X)) . p = p `2 by A4, A7, Th23;
hence E-max X in E-most X by A4, A7, A8, A9, EUCLID:53; ::_thesis: verum
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)} )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (LSeg ((SE-corner X),(E-min X))) /\ X = {(E-min X)} & (LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)} )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((SE-corner_X),(E-min_X)))_/\_X_implies_x_=_E-min_X_)_&_(_x_=_E-min_X_implies_x_in_(LSeg_((SE-corner_X),(E-min_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((SE-corner X),(E-min X))) /\ X implies x = E-min X ) & ( x = E-min X implies x in (LSeg ((SE-corner X),(E-min X))) /\ X ) )
A1: E-min X in LSeg ((SE-corner X),(E-min X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = E-min X implies x in (LSeg ((SE-corner X),(E-min X))) /\ X )
E-min X in E-most X by Th50;
then ( SE-corner X in LSeg ((SE-corner X),(NE-corner X)) & E-min X in LSeg ((SE-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A2: LSeg ((SE-corner X),(E-min X)) c= LSeg ((SE-corner X),(NE-corner X)) by TOPREAL1:6;
assume A3: x in (LSeg ((SE-corner X),(E-min X))) /\ X ; ::_thesis: x = E-min X
then A4: x in LSeg ((SE-corner X),(E-min X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A3;
x in X by A3, XBOOLE_0:def_4;
then p in E-most X by A4, A2, XBOOLE_0:def_4;
then A5: (E-min X) `2 <= p `2 by Th47;
(SE-corner X) `2 <= (E-min X) `2 by Th46;
then p `2 <= (E-min X) `2 by A4, TOPREAL1:4;
then A6: p `2 = (E-min X) `2 by A5, XXREAL_0:1;
(SE-corner X) `1 = (E-min X) `1 by Th45;
then A7: p `1 = (E-min X) `1 by A4, GOBOARD7:5;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = E-min X by A7, A6, EUCLID:53; ::_thesis: verum
end;
E-min X in E-most X by Th50;
then A8: E-min X in X by XBOOLE_0:def_4;
assume x = E-min X ; ::_thesis: x in (LSeg ((SE-corner X),(E-min X))) /\ X
hence x in (LSeg ((SE-corner X),(E-min X))) /\ X by A8, A1, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((SE-corner X),(E-min X))) /\ X = {(E-min X)} by TARSKI:def_1; ::_thesis: (LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)}
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((E-max_X),(NE-corner_X)))_/\_X_implies_x_=_E-max_X_)_&_(_x_=_E-max_X_implies_x_in_(LSeg_((E-max_X),(NE-corner_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((E-max X),(NE-corner X))) /\ X implies x = E-max X ) & ( x = E-max X implies x in (LSeg ((E-max X),(NE-corner X))) /\ X ) )
A9: E-max X in LSeg ((E-max X),(NE-corner X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = E-max X implies x in (LSeg ((E-max X),(NE-corner X))) /\ X )
E-max X in E-most X by Th50;
then ( NE-corner X in LSeg ((SE-corner X),(NE-corner X)) & E-max X in LSeg ((SE-corner X),(NE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A10: LSeg ((E-max X),(NE-corner X)) c= LSeg ((SE-corner X),(NE-corner X)) by TOPREAL1:6;
assume A11: x in (LSeg ((E-max X),(NE-corner X))) /\ X ; ::_thesis: x = E-max X
then A12: x in LSeg ((E-max X),(NE-corner X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A11;
x in X by A11, XBOOLE_0:def_4;
then p in E-most X by A12, A10, XBOOLE_0:def_4;
then A13: p `2 <= (E-max X) `2 by Th47;
(E-max X) `2 <= (NE-corner X) `2 by Th46;
then (E-max X) `2 <= p `2 by A12, TOPREAL1:4;
then A14: p `2 = (E-max X) `2 by A13, XXREAL_0:1;
(NE-corner X) `1 = (E-max X) `1 by Th45;
then A15: p `1 = (E-max X) `1 by A12, GOBOARD7:5;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = E-max X by A15, A14, EUCLID:53; ::_thesis: verum
end;
E-max X in E-most X by Th50;
then A16: E-max X in X by XBOOLE_0:def_4;
assume x = E-max X ; ::_thesis: x in (LSeg ((E-max X),(NE-corner X))) /\ X
hence x in (LSeg ((E-max X),(NE-corner X))) /\ X by A16, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((E-max X),(NE-corner X))) /\ X = {(E-max X)} by TARSKI:def_1; ::_thesis: verum
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)}
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( E-min X = E-max X implies E-most X = {(E-min X)} )
assume E-min X = E-max X ; ::_thesis: E-most X = {(E-min X)}
then E-most X c= LSeg ((E-min X),(E-min X)) by Th48;
then E-most X c= {(E-min X)} by RLTOPSP1:70;
hence E-most X = {(E-min X)} by ZFMISC_1:33; ::_thesis: verum
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 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( (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 )
( (S-min P) `2 = S-bound P & (S-max P) `2 = S-bound P ) by EUCLID:52;
hence ( (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 ) by EUCLID:52; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (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 )
set LX = S-most X;
A1: (S-min X) `1 = lower_bound (proj1 | (S-most X)) by EUCLID:52;
A2: (SW-corner X) `1 = lower_bound (proj1 | X) by EUCLID:52;
hence (SW-corner X) `1 <= (S-min X) `1 by A1, Th16, XBOOLE_1:17; ::_thesis: ( (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 )
A3: (S-max X) `1 = upper_bound (proj1 | (S-most X)) by EUCLID:52;
then A4: (S-min X) `1 <= (S-max X) `1 by A1, Th7;
(SW-corner X) `1 <= (S-min X) `1 by A2, A1, Th16, XBOOLE_1:17;
hence A5: (SW-corner X) `1 <= (S-max X) `1 by A4, XXREAL_0:2; ::_thesis: ( (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 )
A6: (SE-corner X) `1 = upper_bound (proj1 | X) by EUCLID:52;
then A7: (S-max X) `1 <= (SE-corner X) `1 by A3, Th17, XBOOLE_1:17;
hence (SW-corner X) `1 <= (SE-corner X) `1 by A5, XXREAL_0:2; ::_thesis: ( (S-min X) `1 <= (S-max X) `1 & (S-min X) `1 <= (SE-corner X) `1 & (S-max X) `1 <= (SE-corner X) `1 )
thus (S-min X) `1 <= (S-max X) `1 by A1, A3, Th7; ::_thesis: ( (S-min X) `1 <= (SE-corner X) `1 & (S-max X) `1 <= (SE-corner X) `1 )
thus (S-min X) `1 <= (SE-corner X) `1 by A4, A7, XXREAL_0:2; ::_thesis: (S-max X) `1 <= (SE-corner X) `1
thus (S-max X) `1 <= (SE-corner X) `1 by A3, A6, Th17, XBOOLE_1:17; ::_thesis: verum
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 ) ) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: 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 ) ) )
let Z be non empty Subset of (TOP-REAL 2); ::_thesis: ( p in S-most Z implies ( p `2 = (S-min Z) `2 & ( Z is compact implies ( (S-min Z) `1 <= p `1 & p `1 <= (S-max Z) `1 ) ) ) )
A1: ( (SW-corner Z) `2 = S-bound Z & (S-min Z) `2 = S-bound Z ) by EUCLID:52;
A2: (SE-corner Z) `2 = S-bound Z by EUCLID:52;
assume A3: p in S-most Z ; ::_thesis: ( p `2 = (S-min Z) `2 & ( Z is compact implies ( (S-min Z) `1 <= p `1 & p `1 <= (S-max Z) `1 ) ) )
then p in LSeg ((SW-corner Z),(SE-corner Z)) by XBOOLE_0:def_4;
hence p `2 = (S-min Z) `2 by A1, A2, GOBOARD7:6; ::_thesis: ( Z is compact implies ( (S-min Z) `1 <= p `1 & p `1 <= (S-max Z) `1 ) )
assume Z is compact ; ::_thesis: ( (S-min Z) `1 <= p `1 & p `1 <= (S-max Z) `1 )
then reconsider Z = Z as non empty compact Subset of (TOP-REAL 2) ;
( (S-min Z) `1 = lower_bound (proj1 | (S-most Z)) & (S-max Z) `1 = upper_bound (proj1 | (S-most Z)) ) by EUCLID:52;
hence ( (S-min Z) `1 <= p `1 & p `1 <= (S-max Z) `1 ) by A3, Lm3; ::_thesis: verum
end;
theorem Th56: :: PSCOMP_1:56
for X being non empty compact Subset of (TOP-REAL 2) holds S-most X c= LSeg ((S-min X),(S-max X))
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: S-most X c= LSeg ((S-min X),(S-max X))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S-most X or x in LSeg ((S-min X),(S-max X)) )
assume A1: x in S-most X ; ::_thesis: x in LSeg ((S-min X),(S-max X))
then reconsider p = x as Point of (TOP-REAL 2) ;
A2: p `1 <= (S-max X) `1 by A1, Th55;
A3: (S-min X) `2 = (S-max X) `2 by Th53;
( p `2 = (S-min X) `2 & (S-min X) `1 <= p `1 ) by A1, Th55;
hence x in LSeg ((S-min X),(S-max X)) by A3, A2, GOBOARD7:8; ::_thesis: verum
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
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: LSeg ((S-min X),(S-max X)) c= LSeg ((SW-corner X),(SE-corner X))
A1: ( (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:52;
A2: (S-max X) `1 <= (SE-corner X) `1 by Th54;
( (S-max X) `2 = S-bound X & (SW-corner X) `1 <= (S-max X) `1 ) by Th54, EUCLID:52;
then A3: S-max X in LSeg ((SW-corner X),(SE-corner X)) by A1, A2, GOBOARD7:8;
A4: (S-min X) `1 <= (SE-corner X) `1 by Th54;
( (S-min X) `2 = S-bound X & (SW-corner X) `1 <= (S-min X) `1 ) by Th54, EUCLID:52;
then S-min X in LSeg ((SW-corner X),(SE-corner X)) by A1, A4, GOBOARD7:8;
hence LSeg ((S-min X),(S-max X)) c= LSeg ((SW-corner X),(SE-corner X)) by A3, TOPREAL1:6; ::_thesis: verum
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 )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( S-min X in S-most X & S-max X in S-most X )
set p2W = proj1 | (S-most X);
set c = the carrier of ((TOP-REAL 2) | (S-most X));
A1: ( (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:52;
(proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X)) is with_min by MEASURE6:def_13;
then lower_bound ((proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X))) in (proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X)) by MEASURE6:def_5;
then consider p being set such that
A2: p in the carrier of ((TOP-REAL 2) | (S-most X)) and
p in the carrier of ((TOP-REAL 2) | (S-most X)) and
A3: lower_bound ((proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X))) = (proj1 | (S-most X)) . p by FUNCT_2:64;
A4: the carrier of ((TOP-REAL 2) | (S-most X)) = S-most X by PRE_TOPC:8;
then reconsider p = p as Point of (TOP-REAL 2) by A2;
p in LSeg ((SW-corner X),(SE-corner X)) by A4, A2, XBOOLE_0:def_4;
then A5: p `2 = S-bound X by A1, GOBOARD7:6;
A6: ( (SW-corner X) `2 = S-bound X & (SE-corner X) `2 = S-bound X ) by EUCLID:52;
(proj1 | (S-most X)) . p = p `1 by A4, A2, Th22;
hence S-min X in S-most X by A4, A2, A3, A5, EUCLID:53; ::_thesis: S-max X in S-most X
(proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X)) is with_max by MEASURE6:def_12;
then upper_bound ((proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X))) in (proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X)) by MEASURE6:def_4;
then consider p being set such that
A7: p in the carrier of ((TOP-REAL 2) | (S-most X)) and
p in the carrier of ((TOP-REAL 2) | (S-most X)) and
A8: upper_bound ((proj1 | (S-most X)) .: the carrier of ((TOP-REAL 2) | (S-most X))) = (proj1 | (S-most X)) . p by FUNCT_2:64;
reconsider p = p as Point of (TOP-REAL 2) by A4, A7;
p in LSeg ((SW-corner X),(SE-corner X)) by A4, A7, XBOOLE_0:def_4;
then A9: p `2 = S-bound X by A6, GOBOARD7:6;
(proj1 | (S-most X)) . p = p `1 by A4, A7, Th22;
hence S-max X in S-most X by A4, A7, A8, A9, EUCLID:53; ::_thesis: verum
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)} )
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( (LSeg ((SW-corner X),(S-min X))) /\ X = {(S-min X)} & (LSeg ((S-max X),(SE-corner X))) /\ X = {(S-max X)} )
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((SW-corner_X),(S-min_X)))_/\_X_implies_x_=_S-min_X_)_&_(_x_=_S-min_X_implies_x_in_(LSeg_((SW-corner_X),(S-min_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((SW-corner X),(S-min X))) /\ X implies x = S-min X ) & ( x = S-min X implies x in (LSeg ((SW-corner X),(S-min X))) /\ X ) )
A1: S-min X in LSeg ((SW-corner X),(S-min X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = S-min X implies x in (LSeg ((SW-corner X),(S-min X))) /\ X )
S-min X in S-most X by Th58;
then ( SW-corner X in LSeg ((SW-corner X),(SE-corner X)) & S-min X in LSeg ((SW-corner X),(SE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A2: LSeg ((SW-corner X),(S-min X)) c= LSeg ((SW-corner X),(SE-corner X)) by TOPREAL1:6;
assume A3: x in (LSeg ((SW-corner X),(S-min X))) /\ X ; ::_thesis: x = S-min X
then A4: x in LSeg ((SW-corner X),(S-min X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A3;
x in X by A3, XBOOLE_0:def_4;
then p in S-most X by A4, A2, XBOOLE_0:def_4;
then A5: (S-min X) `1 <= p `1 by Th55;
(SW-corner X) `1 <= (S-min X) `1 by Th54;
then p `1 <= (S-min X) `1 by A4, TOPREAL1:3;
then A6: p `1 = (S-min X) `1 by A5, XXREAL_0:1;
(SW-corner X) `2 = (S-min X) `2 by Th53;
then A7: p `2 = (S-min X) `2 by A4, GOBOARD7:6;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = S-min X by A7, A6, EUCLID:53; ::_thesis: verum
end;
S-min X in S-most X by Th58;
then A8: S-min X in X by XBOOLE_0:def_4;
assume x = S-min X ; ::_thesis: x in (LSeg ((SW-corner X),(S-min X))) /\ X
hence x in (LSeg ((SW-corner X),(S-min X))) /\ X by A8, A1, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((SW-corner X),(S-min X))) /\ X = {(S-min X)} by TARSKI:def_1; ::_thesis: (LSeg ((S-max X),(SE-corner X))) /\ X = {(S-max X)}
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(LSeg_((S-max_X),(SE-corner_X)))_/\_X_implies_x_=_S-max_X_)_&_(_x_=_S-max_X_implies_x_in_(LSeg_((S-max_X),(SE-corner_X)))_/\_X_)_)
let x be set ; ::_thesis: ( ( x in (LSeg ((S-max X),(SE-corner X))) /\ X implies x = S-max X ) & ( x = S-max X implies x in (LSeg ((S-max X),(SE-corner X))) /\ X ) )
A9: S-max X in LSeg ((S-max X),(SE-corner X)) by RLTOPSP1:68;
hereby ::_thesis: ( x = S-max X implies x in (LSeg ((S-max X),(SE-corner X))) /\ X )
S-max X in S-most X by Th58;
then ( SE-corner X in LSeg ((SW-corner X),(SE-corner X)) & S-max X in LSeg ((SW-corner X),(SE-corner X)) ) by RLTOPSP1:68, XBOOLE_0:def_4;
then A10: LSeg ((S-max X),(SE-corner X)) c= LSeg ((SW-corner X),(SE-corner X)) by TOPREAL1:6;
assume A11: x in (LSeg ((S-max X),(SE-corner X))) /\ X ; ::_thesis: x = S-max X
then A12: x in LSeg ((S-max X),(SE-corner X)) by XBOOLE_0:def_4;
reconsider p = x as Point of (TOP-REAL 2) by A11;
x in X by A11, XBOOLE_0:def_4;
then p in S-most X by A12, A10, XBOOLE_0:def_4;
then A13: p `1 <= (S-max X) `1 by Th55;
(S-max X) `1 <= (SE-corner X) `1 by Th54;
then (S-max X) `1 <= p `1 by A12, TOPREAL1:3;
then A14: p `1 = (S-max X) `1 by A13, XXREAL_0:1;
(SE-corner X) `2 = (S-max X) `2 by Th53;
then A15: p `2 = (S-max X) `2 by A12, GOBOARD7:6;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence x = S-max X by A15, A14, EUCLID:53; ::_thesis: verum
end;
S-max X in S-most X by Th58;
then A16: S-max X in X by XBOOLE_0:def_4;
assume x = S-max X ; ::_thesis: x in (LSeg ((S-max X),(SE-corner X))) /\ X
hence x in (LSeg ((S-max X),(SE-corner X))) /\ X by A16, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg ((S-max X),(SE-corner X))) /\ X = {(S-max X)} by TARSKI:def_1; ::_thesis: verum
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)}
proof
let X be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( S-min X = S-max X implies S-most X = {(S-min X)} )
assume S-min X = S-max X ; ::_thesis: S-most X = {(S-min X)}
then S-most X c= LSeg ((S-min X),(S-min X)) by Th56;
then S-most X c= {(S-min X)} by RLTOPSP1:70;
hence S-most X = {(S-min X)} by ZFMISC_1:33; ::_thesis: verum
end;
theorem :: PSCOMP_1:61
for P being Subset of (TOP-REAL 2) st W-max P = N-min P holds
W-max P = NW-corner P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( W-max P = N-min P implies W-max P = NW-corner P )
A1: (W-max P) `1 = W-bound P by EUCLID:52;
assume W-max P = N-min P ; ::_thesis: W-max P = NW-corner P
hence W-max P = NW-corner P by A1, EUCLID:52; ::_thesis: verum
end;
theorem :: PSCOMP_1:62
for P being Subset of (TOP-REAL 2) st N-max P = E-max P holds
N-max P = NE-corner P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( N-max P = E-max P implies N-max P = NE-corner P )
A1: (N-max P) `2 = N-bound P by EUCLID:52;
assume N-max P = E-max P ; ::_thesis: N-max P = NE-corner P
hence N-max P = NE-corner P by A1, EUCLID:52; ::_thesis: verum
end;
theorem :: PSCOMP_1:63
for P being Subset of (TOP-REAL 2) st E-min P = S-max P holds
E-min P = SE-corner P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( E-min P = S-max P implies E-min P = SE-corner P )
A1: (E-min P) `1 = E-bound P by EUCLID:52;
assume E-min P = S-max P ; ::_thesis: E-min P = SE-corner P
hence E-min P = SE-corner P by A1, EUCLID:52; ::_thesis: verum
end;
theorem :: PSCOMP_1:64
for P being Subset of (TOP-REAL 2) st S-min P = W-min P holds
S-min P = SW-corner P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( S-min P = W-min P implies S-min P = SW-corner P )
A1: (S-min P) `2 = S-bound P by EUCLID:52;
assume S-min P = W-min P ; ::_thesis: S-min P = SW-corner P
hence S-min P = SW-corner P by A1, EUCLID:52; ::_thesis: verum
end;
theorem :: PSCOMP_1:65
for r, s being real number holds
( proj2 . |[r,s]| = s & proj1 . |[r,s]| = r )
proof
let r, s be real number ; ::_thesis: ( proj2 . |[r,s]| = s & proj1 . |[r,s]| = r )
thus proj2 . |[r,s]| = |[r,s]| `2 by Def6
.= s by EUCLID:52 ; ::_thesis: proj1 . |[r,s]| = r
thus proj1 . |[r,s]| = |[r,s]| `1 by Def5
.= r by EUCLID:52 ; ::_thesis: verum
end;
theorem :: PSCOMP_1:66
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 Th17;
theorem :: PSCOMP_1:67
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 Th17;
theorem :: PSCOMP_1:68
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 Th16;
theorem :: PSCOMP_1:69
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 Th16;