The Mizar abstract of JORDAN6

Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users
The abstract of the Mizar article:: A Decomposition of Simple Closed Curves and the Order of Their Points
by
Yatsuka Nakamura, and
Andrzej Trybulec
Received December 19, 1997
MML identifier: JORDAN6
[ Mizar article, MML identifier index ]
environ

 vocabulary ARYTM, PRE_TOPC, EUCLID, TOPMETR, PCOMPS_1, BORSUK_1, RCOMP_1,
      ARYTM_3, ARYTM_1, RELAT_1, BOOLE, SUBSET_1, ORDINAL2, FUNCT_1, MCART_1,
      FINSEQ_1, TOPREAL1, RELAT_2, TOPS_2, COMPTS_1, JORDAN5C, JORDAN3,
      TREAL_1, SEQ_1, PSCOMP_1, TOPREAL2, SEQ_2, METRIC_1, SEQ_4, ABSVALUE,
      SQUARE_1, FUNCT_5, JORDAN6;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, RCOMP_1, SETWOP_2, STRUCT_0, ABSVALUE, RELAT_1, FUNCT_1,
      FUNCT_2, TOPREAL1, TOPREAL2, CONNSP_1, JORDAN2B, SQUARE_1, TSEP_1,
      TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, EUCLID, METRIC_1,
      PCOMPS_1, SEQ_4, JORDAN5C, TREAL_1, PSCOMP_1;
 constructors RCOMP_1, ABSVALUE, TOPREAL2, CONNSP_1, JORDAN2B, TSEP_1, TOPS_2,
      REAL_1, TOPREAL1, SQUARE_1, SETWOP_2, JORDAN5C, TREAL_1, PSCOMP_1, TSP_1,
      COMPTS_1, YELLOW_8, PARTFUN1, MEMBERED;
 clusters SUBSET_1, STRUCT_0, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR, METRIC_1,
      PSCOMP_1, BORSUK_2, TSEP_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED,
      ZFMISC_1, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Middle Points of Arcs

reserve x,y for set;
reserve s,r for real number;
reserve r1,r2 for Real;
reserve n for Nat;
reserve p,p3,q,q1,q2,q3 for Point of TOP-REAL 2;

canceled;

theorem :: JORDAN6:2
 r<=s implies r <= (r+s)/2 & (r+s)/2 <= s;

theorem :: JORDAN6:3
for TX being non empty TopSpace,
 P being Subset of TX,
 A being Subset of TX|P,
 B being Subset of TX
 st B is closed & A=B/\P holds A is closed;

theorem :: JORDAN6:4
for TX,TY being non empty TopSpace,
P being non empty Subset of TY,f being map of TX,TY|P
holds f is map of TX,TY &
 for f2 being map of TX,TY
  st f2=f & f is continuous holds f2 is continuous;

theorem :: JORDAN6:5
 for r being real number, P being Subset of TOP-REAL 2
  st P={p where p is Point of TOP-REAL 2: p`1>=r} holds P is closed;

theorem :: JORDAN6:6
 for r being real number, P being Subset of TOP-REAL 2
  st P={p where p is Point of TOP-REAL 2: p`1<=r} holds P is closed;

theorem :: JORDAN6:7
 for r being real number,P being Subset of TOP-REAL 2
  st P={p where p is Point of TOP-REAL 2: p`1=r} holds P is closed;

theorem :: JORDAN6:8
 for r being real number, P being Subset of TOP-REAL 2
  st P={p where p is Point of TOP-REAL 2: p`2>=r} holds P is closed;

theorem :: JORDAN6:9
 for r being real number, P being Subset of TOP-REAL 2
  st P={p where p is Point of TOP-REAL 2: p`2<=r} holds P is closed;

theorem :: JORDAN6:10
 for r being real number, P being Subset of TOP-REAL 2
  st P={p where p is Point of TOP-REAL 2: p`2=r} holds P is closed;

