:: Some Properties of Real Maps :: by Adam Grabowski and Yatsuka Nakamura :: :: Received September 10, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users 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 proofend; Lm1: for n being Element of NAT holds ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n ) proofend; 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 ) proofend; 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 ) proofend; Lm2: for n being Element of NAT holds TOP-REAL n is pathwise_connected proofend; 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 ) proofend; 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 proofend; Lm3: for X being Subset of REAL st X is open holds X in Family_open_set RealSpace proofend; Lm4: for X being Subset of REAL st X in Family_open_set RealSpace holds X is open proofend; begin :: Equivalence of analytical and topological definitions of continuity 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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) proofend; 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 proofend; 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 ) proofend; 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)) proofend; 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 ) ) proofend; 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 proofend; 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 proofend; 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 proofend; begin :: On the monotonicity of continuous maps 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 proofend; 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) proofend; 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) proofend; theorem :: JORDAN5A:19 for a, b being real number st a <= b holds ( lower_bound [.a,b.] = a & upper_bound [.a,b.] = b ) proofend; 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.] proofend; 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 ) ) ) proofend; 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 ) ) ) proofend; :: from TOPREAL6, 2011.07.29, A.T. 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 ) proofend; 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 ) proofend; theorem :: JORDAN5A:24 for A being Subset of REAL for B being Subset of R^1 st A = B holds Cl A = Cl B proofend; 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 ) proofend; 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.] ) proofend; :::registration ::: cluster finite -> compact for Subset of REAL; ::: coherence; :::end; :::registration ::: let a, b be real number; ::: cluster [.a,b.] -> compact for Subset of REAL; ::: coherence; :::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 ) proofend;