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