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