theorem :: JORDAN6:11
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 holds P is connected;

theorem :: JORDAN6:12
for P being Subset of TOP-REAL 2,p1,p2
  being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds P is closed;

theorem :: JORDAN6:13
for P being Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
 holds ex q being Point of TOP-REAL 2 st q in P & q `1 = (p1 `1+p2 `1)/2;

theorem :: JORDAN6:14
for P,Q being Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
 Q={q:q`1=(p1`1+p2`1)/2} holds P meets Q & P /\ Q is closed;

theorem :: JORDAN6:15
for P,Q being Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
 Q={q:q`2=(p1`2+p2`2)/2} holds P meets Q & P /\ Q is closed;

definition let P be non empty Subset of TOP-REAL 2,
              p1,p2 be Point of TOP-REAL 2;
 func x_Middle(P,p1,p2) -> Point of TOP-REAL 2 means
:: JORDAN6:def 1
  for Q being Subset of TOP-REAL 2 st
  Q={q:q`1=(p1`1+p2`1)/2}
  holds it=First_Point(P,p1,p2,Q);
end;

definition let P be non empty Subset of TOP-REAL 2,
               p1,p2 be Point of TOP-REAL 2;
 func y_Middle(P,p1,p2) -> Point of TOP-REAL 2 means
:: JORDAN6:def 2
  for Q being Subset of TOP-REAL 2
  st Q={q:q`2=(p1`2+p2`2)/2}
  holds it=First_Point(P,p1,p2,Q);
end;

theorem :: JORDAN6:16
   for P being non empty Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
 x_Middle(P,p1,p2) in P & y_Middle(P,p1,p2) in P;

theorem :: JORDAN6:17
   for P being non empty Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
 p1=x_Middle(P,p1,p2) iff p1`1=p2`1;

theorem :: JORDAN6:18
   for P being non empty Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
 p1=y_Middle(P,p1,p2) iff p1`2=p2`2;

begin ::Segments of Arcs

theorem :: JORDAN6:19
 for P being Subset of TOP-REAL 2,
  p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
  & LE q1,q2,P,p1,p2 holds LE q2,q1,P,p2,p1;

definition let P be Subset of TOP-REAL 2,
  p1,p2,q1 be Point of TOP-REAL 2;
 func L_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals
:: JORDAN6:def 3
  {q : LE q,q1,P,p1,p2};
end;

definition let P be Subset of TOP-REAL 2,
  p1,p2,q1 be Point of TOP-REAL 2;
 func R_Segment(P,p1,p2,q1) -> Subset of TOP-REAL 2 equals
:: JORDAN6:def 4
  {q: LE q1,q,P,p1,p2};
end;

theorem :: JORDAN6:20
for P being Subset of TOP-REAL 2,
 p1,p2,q1 being Point of TOP-REAL 2
 holds L_Segment(P,p1,p2,q1) c= P;

theorem :: JORDAN6:21
for P being Subset of TOP-REAL 2,
 p1,p2,q1 being Point of TOP-REAL 2
 holds R_Segment(P,p1,p2,q1) c= P;

theorem :: JORDAN6:22
   for P being Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
 L_Segment(P,p1,p2,p1)={p1};

canceled 2;

theorem :: JORDAN6:25
   for P being Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
 L_Segment(P,p1,p2,p2)=P;

theorem :: JORDAN6:26
   for P being Subset of TOP-REAL 2,
 p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
 R_Segment(P,p1,p2,p2)={p2};

theorem :: JORDAN6:27
   for P being Subset of TOP-REAL 2,p1,p2 being
 Point of TOP-REAL 2 st P is_an_arc_of p1,p2 holds
 R_Segment(P,p1,p2,p1)=P;

theorem :: JORDAN6:28
   for P being Subset of TOP-REAL 2,
 p1,p2,q1 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & q1 in P holds
 R_Segment(P,p1,p2,q1)=L_Segment(P,p2,p1,q1);

definition let P be Subset of TOP-REAL 2,
               p1,p2,q1,q2 be Point of TOP-REAL 2;
 func Segment(P,p1,p2,q1,q2) -> Subset of TOP-REAL 2 equals
:: JORDAN6:def 5
   R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2);
end;

theorem :: JORDAN6:29
   for P being Subset of TOP-REAL 2,
 p1,p2,q1,q2 being Point of TOP-REAL 2
 holds Segment(P,p1,p2,q1,q2)={q:LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2};

theorem :: JORDAN6:30
 for P being Subset of TOP-REAL 2,
  p1,p2,q1,q2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2
 holds LE q1,q2,P,p1,p2 iff LE q2,q1,P,p2,p1;

theorem :: JORDAN6:31
for P being Subset of TOP-REAL 2,
  p1,p2,q being Point of TOP-REAL 2 st
  P is_an_arc_of p1,p2 & q in P
 holds L_Segment(P,p1,p2,q)=R_Segment(P,p2,p1,q);

theorem :: JORDAN6:32
   for P being Subset of TOP-REAL 2,
  p1,p2,q1,q2 being Point of TOP-REAL 2 st
  P is_an_arc_of p1,p2 & q1 in P & q2 in P
 holds Segment(P,p1,p2,q1,q2)=Segment(P,p2,p1,q2,q1);

begin ::Decomposition of a Simple Closed Curve into Two Arcs

definition let s be real number;
 func Vertical_Line(s) -> Subset of TOP-REAL 2 equals
:: JORDAN6:def 6
  {p where p is Point of TOP-REAL 2: p`1=s};

 func Horizontal_Line(s) -> Subset of TOP-REAL 2 equals
