The abstract of the Mizar article:

On the Decomposition of a Simple Closed Curve into Two Arcs

by

Andrzej Trybulec, and

Yatsuka Nakamura

Received September 16, 2002

MML identifier: JORDAN16

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, PRE_TOPC, SUBSET_1, COMPTS_1, BOOLE, RELAT_1, ORDINAL2,
      FUNCT_1, RCOMP_1, ARYTM_1, PCOMPS_1, EUCLID, BORSUK_1, ARYTM_3, TOPMETR,
      PSCOMP_1, JORDAN2C, SQUARE_1, JORDAN6, TOPREAL1, TOPS_2, TOPREAL2,
      JORDAN3, JGRAPH_2, PARTFUN1, FCONT_1, CONNSP_2, SGRAPH1, REALSET1,
      FINSET_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, NAT_1, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, FUNCT_2,
      FCONT_1, REALSET1, PRE_CIRC, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1,
      CONNSP_2, PCOMPS_1, RCOMP_1, TMAP_1, EUCLID, PSCOMP_1, TOPMETR, JORDAN2C,
      JORDAN6, TOPREAL1, JORDAN5C, TOPREAL2, JORDAN7;
 constructors REAL_1, DOMAIN_1, TOPS_2, RCOMP_1, JORDAN6, JORDAN5C, PSCOMP_1,
      CONNSP_1, FCONT_1, TMAP_1, JORDAN7, PRE_CIRC, JORDAN2C, REALSET1,
      JORDAN9, JORDAN1K;
 clusters FUNCT_1, PRE_TOPC, STRUCT_0, XREAL_0, RELSET_1, EUCLID, TOPMETR,
      JORDAN1B, BORSUK_1, SEQ_1, TEX_2, GROUP_2, MEMBERED, FUNCT_2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

theorem :: JORDAN16:1
   for S1 being finite non empty Subset of REAL, e being Real st
   for r being Real st r in S1 holds r < e
 holds max S1 < e;

reserve C for Simple_closed_curve,
        A,A1,A2 for Subset of TOP-REAL 2,
        p,p1,p2,q,q1,q2 for Point of TOP-REAL 2,
        n for Nat;

definition let n;
 cluster trivial Subset of TOP-REAL n;
end;

theorem :: JORDAN16:2
  for a,b,c,X being set st a in X & b in X & c in X
  holds {a,b,c} c= X;

theorem :: JORDAN16:3
   {}TOP-REAL n is Bounded;

theorem :: JORDAN16:4
   Lower_Arc C <> Upper_Arc C;

theorem :: JORDAN16:5
  Segment(A,p1,p2,q1,q2) c= A;

theorem :: JORDAN16:6
 for T being non empty TopSpace,
     A,B being Subset of T st A c= B
   holds T|A is SubSpace of T|B;

theorem :: JORDAN16:7
 A is_an_arc_of p1,p2 & q in A implies q in L_Segment(A,p1,p2,q);

theorem :: JORDAN16:8
 A is_an_arc_of p1,p2 & q in A implies q in R_Segment(A,p1,p2,q);

theorem :: JORDAN16:9
 A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2
   implies q1 in Segment(A,p1,p2,q1,q2) & q2 in Segment(A,p1,p2,q1,q2);

theorem :: JORDAN16:10
   Segment(p,q,C) c= C;

theorem :: JORDAN16:11
   p in C & q in C implies LE p,q,C or LE q,p,C;

theorem :: JORDAN16:12
 for X,Y being non empty TopSpace, Y0 being non empty SubSpace of Y,
     f being map of X,Y,
     g being map of X,Y0 st f = g & f is continuous
 holds g is continuous;

theorem :: JORDAN16:13
 for S,T being non empty TopSpace,
     S0 being non empty SubSpace of S, T0 being non empty SubSpace of T,
     f being map of S,T st f is_homeomorphism
 for g being map of S0,T0 st g = f|S0 & g is onto
  holds g is_homeomorphism;

theorem :: JORDAN16:14
 for P1,P2,P3 being Subset of TOP-REAL 2
 for p1,p2 being Point of TOP-REAL 2
 st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2
  & P2 /\ P3={p1,p2} & P1 c= P2 \/ P3
 holds P1=P2 or P1=P3;


theorem :: JORDAN16:15
 for C being Simple_closed_curve,
     A1,A2 being Subset of TOP-REAL 2,
     p1,p2 being Point of TOP-REAL 2
  st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2
     & A1 c= C & A2 c= C & A1 <> A2
 holds A1 \/ A2 = C & A1 /\ A2 = {p1,p2};

