The abstract of the Mizar article:

The Ordering of Points on a Curve. Part II

by

Adam Grabowski, and

Yatsuka Nakamura

Received September 10, 1997

MML identifier: JORDAN5C

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_1, EUCLID, PRE_TOPC, BORSUK_1, RELAT_1, TOPREAL1, FUNCT_1,
      TOPS_2, SUBSET_1, ORDINAL2, BOOLE, COMPTS_1, JORDAN3, RCOMP_1, FINSEQ_1,
      TREAL_1, SEQ_1, TOPMETR, JORDAN5C, FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, REAL_1, NAT_1, RCOMP_1, RELAT_1,
      FINSEQ_1, FUNCT_1, FUNCT_2, TOPMETR, FINSEQ_4, JORDAN3, STRUCT_0,
      TOPREAL1, PRE_TOPC, TOPS_2, COMPTS_1, EUCLID, TREAL_1;
 constructors REAL_1, NAT_1, TOPS_2, COMPTS_1, RCOMP_1, TREAL_1, JORDAN3,
      TOPREAL1, FINSEQ_4, MEMBERED;
 clusters BORSUK_1, EUCLID, FUNCT_1, PRE_TOPC, RELSET_1, STRUCT_0, XREAL_0,
      ARYTM_3, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

theorem :: JORDAN5C:1    :: Characterization of First Point Intersecting Q
 for P, Q being Subset of TOP-REAL 2,
     p1, p2, q1 being Point of TOP-REAL 2,
     f being map of I[01], (TOP-REAL 2)|P, s1 be Real
  st P is_an_arc_of p1,p2 & q1 in P & q1 in Q & f.s1 = q1 & f is_homeomorphism
  & f.0 = p1 & f.1 = p2 & 0 <= s1 & s1 <= 1 &
  (for t being Real st 0 <= t & t < s1 holds not f.t in Q) holds
  for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
  g is_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = q1
  & 0 <= s2 & s2 <= 1 holds
  (for t being Real st 0 <= t & t < s2 holds not g.t in Q);

definition
 let P, Q be Subset of TOP-REAL 2,
     p1, p2 be Point of TOP-REAL 2;
 assume  P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2;
  func First_Point(P,p1,p2,Q) -> Point of TOP-REAL 2 means
:: JORDAN5C:def 1
   it in P /\ Q &
   for 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 = it & 0 <= s2 & s2 <= 1 holds
    (for t being Real st 0 <= t & t < s2 holds not g.t in Q);
end;

theorem :: JORDAN5C:2
   for P, Q being Subset of TOP-REAL 2,
     p, p1, p2 being Point of TOP-REAL 2 st
    p in P & P is_an_arc_of p1, p2 & Q = {p} holds
 First_Point (P,p1,p2,Q) = p;

theorem :: JORDAN5C:3
 for P being Subset of TOP-REAL 2,
     Q being Subset of TOP-REAL 2,
     p1, p2 being Point of TOP-REAL 2 st
  p1 in Q & P /\ Q is closed & P is_an_arc_of p1, p2 holds
   First_Point (P, p1, p2, Q) = p1;

theorem :: JORDAN5C:4    ::Characterization of Last Point Intersecting Q

 for P, Q being Subset of TOP-REAL 2,
     p1, p2, q1 being Point of TOP-REAL 2,
     f being map of I[01], (TOP-REAL 2)|P,
     s1 be Real
   st P is_an_arc_of p1,p2 & q1 in P & q1 in Q & f.s1 = q1 &
      f is_homeomorphism & f.0 = p1 & f.1 = p2 & 0 <= s1 & s1 <= 1 &
   (for t being Real st 1 >= t & t > s1 holds not f.t in Q) holds
   for 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 = q1
   & 0 <= s2 & s2 <= 1 holds
    (for t being Real st 1 >= t & t > s2 holds not g.t in Q);

definition
 let P, Q be Subset of TOP-REAL 2,
     p1,p2 be Point of TOP-REAL 2;
  assume  P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2;
  func Last_Point (P,p1,p2,Q) -> Point of TOP-REAL 2 means
:: JORDAN5C:def 2
  it in P /\ Q &
  for g being map of I[01], (TOP-REAL 2)|P, s2 be Real st
  g is_homeomorphism
  & g.0 = p1 & g.1 = p2
  & g.s2 = it & 0 <= s2 & s2 <= 1 holds
   for t being Real st 1 >= t & t > s2 holds not g.t in Q;
end;

