:: JORDAN5A semantic presentation begin theorem Th1: :: JORDAN5A:1 for n being Element of NAT for p, q being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds P is compact proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds P is compact let p, q be Point of (TOP-REAL n); ::_thesis: for P being Subset of (TOP-REAL n) st P is_an_arc_of p,q holds P is compact let P be Subset of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p,q implies P is compact ) assume P is_an_arc_of p,q ; ::_thesis: P is compact then consider f being Function of I[01],((TOP-REAL n) | P) such that A1: f is being_homeomorphism and f . 0 = p and f . 1 = q by TOPREAL1:def_1; percases ( P <> {} or P = {} (TOP-REAL n) ) ; suppose P <> {} ; ::_thesis: P is compact then reconsider P9 = P as non empty Subset of (TOP-REAL n) ; ( f is continuous & rng f = [#] ((TOP-REAL n) | P9) ) by A1, TOPS_2:def_5; then (TOP-REAL n) | P9 is compact by COMPTS_1:14; hence P is compact by COMPTS_1:3; ::_thesis: verum end; suppose P = {} (TOP-REAL n) ; ::_thesis: P is compact hence P is compact ; ::_thesis: verum end; end; end; Lm1: for n being Element of NAT holds ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n ) proof let n be Element of NAT ; ::_thesis: ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n ) Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) by EUCLID:def_7; hence ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n ) by EUCLID:67; ::_thesis: verum end; theorem Th2: :: JORDAN5A:2 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for r1, r2 being real number holds ( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 ) proof let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) for r1, r2 being real number holds ( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 ) let p1, p2 be Point of (TOP-REAL n); ::_thesis: for r1, r2 being real number holds ( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 ) let r1, r2 be real number ; ::_thesis: ( not ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or r1 = r2 or p1 = p2 ) assume A1: ((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: ( r1 = r2 or p1 = p2 ) A2: (1 * p1) + ((- (r1 * p1)) + (r1 * p2)) = ((1 * p1) + (- (r1 * p1))) + (r1 * p2) by EUCLID:26 .= ((1 * p1) - (r1 * p1)) + (r1 * p2) by EUCLID:41 .= ((1 - r2) * p1) + (r2 * p2) by A1, EUCLID:50 .= ((1 * p1) - (r2 * p1)) + (r2 * p2) by EUCLID:50 .= ((1 * p1) + (- (r2 * p1))) + (r2 * p2) by EUCLID:41 .= (1 * p1) + ((- (r2 * p1)) + (r2 * p2)) by EUCLID:26 ; A3: ((r2 - r1) * p1) + (r1 * p2) = ((r2 * p1) - (r1 * p1)) + (r1 * p2) by EUCLID:50 .= ((r2 * p1) + (- (r1 * p1))) + (r1 * p2) by EUCLID:41 .= (r2 * p1) + ((- (r1 * p1)) + (r1 * p2)) by EUCLID:26 .= (r2 * p1) + ((- (r2 * p1)) + (r2 * p2)) by A2, GOBOARD7:4 .= ((r2 * p1) + (- (r2 * p1))) + (r2 * p2) by EUCLID:26 .= (0. (TOP-REAL n)) + (r2 * p2) by EUCLID:36 .= r2 * p2 by EUCLID:27 ; (r2 - r1) * p1 = ((r2 - r1) * p1) + (0. (TOP-REAL n)) by EUCLID:27 .= ((r2 - r1) * p1) + ((r1 * p2) - (r1 * p2)) by EUCLID:42 .= (r2 * p2) - (r1 * p2) by A3, EUCLID:45 .= (r2 - r1) * p2 by EUCLID:50 ; then ( r2 - r1 = 0 or p1 = p2 ) by EUCLID:34; hence ( r1 = r2 or p1 = p2 ) ; ::_thesis: verum end; theorem Th3: :: JORDAN5A:3 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st ( ( for x being Real st x in [.0,1.] holds f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) proof let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st ( ( for x being Real st x in [.0,1.] holds f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p1 <> p2 implies ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st ( ( for x being Real st x in [.0,1.] holds f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) ) reconsider p19 = p1, p29 = p2 as Element of REAL n by Lm1; set P = LSeg (p1,p2); reconsider PP = LSeg (p1,p2) as Subset of (Euclid n) by TOPREAL3:8; reconsider PP = PP as non empty Subset of (Euclid n) ; defpred S1[ set , set ] means for x being Real st x = $1 holds $2 = ((1 - x) * p1) + (x * p2); A1: for a being set st a in [.0,1.] holds ex u being set st S1[a,u] proof let a be set ; ::_thesis: ( a in [.0,1.] implies ex u being set st S1[a,u] ) assume a in [.0,1.] ; ::_thesis: ex u being set st S1[a,u] then reconsider x = a as Real ; take ((1 - x) * p1) + (x * p2) ; ::_thesis: S1[a,((1 - x) * p1) + (x * p2)] thus S1[a,((1 - x) * p1) + (x * p2)] ; ::_thesis: verum end; consider f being Function such that A2: dom f = [.0,1.] and A3: for a being set st a in [.0,1.] holds S1[a,f . a] from CLASSES1:sch_1(A1); rng f c= the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ) assume y in rng f ; ::_thesis: y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) then consider x being set such that A4: x in dom f and A5: y = f . x by FUNCT_1:def_3; x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A2, A4, RCOMP_1:def_1; then consider r being Real such that A6: r = x and A7: ( 0 <= r & r <= 1 ) ; y = ((1 - r) * p1) + (r * p2) by A2, A3, A4, A5, A6; then y in LSeg (p1,p2) by A7; then y in [#] ((TOP-REAL n) | (LSeg (p1,p2))) by PRE_TOPC:def_5; hence y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: verum end; then reconsider f = f as Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) by A2, BORSUK_1:40, FUNCT_2:def_1, RELSET_1:4; assume A8: p1 <> p2 ; ::_thesis: ex f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) st ( ( for x being Real st x in [.0,1.] holds f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A9: x1 in dom f and A10: x2 in dom f and A11: f . x1 = f . x2 ; ::_thesis: x1 = x2 x2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A2, A10, RCOMP_1:def_1; then consider r2 being Real such that A12: r2 = x2 and 0 <= r2 and r2 <= 1 ; A13: f . x2 = ((1 - r2) * p1) + (r2 * p2) by A2, A3, A10, A12; x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A2, A9, RCOMP_1:def_1; then consider r1 being Real such that A14: r1 = x1 and 0 <= r1 and r1 <= 1 ; f . x1 = ((1 - r1) * p1) + (r1 * p2) by A2, A3, A9, A14; hence x1 = x2 by A8, A11, A14, A12, A13, Th2; ::_thesis: verum end; then A15: f is one-to-one by FUNCT_1:def_4; A16: (TOP-REAL n) | (LSeg (p1,p2)) = TopSpaceMetr ((Euclid n) | PP) by EUCLID:63; for W being Point of I[01] for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G proof reconsider p11 = p1, p22 = p2 as Point of (Euclid n) by TOPREAL3:8; let W be Point of I[01]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G reconsider W9 = W as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10; reconsider W1 = W as Real by BORSUK_1:40, TARSKI:def_3; f . W in Int G by CONNSP_2:def_1; then consider Q being Subset of ((TOP-REAL n) | (LSeg (p1,p2))) such that A17: Q is open and A18: Q c= G and A19: f . W in Q by TOPS_1:22; [#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5; then reconsider Y = f . W as Point of ((Euclid n) | PP) by TOPMETR:def_2; consider r being real number such that A20: r > 0 and A21: Ball (Y,r) c= Q by A16, A17, A19, TOPMETR:15; reconsider r = r as Element of REAL by XREAL_0:def_1; set delta = r / ((Pitag_dist n) . (p19,p29)); reconsider H = Ball (W9,(r / ((Pitag_dist n) . (p19,p29)))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10; Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7; then A22: H is open by TOPMETR:14, TOPMETR:20; LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2; then reconsider WW9 = Y as Point of (Euclid n) by TARSKI:def_3; Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) by EUCLID:def_7; then A23: (Pitag_dist n) . (p19,p29) = dist (p11,p22) by METRIC_1:def_1; A24: ( dist (p11,p22) >= 0 & dist (p11,p22) <> 0 ) by A8, METRIC_1:2, METRIC_1:5; then W in H by A20, A23, TBSP_1:11, XREAL_1:139; then W in Int H by A22, TOPS_1:23; then reconsider H = H as a_neighborhood of W by CONNSP_2:def_1; take H ; ::_thesis: f .: H c= G A25: r / ((Pitag_dist n) . (p19,p29)) > 0 by A20, A23, A24, XREAL_1:139; f .: H c= Ball (Y,r) proof reconsider WW1 = WW9 as Element of REAL n by Lm1; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in Ball (Y,r) ) A26: [#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5; assume a in f .: H ; ::_thesis: a in Ball (Y,r) then consider u being set such that A27: u in dom f and A28: u in H and A29: a = f . u by FUNCT_1:def_6; reconsider u1 = u as Real by A2, A27; A30: f . W = ((1 - W1) * p1) + (W1 * p2) by A3, BORSUK_1:40; reconsider u9 = u as Point of (Closed-Interval-MSpace (0,1)) by A28; reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR:8; A31: dist (W9,u9) = the distance of (Closed-Interval-MSpace (0,1)) . (W9,u9) by METRIC_1:def_1 .= the distance of RealSpace . (W99,u99) by TOPMETR:def_1 .= dist (W99,u99) by METRIC_1:def_1 ; dist (W9,u9) < r / ((Pitag_dist n) . (p19,p29)) by A28, METRIC_1:11; then abs (W1 - u1) < r / ((Pitag_dist n) . (p19,p29)) by A31, TOPMETR:11; then abs (- (u1 - W1)) < r / ((Pitag_dist n) . (p19,p29)) ; then A32: abs (u1 - W1) < r / ((Pitag_dist n) . (p19,p29)) by COMPLEX1:52; A33: r / ((Pitag_dist n) . (p19,p29)) <> 0 by A20, A23, A24, XREAL_1:139; then (Pitag_dist n) . (p19,p29) = r / (r / ((Pitag_dist n) . (p19,p29))) by XCMPLX_1:54; then A34: |.(p19 - p29).| = r / (r / ((Pitag_dist n) . (p19,p29))) by EUCLID:def_6; f . u in rng f by A27, FUNCT_1:def_3; then reconsider aa = a as Point of ((Euclid n) | PP) by A29, A26, TOPMETR:def_2; LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2; then reconsider aa9 = aa as Point of (Euclid n) by TARSKI:def_3; reconsider aa1 = aa9 as Element of REAL n by Lm1; aa1 = ((1 - u1) * p1) + (u1 * p2) by A2, A3, A27, A29; then WW1 - aa1 = (((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2)) by A30 .= (((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2) by EUCLID:46 .= ((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2) by EUCLID:45 .= ((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2) by EUCLID:50 .= ((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2)) by EUCLID:45 .= ((u1 - W1) * p1) + ((W1 - u1) * p2) by EUCLID:50 .= ((u1 - W1) * p1) + ((- (u1 - W1)) * p2) .= ((u1 - W1) * p1) + (- ((u1 - W1) * p2)) by EUCLID:40 .= ((u1 - W1) * p1) - ((u1 - W1) * p2) by EUCLID:41 .= (u1 - W1) * (p1 - p2) by EUCLID:49 .= (u1 - W1) * (p19 - p29) ; then A35: |.(WW1 - aa1).| = (abs (u1 - W1)) * |.(p19 - p29).| by EUCLID:11; r / (r / ((Pitag_dist n) . (p19,p29))) > 0 by A20, A25, XREAL_1:139; then |.(WW1 - aa1).| < (r / ((Pitag_dist n) . (p19,p29))) * (r / (r / ((Pitag_dist n) . (p19,p29)))) by A35, A32, A34, XREAL_1:68; then ( Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) & |.(WW1 - aa1).| < r ) by A33, EUCLID:def_7, XCMPLX_1:87; then the distance of (Euclid n) . (WW9,aa9) < r by EUCLID:def_6; then the distance of ((Euclid n) | PP) . (Y,aa) < r by TOPMETR:def_1; then dist (Y,aa) < r by METRIC_1:def_1; hence a in Ball (Y,r) by METRIC_1:11; ::_thesis: verum end; then f .: H c= Q by A21, XBOOLE_1:1; hence f .: H c= G by A18, XBOOLE_1:1; ::_thesis: verum end; then A36: f is continuous by BORSUK_1:def_1; take f ; ::_thesis: ( ( for x being Real st x in [.0,1.] holds f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) thus for x being Real st x in [.0,1.] holds f . x = ((1 - x) * p1) + (x * p2) by A3; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) [#] ((TOP-REAL n) | (LSeg (p1,p2))) c= rng f proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) or a in rng f ) assume a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: a in rng f then a in { (((1 - l) * p1) + (l * p2)) where l is Real : ( 0 <= l & l <= 1 ) } by PRE_TOPC:def_5; then consider lambda being Real such that A37: a = ((1 - lambda) * p1) + (lambda * p2) and A38: ( 0 <= lambda & lambda <= 1 ) ; lambda in { r where r is Real : ( 0 <= r & r <= 1 ) } by A38; then A39: lambda in dom f by A2, RCOMP_1:def_1; then a = f . lambda by A2, A3, A37; hence a in rng f by A39, FUNCT_1:def_3; ::_thesis: verum end; then ( [#] I[01] = [.0,1.] & rng f = [#] ((TOP-REAL n) | (LSeg (p1,p2))) ) by BORSUK_1:40, XBOOLE_0:def_10; hence f is being_homeomorphism by A2, A15, A36, COMPTS_1:17; ::_thesis: ( f . 0 = p1 & f . 1 = p2 ) 0 in [.0,1.] by XXREAL_1:1; hence f . 0 = ((1 - 0) * p1) + (0 * p2) by A3 .= p1 + (0 * p2) by EUCLID:29 .= p1 + (0. (TOP-REAL n)) by EUCLID:29 .= p1 by EUCLID:27 ; ::_thesis: f . 1 = p2 1 in [.0,1.] by XXREAL_1:1; hence f . 1 = ((1 - 1) * p1) + (1 * p2) by A3 .= (0. (TOP-REAL n)) + (1 * p2) by EUCLID:29 .= 1 * p2 by EUCLID:27 .= p2 by EUCLID:29 ; ::_thesis: verum end; Lm2: for n being Element of NAT holds TOP-REAL n is pathwise_connected proof let n be Element of NAT ; ::_thesis: TOP-REAL n is pathwise_connected set T = TOP-REAL n; let a, b be Point of (TOP-REAL n); :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected set L = LSeg (a,b); percases ( a <> b or a = b ) ; suppose a <> b ; ::_thesis: a,b are_connected then consider f being Function of I[01],((TOP-REAL n) | (LSeg (a,b))) such that for x being Real st x in [.0,1.] holds f . x = ((1 - x) * a) + (x * b) and A1: f is being_homeomorphism and A2: ( f . 0 = a & f . 1 = b ) by Th3; rng f c= [#] ((TOP-REAL n) | (LSeg (a,b))) ; then rng f c= LSeg (a,b) by PRE_TOPC:def_5; then ( dom f = the carrier of I[01] & rng f c= the carrier of (TOP-REAL n) ) by FUNCT_2:def_1, XBOOLE_1:1; then reconsider g = f as Function of I[01],(TOP-REAL n) by RELSET_1:4; f is continuous by A1, TOPS_2:def_5; then g is continuous by PRE_TOPC:26; hence a,b are_connected by A2, BORSUK_2:def_1; ::_thesis: verum end; suppose a = b ; ::_thesis: a,b are_connected hence a,b are_connected ; ::_thesis: verum end; end; end; registration let n be Element of NAT ; cluster TOP-REAL n -> pathwise_connected ; coherence TOP-REAL n is pathwise_connected by Lm2; end; registration let n be Element of NAT ; cluster non empty strict TopSpace-like T_0 T_1 T_2 compact for SubSpace of TOP-REAL n; existence ex b1 being SubSpace of TOP-REAL n st ( b1 is compact & not b1 is empty & b1 is strict ) proof set A = the non empty compact Subset of (TOP-REAL n); reconsider T = (TOP-REAL n) | the non empty compact Subset of (TOP-REAL n) as non empty SubSpace of TOP-REAL n ; T is compact ; hence ex b1 being SubSpace of TOP-REAL n st ( b1 is compact & not b1 is empty & b1 is strict ) ; ::_thesis: verum end; end; theorem :: JORDAN5A:4 for a, b being Point of (TOP-REAL 2) for f being Path of a,b for P being non empty compact SubSpace of TOP-REAL 2 for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds g is being_homeomorphism proof let a, b be Point of (TOP-REAL 2); ::_thesis: for f being Path of a,b for P being non empty compact SubSpace of TOP-REAL 2 for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds g is being_homeomorphism let f be Path of a,b; ::_thesis: for P being non empty compact SubSpace of TOP-REAL 2 for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds g is being_homeomorphism let P be non empty compact SubSpace of TOP-REAL 2; ::_thesis: for g being Function of I[01],P st f is one-to-one & g = f & [#] P = rng f holds g is being_homeomorphism let g be Function of I[01],P; ::_thesis: ( f is one-to-one & g = f & [#] P = rng f implies g is being_homeomorphism ) A1: dom g = [#] I[01] by FUNCT_2:def_1; assume ( f is one-to-one & g = f & [#] P = rng f ) ; ::_thesis: g is being_homeomorphism hence g is being_homeomorphism by A1, COMPTS_1:17, PRE_TOPC:27; ::_thesis: verum end; Lm3: for X being Subset of REAL st X is open holds X in Family_open_set RealSpace proof let X be Subset of REAL; ::_thesis: ( X is open implies X in Family_open_set RealSpace ) reconsider V = X as Subset of RealSpace by METRIC_1:def_13; assume A1: X is open ; ::_thesis: X in Family_open_set RealSpace for x being Element of RealSpace st x in X holds ex r being Real st ( r > 0 & Ball (x,r) c= X ) proof let x be Element of RealSpace; ::_thesis: ( x in X implies ex r being Real st ( r > 0 & Ball (x,r) c= X ) ) reconsider r = x as Real by METRIC_1:def_13; assume x in X ; ::_thesis: ex r being Real st ( r > 0 & Ball (x,r) c= X ) then consider N being Neighbourhood of r such that A2: N c= X by A1, RCOMP_1:18; consider g being real number such that A3: 0 < g and A4: N = ].(r - g),(r + g).[ by RCOMP_1:def_6; reconsider g = g as Real by XREAL_0:def_1; A5: N c= Ball (x,g) proof reconsider r9 = r as Element of RealSpace ; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in N or a in Ball (x,g) ) assume A6: a in N ; ::_thesis: a in Ball (x,g) then reconsider a9 = a as Real ; reconsider a1 = a9, r1 = r9 as Element of REAL ; a9 is Element of REAL ; then reconsider a99 = a as Element of RealSpace by METRIC_1:def_13; abs (a9 - r) < g by A4, A6, RCOMP_1:1; then real_dist . (a9,r) < g by METRIC_1:def_12; then ( dist (r9,a99) = real_dist . (r,a9) & real_dist . (r1,a1) < g ) by METRIC_1:9, METRIC_1:def_1, METRIC_1:def_13; hence a in Ball (x,g) by METRIC_1:11; ::_thesis: verum end; Ball (x,g) c= N proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Ball (x,g) or a in N ) assume a in Ball (x,g) ; ::_thesis: a in N then a in { q where q is Element of RealSpace : dist (x,q) < g } by METRIC_1:17; then consider q being Element of RealSpace such that A7: q = a and A8: dist (x,q) < g ; reconsider a9 = a as Real by A7, METRIC_1:def_13; reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def_13; real_dist . (q1,x1) < g by A8, METRIC_1:def_1, METRIC_1:def_13; then abs (a9 - r) < g by A7, METRIC_1:def_12; hence a in N by A4, RCOMP_1:1; ::_thesis: verum end; then N = Ball (x,g) by A5, XBOOLE_0:def_10; hence ex r being Real st ( r > 0 & Ball (x,r) c= X ) by A2, A3; ::_thesis: verum end; then V in Family_open_set RealSpace by PCOMPS_1:def_4; hence X in Family_open_set RealSpace ; ::_thesis: verum end; Lm4: for X being Subset of REAL st X in Family_open_set RealSpace holds X is open proof let X be Subset of REAL; ::_thesis: ( X in Family_open_set RealSpace implies X is open ) assume A1: X in Family_open_set RealSpace ; ::_thesis: X is open for r being real number st r in X holds ex N being Neighbourhood of r st N c= X proof let r be real number ; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X ) assume A2: r in X ; ::_thesis: ex N being Neighbourhood of r st N c= X reconsider r = r as Real by XREAL_0:def_1; reconsider x = r as Element of RealSpace by METRIC_1:def_13; ex N being Neighbourhood of r st N c= X proof consider r1 being Real such that A3: r1 > 0 and A4: Ball (x,r1) c= X by A1, A2, PCOMPS_1:def_4; reconsider N1 = Ball (x,r1) as Subset of REAL by METRIC_1:def_13; ex g being Real st ( 0 < g & Ball (x,r1) = ].(r - g),(r + g).[ ) proof take g = r1; ::_thesis: ( 0 < g & Ball (x,r1) = ].(r - g),(r + g).[ ) A5: ].(r - g),(r + g).[ c= N1 proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ].(r - g),(r + g).[ or a in N1 ) assume A6: a in ].(r - g),(r + g).[ ; ::_thesis: a in N1 then reconsider a9 = a as Real ; a9 is Element of REAL ; then reconsider a99 = a, r9 = r as Element of RealSpace by METRIC_1:def_13; reconsider a1 = a9, r1 = r9 as Element of REAL ; abs (a9 - r) < g by A6, RCOMP_1:1; then real_dist . (a9,r) < g by METRIC_1:def_12; then ( dist (r9,a99) = real_dist . (r,a9) & real_dist . (r1,a1) < g ) by METRIC_1:9, METRIC_1:def_1, METRIC_1:def_13; hence a in N1 by METRIC_1:11; ::_thesis: verum end; N1 c= ].(r - g),(r + g).[ proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in N1 or a in ].(r - g),(r + g).[ ) assume a in N1 ; ::_thesis: a in ].(r - g),(r + g).[ then a in { q where q is Element of RealSpace : dist (x,q) < g } by METRIC_1:17; then consider q being Element of RealSpace such that A7: q = a and A8: dist (x,q) < g ; reconsider a9 = a as Real by A7, METRIC_1:def_13; reconsider x1 = x, q1 = q as Element of REAL by METRIC_1:def_13; real_dist . (q1,x1) < g by A8, METRIC_1:def_1, METRIC_1:def_13; then abs (a9 - r) < g by A7, METRIC_1:def_12; hence a in ].(r - g),(r + g).[ by RCOMP_1:1; ::_thesis: verum end; hence ( 0 < g & Ball (x,r1) = ].(r - g),(r + g).[ ) by A3, A5, XBOOLE_0:def_10; ::_thesis: verum end; then reconsider N = N1 as Neighbourhood of r by RCOMP_1:def_6; take N ; ::_thesis: N c= X thus N c= X by A4; ::_thesis: verum end; hence ex N being Neighbourhood of r st N c= X ; ::_thesis: verum end; hence X is open by RCOMP_1:20; ::_thesis: verum end; begin theorem Th5: :: JORDAN5A:5 for X being Subset of REAL holds ( X in Family_open_set RealSpace iff X is open ) by Lm3, Lm4; theorem Th6: :: JORDAN5A:6 for f being Function of R^1,R^1 for x being Point of R^1 for g being PartFunc of REAL,REAL for x1 being Real st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1 proof let f be Function of R^1,R^1; ::_thesis: for x being Point of R^1 for g being PartFunc of REAL,REAL for x1 being Real st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1 let x be Point of R^1; ::_thesis: for g being PartFunc of REAL,REAL for x1 being Real st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1 let g be PartFunc of REAL,REAL; ::_thesis: for x1 being Real st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1 let x1 be Real; ::_thesis: ( f is_continuous_at x & f = g & x = x1 implies g is_continuous_in x1 ) assume that A1: f is_continuous_at x and A2: f = g and A3: x = x1 ; ::_thesis: g is_continuous_in x1 for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1 proof reconsider fx = f . x as Point of R^1 ; let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1 reconsider N19 = N1 as Subset of R^1 by TOPMETR:17; reconsider N2 = N1 as Subset of RealSpace by TOPMETR:12, TOPMETR:17, TOPMETR:def_6; N2 in Family_open_set RealSpace by Lm3; then N2 in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12; then N19 is open by PRE_TOPC:def_2, TOPMETR:def_6; then reconsider G = N19 as a_neighborhood of fx by A2, A3, CONNSP_2:3, RCOMP_1:16; consider H being a_neighborhood of x such that A4: f .: H c= G by A1, TMAP_1:def_2; consider V being Subset of R^1 such that A5: V is open and A6: V c= H and A7: x in V by CONNSP_2:6; reconsider V1 = V as Subset of REAL by TOPMETR:17; V in the topology of R^1 by A5, PRE_TOPC:def_2; then V in Family_open_set RealSpace by TOPMETR:12, TOPMETR:def_6; then V1 is open by Lm4; then consider N being Neighbourhood of x1 such that A8: N c= V1 by A3, A7, RCOMP_1:18; N c= H by A6, A8, XBOOLE_1:1; then g .: N c= g .: H by RELAT_1:123; hence ex N being Neighbourhood of x1 st g .: N c= N1 by A2, A4, XBOOLE_1:1; ::_thesis: verum end; hence g is_continuous_in x1 by FCONT_1:5; ::_thesis: verum end; theorem Th7: :: JORDAN5A:7 for f being continuous Function of R^1,R^1 for g being PartFunc of REAL,REAL st f = g holds g is continuous proof let f be continuous Function of R^1,R^1; ::_thesis: for g being PartFunc of REAL,REAL st f = g holds g is continuous let g be PartFunc of REAL,REAL; ::_thesis: ( f = g implies g is continuous ) assume A1: f = g ; ::_thesis: g is continuous for x0 being real number st x0 in dom g holds g is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom g implies g is_continuous_in x0 ) assume x0 in dom g ; ::_thesis: g is_continuous_in x0 reconsider x0 = x0 as Real by XREAL_0:def_1; reconsider x1 = x0 as Point of R^1 by TOPMETR:17; f is_continuous_at x1 by TMAP_1:44; hence g is_continuous_in x0 by A1, Th6; ::_thesis: verum end; hence g is continuous by FCONT_1:def_2; ::_thesis: verum end; Lm5: for f being one-to-one continuous Function of R^1,R^1 for g being PartFunc of REAL,REAL holds ( not f = g or g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) proof let f be one-to-one continuous Function of R^1,R^1; ::_thesis: for g being PartFunc of REAL,REAL holds ( not f = g or g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) let g be PartFunc of REAL,REAL; ::_thesis: ( not f = g or g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) assume A1: f = g ; ::_thesis: ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) then ( dom f = REAL & g is continuous ) by Th7, FUNCT_2:def_1, TOPMETR:17; hence ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) by A1, FCONT_2:17; ::_thesis: verum end; theorem :: JORDAN5A:8 for f being one-to-one continuous Function of R^1,R^1 holds ( for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy or for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx > fy ) proof let f be one-to-one continuous Function of R^1,R^1; ::_thesis: ( for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy or for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx > fy ) A1: [.0,1.] /\ (dom f) = [.0,1.] /\ the carrier of R^1 by FUNCT_2:def_1 .= [.0,1.] by BORSUK_1:1, BORSUK_1:40, TOPMETR:20, XBOOLE_1:28 ; reconsider g = f as PartFunc of REAL,REAL by TOPMETR:17; percases ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) by Lm5; suppose g | [.0,1.] is increasing ; ::_thesis: ( for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy or for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx > fy ) hence ( for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy or for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx > fy ) by A1, BORSUK_1:40, RFUNCT_2:20; ::_thesis: verum end; suppose g | [.0,1.] is decreasing ; ::_thesis: ( for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy or for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx > fy ) hence ( for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy or for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx > fy ) by A1, BORSUK_1:40, RFUNCT_2:21; ::_thesis: verum end; end; end; theorem Th9: :: JORDAN5A:9 for r, gg, a, b being Real for x being Element of (Closed-Interval-MSpace (a,b)) st a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] holds ].(r - gg),(r + gg).[ = Ball (x,gg) proof let r, gg, a, b be Real; ::_thesis: for x being Element of (Closed-Interval-MSpace (a,b)) st a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] holds ].(r - gg),(r + gg).[ = Ball (x,gg) let x be Element of (Closed-Interval-MSpace (a,b)); ::_thesis: ( a <= b & x = r & ].(r - gg),(r + gg).[ c= [.a,b.] implies ].(r - gg),(r + gg).[ = Ball (x,gg) ) assume that A1: a <= b and A2: x = r and A3: ].(r - gg),(r + gg).[ c= [.a,b.] ; ::_thesis: ].(r - gg),(r + gg).[ = Ball (x,gg) set g = gg; set CM = Closed-Interval-MSpace (a,b); set N1 = Ball (x,gg); A4: the carrier of (Closed-Interval-MSpace (a,b)) c= the carrier of RealSpace by TOPMETR:def_1; A5: Ball (x,gg) c= ].(r - gg),(r + gg).[ proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in Ball (x,gg) or i in ].(r - gg),(r + gg).[ ) assume i in Ball (x,gg) ; ::_thesis: i in ].(r - gg),(r + gg).[ then i in { q where q is Element of (Closed-Interval-MSpace (a,b)) : dist (x,q) < gg } by METRIC_1:17; then consider q being Element of (Closed-Interval-MSpace (a,b)) such that A6: q = i and A7: dist (x,q) < gg ; reconsider a9 = i as Real by A4, A6, METRIC_1:def_13, TARSKI:def_3; reconsider x2 = x, q2 = q as Element of (Closed-Interval-MSpace (a,b)) ; reconsider x1 = x, q1 = q as Element of REAL by A4, METRIC_1:def_13, TARSKI:def_3; dist (x2,q2) = the distance of (Closed-Interval-MSpace (a,b)) . (x2,q2) by METRIC_1:def_1 .= real_dist . (x2,q2) by METRIC_1:def_13, TOPMETR:def_1 ; then real_dist . (q1,x1) < gg by A7, METRIC_1:9; then abs (a9 - r) < gg by A2, A6, METRIC_1:def_12; hence i in ].(r - gg),(r + gg).[ by RCOMP_1:1; ::_thesis: verum end; ].(r - gg),(r + gg).[ c= Ball (x,gg) proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in ].(r - gg),(r + gg).[ or i in Ball (x,gg) ) assume A8: i in ].(r - gg),(r + gg).[ ; ::_thesis: i in Ball (x,gg) then reconsider a9 = i as Real ; reconsider a99 = i as Element of (Closed-Interval-MSpace (a,b)) by A1, A3, A8, TOPMETR:10; abs (a9 - r) < gg by A8, RCOMP_1:1; then A9: real_dist . (a9,r) < gg by METRIC_1:def_12; dist (x,a99) = the distance of (Closed-Interval-MSpace (a,b)) . (x,a99) by METRIC_1:def_1 .= real_dist . (x,a99) by METRIC_1:def_13, TOPMETR:def_1 ; then dist (x,a99) < gg by A2, A9, METRIC_1:9; hence i in Ball (x,gg) by METRIC_1:11; ::_thesis: verum end; hence ].(r - gg),(r + gg).[ = Ball (x,gg) by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th10: :: JORDAN5A:10 for a, b being Real for X being Subset of REAL st a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) holds X is open proof let a, b be Real; ::_thesis: for X being Subset of REAL st a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) holds X is open let X be Subset of REAL; ::_thesis: ( a < b & not a in X & not b in X & X in Family_open_set (Closed-Interval-MSpace (a,b)) implies X is open ) assume that A1: a < b and A2: not a in X and A3: not b in X ; ::_thesis: ( not X in Family_open_set (Closed-Interval-MSpace (a,b)) or X is open ) assume A4: X in Family_open_set (Closed-Interval-MSpace (a,b)) ; ::_thesis: X is open then reconsider V = X as Subset of (Closed-Interval-MSpace (a,b)) ; for r being real number st r in X holds ex N being Neighbourhood of r st N c= X proof let r be real number ; ::_thesis: ( r in X implies ex N being Neighbourhood of r st N c= X ) assume A5: r in X ; ::_thesis: ex N being Neighbourhood of r st N c= X reconsider r = r as Real by XREAL_0:def_1; r in V by A5; then reconsider x = r as Element of (Closed-Interval-MSpace (a,b)) ; the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10; then x in [.a,b.] ; then x in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1; then A6: ex r2 being Real st ( r2 = x & a <= r2 & r2 <= b ) ; A7: r - a <> 0 by A2, A5; ex N being Neighbourhood of r st N c= X proof consider r1 being Real such that A8: r1 > 0 and A9: Ball (x,r1) c= X by A4, A5, PCOMPS_1:def_4; percases ( r <= (a + b) / 2 or r > (a + b) / 2 ) ; supposeA10: r <= (a + b) / 2 ; ::_thesis: ex N being Neighbourhood of r st N c= X set gg = min ((r - a),r1); min ((r - a),r1) > 0 proof percases ( min ((r - a),r1) = r - a or min ((r - a),r1) = r1 ) by XXREAL_0:15; suppose min ((r - a),r1) = r - a ; ::_thesis: min ((r - a),r1) > 0 hence min ((r - a),r1) > 0 by A7, A6, XREAL_1:48; ::_thesis: verum end; suppose min ((r - a),r1) = r1 ; ::_thesis: min ((r - a),r1) > 0 hence min ((r - a),r1) > 0 by A8; ::_thesis: verum end; end; end; then reconsider N = ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ as Neighbourhood of r by RCOMP_1:def_6; take N ; ::_thesis: N c= X ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ c= [.a,b.] proof 2 * r <= 2 * ((a + b) / 2) by A10, XREAL_1:64; then A11: (2 * r) - a <= (a + b) - a by XREAL_1:13; let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ or i in [.a,b.] ) assume i in ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ ; ::_thesis: i in [.a,b.] then i in { l where l is Real : ( r - (min ((r - a),r1)) < l & l < r + (min ((r - a),r1)) ) } by RCOMP_1:def_2; then consider j being Real such that A12: j = i and A13: r - (min ((r - a),r1)) < j and A14: j < r + (min ((r - a),r1)) ; A15: min ((r - a),r1) <= r - a by XXREAL_0:17; then r + (min ((r - a),r1)) <= r + (r - a) by XREAL_1:6; then r + (min ((r - a),r1)) <= (a + b) - a by A11, XXREAL_0:2; then A16: j <= b by A14, XXREAL_0:2; (min ((r - a),r1)) + a <= r by A15, XREAL_1:19; then r - (min ((r - a),r1)) >= a by XREAL_1:19; then a <= j by A13, XXREAL_0:2; then j in { l where l is Real : ( a <= l & l <= b ) } by A16; hence i in [.a,b.] by A12, RCOMP_1:def_1; ::_thesis: verum end; then ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ = Ball (x,(min ((r - a),r1))) by A1, Th9; then ].(r - (min ((r - a),r1))),(r + (min ((r - a),r1))).[ c= Ball (x,r1) by PCOMPS_1:1, XXREAL_0:17; hence N c= X by A9, XBOOLE_1:1; ::_thesis: verum end; supposeA17: r > (a + b) / 2 ; ::_thesis: ex N being Neighbourhood of r st N c= X set gg = min ((b - r),r1); A18: b - r <> 0 by A3, A5; min ((b - r),r1) > 0 proof percases ( min ((b - r),r1) = b - r or min ((b - r),r1) = r1 ) by XXREAL_0:15; suppose min ((b - r),r1) = b - r ; ::_thesis: min ((b - r),r1) > 0 hence min ((b - r),r1) > 0 by A6, A18, XREAL_1:48; ::_thesis: verum end; suppose min ((b - r),r1) = r1 ; ::_thesis: min ((b - r),r1) > 0 hence min ((b - r),r1) > 0 by A8; ::_thesis: verum end; end; end; then reconsider N = ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ as Neighbourhood of r by RCOMP_1:def_6; take N ; ::_thesis: N c= X ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ c= [.a,b.] proof 2 * r >= ((a + b) / 2) * 2 by A17, XREAL_1:64; then A19: (2 * r) - b >= (a + b) - b by XREAL_1:13; let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ or i in [.a,b.] ) assume i in ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ ; ::_thesis: i in [.a,b.] then i in { l where l is Real : ( r - (min ((b - r),r1)) < l & l < r + (min ((b - r),r1)) ) } by RCOMP_1:def_2; then consider j being Real such that A20: j = i and A21: r - (min ((b - r),r1)) < j and A22: j < r + (min ((b - r),r1)) ; A23: min ((b - r),r1) <= b - r by XXREAL_0:17; then r + (min ((b - r),r1)) <= b by XREAL_1:19; then A24: j <= b by A22, XXREAL_0:2; r - (min ((b - r),r1)) >= r - (b - r) by A23, XREAL_1:13; then r - (min ((b - r),r1)) >= a by A19, XXREAL_0:2; then a <= j by A21, XXREAL_0:2; then j in { l where l is Real : ( a <= l & l <= b ) } by A24; hence i in [.a,b.] by A20, RCOMP_1:def_1; ::_thesis: verum end; then ].(r - (min ((b - r),r1))),(r + (min ((b - r),r1))).[ = Ball (x,(min ((b - r),r1))) by A1, Th9; then N c= Ball (x,r1) by PCOMPS_1:1, XXREAL_0:17; hence N c= X by A9, XBOOLE_1:1; ::_thesis: verum end; end; end; hence ex N being Neighbourhood of r st N c= X ; ::_thesis: verum end; hence X is open by RCOMP_1:20; ::_thesis: verum end; theorem Th11: :: JORDAN5A:11 for X being open Subset of REAL for a, b being Real st X c= [.a,b.] holds ( not a in X & not b in X ) proof let X be open Subset of REAL; ::_thesis: for a, b being Real st X c= [.a,b.] holds ( not a in X & not b in X ) let a, b be Real; ::_thesis: ( X c= [.a,b.] implies ( not a in X & not b in X ) ) assume A1: X c= [.a,b.] ; ::_thesis: ( not a in X & not b in X ) assume A2: ( a in X or b in X ) ; ::_thesis: contradiction percases ( a in X or b in X ) by A2; suppose a in X ; ::_thesis: contradiction then consider g being real number such that A3: 0 < g and A4: ].(a - g),(a + g).[ c= X by RCOMP_1:19; g / 2 <> 0 by A3; then A5: a - (g / 2) < a - 0 by A3, XREAL_1:15; g > g / 2 by A3, XREAL_1:216; then A6: a - g < a - (g / 2) by XREAL_1:15; a + 0 < a + g by A3, XREAL_1:8; then a - (g / 2) < a + g by A5, XXREAL_0:2; then a - (g / 2) in { l where l is Real : ( a - g < l & l < a + g ) } by A6; then A7: a - (g / 2) in ].(a - g),(a + g).[ by RCOMP_1:def_2; ].(a - g),(a + g).[ c= [.a,b.] by A1, A4, XBOOLE_1:1; then a - (g / 2) in [.a,b.] by A7; then a - (g / 2) in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1; then ex l being Real st ( l = a - (g / 2) & a <= l & l <= b ) ; hence contradiction by A5; ::_thesis: verum end; suppose b in X ; ::_thesis: contradiction then consider g being real number such that A8: 0 < g and A9: ].(b - g),(b + g).[ c= X by RCOMP_1:19; g / 2 <> 0 by A8; then A10: b + (g / 2) > b + 0 by A8, XREAL_1:6; g > g / 2 by A8, XREAL_1:216; then A11: b + (g / 2) < b + g by XREAL_1:8; b - g < b - 0 by A8, XREAL_1:15; then b - g < b + (g / 2) by A10, XXREAL_0:2; then b + (g / 2) in { l where l is Real : ( b - g < l & l < b + g ) } by A11; then A12: b + (g / 2) in ].(b - g),(b + g).[ by RCOMP_1:def_2; ].(b - g),(b + g).[ c= [.a,b.] by A1, A9, XBOOLE_1:1; then b + (g / 2) in [.a,b.] by A12; then b + (g / 2) in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1; then ex l being Real st ( l = b + (g / 2) & a <= l & l <= b ) ; hence contradiction by A10; ::_thesis: verum end; end; end; theorem Th12: :: JORDAN5A:12 for a, b being Real for X being Subset of REAL for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds V in Family_open_set (Closed-Interval-MSpace (a,b)) proof let a, b be Real; ::_thesis: for X being Subset of REAL for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds V in Family_open_set (Closed-Interval-MSpace (a,b)) let X be Subset of REAL; ::_thesis: for V being Subset of (Closed-Interval-MSpace (a,b)) st V = X & X is open holds V in Family_open_set (Closed-Interval-MSpace (a,b)) let V be Subset of (Closed-Interval-MSpace (a,b)); ::_thesis: ( V = X & X is open implies V in Family_open_set (Closed-Interval-MSpace (a,b)) ) assume A1: V = X ; ::_thesis: ( not X is open or V in Family_open_set (Closed-Interval-MSpace (a,b)) ) assume A2: X is open ; ::_thesis: V in Family_open_set (Closed-Interval-MSpace (a,b)) for x being Element of (Closed-Interval-MSpace (a,b)) st x in V holds ex r being Real st ( r > 0 & Ball (x,r) c= V ) proof let x be Element of (Closed-Interval-MSpace (a,b)); ::_thesis: ( x in V implies ex r being Real st ( r > 0 & Ball (x,r) c= V ) ) assume A3: x in V ; ::_thesis: ex r being Real st ( r > 0 & Ball (x,r) c= V ) then reconsider r = x as Real by A1; consider N being Neighbourhood of r such that A4: N c= X by A1, A2, A3, RCOMP_1:18; consider g being real number such that A5: 0 < g and A6: N = ].(r - g),(r + g).[ by RCOMP_1:def_6; reconsider g = g as Real by XREAL_0:def_1; A7: Ball (x,g) c= N proof let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in Ball (x,g) or aa in N ) assume aa in Ball (x,g) ; ::_thesis: aa in N then aa in { q where q is Element of (Closed-Interval-MSpace (a,b)) : dist (x,q) < g } by METRIC_1:17; then consider q being Element of (Closed-Interval-MSpace (a,b)) such that A8: q = aa and A9: dist (x,q) < g ; A10: ( q in the carrier of (Closed-Interval-MSpace (a,b)) & the carrier of (Closed-Interval-MSpace (a,b)) c= the carrier of RealSpace ) by TOPMETR:def_1; then reconsider a9 = aa as Real by A8, METRIC_1:def_13; reconsider x1 = x, q1 = q as Element of REAL by A1, A3, A10, METRIC_1:def_13; dist (x,q) = the distance of (Closed-Interval-MSpace (a,b)) . (x,q) by METRIC_1:def_1 .= real_dist . (x,q) by METRIC_1:def_13, TOPMETR:def_1 ; then real_dist . (q1,x1) < g by A9, METRIC_1:9; then abs (a9 - r) < g by A8, METRIC_1:def_12; hence aa in N by A6, RCOMP_1:1; ::_thesis: verum end; N c= Ball (x,g) proof let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in N or aa in Ball (x,g) ) assume A11: aa in N ; ::_thesis: aa in Ball (x,g) then reconsider a9 = aa as Real ; abs (a9 - r) < g by A6, A11, RCOMP_1:1; then A12: real_dist . (a9,r) < g by METRIC_1:def_12; aa in X by A4, A11; then reconsider a99 = aa, r9 = r as Element of (Closed-Interval-MSpace (a,b)) by A1; dist (r9,a99) = the distance of (Closed-Interval-MSpace (a,b)) . (r9,a99) by METRIC_1:def_1 .= real_dist . (r9,a99) by METRIC_1:def_13, TOPMETR:def_1 ; then dist (r9,a99) < g by A12, METRIC_1:9; hence aa in Ball (x,g) by METRIC_1:11; ::_thesis: verum end; then N = Ball (x,g) by A7, XBOOLE_0:def_10; hence ex r being Real st ( r > 0 & Ball (x,r) c= V ) by A1, A4, A5; ::_thesis: verum end; hence V in Family_open_set (Closed-Interval-MSpace (a,b)) by PCOMPS_1:def_4; ::_thesis: verum end; Lm6: for a, b, c being real number st a <= b holds ( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) ) proof let a, b, c be real number ; ::_thesis: ( a <= b implies ( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) ) ) A1: c is Real by XREAL_0:def_1; assume a <= b ; ::_thesis: ( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) ) then A2: the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] by TOPMETR:18; hereby ::_thesis: ( a <= c & c <= b implies c in the carrier of (Closed-Interval-TSpace (a,b)) ) assume c in the carrier of (Closed-Interval-TSpace (a,b)) ; ::_thesis: ( a <= c & c <= b ) then c in { l where l is Real : ( a <= l & l <= b ) } by A2, RCOMP_1:def_1; then ex c1 being Real st ( c1 = c & a <= c1 & c1 <= b ) ; hence ( a <= c & c <= b ) ; ::_thesis: verum end; assume ( a <= c & c <= b ) ; ::_thesis: c in the carrier of (Closed-Interval-TSpace (a,b)) then c in { l where l is Real : ( a <= l & l <= b ) } by A1; hence c in the carrier of (Closed-Interval-TSpace (a,b)) by A2, RCOMP_1:def_1; ::_thesis: verum end; Lm7: for a, b, c, d being Real for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for x being Point of (Closed-Interval-TSpace (a,b)) for g being PartFunc of REAL,REAL for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g is_continuous_in x1 proof let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for x being Point of (Closed-Interval-TSpace (a,b)) for g being PartFunc of REAL,REAL for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g is_continuous_in x1 let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b)) for g being PartFunc of REAL,REAL for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g is_continuous_in x1 let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for g being PartFunc of REAL,REAL for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g is_continuous_in x1 let g be PartFunc of REAL,REAL; ::_thesis: for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g is_continuous_in x1 let x1 be Real; ::_thesis: ( a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 implies g is_continuous_in x1 ) assume that A1: a < b and A2: c < d and A3: f is_continuous_at x and A4: x <> a and A5: x <> b and A6: f . a = c and A7: f . b = d and A8: f is one-to-one and A9: f = g and A10: x = x1 ; ::_thesis: g is_continuous_in x1 A11: dom f = the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_1; for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1 proof reconsider fx = f . x as Point of (Closed-Interval-TSpace (c,d)) ; set Rm = min (((g . x1) - c),(d - (g . x1))); let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1 Closed-Interval-TSpace (c,d) = TopSpaceMetr (Closed-Interval-MSpace (c,d)) by TOPMETR:def_7; then A12: the topology of (Closed-Interval-TSpace (c,d)) = Family_open_set (Closed-Interval-MSpace (c,d)) by TOPMETR:12; min (((g . x1) - c),(d - (g . x1))) > 0 proof A13: b in dom f by A1, A11, Lm6; A14: a in dom f by A1, A11, Lm6; percases ( min (((g . x1) - c),(d - (g . x1))) = (g . x1) - c or min (((g . x1) - c),(d - (g . x1))) = d - (g . x1) ) by XXREAL_0:15; supposeA15: min (((g . x1) - c),(d - (g . x1))) = (g . x1) - c ; ::_thesis: min (((g . x1) - c),(d - (g . x1))) > 0 g . x1 in the carrier of (Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2:5; then A16: g . x1 >= c by A2, Lm6; min (((g . x1) - c),(d - (g . x1))) <> 0 by A4, A6, A8, A9, A10, A11, A14, A15, FUNCT_1:def_4; hence min (((g . x1) - c),(d - (g . x1))) > 0 by A15, A16, XREAL_1:48; ::_thesis: verum end; supposeA17: min (((g . x1) - c),(d - (g . x1))) = d - (g . x1) ; ::_thesis: min (((g . x1) - c),(d - (g . x1))) > 0 g . x1 in the carrier of (Closed-Interval-TSpace (c,d)) by A9, A10, FUNCT_2:5; then A18: g . x1 <= d by A2, Lm6; d - (g . x1) <> d - d by A5, A7, A8, A9, A10, A11, A13, FUNCT_1:def_4; hence min (((g . x1) - c),(d - (g . x1))) > 0 by A17, A18, XREAL_1:48; ::_thesis: verum end; end; end; then reconsider Wuj = ].((g . x1) - (min (((g . x1) - c),(d - (g . x1))))),((g . x1) + (min (((g . x1) - c),(d - (g . x1))))).[ as Neighbourhood of g . x1 by RCOMP_1:def_6; consider Ham being Neighbourhood of g . x1 such that A19: Ham c= N1 and A20: Ham c= Wuj by RCOMP_1:17; A21: Wuj c= ].c,d.[ proof let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in Wuj or aa in ].c,d.[ ) assume aa in Wuj ; ::_thesis: aa in ].c,d.[ then aa in { l where l is Real : ( (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) < l & l < (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) ) } by RCOMP_1:def_2; then consider A being Real such that A22: A = aa and A23: (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) < A and A24: A < (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) ; min (((g . x1) - c),(d - (g . x1))) <= d - (g . x1) by XXREAL_0:17; then (g . x1) + (min (((g . x1) - c),(d - (g . x1)))) <= (g . x1) + (d - (g . x1)) by XREAL_1:6; then A25: A < d by A24, XXREAL_0:2; min (((g . x1) - c),(d - (g . x1))) <= (g . x1) - c by XXREAL_0:17; then c + (min (((g . x1) - c),(d - (g . x1)))) <= g . x1 by XREAL_1:19; then c <= (g . x1) - (min (((g . x1) - c),(d - (g . x1)))) by XREAL_1:19; then c < A by A23, XXREAL_0:2; then A in { l where l is Real : ( c < l & l < d ) } by A25; hence aa in ].c,d.[ by A22, RCOMP_1:def_2; ::_thesis: verum end; ].c,d.[ c= [.c,d.] by XXREAL_1:25; then A26: Wuj c= [.c,d.] by A21, XBOOLE_1:1; then Wuj c= the carrier of (Closed-Interval-MSpace (c,d)) by A2, TOPMETR:10; then reconsider N21 = Ham as Subset of (Closed-Interval-MSpace (c,d)) by A20, XBOOLE_1:1; the carrier of (Closed-Interval-MSpace (c,d)) = the carrier of (TopSpaceMetr (Closed-Interval-MSpace (c,d))) by TOPMETR:12 .= the carrier of (Closed-Interval-TSpace (c,d)) by TOPMETR:def_7 ; then reconsider N19 = N21 as Subset of (Closed-Interval-TSpace (c,d)) ; N21 in Family_open_set (Closed-Interval-MSpace (c,d)) by Th12; then N19 is open by A12, PRE_TOPC:def_2; then reconsider G = N19 as a_neighborhood of fx by A9, A10, CONNSP_2:3, RCOMP_1:16; consider H being a_neighborhood of x such that A27: f .: H c= G by A3, TMAP_1:def_2; consider V being Subset of (Closed-Interval-TSpace (a,b)) such that A28: V is open and A29: V c= H and A30: x in V by CONNSP_2:6; A31: the carrier of (Closed-Interval-MSpace (a,b)) = the carrier of (TopSpaceMetr (Closed-Interval-MSpace (a,b))) by TOPMETR:12 .= the carrier of (Closed-Interval-TSpace (a,b)) by TOPMETR:def_7 ; then reconsider V2 = V as Subset of (Closed-Interval-MSpace (a,b)) ; V c= the carrier of (Closed-Interval-MSpace (a,b)) by A31; then V c= [.a,b.] by A1, TOPMETR:10; then reconsider V1 = V as Subset of REAL by XBOOLE_1:1; A32: Ham c= [.c,d.] by A20, A26, XBOOLE_1:1; A33: ( not a in V1 & not b in V1 ) proof assume A34: ( a in V1 or b in V1 ) ; ::_thesis: contradiction percases ( a in V1 or b in V1 ) by A34; suppose a in V1 ; ::_thesis: contradiction then f . a in f .: H by A11, A29, FUNCT_1:def_6; hence contradiction by A6, A32, A27, Th11; ::_thesis: verum end; suppose b in V1 ; ::_thesis: contradiction then f . b in f .: H by A11, A29, FUNCT_1:def_6; hence contradiction by A7, A32, A27, Th11; ::_thesis: verum end; end; end; Closed-Interval-TSpace (a,b) = TopSpaceMetr (Closed-Interval-MSpace (a,b)) by TOPMETR:def_7; then the topology of (Closed-Interval-TSpace (a,b)) = Family_open_set (Closed-Interval-MSpace (a,b)) by TOPMETR:12; then V2 in Family_open_set (Closed-Interval-MSpace (a,b)) by A28, PRE_TOPC:def_2; then V1 is open by A1, A33, Th10; then consider N being Neighbourhood of x1 such that A35: N c= V1 by A10, A30, RCOMP_1:18; N c= H by A29, A35, XBOOLE_1:1; then A36: g .: N c= g .: H by RELAT_1:123; f .: H c= N1 by A19, A27, XBOOLE_1:1; hence ex N being Neighbourhood of x1 st g .: N c= N1 by A9, A36, XBOOLE_1:1; ::_thesis: verum end; hence g is_continuous_in x1 by FCONT_1:5; ::_thesis: verum end; theorem Th13: :: JORDAN5A:13 for a, b, c, d, x1 being Real for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for x being Point of (Closed-Interval-TSpace (a,b)) for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g | [.a,b.] is_continuous_in x1 proof let a, b, c, d, x1 be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for x being Point of (Closed-Interval-TSpace (a,b)) for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g | [.a,b.] is_continuous_in x1 let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for x being Point of (Closed-Interval-TSpace (a,b)) for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g | [.a,b.] is_continuous_in x1 let x be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for g being PartFunc of REAL,REAL st a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds g | [.a,b.] is_continuous_in x1 let g be PartFunc of REAL,REAL; ::_thesis: ( a < b & c < d & f is_continuous_at x & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 implies g | [.a,b.] is_continuous_in x1 ) assume that A1: a < b and A2: c < d and A3: f is_continuous_at x and A4: f . a = c and A5: f . b = d and A6: f is one-to-one and A7: f = g and A8: x = x1 ; ::_thesis: g | [.a,b.] is_continuous_in x1 A9: for c being Element of REAL st c in dom g holds g /. c = g /. c ; dom g = the carrier of (Closed-Interval-TSpace (a,b)) by A7, FUNCT_2:def_1; then dom g = [.a,b.] by A1, TOPMETR:18; then dom g = (dom g) /\ [.a,b.] ; then A10: g = g | [.a,b.] by A9, PARTFUN2:15; percases ( x1 = a or x1 = b or ( x1 <> a & x1 <> b ) ) ; supposeA11: x1 = a ; ::_thesis: g | [.a,b.] is_continuous_in x1 for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1 proof reconsider f0 = f . a as Point of (Closed-Interval-TSpace (c,d)) by A2, A4, Lm6; let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1 reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def_13; set NN1 = N1 /\ [.c,d.]; N2 in Family_open_set RealSpace by Lm3; then A12: N2 in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12; N1 /\ [.c,d.] = N1 /\ the carrier of (Closed-Interval-TSpace (c,d)) by A2, TOPMETR:18; then reconsider NN = N1 /\ [.c,d.] as Subset of (Closed-Interval-TSpace (c,d)) by XBOOLE_1:17; N1 /\ [.c,d.] = N1 /\ ([#] (Closed-Interval-TSpace (c,d))) by A2, TOPMETR:18; then NN in the topology of (Closed-Interval-TSpace (c,d)) by A12, PRE_TOPC:def_4, TOPMETR:def_6; then A13: NN is open by PRE_TOPC:def_2; f . a in the carrier of (Closed-Interval-TSpace (c,d)) by A2, A4, Lm6; then ( g . x1 in N1 & g . x1 in [.c,d.] ) by A2, A7, A11, RCOMP_1:16, TOPMETR:18; then g . x1 in N1 /\ [.c,d.] by XBOOLE_0:def_4; then reconsider N19 = NN as a_neighborhood of f0 by A7, A11, A13, CONNSP_2:3; consider H being a_neighborhood of x such that A14: f .: H c= N19 by A3, A8, A11, TMAP_1:def_2; consider H1 being Subset of (Closed-Interval-TSpace (a,b)) such that A15: H1 is open and A16: H1 c= H and A17: x in H1 by CONNSP_2:6; H1 in the topology of (Closed-Interval-TSpace (a,b)) by A15, PRE_TOPC:def_2; then consider Q being Subset of R^1 such that A18: Q in the topology of R^1 and A19: H1 = Q /\ ([#] (Closed-Interval-TSpace (a,b))) by PRE_TOPC:def_4; reconsider Q9 = Q as Subset of RealSpace by TOPMETR:12, TOPMETR:def_6; reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def_13; Q9 in Family_open_set RealSpace by A18, TOPMETR:12, TOPMETR:def_6; then A20: Q1 is open by Lm4; x1 in Q1 by A8, A17, A19, XBOOLE_0:def_4; then consider N being Neighbourhood of x1 such that A21: N c= Q1 by A20, RCOMP_1:18; take N ; ::_thesis: g .: N c= N1 g .: N c= N1 proof let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in g .: N or aa in N1 ) assume A22: aa in g .: N ; ::_thesis: aa in N1 then reconsider a9 = aa as Element of REAL ; consider cc being Element of REAL such that A23: cc in dom g and A24: cc in N and A25: a9 = g . cc by A22, PARTFUN2:59; cc in the carrier of (Closed-Interval-TSpace (a,b)) by A7, A23, FUNCT_2:def_1; then cc in H1 by A19, A21, A24, XBOOLE_0:def_4; then g . cc in f .: H by A7, A16, FUNCT_2:35; hence aa in N1 by A14, A25, XBOOLE_0:def_4; ::_thesis: verum end; hence g .: N c= N1 ; ::_thesis: verum end; hence g | [.a,b.] is_continuous_in x1 by A10, FCONT_1:5; ::_thesis: verum end; supposeA26: x1 = b ; ::_thesis: g | [.a,b.] is_continuous_in x1 for N1 being Neighbourhood of g . x1 ex N being Neighbourhood of x1 st g .: N c= N1 proof reconsider f0 = f . b as Point of (Closed-Interval-TSpace (c,d)) by A2, A5, Lm6; let N1 be Neighbourhood of g . x1; ::_thesis: ex N being Neighbourhood of x1 st g .: N c= N1 reconsider N2 = N1 as Subset of RealSpace by METRIC_1:def_13; set NN1 = N1 /\ ([#] (Closed-Interval-TSpace (c,d))); reconsider NN = N1 /\ ([#] (Closed-Interval-TSpace (c,d))) as Subset of (Closed-Interval-TSpace (c,d)) ; N2 in Family_open_set RealSpace by Lm3; then N2 in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12; then NN in the topology of (Closed-Interval-TSpace (c,d)) by PRE_TOPC:def_4, TOPMETR:def_6; then A27: NN is open by PRE_TOPC:def_2; ( g . x1 in N1 & g . x1 in [#] (Closed-Interval-TSpace (c,d)) ) by A2, A5, A7, A26, Lm6, RCOMP_1:16; then g . x1 in N1 /\ ([#] (Closed-Interval-TSpace (c,d))) by XBOOLE_0:def_4; then reconsider N19 = NN as a_neighborhood of f0 by A7, A26, A27, CONNSP_2:3; consider H being a_neighborhood of x such that A28: f .: H c= N19 by A3, A8, A26, TMAP_1:def_2; consider H1 being Subset of (Closed-Interval-TSpace (a,b)) such that A29: H1 is open and A30: H1 c= H and A31: x in H1 by CONNSP_2:6; H1 in the topology of (Closed-Interval-TSpace (a,b)) by A29, PRE_TOPC:def_2; then consider Q being Subset of R^1 such that A32: Q in the topology of R^1 and A33: H1 = Q /\ ([#] (Closed-Interval-TSpace (a,b))) by PRE_TOPC:def_4; reconsider Q9 = Q as Subset of RealSpace by TOPMETR:12, TOPMETR:def_6; reconsider Q1 = Q9 as Subset of REAL by METRIC_1:def_13; Q9 in Family_open_set RealSpace by A32, TOPMETR:12, TOPMETR:def_6; then A34: Q1 is open by Lm4; x1 in Q1 by A8, A31, A33, XBOOLE_0:def_4; then consider N being Neighbourhood of x1 such that A35: N c= Q1 by A34, RCOMP_1:18; take N ; ::_thesis: g .: N c= N1 g .: N c= N1 proof let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in g .: N or aa in N1 ) assume A36: aa in g .: N ; ::_thesis: aa in N1 then reconsider a9 = aa as Element of REAL ; consider cc being Element of REAL such that A37: cc in dom g and A38: cc in N and A39: a9 = g . cc by A36, PARTFUN2:59; cc in the carrier of (Closed-Interval-TSpace (a,b)) by A7, A37, FUNCT_2:def_1; then cc in H1 by A33, A35, A38, XBOOLE_0:def_4; then g . cc in f .: H by A7, A30, FUNCT_2:35; hence aa in N1 by A28, A39, XBOOLE_0:def_4; ::_thesis: verum end; hence g .: N c= N1 ; ::_thesis: verum end; hence g | [.a,b.] is_continuous_in x1 by A10, FCONT_1:5; ::_thesis: verum end; suppose ( x1 <> a & x1 <> b ) ; ::_thesis: g | [.a,b.] is_continuous_in x1 hence g | [.a,b.] is_continuous_in x1 by A1, A2, A3, A4, A5, A6, A7, A8, A10, Lm7; ::_thesis: verum end; end; end; theorem Th14: :: JORDAN5A:14 for a, b, c, d being Real for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds g | [.a,b.] is continuous proof let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds g | [.a,b.] is continuous let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for g being PartFunc of REAL,REAL st f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d holds g | [.a,b.] is continuous let g be PartFunc of REAL,REAL; ::_thesis: ( f is continuous & f is one-to-one & a < b & c < d & f = g & f . a = c & f . b = d implies g | [.a,b.] is continuous ) assume that A1: ( f is continuous & f is one-to-one ) and A2: a < b and A3: ( c < d & f = g & f . a = c & f . b = d ) ; ::_thesis: g | [.a,b.] is continuous for x0 being real number st x0 in dom (g | [.a,b.]) holds g | [.a,b.] is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (g | [.a,b.]) implies g | [.a,b.] is_continuous_in x0 ) assume x0 in dom (g | [.a,b.]) ; ::_thesis: g | [.a,b.] is_continuous_in x0 then x0 in [.a,b.] by RELAT_1:57; then reconsider x1 = x0 as Point of (Closed-Interval-TSpace (a,b)) by A2, TOPMETR:18; ( f is_continuous_at x1 & x0 is Real ) by A1, TMAP_1:44, XREAL_0:def_1; hence g | [.a,b.] is_continuous_in x0 by A1, A2, A3, Th13; ::_thesis: verum end; hence g | [.a,b.] is continuous by FCONT_1:def_2; ::_thesis: verum end; begin theorem Th15: :: JORDAN5A:15 for a, b, c, d being Real for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d holds for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy proof let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d holds for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: ( a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d implies for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy ) assume that A1: a < b and A2: c < d and A3: ( f is continuous & f is one-to-one ) and A4: ( f . a = c & f . b = d ) ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy A5: [.a,b.] = the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; A6: dom f = the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_1; rng f c= REAL by MEMBERED:3; then reconsider g = f as PartFunc of [.a,b.],REAL by A5, A6, RELSET_1:4; reconsider g = g as PartFunc of REAL,REAL by A5, A6, RELSET_1:5; A7: g | [.a,b.] is continuous by A1, A2, A3, A4, Th14; A8: [.a,b.] /\ (dom f) = [.a,b.] /\ the carrier of (Closed-Interval-TSpace (a,b)) by FUNCT_2:def_1 .= [.a,b.] by A5 ; percases ( g | [.a,b.] is increasing or g | [.a,b.] is decreasing ) by A1, A3, A8, A7, FCONT_2:17, XBOOLE_1:18; supposeA9: g | [.a,b.] is increasing ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy proof let x, y be Point of (Closed-Interval-TSpace (a,b)); ::_thesis: for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy let p, q, fx, fy be Real; ::_thesis: ( x = p & y = q & p < q & fx = f . x & fy = f . y implies fx < fy ) assume that A10: x = p and A11: y = q and A12: ( p < q & fx = f . x & fy = f . y ) ; ::_thesis: fx < fy y in the carrier of (Closed-Interval-TSpace (a,b)) ; then A13: q in [.a,b.] /\ (dom g) by A1, A8, A11, TOPMETR:18; x in the carrier of (Closed-Interval-TSpace (a,b)) ; then p in [.a,b.] /\ (dom g) by A1, A8, A10, TOPMETR:18; hence fx < fy by A9, A10, A11, A12, A13, RFUNCT_2:20; ::_thesis: verum end; hence for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy ; ::_thesis: verum end; supposeA14: g | [.a,b.] is decreasing ; ::_thesis: for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy ( a in [.a,b.] /\ (dom g) & b in [.a,b.] /\ (dom g) ) by A1, A5, A8, Lm6; hence for x, y being Point of (Closed-Interval-TSpace (a,b)) for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy by A1, A2, A4, A14, RFUNCT_2:21; ::_thesis: verum end; end; end; theorem :: JORDAN5A:16 for f being one-to-one continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 holds for x, y being Point of I[01] for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds fx < fy by Th15, TOPMETR:20; theorem :: JORDAN5A:17 for a, b, c, d being Real for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for P being non empty Subset of (Closed-Interval-TSpace (a,b)) for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) proof let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for P being non empty Subset of (Closed-Interval-TSpace (a,b)) for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for P being non empty Subset of (Closed-Interval-TSpace (a,b)) for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) let P be non empty Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) let PP, QQ be Subset of R^1; ::_thesis: ( a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ implies f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) ) assume that A1: ( a < b & c < d ) and A2: PP = P and A3: f is continuous and A4: f is one-to-one and A5: PP is compact and A6: ( f . a = c & f . b = d ) and A7: f .: P = QQ ; ::_thesis: f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) A8: [#] (Closed-Interval-TSpace (c,d)) = the carrier of (Closed-Interval-TSpace (c,d)) ; set IT = f . (lower_bound ([#] PP)); A9: [#] PP is real-bounded by A5, WEIERSTR:11; [#] PP <> {} by A2, WEIERSTR:def_1; then A10: lower_bound ([#] PP) in [#] PP by A5, A9, RCOMP_1:13, WEIERSTR:12; then A11: lower_bound ([#] PP) in P by A2, WEIERSTR:def_1; P c= the carrier of (Closed-Interval-TSpace (a,b)) ; then A12: [#] PP c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, WEIERSTR:def_1; then A13: f . (lower_bound ([#] PP)) in the carrier of (Closed-Interval-TSpace (c,d)) by A10, FUNCT_2:5; A14: [#] R^1 = the carrier of R^1 ; then A15: the carrier of (Closed-Interval-TSpace (c,d)) c= the carrier of R^1 by A8, PRE_TOPC:def_4; then reconsider IT = f . (lower_bound ([#] PP)) as Real by A13, TOPMETR:17; [#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ; then A16: the carrier of (Closed-Interval-TSpace (a,b)) c= the carrier of R^1 by A14, PRE_TOPC:def_4; A17: for r being real number st r in [#] QQ holds IT <= r proof let r be real number ; ::_thesis: ( r in [#] QQ implies IT <= r ) assume r in [#] QQ ; ::_thesis: IT <= r then r in f .: P by A7, WEIERSTR:def_1; then r in f .: ([#] PP) by A2, WEIERSTR:def_1; then consider x being set such that A18: x in dom f and A19: x in [#] PP and A20: r = f . x by FUNCT_1:def_6; reconsider x1 = x, x2 = lower_bound ([#] PP) as Point of (Closed-Interval-TSpace (a,b)) by A11, A18; x1 in the carrier of (Closed-Interval-TSpace (a,b)) ; then reconsider r1 = x, r2 = x2 as Real by A16, TOPMETR:17; A21: r2 <= r1 by A9, A19, SEQ_4:def_2; ( f . x1 in the carrier of (Closed-Interval-TSpace (c,d)) & f . x2 in the carrier of (Closed-Interval-TSpace (c,d)) ) ; then reconsider fr = f . x2, fx = f . x1 as Real by A15, TOPMETR:17; percases ( r2 <> r1 or r2 = r1 ) ; suppose r2 <> r1 ; ::_thesis: IT <= r then r2 < r1 by A21, XXREAL_0:1; then fr < fx by A1, A3, A4, A6, Th15; hence IT <= r by A20; ::_thesis: verum end; suppose r2 = r1 ; ::_thesis: IT <= r hence IT <= r by A20; ::_thesis: verum end; end; end; [#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ; then P is compact by A2, A5, COMPTS_1:2; then for P1 being Subset of (Closed-Interval-TSpace (c,d)) st P1 = QQ holds P1 is compact by A3, A7, WEIERSTR:8; then QQ is compact by A7, A8, COMPTS_1:2; then A22: [#] QQ is real-bounded by WEIERSTR:11; lower_bound ([#] PP) in the carrier of (Closed-Interval-TSpace (a,b)) by A12, A10; then lower_bound ([#] PP) in dom f by FUNCT_2:def_1; then IT in QQ by A7, A11, FUNCT_1:def_6; then A23: IT in [#] QQ by WEIERSTR:def_1; for s being real number st 0 < s holds ex r being real number st ( r in [#] QQ & r < IT + s ) proof given s being real number such that A24: 0 < s and A25: for r being real number holds ( not r in [#] QQ or not r < IT + s ) ; ::_thesis: contradiction IT + 0 < IT + s by A24, XREAL_1:8; hence contradiction by A23, A25; ::_thesis: verum end; hence f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) by A22, A23, A17, SEQ_4:def_2; ::_thesis: verum end; theorem :: JORDAN5A:18 for a, b, c, d being Real for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for P, Q being non empty Subset of (Closed-Interval-TSpace (a,b)) for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) proof let a, b, c, d be Real; ::_thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) for P, Q being non empty Subset of (Closed-Interval-TSpace (a,b)) for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: for P, Q being non empty Subset of (Closed-Interval-TSpace (a,b)) for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) let P, Q be non empty Subset of (Closed-Interval-TSpace (a,b)); ::_thesis: for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) let PP, QQ be Subset of R^1; ::_thesis: ( a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q implies f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) ) assume that A1: ( a < b & c < d ) and A2: PP = P and A3: QQ = Q and A4: ( f is continuous & f is one-to-one ) and A5: PP is compact and A6: ( f . a = c & f . b = d ) and A7: f .: P = Q ; ::_thesis: f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) A8: [#] (Closed-Interval-TSpace (c,d)) = the carrier of (Closed-Interval-TSpace (c,d)) ; set IT = f . (upper_bound ([#] PP)); A9: [#] PP is real-bounded by A5, WEIERSTR:11; [#] PP <> {} by A2, WEIERSTR:def_1; then A10: upper_bound ([#] PP) in [#] PP by A5, A9, RCOMP_1:12, WEIERSTR:12; then A11: upper_bound ([#] PP) in P by A2, WEIERSTR:def_1; P c= the carrier of (Closed-Interval-TSpace (a,b)) ; then A12: [#] PP c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, WEIERSTR:def_1; then A13: f . (upper_bound ([#] PP)) in the carrier of (Closed-Interval-TSpace (c,d)) by A10, FUNCT_2:5; A14: [#] R^1 = the carrier of R^1 ; then A15: the carrier of (Closed-Interval-TSpace (c,d)) c= the carrier of R^1 by A8, PRE_TOPC:def_4; then reconsider IT = f . (upper_bound ([#] PP)) as Real by A13, TOPMETR:17; [#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ; then A16: the carrier of (Closed-Interval-TSpace (a,b)) c= the carrier of R^1 by A14, PRE_TOPC:def_4; A17: for r being real number st r in [#] QQ holds IT >= r proof let r be real number ; ::_thesis: ( r in [#] QQ implies IT >= r ) assume r in [#] QQ ; ::_thesis: IT >= r then r in f .: P by A3, A7, WEIERSTR:def_1; then r in f .: ([#] PP) by A2, WEIERSTR:def_1; then consider x being set such that A18: x in dom f and A19: x in [#] PP and A20: r = f . x by FUNCT_1:def_6; reconsider x1 = x, x2 = upper_bound ([#] PP) as Point of (Closed-Interval-TSpace (a,b)) by A11, A18; x1 in the carrier of (Closed-Interval-TSpace (a,b)) ; then reconsider r1 = x, r2 = x2 as Real by A16, TOPMETR:17; A21: r2 >= r1 by A9, A19, SEQ_4:def_1; ( f . x1 in the carrier of (Closed-Interval-TSpace (c,d)) & f . x2 in the carrier of (Closed-Interval-TSpace (c,d)) ) ; then reconsider fr = f . x2, fx = f . x1 as Real by A15, TOPMETR:17; percases ( r2 <> r1 or r2 = r1 ) ; suppose r2 <> r1 ; ::_thesis: IT >= r then r2 > r1 by A21, XXREAL_0:1; then fr > fx by A1, A4, A6, Th15; hence IT >= r by A20; ::_thesis: verum end; suppose r2 = r1 ; ::_thesis: IT >= r hence IT >= r by A20; ::_thesis: verum end; end; end; [#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ; then P is compact by A2, A5, COMPTS_1:2; then for P1 being Subset of (Closed-Interval-TSpace (c,d)) st P1 = QQ holds P1 is compact by A3, A4, A7, WEIERSTR:8; then QQ is compact by A3, A7, A8, COMPTS_1:2; then A22: [#] QQ is real-bounded by WEIERSTR:11; upper_bound ([#] PP) in the carrier of (Closed-Interval-TSpace (a,b)) by A12, A10; then upper_bound ([#] PP) in dom f by FUNCT_2:def_1; then IT in QQ by A3, A7, A11, FUNCT_1:def_6; then A23: IT in [#] QQ by WEIERSTR:def_1; for s being real number st 0 < s holds ex r being real number st ( r in [#] QQ & r > IT - s ) proof given s being real number such that A24: 0 < s and A25: for r being real number holds ( not r in [#] QQ or not r > IT - s ) ; ::_thesis: contradiction IT - s < IT - 0 by A24, XREAL_1:15; hence contradiction by A23, A25; ::_thesis: verum end; hence f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) by A22, A23, A17, SEQ_4:def_1; ::_thesis: verum end; theorem :: JORDAN5A:19 for a, b being real number st a <= b holds ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) proof let a, b be real number ; ::_thesis: ( a <= b implies ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) ) assume A1: a <= b ; ::_thesis: ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) set X = [.a,b.]; a is Real by XREAL_0:def_1; then A2: a in { l where l is Real : ( a <= l & l <= b ) } by A1; A3: for s being real number st 0 < s holds ex r being real number st ( r in [.a,b.] & r < a + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in [.a,b.] & r < a + s ) ) assume A4: 0 < s ; ::_thesis: ex r being real number st ( r in [.a,b.] & r < a + s ) A5: a in [.a,b.] by A2, RCOMP_1:def_1; assume for r being real number st r in [.a,b.] holds r >= a + s ; ::_thesis: contradiction hence contradiction by A4, A5, XREAL_1:29; ::_thesis: verum end; b is Real by XREAL_0:def_1; then A6: b in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } by A1; A7: for s being real number st 0 < s holds ex r being real number st ( r in [.a,b.] & b - s < r ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in [.a,b.] & b - s < r ) ) assume A8: 0 < s ; ::_thesis: ex r being real number st ( r in [.a,b.] & b - s < r ) A9: b in [.a,b.] by A6, RCOMP_1:def_1; assume for r being real number st r in [.a,b.] holds r <= b - s ; ::_thesis: contradiction hence contradiction by A8, A9, XREAL_1:44; ::_thesis: verum end; A10: for r being real number st r in [.a,b.] holds a <= r proof let r be real number ; ::_thesis: ( r in [.a,b.] implies a <= r ) assume r in [.a,b.] ; ::_thesis: a <= r then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1; then ex r1 being Real st ( r1 = r & a <= r1 & r1 <= b ) ; hence a <= r ; ::_thesis: verum end; b is UpperBound of [.a,b.] proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in [.a,b.] or r <= b ) assume r in [.a,b.] ; ::_thesis: r <= b then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1; then ex r1 being Real st ( r1 = r & a <= r1 & r1 <= b ) ; hence r <= b ; ::_thesis: verum end; then A11: [.a,b.] is bounded_above by XXREAL_2:def_10; a is LowerBound of [.a,b.] proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in [.a,b.] or a <= r ) assume r in [.a,b.] ; ::_thesis: a <= r then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1; then ex r1 being Real st ( r1 = r & a <= r1 & r1 <= b ) ; hence a <= r ; ::_thesis: verum end; then A12: [.a,b.] is bounded_below by XXREAL_2:def_9; A13: for r being real number st r in [.a,b.] holds b >= r proof let r be real number ; ::_thesis: ( r in [.a,b.] implies b >= r ) assume r in [.a,b.] ; ::_thesis: b >= r then r in { l where l is Real : ( a <= l & l <= b ) } by RCOMP_1:def_1; then ex r1 being Real st ( r1 = r & a <= r1 & r1 <= b ) ; hence b >= r ; ::_thesis: verum end; a in [.a,b.] by A2, RCOMP_1:def_1; hence ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) by A12, A11, A10, A3, A13, A7, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum end; theorem :: JORDAN5A:20 for a, b, c, d, e, f, g, h being Real for F being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f holds F .: [.e,f.] = [.g,h.] proof let a, b, c, d, e, f, g, h be Real; ::_thesis: for F being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) st a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f holds F .: [.e,f.] = [.g,h.] let F be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); ::_thesis: ( a < b & c < d & e < f & a <= e & f <= b & F is being_homeomorphism & F . a = c & F . b = d & g = F . e & h = F . f implies F .: [.e,f.] = [.g,h.] ) assume that A1: a < b and A2: c < d and A3: e < f and A4: a <= e and A5: f <= b and A6: F is being_homeomorphism and A7: ( F . a = c & F . b = d ) and A8: g = F . e and A9: h = F . f ; ::_thesis: F .: [.e,f.] = [.g,h.] a <= f by A3, A4, XXREAL_0:2; then f in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } by A5; then A10: f in [.a,b.] by RCOMP_1:def_1; then f in the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; then h in the carrier of (Closed-Interval-TSpace (c,d)) by A9, FUNCT_2:5; then A11: h in [.c,d.] by A2, TOPMETR:18; e <= b by A3, A5, XXREAL_0:2; then e in { l1 where l1 is Real : ( a <= l1 & l1 <= b ) } by A4; then A12: e in [.a,b.] by RCOMP_1:def_1; then e in the carrier of (Closed-Interval-TSpace (a,b)) by A1, TOPMETR:18; then g in the carrier of (Closed-Interval-TSpace (c,d)) by A8, FUNCT_2:5; then g in [.c,d.] by A2, TOPMETR:18; then [.g,h.] c= [.c,d.] by A11, XXREAL_2:def_12; then A13: [.g,h.] c= the carrier of (Closed-Interval-TSpace (c,d)) by A2, TOPMETR:18; A14: ( F is continuous & F is one-to-one ) by A6, TOPS_2:def_5; A15: [.g,h.] c= F .: [.e,f.] proof let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in [.g,h.] or aa in F .: [.e,f.] ) A16: F is one-to-one by A6, TOPS_2:def_5; assume aa in [.g,h.] ; ::_thesis: aa in F .: [.e,f.] then aa in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by RCOMP_1:def_1; then consider l being Real such that A17: aa = l and A18: g <= l and A19: l <= h ; A20: rng F = [#] (Closed-Interval-TSpace (c,d)) by A6, TOPS_2:def_5; l in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by A18, A19; then A21: l in [.g,h.] by RCOMP_1:def_1; then l in rng F by A13, A20; then l in dom (F ") by A16, A20, TOPS_2:49; then (F ") . l in rng (F ") by FUNCT_1:def_3; then (F ") . l in [#] (Closed-Interval-TSpace (a,b)) ; then (F ") . l in [.a,b.] by A1, TOPMETR:18; then reconsider x = (F ") . l as Real ; F is onto by A20, FUNCT_2:def_3; then A22: x = (F ") . l by A16, TOPS_2:def_4; then A23: x in dom F by A13, A16, A20, A21, FUNCT_1:32; dom F = [#] (Closed-Interval-TSpace (a,b)) by A6, TOPS_2:def_5; then reconsider e9 = e, f9 = f, x9 = x as Point of (Closed-Interval-TSpace (a,b)) by A1, A12, A10, A13, A16, A20, A21, A22, FUNCT_1:32, TOPMETR:18; reconsider g9 = F . e9, h9 = F . f9, l9 = F . x9 as Point of (Closed-Interval-TSpace (c,d)) ; l9 in the carrier of (Closed-Interval-TSpace (c,d)) ; then l9 in [.c,d.] by A2, TOPMETR:18; then reconsider gg = g9, hh = h9, ll = l9 as Real by A8, A9; A24: x <= f proof assume x > f ; ::_thesis: contradiction then ll > hh by A1, A2, A7, A14, Th15; hence contradiction by A9, A13, A19, A16, A20, A21, A22, FUNCT_1:32; ::_thesis: verum end; e <= x proof assume e > x ; ::_thesis: contradiction then gg > ll by A1, A2, A7, A14, Th15; hence contradiction by A8, A13, A18, A16, A20, A21, A22, FUNCT_1:32; ::_thesis: verum end; then x in { l1 where l1 is Real : ( e <= l1 & l1 <= f ) } by A24; then A25: x in [.e,f.] by RCOMP_1:def_1; aa = F . x by A13, A17, A16, A20, A21, A22, FUNCT_1:32; hence aa in F .: [.e,f.] by A23, A25, FUNCT_1:def_6; ::_thesis: verum end; F .: [.e,f.] c= [.g,h.] proof let aa be set ; :: according to TARSKI:def_3 ::_thesis: ( not aa in F .: [.e,f.] or aa in [.g,h.] ) assume aa in F .: [.e,f.] ; ::_thesis: aa in [.g,h.] then consider x being set such that A26: x in dom F and A27: x in [.e,f.] and A28: aa = F . x by FUNCT_1:def_6; x in { l where l is Real : ( e <= l & l <= f ) } by A27, RCOMP_1:def_1; then consider x9 being Real such that A29: x9 = x and A30: e <= x9 and A31: x9 <= f ; F . x9 in rng F by A26, A29, FUNCT_1:def_3; then F . x9 in [#] (Closed-Interval-TSpace (c,d)) ; then A32: F . x9 in [.c,d.] by A2, TOPMETR:18; then reconsider Fx = F . x9 as Real ; reconsider e1 = e, f1 = f, x1 = x9 as Point of (Closed-Interval-TSpace (a,b)) by A1, A12, A10, A26, A29, TOPMETR:18; reconsider gg = F . e1, hh = F . f1, FFx = F . x1 as Real by A8, A9, A32; A33: Fx <= h proof percases ( f = x or f <> x ) ; suppose f = x ; ::_thesis: Fx <= h hence Fx <= h by A9, A29; ::_thesis: verum end; suppose f <> x ; ::_thesis: Fx <= h then f > x9 by A29, A31, XXREAL_0:1; then hh > FFx by A1, A2, A7, A14, Th15; hence Fx <= h by A9; ::_thesis: verum end; end; end; g <= Fx proof percases ( e = x or e <> x ) ; suppose e = x ; ::_thesis: g <= Fx hence g <= Fx by A8, A29; ::_thesis: verum end; suppose e <> x ; ::_thesis: g <= Fx then e < x9 by A29, A30, XXREAL_0:1; then gg < FFx by A1, A2, A7, A14, Th15; hence g <= Fx by A8; ::_thesis: verum end; end; end; then Fx in { l1 where l1 is Real : ( g <= l1 & l1 <= h ) } by A33; hence aa in [.g,h.] by A28, A29, RCOMP_1:def_1; ::_thesis: verum end; hence F .: [.e,f.] = [.g,h.] by A15, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: JORDAN5A:21 for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ) proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ) ) assume that A1: P meets Q and A2: P /\ Q is closed and A3: P is_an_arc_of p1,p2 ; ::_thesis: ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ) P /\ Q <> {} by A1, XBOOLE_0:def_7; then reconsider P = P as non empty Subset of (TOP-REAL 2) ; consider f being Function of I[01],((TOP-REAL 2) | P) such that A4: f is being_homeomorphism and A5: ( f . 0 = p1 & f . 1 = p2 ) by A3, TOPREAL1:def_1; A6: f is one-to-one by A4, TOPS_2:def_5; [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; then reconsider PQ = P /\ Q as non empty Subset of ((TOP-REAL 2) | P) by A1, XBOOLE_0:def_7, XBOOLE_1:17; reconsider P1 = P, Q1 = Q as non empty Subset of (TOP-REAL 2) by A1, A2, XBOOLE_0:def_7; consider OO being set such that A7: OO in PQ by XBOOLE_0:def_1; reconsider PP = P as Subset of (TOP-REAL 2) ; PP is compact by A3, Th1; then A8: P /\ Q is compact by A2, COMPTS_1:9, XBOOLE_1:17; PQ <> {} ((TOP-REAL 2) | P) ; then reconsider PQ1 = P /\ Q as non empty Subset of ((TOP-REAL 2) | P1) ; (TOP-REAL 2) | (P1 /\ Q1) = ((TOP-REAL 2) | P1) | PQ1 by GOBOARD9:2; then A9: PQ is compact by A8, COMPTS_1:3; set g = f " ; reconsider g1 = f " as Function ; A10: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def_5; [#] I[01] c= [#] R^1 by PRE_TOPC:def_4; then reconsider GPQ = (f ") .: PQ as Subset of R^1 by XBOOLE_1:1; f " is continuous by A4, TOPS_2:def_5; then ( (f ") .: PQ c= [#] I[01] & ( for P being Subset of I[01] st P = GPQ holds P is compact ) ) by A9, WEIERSTR:8; then A11: GPQ is compact by COMPTS_1:2; then A12: [#] GPQ is real-bounded by WEIERSTR:11; set Ex = lower_bound ([#] GPQ); reconsider f1 = f as Function ; take f . (lower_bound ([#] GPQ)) ; ::_thesis: ( f . (lower_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (lower_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (lower_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ) A13: dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1; dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1; then (f ") . OO in GPQ by A7, FUNCT_1:def_6; then [#] GPQ <> {} by WEIERSTR:def_1; then lower_bound ([#] GPQ) in [#] GPQ by A11, A12, RCOMP_1:13, WEIERSTR:12; then A14: lower_bound ([#] GPQ) in GPQ by WEIERSTR:def_1; then A15: lower_bound ([#] GPQ) <= 1 by BORSUK_1:43; A16: dom f = the carrier of I[01] by FUNCT_2:def_1; A17: for t being Real st 0 <= t & t < lower_bound ([#] GPQ) holds not f . t in Q proof let t be Real; ::_thesis: ( 0 <= t & t < lower_bound ([#] GPQ) implies not f . t in Q ) assume that A18: 0 <= t and A19: t < lower_bound ([#] GPQ) ; ::_thesis: not f . t in Q A20: t <= 1 by A15, A19, XXREAL_0:2; then t in the carrier of I[01] by A18, BORSUK_1:43; then f . t in the carrier of ((TOP-REAL 2) | P) by FUNCT_2:5; then A21: f . t in P by PRE_TOPC:8; f is onto by A10, FUNCT_2:def_3; then A22: f " = f1 " by A6, TOPS_2:def_4; assume f . t in Q ; ::_thesis: contradiction then f . t in PQ by A21, XBOOLE_0:def_4; then A23: (f ") . (f . t) in GPQ by A13, FUNCT_1:def_6; t in dom f by A16, A18, A20, BORSUK_1:43; then (f ") . (f . t) = t by A6, A22, FUNCT_1:34; then t in [#] GPQ by A23, WEIERSTR:def_1; hence contradiction by A12, A19, SEQ_4:def_2; ::_thesis: verum end; A24: f " is one-to-one by A10, A6, TOPS_2:50; f " is being_homeomorphism by A4, TOPS_2:56; then rng (f ") = [#] I[01] by TOPS_2:def_5; then f " is onto by FUNCT_2:def_3; then (f ") " = g1 " by A24, TOPS_2:def_4; then A25: f = g1 " by A10, A6, TOPS_2:51; A26: ( ex pq being set st ( pq in dom (f ") & pq in PQ & lower_bound ([#] GPQ) = (f ") . pq ) & 0 <= lower_bound ([#] GPQ) ) by A14, BORSUK_1:43, FUNCT_1:def_6; f " is one-to-one by A10, A6, TOPS_2:50; hence ( f . (lower_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (lower_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (lower_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ) by A4, A5, A25, A26, A15, A17, FUNCT_1:34; ::_thesis: verum end; theorem :: JORDAN5A:22 for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ) proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ) ) assume that A1: P meets Q and A2: P /\ Q is closed and A3: P is_an_arc_of p1,p2 ; ::_thesis: ex EX being Point of (TOP-REAL 2) st ( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ) P /\ Q <> {} by A1, XBOOLE_0:def_7; then reconsider P = P as non empty Subset of (TOP-REAL 2) ; consider f being Function of I[01],((TOP-REAL 2) | P) such that A4: f is being_homeomorphism and A5: ( f . 0 = p1 & f . 1 = p2 ) by A3, TOPREAL1:def_1; A6: f is one-to-one by A4, TOPS_2:def_5; [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; then reconsider PQ = P /\ Q as non empty Subset of ((TOP-REAL 2) | P) by A1, XBOOLE_0:def_7, XBOOLE_1:17; reconsider P1 = P, Q1 = Q as non empty Subset of (TOP-REAL 2) by A1, A2, XBOOLE_0:def_7; consider OO being set such that A7: OO in PQ by XBOOLE_0:def_1; reconsider PP = P as Subset of (TOP-REAL 2) ; PP is compact by A3, Th1; then A8: P /\ Q is compact by A2, COMPTS_1:9, XBOOLE_1:17; PQ <> {} ((TOP-REAL 2) | P) ; then reconsider PQ1 = P /\ Q as non empty Subset of ((TOP-REAL 2) | P1) ; (TOP-REAL 2) | (P1 /\ Q1) = ((TOP-REAL 2) | P1) | PQ1 by GOBOARD9:2; then A9: PQ is compact by A8, COMPTS_1:3; set g = f " ; reconsider g1 = f " as Function ; A10: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def_5; A11: f " is one-to-one by A10, A6, TOPS_2:50; f " is being_homeomorphism by A4, TOPS_2:56; then rng (f ") = [#] I[01] by TOPS_2:def_5; then f " is onto by FUNCT_2:def_3; then (f ") " = g1 " by A11, TOPS_2:def_4; then A12: f = g1 " by A10, A6, TOPS_2:51; [#] I[01] c= [#] R^1 by PRE_TOPC:def_4; then reconsider GPQ = (f ") .: PQ as Subset of R^1 by XBOOLE_1:1; f " is continuous by A4, TOPS_2:def_5; then ( (f ") .: PQ c= [#] I[01] & ( for P being Subset of I[01] st P = GPQ holds P is compact ) ) by A9, WEIERSTR:8; then A13: GPQ is compact by COMPTS_1:2; then A14: [#] GPQ is real-bounded by WEIERSTR:11; set Ex = upper_bound ([#] GPQ); reconsider f1 = f as Function ; take f . (upper_bound ([#] GPQ)) ; ::_thesis: ( f . (upper_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (upper_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (upper_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ) A15: dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1; dom (f ") = the carrier of ((TOP-REAL 2) | P) by FUNCT_2:def_1; then (f ") . OO in GPQ by A7, FUNCT_1:def_6; then [#] GPQ <> {} by WEIERSTR:def_1; then upper_bound ([#] GPQ) in [#] GPQ by A13, A14, RCOMP_1:12, WEIERSTR:12; then A16: upper_bound ([#] GPQ) in GPQ by WEIERSTR:def_1; then A17: 0 <= upper_bound ([#] GPQ) by BORSUK_1:43; A18: dom f = the carrier of I[01] by FUNCT_2:def_1; A19: for t being Real st 1 >= t & t > upper_bound ([#] GPQ) holds not f . t in Q proof let t be Real; ::_thesis: ( 1 >= t & t > upper_bound ([#] GPQ) implies not f . t in Q ) assume that A20: 1 >= t and A21: t > upper_bound ([#] GPQ) ; ::_thesis: not f . t in Q t in the carrier of I[01] by A17, A20, A21, BORSUK_1:43; then f . t in the carrier of ((TOP-REAL 2) | P) by FUNCT_2:5; then A22: f . t in P by PRE_TOPC:8; f is onto by A10, FUNCT_2:def_3; then A23: f " = f1 " by A6, TOPS_2:def_4; assume f . t in Q ; ::_thesis: contradiction then f . t in PQ by A22, XBOOLE_0:def_4; then A24: (f ") . (f . t) in GPQ by A15, FUNCT_1:def_6; t in dom f by A18, A17, A20, A21, BORSUK_1:43; then (f ") . (f . t) = t by A6, A23, FUNCT_1:34; then t in [#] GPQ by A24, WEIERSTR:def_1; hence contradiction by A14, A21, SEQ_4:def_1; ::_thesis: verum end; A25: ( ex pq being set st ( pq in dom (f ") & pq in PQ & upper_bound ([#] GPQ) = (f ") . pq ) & upper_bound ([#] GPQ) <= 1 ) by A16, BORSUK_1:43, FUNCT_1:def_6; f " is one-to-one by A10, A6, TOPS_2:50; hence ( f . (upper_bound ([#] GPQ)) is Point of (TOP-REAL 2) & f . (upper_bound ([#] GPQ)) in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = f . (upper_bound ([#] GPQ)) & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ) by A4, A5, A12, A17, A25, A19, FUNCT_1:34; ::_thesis: verum end; registration cluster non empty V45() V46() V47() finite real-bounded for Element of K6(REAL); existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is finite & b1 is real-bounded ) proof reconsider a = {0} as finite Subset of REAL ; take a ; ::_thesis: ( not a is empty & a is finite & a is real-bounded ) thus ( not a is empty & a is finite & a is real-bounded ) ; ::_thesis: verum end; end; Lm8: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) by PCOMPS_1:def_5, TOPMETR:def_6; theorem Th23: :: JORDAN5A:23 for A being Subset of REAL for B being Subset of R^1 st A = B holds ( A is closed iff B is closed ) proof let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds ( A is closed iff B is closed ) let B be Subset of R^1; ::_thesis: ( A = B implies ( A is closed iff B is closed ) ) assume A1: A = B ; ::_thesis: ( A is closed iff B is closed ) thus ( A is closed implies B is closed ) ::_thesis: ( B is closed implies A is closed ) proof assume A is closed ; ::_thesis: B is closed then (A `) ` is closed ; then A ` is open by RCOMP_1:def_5; then A ` in the topology of R^1 by Lm8, Th5; hence ([#] R^1) \ B is open by PRE_TOPC:def_2, A1, TOPMETR:17; :: according to PRE_TOPC:def_3 ::_thesis: verum end; assume B is closed ; ::_thesis: A is closed then B ` in the topology of R^1 by PRE_TOPC:def_2; then A ` is open by A1, Lm8, Th5, TOPMETR:17; then (A `) ` is closed by RCOMP_1:def_5; hence A is closed ; ::_thesis: verum end; theorem :: JORDAN5A:24 for A being Subset of REAL for B being Subset of R^1 st A = B holds Cl A = Cl B proof let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds Cl A = Cl B let B be Subset of R^1; ::_thesis: ( A = B implies Cl A = Cl B ) assume A1: A = B ; ::_thesis: Cl A = Cl B thus Cl A c= Cl B :: according to XBOOLE_0:def_10 ::_thesis: Cl B c= Cl A proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl A or a in Cl B ) assume A2: a in Cl A ; ::_thesis: a in Cl B for G being Subset of R^1 st G is open & a in G holds B meets G proof let G be Subset of R^1; ::_thesis: ( G is open & a in G implies B meets G ) assume that A3: G is open and A4: a in G ; ::_thesis: B meets G reconsider H = G as Subset of REAL by TOPMETR:17; G in Family_open_set RealSpace by A3, Lm8, PRE_TOPC:def_2; then H is open by Th5; then not A /\ H is empty by A2, A4, MEASURE6:63; hence B meets G by A1, XBOOLE_0:def_7; ::_thesis: verum end; hence a in Cl B by A2, PRE_TOPC:def_7, TOPMETR:17; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl B or a in Cl A ) assume A5: a in Cl B ; ::_thesis: a in Cl A for O being open Subset of REAL st a in O holds not O /\ A is empty proof let O be open Subset of REAL; ::_thesis: ( a in O implies not O /\ A is empty ) assume A6: a in O ; ::_thesis: not O /\ A is empty reconsider P = O as Subset of R^1 by TOPMETR:17; P in Family_open_set RealSpace by Th5; then P is open by Lm8, PRE_TOPC:def_2; then P meets B by A5, A6, PRE_TOPC:def_7; hence not O /\ A is empty by A1, XBOOLE_0:def_7; ::_thesis: verum end; hence a in Cl A by A5, MEASURE6:63, TOPMETR:17; ::_thesis: verum end; registration let a, b be real number ; clusterK289(a,b) -> compact for Subset of REAL; coherence for b1 being Subset of REAL st b1 = [.a,b.] holds b1 is compact by RCOMP_1:6; end; theorem Th25: :: JORDAN5A:25 for A being Subset of REAL for B being Subset of R^1 st A = B holds ( A is compact iff B is compact ) proof let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds ( A is compact iff B is compact ) let B be Subset of R^1; ::_thesis: ( A = B implies ( A is compact iff B is compact ) ) assume A1: A = B ; ::_thesis: ( A is compact iff B is compact ) thus ( A is compact implies B is compact ) ::_thesis: ( B is compact implies A is compact ) proof assume A2: A is compact ; ::_thesis: B is compact percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: B is compact then reconsider C = B as empty Subset of R^1 by A1; C is compact ; hence B is compact ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: B is compact then reconsider A = A as non empty real-bounded Subset of REAL by A2, RCOMP_1:10; reconsider i = inf A, s = sup A as real number ; reconsider X = [.i,s.] as Subset of R^1 by TOPMETR:17; A3: i <= s by XXREAL_2:40; then A4: Closed-Interval-TSpace (i,s) = R^1 | X by TOPMETR:19; A5: B is closed by A1, A2, Th23; A6: X <> {} by A3, XXREAL_1:30; A7: B c= X by A1, XXREAL_2:69; Closed-Interval-TSpace (i,s) is compact by HEINE:4, A3; then X is compact by A6, A4, COMPTS_1:3; hence B is compact by A5, COMPTS_1:9, A7; ::_thesis: verum end; end; end; assume B is compact ; ::_thesis: A is compact then [#] B is compact by WEIERSTR:13; hence A is compact by A1, WEIERSTR:def_1; ::_thesis: verum end; registration cluster finite -> compact for Element of K6(REAL); coherence for b1 being Subset of REAL st b1 is finite holds b1 is compact by Th25, TOPMETR:17; end; theorem :: JORDAN5A:26 for a, b being real number holds ( a <> b iff Cl ].a,b.[ = [.a,b.] ) proof let a, b be real number ; ::_thesis: ( a <> b iff Cl ].a,b.[ = [.a,b.] ) thus ( a <> b implies Cl ].a,b.[ = [.a,b.] ) ::_thesis: ( Cl ].a,b.[ = [.a,b.] implies a <> b ) proof reconsider a1 = a, b1 = b as Real by XREAL_0:def_1; assume A1: a <> b ; ::_thesis: Cl ].a,b.[ = [.a,b.] percases ( a > b or a < b ) by A1, XXREAL_0:1; supposeA2: a > b ; ::_thesis: Cl ].a,b.[ = [.a,b.] hence Cl ].a,b.[ = {} by MEASURE6:60, XXREAL_1:28 .= [.a,b.] by A2, XXREAL_1:29 ; ::_thesis: verum end; supposeA3: a < b ; ::_thesis: Cl ].a,b.[ = [.a,b.] then A4: (a1 + b1) / 2 < b1 by XREAL_1:226; thus Cl ].a,b.[ c= [.a,b.] by MEASURE6:57, XXREAL_1:25; :: according to XBOOLE_0:def_10 ::_thesis: [.a,b.] c= Cl ].a,b.[ let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in [.a,b.] or p in Cl ].a,b.[ ) A5: ].a,b.[ = { w where w is Real : ( a < w & w < b ) } by RCOMP_1:def_2; assume A6: p in [.a,b.] ; ::_thesis: p in Cl ].a,b.[ [.a,b.] = { w where w is Real : ( a <= w & w <= b ) } by RCOMP_1:def_1; then consider r being Real such that A7: p = r and A8: a <= r and A9: r <= b by A6; a1 < (a1 + b1) / 2 by A3, XREAL_1:226; then A10: (a1 + b1) / 2 in ].a1,b1.[ by A5, A4; now__::_thesis:_(_(_a_<_r_&_r_<_b_&_p_in_Cl_].a,b.[_)_or_(_a_=_r_&_p_in_Cl_].a,b.[_)_or_(_b_=_r_&_p_in_Cl_].a,b.[_)_) percases ( ( a < r & r < b ) or a = r or b = r ) by A8, A9, XXREAL_0:1; caseA11: ( a < r & r < b ) ; ::_thesis: p in Cl ].a,b.[ A12: ].a,b.[ c= Cl ].a,b.[ by MEASURE6:58; r in ].a,b.[ by A5, A11; hence p in Cl ].a,b.[ by A7, A12; ::_thesis: verum end; caseA13: a = r ; ::_thesis: p in Cl ].a,b.[ for O being open Subset of REAL st a in O holds not O /\ ].a,b.[ is empty proof let O be open Subset of REAL; ::_thesis: ( a in O implies not O /\ ].a,b.[ is empty ) assume a in O ; ::_thesis: not O /\ ].a,b.[ is empty then consider g being real number such that A14: 0 < g and A15: ].(a - g),(a + g).[ c= O by RCOMP_1:19; reconsider g = g as Real by XREAL_0:def_1; A16: a - g < a - 0 by A14, XREAL_1:15; A17: ].(a - g),(a + g).[ = { w where w is Real : ( a - g < w & w < a + g ) } by RCOMP_1:def_2; percases ( a + g < b or a + g >= b ) ; supposeA18: a + g < b ; ::_thesis: not O /\ ].a,b.[ is empty A19: a + 0 < a + g by A14, XREAL_1:6; then A20: a1 < (a1 + (a1 + g)) / 2 by XREAL_1:226; A21: (a1 + (a1 + g)) / 2 < a1 + g by A19, XREAL_1:226; then (a + (a + g)) / 2 < b by A18, XXREAL_0:2; then A22: (a1 + (a1 + g)) / 2 in ].a1,b1.[ by A5, A20; a - g < (a + (a + g)) / 2 by A16, A20, XXREAL_0:2; then (a1 + (a1 + g)) / 2 in ].(a1 - g),(a1 + g).[ by A17, A21; hence not O /\ ].a,b.[ is empty by A15, A22, XBOOLE_0:def_4; ::_thesis: verum end; supposeA23: a + g >= b ; ::_thesis: not O /\ ].a,b.[ is empty (a1 + b1) / 2 < b1 by A3, XREAL_1:226; then A24: (a + b) / 2 < a + g by A23, XXREAL_0:2; a1 < (a1 + b1) / 2 by A3, XREAL_1:226; then a - g < (a + b) / 2 by A16, XXREAL_0:2; then (a1 + b1) / 2 in ].(a1 - g),(a1 + g).[ by A17, A24; hence not O /\ ].a,b.[ is empty by A10, A15, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence p in Cl ].a,b.[ by A7, A13, MEASURE6:63; ::_thesis: verum end; caseA25: b = r ; ::_thesis: p in Cl ].a,b.[ for O being open Subset of REAL st b in O holds not O /\ ].a,b.[ is empty proof let O be open Subset of REAL; ::_thesis: ( b in O implies not O /\ ].a,b.[ is empty ) assume b in O ; ::_thesis: not O /\ ].a,b.[ is empty then consider g being real number such that A26: 0 < g and A27: ].(b - g),(b + g).[ c= O by RCOMP_1:19; reconsider g = g as Real by XREAL_0:def_1; A28: b - g < b - 0 by A26, XREAL_1:15; A29: b + 0 < b + g by A26, XREAL_1:6; A30: ].(b - g),(b + g).[ = { w where w is Real : ( b - g < w & w < b + g ) } by RCOMP_1:def_2; percases ( b - g > a or b - g <= a ) ; supposeA31: b - g > a ; ::_thesis: not O /\ ].a,b.[ is empty A32: (b1 + (b1 - g)) / 2 < b1 by A28, XREAL_1:226; A33: b1 - g < (b1 + (b1 - g)) / 2 by A28, XREAL_1:226; then a < (b + (b - g)) / 2 by A31, XXREAL_0:2; then A34: (b1 + (b1 - g)) / 2 in ].a1,b1.[ by A5, A32; (b1 + (b1 - g)) / 2 < b1 by A28, XREAL_1:226; then (b + (b - g)) / 2 < b + g by A29, XXREAL_0:2; then (b1 + (b1 - g)) / 2 in ].(b1 - g),(b1 + g).[ by A30, A33; hence not O /\ ].a,b.[ is empty by A27, A34, XBOOLE_0:def_4; ::_thesis: verum end; supposeA35: b - g <= a ; ::_thesis: not O /\ ].a,b.[ is empty (a1 + b1) / 2 < b1 by A3, XREAL_1:226; then A36: (a + b) / 2 < b + g by A29, XXREAL_0:2; a1 < (a1 + b1) / 2 by A3, XREAL_1:226; then b - g < (a + b) / 2 by A35, XXREAL_0:2; then (a1 + b1) / 2 in ].(b1 - g),(b1 + g).[ by A30, A36; hence not O /\ ].a,b.[ is empty by A10, A27, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence p in Cl ].a,b.[ by A7, A25, MEASURE6:63; ::_thesis: verum end; end; end; hence p in Cl ].a,b.[ ; ::_thesis: verum end; end; end; assume that A37: Cl ].a,b.[ = [.a,b.] and A38: a = b ; ::_thesis: contradiction [.a,b.] = {a} by A38, XXREAL_1:17; hence contradiction by A37, A38, MEASURE6:60, XXREAL_1:28; ::_thesis: verum end; theorem :: JORDAN5A:27 for T being TopStruct for f being RealMap of T for g being Function of T,R^1 st f = g holds ( f is continuous iff g is continuous ) proof let T be TopStruct ; ::_thesis: for f being RealMap of T for g being Function of T,R^1 st f = g holds ( f is continuous iff g is continuous ) let f be RealMap of T; ::_thesis: for g being Function of T,R^1 st f = g holds ( f is continuous iff g is continuous ) let g be Function of T,R^1; ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) ) assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous ) thus ( f is continuous implies g is continuous ) ::_thesis: ( g is continuous implies f is continuous ) proof assume A2: for Y being Subset of REAL st Y is closed holds f " Y is closed ; :: according to PSCOMP_1:def_3 ::_thesis: g is continuous let P be Subset of R^1; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or g " P is closed ) assume A3: P is closed ; ::_thesis: g " P is closed reconsider R = P as Subset of REAL by TOPMETR:17; R is closed by A3, Th23; hence g " P is closed by A1, A2; ::_thesis: verum end; assume A4: for Y being Subset of R^1 st Y is closed holds g " Y is closed ; :: according to PRE_TOPC:def_6 ::_thesis: f is continuous let P be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not P is closed or f " P is closed ) assume A5: P is closed ; ::_thesis: f " P is closed reconsider R = P as Subset of R^1 by TOPMETR:17; R is closed by A5, Th23; hence f " P is closed by A1, A4; ::_thesis: verum end;