theorem :: JORDAN16:16
 for A1,A2 being Subset of TOP-REAL 2,
     p1,p2,q1,q2 being Point of TOP-REAL 2
  st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2}
 holds A1 <> A2;


theorem :: JORDAN16:17
   for C being Simple_closed_curve,
     A1,A2 being Subset of TOP-REAL 2,
     p1,p2 being Point of TOP-REAL 2
  st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2
     & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2}
 holds A1 \/ A2 = C;

theorem :: JORDAN16:18
   A1 c= C & A2 c= C & A1 <> A2 &
 A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2
 implies
  for A st A is_an_arc_of p1,p2 & A c= C holds A = A1 or A = A2;

theorem :: JORDAN16:19
 for C being Simple_closed_curve,
     A being non empty Subset of TOP-REAL 2
  st A is_an_arc_of W-min C, E-max C & A c= C
 holds A = Lower_Arc C or A = Upper_Arc C;

theorem :: JORDAN16:20
 A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2
  implies ex g being map of I[01], (TOP-REAL 2)|A, s1, s2 being Real st
  g is_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 & g.s2 = q2 &
   0 <= s1 & s1 <= s2 & s2 <= 1;

theorem :: JORDAN16:21
 A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2 & q1 <> q2
  implies ex g being map of I[01], (TOP-REAL 2)|A, s1, s2 being Real st
  g is_homeomorphism & g.0 = p1 & g.1 = p2 & g.s1 = q1 & g.s2 = q2 &
   0 <= s1 & s1 < s2 & s2 <= 1;

theorem :: JORDAN16:22
   A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2
   implies Segment(A,p1,p2,q1,q2) is non empty;

theorem :: JORDAN16:23
   p in C implies
  p in Segment(p,W-min C,C) & W-min C in Segment(p,W-min C,C);

definition let f be PartFunc of REAL, REAL;
 attr f is continuous means
:: JORDAN16:def 1
 f is_continuous_on dom f;
end;

definition let f be Function of REAL, REAL;
 redefine attr f is continuous means
:: JORDAN16:def 2
     f is_continuous_on REAL;
end;

definition let a,b be real number;
 func AffineMap(a,b) -> Function of REAL, REAL means
:: JORDAN16:def 3
 for x being real number holds it.x = a*x + b;
end;

definition let a,b be real number;
 cluster AffineMap(a,b) -> continuous;
end;

definition
 cluster continuous Function of REAL, REAL;
end;

theorem :: JORDAN16:24
   for f,g being continuous PartFunc of REAL, REAL
  holds g*f is continuous PartFunc of REAL, REAL;

theorem :: JORDAN16:25
 for a,b being real number holds AffineMap(a,b).0 = b;

theorem :: JORDAN16:26
 for a,b being real number holds AffineMap(a,b).1 = a+b;

theorem :: JORDAN16:27
 for a,b being real number st a<> 0
    holds AffineMap(a,b) is one-to-one;

theorem :: JORDAN16:28
   for a,b,x,y being real number st a > 0 & x < y
    holds AffineMap(a,b).x < AffineMap(a,b).y;

theorem :: JORDAN16:29
   for a,b,x,y being real number st a < 0 & x < y
    holds AffineMap(a,b).x > AffineMap(a,b).y;

theorem :: JORDAN16:30
 for a,b,x,y being real number st a >= 0 & x <= y
    holds AffineMap(a,b).x <= AffineMap(a,b).y;

theorem :: JORDAN16:31
   for a,b,x,y being real number st a <= 0 & x <= y
    holds AffineMap(a,b).x >= AffineMap(a,b).y;

theorem :: JORDAN16:32
 for a,b being real number st a <> 0
    holds rng AffineMap(a,b) = REAL;

theorem :: JORDAN16:33
 for a,b being real number st a <> 0
    holds AffineMap(a,b)" = AffineMap(a",-b/a);

theorem :: JORDAN16:34
 for a,b being real number st a > 0
    holds AffineMap(a,b).:[.0,1.] = [.b,a+b.];

theorem :: JORDAN16:35
 for f being map of R^1, R^1
 for a,b being Real st a <> 0 & f = AffineMap(a,b)
  holds f is_homeomorphism;

theorem :: JORDAN16:36
 A is_an_arc_of p1,p2 & LE q1, q2, A, p1, p2 & q1 <> q2
   implies Segment(A,p1,p2,q1,q2) is_an_arc_of q1,q2;

theorem :: JORDAN16:37
   for p1,p2 being Point of TOP-REAL 2
 for P being Subset of TOP-REAL 2 st P c= C
  & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P
 holds Upper_Arc C c= P or Lower_Arc C c= P;