theorem :: JORDAN5C:5
   for P, Q being Subset of TOP-REAL 2,
     p, p1,p2 being Point of TOP-REAL 2 st
   p in P & P is_an_arc_of p1, p2 & Q = {p} holds
 Last_Point (P, p1, p2, Q) = p;

theorem :: JORDAN5C:6
 for P,Q being Subset of TOP-REAL 2,
    p1, p2 being Point of TOP-REAL 2 st
  p2 in Q & P /\ Q is closed & P is_an_arc_of p1, p2 holds
   Last_Point (P, p1, p2, Q) = p2;

theorem :: JORDAN5C:7
 for P being Subset of TOP-REAL 2,
     Q being Subset of TOP-REAL 2,
    p1, p2 being Point of TOP-REAL 2 st
    P c= Q & P is closed & P is_an_arc_of p1, p2 holds
   First_Point (P, p1, p2, Q) = p1 &
    Last_Point (P, p1, p2, Q) = p2;

begin :: The ordering of points on a curve

definition let P be Subset of TOP-REAL 2,
               p1, p2, q1, q2 be Point of TOP-REAL 2;
 pred LE q1, q2, P, p1, p2 means
:: JORDAN5C:def 3
  q1 in P & q2 in P &
  for g being map of I[01], (TOP-REAL 2)|P,
      s1, s2 being Real st
  g is_homeomorphism
  & g.0 = p1 & g.1 = p2
  & g.s1 = q1 & 0 <= s1 & s1 <= 1
  & g.s2 = q2 & 0 <= s2 & s2 <= 1
  holds s1 <= s2;
end;

theorem :: JORDAN5C:8
 for P being Subset of TOP-REAL 2,
     p1, p2, q1, q2 being Point of TOP-REAL 2,
     g being map of I[01], (TOP-REAL 2)|P,
     s1, s2 being Real st
  P is_an_arc_of p1,p2 & g is_homeomorphism & g.0 = p1 & g.1 = p2
  & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <=
 s2 holds
  LE q1,q2,P,p1,p2;

theorem :: JORDAN5C:9
  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
   LE q1,q1,P,p1,p2;

theorem :: JORDAN5C:10
 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
   LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2;

theorem :: JORDAN5C:11
   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
  LE p1,p2,P,p1,p2;

theorem :: JORDAN5C:12
 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 & LE q2,q1,P,p1,p2 holds q1=q2;

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

theorem :: JORDAN5C:14
   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 & q1 <> q2
    holds
 LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 or
 LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2;

begin :: Some properties of the ordering of points on a curve

theorem :: JORDAN5C:15
for f being FinSequence of TOP-REAL 2,
    Q being Subset of TOP-REAL 2,
    q being Point of TOP-REAL 2 st
     f is_S-Seq & L~f /\ Q is closed & q in L~f & q in Q holds
    LE First_Point(L~f,f/.1,f/.len f,Q), q, L~f, f/.1, f/.len f;

theorem :: JORDAN5C:16
for f being FinSequence of TOP-REAL 2,
    Q being Subset of TOP-REAL 2,
    q being Point of TOP-REAL 2 st
     f is_S-Seq & L~f /\ Q is closed & q in L~f & q in Q holds
    LE q, Last_Point(L~f,f/.1,f/.len f,Q), L~f, f/.1, f/.len f;

theorem :: JORDAN5C:17
 for q1, q2, p1, p2 being Point of TOP-REAL 2 st p1 <> p2 holds
  LE q1, q2, LSeg(p1, p2), p1, p2 implies LE q1, q2, p1, p2;

theorem :: JORDAN5C:18
   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 & P meets Q & P /\ Q is closed holds
   First_Point(P,p1,p2,Q) = Last_Point(P,p2,p1,Q) &
   Last_Point(P,p1,p2,Q) = First_Point(P,p2,p1,Q);

theorem :: JORDAN5C:19
  for f being FinSequence of TOP-REAL 2,
      Q being Subset of TOP-REAL 2,
      i being Nat
      st L~f meets Q & Q is closed & f is_S-Seq & 1 <= i & i+1 <= len f &
      First_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i) holds
   First_Point (L~f, f/.1, f/.len f, Q) =
          First_Point (LSeg (f, i), f/.i, f/.(i+1), Q);

