Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Some Properties of Real Maps

**by****Adam Grabowski, and****Yatsuka Nakamura**- Received September 10, 1997
- MML identifier: JORDAN5A

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, EUCLID, TOPREAL1, COMPTS_1, BORSUK_1, RELAT_1, TOPS_2, FUNCT_1, BOOLE, ORDINAL2, SUBSET_1, METRIC_1, PCOMPS_1, RCOMP_1, ARYTM_1, CONNSP_2, TOPS_1, ARYTM_3, TOPMETR, COMPLEX1, ABSVALUE, BORSUK_2, GRAPH_1, PARTFUN1, TMAP_1, FCONT_1, RFUNCT_2, SQUARE_1, SEQ_4, LATTICES, SEQ_2, FINSEQ_4, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, SQUARE_1, FCONT_1, RFUNCT_2, TOPMETR, BINOP_1, RCOMP_1, PARTFUN1, NAT_1, FINSEQ_4, TOPS_1, SEQ_1, SEQ_4, METRIC_1, CONNSP_2, STRUCT_0, TOPREAL1, PRE_TOPC, TOPS_2, COMPTS_1, EUCLID, TMAP_1, ABSVALUE, PCOMPS_1, WEIERSTR, BORSUK_2; constructors REAL_1, ABSVALUE, SQUARE_1, TOPS_1, TOPREAL1, TOPS_2, COMPTS_1, RCOMP_1, SEQ_4, WEIERSTR, FCONT_1, RFUNCT_2, TMAP_1, BORSUK_2, TSP_1, YELLOW_8, FINSEQ_4, SEQ_1; clusters PRE_TOPC, RCOMP_1, RELSET_1, STRUCT_0, TOPMETR, EUCLID, BORSUK_2, WAYBEL_9, PSCOMP_1, XREAL_0, METRIC_1, TOPREAL1, MEMBERED, ORDINAL2; 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 r being real number holds 0 <= r & r <= 1 iff r in the carrier of I[01]; theorem :: JORDAN5A:3 for n being Nat, p1, p2 being Point of TOP-REAL n, r1, r2 being real number st (1-r1)*p1+r1*p2 = (1-r2)*p1+r2*p2 holds r1 = r2 or p1 = p2; theorem :: JORDAN5A:4 for n being Nat for p1,p2 being Point of TOP-REAL n st p1 <> p2 ex f being map 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_homeomorphism & f.0 = p1 & f.1 = p2; definition let n be Nat; cluster TOP-REAL n -> arcwise_connected; end; definition let n be Nat; cluster compact non empty SubSpace of TOP-REAL n; end; theorem :: JORDAN5A:5 for a, b be Point of TOP-REAL 2, f be Path of a, b, P be non empty compact SubSpace of TOP-REAL 2, g be map of I[01], P st f is one-to-one & g = f & [#]P = rng f holds g is_homeomorphism; begin :: Equivalence of analytical and topological definitions of continuity theorem :: JORDAN5A:6 for X being Subset of REAL holds X in Family_open_set RealSpace iff X is open; theorem :: JORDAN5A:7 for f being map 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:8 for f being continuous map of R^1, R^1, g being PartFunc of REAL, REAL st f = g holds g is_continuous_on REAL; theorem :: JORDAN5A:9 for f being continuous one-to-one map 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:10 for r, gg, a, b being Real, x being Element of Closed-Interval-MSpace (a, b) st a <= b & x = r & gg > 0 & ].r-gg, r+gg.[ c= [.a,b.] holds ].r-gg, r+gg.[ = Ball (x, gg); theorem :: JORDAN5A:11 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:12 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:13 for a, b being Real, X being Subset of REAL, V being Subset of Closed-Interval-MSpace(a,b) st a <= b & V = X holds X is open implies V in Family_open_set Closed-Interval-MSpace(a,b); theorem :: JORDAN5A:14 for a, b, c, d, x1 being Real, f being map 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:15 for a, b, c, d being Real, f being map 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 is_continuous_on [.a,b.]; begin :: On the monotonicity of continuous maps theorem :: JORDAN5A:16 for a, b, c, d being Real for f being map 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:17 for f being continuous one-to-one map 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:18 for a, b, c, d being Real, f being map 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:19 for a, b, c, d being Real, f being map 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:20 for a, b be Real st a <= b holds lower_bound [.a,b.] = a & upper_bound [.a,b.] = b; theorem :: JORDAN5A:21 for a, b, c, d, e, f, g, h being Real for F being map of Closed-Interval-TSpace (a,b), Closed-Interval-TSpace (c,d) st a < b & c < d & e < f & a <= e & f <= b & F is_homeomorphism & F.a = c & F.b = d & g = F.e & h = F.f holds F.:[.e, f.] = [.g, h.]; 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 being Point of TOP-REAL 2 st ( EX in P /\ Q & ex g being map of I[01], (TOP-REAL 2)|P, s2 being Real st g is_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:23 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 map of I[01], (TOP-REAL 2)|P, s2 being Real st g is_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));

Back to top