:: JORDAN6:def 7
  {p: p`2=s};
end;

theorem :: JORDAN6:33
for r being real number holds
  Vertical_Line(r) is closed & Horizontal_Line(r) is closed;

theorem :: JORDAN6:34
 for r being real number,p being Point of TOP-REAL 2 holds
  p in Vertical_Line(r) iff p`1=r;

theorem :: JORDAN6:35
   for r being real number,p being Point of TOP-REAL 2 holds
  p in Horizontal_Line(r) iff p`2=r;

canceled 4;

theorem :: JORDAN6:40
for P being compact non empty Subset of TOP-REAL 2
 st P is_simple_closed_curve
  ex P1,P2 being non empty Subset of TOP-REAL 2 st
   P1 is_an_arc_of W-min(P),E-max(P)
  & P2 is_an_arc_of E-max(P),W-min(P)
  & P1 /\ P2={W-min(P),E-max(P)}
  & P1 \/ P2=P
  & First_Point(P1,W-min(P),E-max(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
   Last_Point(P2,E-max(P),W-min(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2;

begin ::Uniqueness of Decomposition of a Simple Closed Curve

theorem :: JORDAN6:41
for P being Subset of I[01] st
 P=(the carrier of I[01]) \{0,1} holds P is open;

canceled 2;

theorem :: JORDAN6:44
for r,s being real number holds ].r,s.[ misses {r,s};

theorem :: JORDAN6:45
for a,b,c being real number holds c in ].a,b.[ iff a < c & c < b;

theorem :: JORDAN6:46
  for P being Subset of R^1, r,s being real number st
  P=].r,s.[ holds P is open;

theorem :: JORDAN6:47
for S being non empty TopSpace,
  P1,P2 being Subset of S,
  P1' being Subset of S|P2 st P1=P1' & P1 c= P2
  holds S|P1=(S|P2)|P1';

theorem :: JORDAN6:48
for P7 being Subset of I[01] st
P7=(the carrier of I[01]) \{0,1} holds P7<>{} & P7 is connected;

theorem :: JORDAN6:49
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2
holds p1<>p2;

theorem :: JORDAN6:50
   for P being Subset of TOP-REAL n,
     Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is open;

::A proof of the following is almost same as JORDAN5A:1.

canceled;

theorem :: JORDAN6:52
for P being Subset of TOP-REAL n,
    P1,P2 being non empty Subset of TOP-REAL n,
    Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st p1 in P & p2 in P &
P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2
& P1 \/ P2 = P & P1 /\ P2={p1,p2} & Q=P1\{p1,p2}
holds Q is open;

theorem :: JORDAN6:53
for P being Subset of TOP-REAL n,
Q being Subset of (TOP-REAL n)|P,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 & Q=P\{p1,p2} holds Q is connected;

theorem :: JORDAN6:54
for GX being non empty TopSpace,
 P1, P being Subset of GX,
 Q' being Subset of GX|P1,
 Q being Subset of GX|P st P1 c=P & Q=Q' &
 Q' is connected holds Q is connected;

theorem :: JORDAN6:55
for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 ex p3 being Point of TOP-REAL n st
p3 in P & p3<>p1 & p3<>p2;

theorem :: JORDAN6:56
   for P being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st P is_an_arc_of p1,p2
holds P\{p1,p2}<>{};

theorem :: JORDAN6:57
   for P1 being Subset of TOP-REAL n,
     P being Subset of TOP-REAL n,
    Q being Subset of (TOP-REAL n)|P,
    p1,p2 being Point of TOP-REAL n st
P1 is_an_arc_of p1,p2 & P1 c=P & Q=P1\{p1,p2} holds Q is connected;

theorem :: JORDAN6:58
for T,S,V being non empty TopSpace,
  P1 being non empty Subset of S,
  P2 being Subset of S,
  f being map of T,S|P1, g being map of S|P2,V st
  P1 c= P2 & f is continuous & g is continuous
  ex h being map of T,V st h=g*f & h is continuous;

theorem :: JORDAN6:59
for P1,P2 being Subset of TOP-REAL n,
p1,p2 being Point of TOP-REAL n st
P1 is_an_arc_of p1,p2 &
P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1=P2;

theorem :: JORDAN6:60
for P being non empty Subset of TOP-REAL 2,
Q being Subset of (TOP-REAL 2)|P,
p1,p2 being Point of TOP-REAL 2
st P is_simple_closed_curve & p1 in P & p2 in P & p1<>p2 & Q=P\{p1,p2}
holds not Q is connected;

theorem :: JORDAN6:61
for P being non empty Subset of TOP-REAL 2,
    P1,P2,P1',P2' being Subset of TOP-REAL 2,
   p1,p2 being Point of TOP-REAL 2
  st P is_simple_closed_curve
  & P1 is_an_arc_of p1,p2
  & P2 is_an_arc_of p1,p2 & P1 \/ P2=P
  & P1' is_an_arc_of p1,p2
  & P2' is_an_arc_of p1,p2 & P1' \/ P2'=P
 holds P1=P1' & P2=P2' or P1=P2' & P2=P1';

begin ::Lower Arcs and Upper Arcs

definition
  cluster -> real Element of R^1;
end;

canceled 2;

theorem :: JORDAN6:64
for P1 being Subset of TOP-REAL 2,
r being Real,p1,p2 being Point of TOP-REAL 2 st
p1`1<=r & r<=p2`1 & P1 is_an_arc_of p1,p2
holds P1 meets Vertical_Line(r) &
 P1 /\ Vertical_Line(r) is closed;

definition let P be compact non empty Subset of TOP-REAL 2
 such that P is_simple_closed_curve;
 func Upper_Arc(P) -> non empty Subset of TOP-REAL 2 means
:: JORDAN6:def 8

  it is_an_arc_of W-min(P),E-max(P) &
 ex P2 being non empty Subset of TOP-REAL 2 st
  P2 is_an_arc_of E-max(P),W-min(P)
  & it /\ P2={W-min(P),E-max(P)}
  & it \/ P2=P
  & First_Point(it,W-min(P),E-max(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
   Last_Point(P2,E-max(P),W-min(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
end;

definition let P be compact non empty Subset of TOP-REAL 2; assume
 P is_simple_closed_curve;
 func Lower_Arc(P) -> non empty Subset of TOP-REAL 2 means
:: JORDAN6:def 9

  it is_an_arc_of E-max(P),W-min(P)
  & Upper_Arc(P) /\ it={W-min(P),E-max(P)}
  & Upper_Arc(P) \/ it=P
  & First_Point(Upper_Arc(P),W-min(P),E-max(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
   Last_Point(it,E-max(P),W-min(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2;
end;

theorem :: JORDAN6:65
for P being compact non empty Subset of (TOP-REAL 2)
 st P is_simple_closed_curve holds
  Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) &
  Upper_Arc(P) is_an_arc_of E-max(P),W-min(P) &
  Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) &
  Lower_Arc(P) is_an_arc_of W-min(P),E-max(P) &
  Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)}
  & Upper_Arc(P) \/ Lower_Arc(P)=P
  & First_Point(Upper_Arc(P),W-min(P),E-max(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2>
   Last_Point(Lower_Arc(P),E-max(P),W-min(P),
                  Vertical_Line((W-bound(P)+E-bound(P))/2))`2;

theorem :: JORDAN6:66
for P being compact non empty Subset of (TOP-REAL 2)
 st P is_simple_closed_curve
 holds Lower_Arc(P)=(P\Upper_Arc(P)) \/ {W-min(P),E-max(P)} &
       Upper_Arc(P)=(P\Lower_Arc(P)) \/ {W-min(P),E-max(P)};

theorem :: JORDAN6:67
   for P being compact non empty Subset of (TOP-REAL 2),
 P1 being Subset of (TOP-REAL 2)|P
 st P is_simple_closed_curve
 & Upper_Arc(P) /\ P1={W-min(P),E-max(P)} & Upper_Arc(P) \/ P1=P
 holds P1=Lower_Arc(P);

theorem :: JORDAN6:68
   for P being compact non empty Subset of (TOP-REAL 2),
 P1 being Subset of (TOP-REAL 2)|P
 st P is_simple_closed_curve
 & P1 /\ Lower_Arc(P)={W-min(P),E-max(P)} & P1 \/ Lower_Arc(P)=P
 holds P1=Upper_Arc(P);

begin ::An Order of Points in a Simple Closed Curve

theorem :: JORDAN6:69
for P being Subset of TOP-REAL 2,
  p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
  LE q,p1,P,p1,p2 holds q=p1;

theorem :: JORDAN6:70
for P being Subset of TOP-REAL 2,
  p1, p2, q being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 &
  LE p2,q,P,p1,p2 holds q=p2;

definition
 let P be compact non empty Subset of TOP-REAL 2,
     q1,q2 be Point of TOP-REAL 2;
 pred LE q1,q2,P means
:: JORDAN6:def 10
  q1 in Upper_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) or
          q1 in Upper_Arc(P) & q2 in Upper_Arc(P) &
            LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) or
          q1 in Lower_Arc(P) & q2 in Lower_Arc(P)& not q2=W-min(P) &
            LE q1,q2,Lower_Arc(P),E-max(P),W-min(P);
end;

theorem :: JORDAN6:71
   for P being compact non empty Subset of (TOP-REAL 2),
  q being Point of TOP-REAL 2
 st P is_simple_closed_curve & q in P
 holds LE q,q,P;

theorem :: JORDAN6:72
   for P being compact non empty Subset of TOP-REAL 2,
 q1,q2 being Point of TOP-REAL 2
 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q1,P
 holds q1=q2;

theorem :: JORDAN6:73
   for P being compact non empty Subset of TOP-REAL 2,
 q1,q2,q3 being Point of TOP-REAL 2
 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P
 holds LE q1,q3,P;
The abstract of the Mizar article:

A Decomposition of Simple Closed Curves and the Order of Their Points