theorem :: JORDAN5C:20
  for f being FinSequence of TOP-REAL 2,
      Q being Subset of TOP-REAL 2,
      i being Nat
      st L~f meets Q & Q is closed & f is_S-Seq & 1 <= i & i+1 <= len f &
      Last_Point (L~f, f/.1, f/.len f, Q) in LSeg (f, i) holds
   Last_Point (L~f, f/.1, f/.len f, Q) =
          Last_Point (LSeg (f, i), f/.i, f/.(i+1), Q);

theorem :: JORDAN5C:21
   for f being FinSequence of TOP-REAL 2,
     i be Nat st 1 <= i & i+1 <= len f & f is_S-Seq &
   First_Point (L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i) holds
  First_Point (L~f, f/.1, f/.len f, LSeg (f,i) ) = f/.i;

theorem :: JORDAN5C:22
   for f being FinSequence of TOP-REAL 2,
     i be Nat st 1 <= i & i+1 <= len f & f is_S-Seq &
   Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) in LSeg (f,i)
     holds
  Last_Point ( L~f, f/.1, f/.len f, LSeg (f,i) ) = f/.(i+1);

theorem :: JORDAN5C:23
 for f be FinSequence of TOP-REAL 2,
     i be Nat st
   f is_S-Seq & 1 <= i & i+1 <= len f holds
  LE f/.i, f/.(i+1), L~f, f/.1, f/.len f;

theorem :: JORDAN5C:24
 for f be FinSequence of TOP-REAL 2,
     i, j be Nat st
   f is_S-Seq & 1 <= i & i <= j & j <= len f holds
  LE f/.i, f/.j, L~f, f/.1, f/.len f;

theorem :: JORDAN5C:25
for f being FinSequence of TOP-REAL 2,
    q being Point of TOP-REAL 2,
    i being Nat st
     f is_S-Seq & 1 <= i & i+1 <= len f & q in LSeg(f,i) holds
        LE f/.i, q, L~f, f/.1, f/.len f;

theorem :: JORDAN5C:26
for f being FinSequence of TOP-REAL 2,
    q being Point of TOP-REAL 2,
    i being Nat st
     f is_S-Seq & 1<=i & i+1<=len f & q in LSeg(f,i) holds
        LE q, f/.(i+1), L~f, f/.1, f/.len f;

theorem :: JORDAN5C:27
  for f being FinSequence of TOP-REAL 2,
    Q being Subset of TOP-REAL 2,
    q being Point of TOP-REAL 2,
    i, j being Nat st
     L~f meets Q & f is_S-Seq & Q is closed &
     First_Point (L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f &
      q in LSeg(f,j) & 1 <= j & j + 1 <= len f & q in Q &
       First_Point (L~f,f/.1,f/.len f,Q) <> q
    holds
  i <= j &
  (i=j implies LE First_Point(L~f,f/.1,f/.len f,Q), q, f/.i, f/.(i+1));

theorem :: JORDAN5C:28
  for f being FinSequence of TOP-REAL 2,
    Q being Subset of TOP-REAL 2,
    q being Point of TOP-REAL 2,
    i, j being Nat st
     L~f meets Q & f is_S-Seq & Q is closed &
     Last_Point (L~f,f/.1,f/.len f,Q) in LSeg(f,i) & 1<=i & i+1<=len f &
      q in LSeg(f,j) & 1 <= j & j + 1 <= len f & q in Q &
       Last_Point (L~f,f/.1,f/.len f,Q) <> q holds
  i >= j &
  (i=j implies LE q, Last_Point(L~f,f/.1,f/.len f,Q), f/.i, f/.(i+1));

theorem :: JORDAN5C:29
 for f being FinSequence of TOP-REAL 2,
     q1, q2 being Point of TOP-REAL 2,
     i being Nat st
     q1 in LSeg(f,i) & q2 in LSeg(f,i) & f is_S-Seq & 1 <= i & i + 1 <= len f
 holds LE q1, q2, L~f, f/.1, f/.len f implies
         LE q1, q2, LSeg (f,i), f/.i, f/.(i+1);

theorem :: JORDAN5C:30
   for f being FinSequence of TOP-REAL 2,
     q1, q2 being Point of TOP-REAL 2 st
     q1 in L~f & q2 in L~f & f is_S-Seq & q1 <> q2
 holds LE q1, q2, L~f, f/.1, f/.len f iff
 for i, j being Nat st q1 in LSeg(f,i) & q2 in LSeg(f,j)
  & 1 <= i & i+1 <= len f
  & 1 <= j & j+1 <= len f holds
       i <= j & (i = j implies LE q1,q2,f/.i,f/.(i+1));