:: Some Properties of Real Maps :: by Adam Grabowski and Yatsuka Nakamura :: :: Received September 10, 1997 :: Copyright (c) 1997-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, TOPREAL1, RCOMP_1, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, CARD_1, XBOOLE_0, ORDINAL2, STRUCT_0, METRIC_1, ARYTM_1, ARYTM_3, SUPINF_2, RLTOPSP1, REAL_1, XXREAL_1, TARSKI, XXREAL_0, PCOMPS_1, CONNSP_2, TOPMETR, TOPS_1, COMPLEX1, BORSUK_2, GRAPH_1, PARTFUN1, TMAP_1, FCONT_1, VALUED_0, SEQ_4, XXREAL_2, FUNCT_2, PSCOMP_1, FINSET_1, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, XXREAL_2, REAL_1, RELAT_1, FUNCT_1, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, FCONT_1, RFUNCT_2, SEQ_4, MEASURE6, TOPMETR, BINOP_1, TOPS_1, METRIC_1, CONNSP_2, STRUCT_0, TOPREAL1, PRE_TOPC, TOPS_2, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, TMAP_1, PSCOMP_1, PCOMPS_1, WEIERSTR, BORSUK_2, RCOMP_1; constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, FCONT_1, TOPS_1, TOPS_2, COMPTS_1, TMAP_1, TOPREAL1, WEIERSTR, BORSUK_2, RVSUM_1, CONVEX1, BINOP_2, PSCOMP_1, MEASURE6, BINOP_1; registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, PSCOMP_1, BORSUK_2, VALUED_0, COMPTS_1, XXREAL_2, RLTOPSP1, FCONT_1, FUNCT_2, FUNCT_1, TOPS_1, SUBSET_1, FINSET_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries theorem :: JORDAN5A:1 for n being Nat, p, q being Point of TOP-REAL n, P being Subset of TOP-REAL n st P is_an_arc_of p, q holds P is compact; theorem :: JORDAN5A:2 for n being Nat, p1, p2 being Point of TOP-REAL n, r1, r2 being Real st (1-r1)*p1+r1*p2 = (1-r2)*p1+r2*p2 holds r1 = r2 or p1 = p2; theorem :: JORDAN5A:3 for n being Nat for p1,p2 being Point of TOP-REAL n st p1 <> p2 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; registration let n be Nat; cluster TOP-REAL n -> pathwise_connected; end; registration let n be Nat; cluster compact non empty strict for SubSpace of TOP-REAL n; end; theorem :: JORDAN5A:4 for a, b being Point of TOP-REAL 2, f being Path of a, b, P being non empty compact SubSpace of TOP-REAL 2, g being Function of I[01], P st f is one-to-one & g = f & [#]P = rng f holds g is being_homeomorphism; begin :: Equivalence of analytical and topological definitions of continuity theorem :: JORDAN5A:5 for X being Subset of REAL holds X in Family_open_set RealSpace iff X is open; theorem :: JORDAN5A:6 for f being Function of R^1, R^1, x being Point of R^1 for g being PartFunc of REAL, REAL, x1 being Real st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1; theorem :: JORDAN5A:7 for f being continuous Function of R^1, R^1, g being PartFunc of REAL, REAL st f = g holds g is continuous; theorem :: JORDAN5A:8 for f being continuous one-to-one Function of R^1, R^1 holds (for x, y being Point of I[01], 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], p, q, fx, fy being Real st x = p & y = q & p < q & fx = f.x & fy = f.y holds fx > fy; theorem :: JORDAN5A:9 for r, gg, a, b being Real, 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); theorem :: JORDAN5A:10 for a, b being Real, X being Subset of REAL st a < b & not a in X & not b in X holds X in Family_open_set Closed-Interval-MSpace(a,b) implies X is open; theorem :: JORDAN5A:11 for X being open Subset of REAL, a, b being Real st X c= [.a,b.] holds not a in X & not b in X; theorem :: JORDAN5A:12 for a, b being Real, X being Subset of REAL, V being Subset of Closed-Interval-MSpace(a,b) st V = X holds X is open implies V in Family_open_set Closed-Interval-MSpace(a,b); theorem :: JORDAN5A:13 for a, b, c, d, x1 being Real, f being Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d), x being Point of Closed-Interval-TSpace(a,b), 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; theorem :: JORDAN5A:14 for a, b, c, d being Real, f being Function of Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d), g being PartFunc of REAL, REAL st f is continuous one-to-one & a < b & c < d & f = g & f.a = c & f. b = d holds g| [.a,b.] is continuous; begin :: On the monotonicity of continuous maps theorem :: 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 one-to-one & f.a = c & f.b = d holds for x, y be Point of Closed-Interval-TSpace(a,b), p, q, fx, fy being Real st x = p & y = q & p < q & fx = f.x & fy = f.y holds fx < fy; theorem :: JORDAN5A:16 for f being continuous one-to-one Function of I[01], I[01] st f.0 = 0 & f.1 = 1 holds for x, y being Point of I[01], p, q, fx, fy being Real st x = p & y = q & p < q & fx = f.x & fy = f.y holds fx < fy; theorem :: JORDAN5A:17 for a, b, c, d being Real, f being Function of Closed-Interval-TSpace( a,b), Closed-Interval-TSpace(c,d), P being non empty Subset of Closed-Interval-TSpace(a,b), PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous one-to-one & PP is compact & f.a = c & f.b = d & f.:P = QQ holds f.(lower_bound [#]PP) = lower_bound [#]QQ; theorem :: JORDAN5A:18 for a, b, c, d being Real, f being Function of Closed-Interval-TSpace( a,b), Closed-Interval-TSpace(c,d), P, Q being non empty Subset of Closed-Interval-TSpace(a,b), PP, QQ being Subset of R^1 st a < b & c < d & PP = P & QQ = Q & f is continuous one-to-one & PP is compact & f.a = c & f.b = d & f .:P = Q holds f.(upper_bound [#]PP) = upper_bound [#]QQ; theorem :: JORDAN5A:19 for a, b being Real st a <= b holds lower_bound [.a,b.] = a & upper_bound [.a,b.] = b; 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.]; theorem :: JORDAN5A:21 for P, Q being Subset of TOP-REAL 2, 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, 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 ); theorem :: JORDAN5A:22 for P, Q being Subset of TOP-REAL 2, 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 be Point of TOP-REAL 2 st ( EX in P /\ Q & ex g being Function of I[01], (TOP-REAL 2)|P, 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 ); :: from TOPREAL6, 2011.07.29, A.T. registration cluster non empty finite real-bounded for Subset of REAL; end; theorem :: JORDAN5A:23 for A being Subset of REAL, B being Subset of R^1 st A = B holds A is closed iff B is closed; theorem :: JORDAN5A:24 for A being Subset of REAL, B being Subset of R^1 st A = B holds Cl A = Cl B; registration let a, b be Real; cluster [.a,b.] -> compact for Subset of REAL; end; theorem :: JORDAN5A:25 for A being Subset of REAL, B being Subset of R^1 st A = B holds A is compact iff B is compact; registration cluster finite -> compact for Subset of REAL; end; theorem :: JORDAN5A:26 for a, b being Real holds a <> b iff Cl ].a,b.[ = [.a,b.]; theorem :: JORDAN5A:27 for T being TopStruct, f being RealMap of T, g being Function of T, R^1 st f = g holds f is continuous iff g is continuous;