The abstract of the Mizar article:

The Ordering of Points on a Curve. Part I

by

Adam Grabowski, and

Yatsuka Nakamura

Received September 10, 1997

MML identifier: JORDAN5B

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_1, BORSUK_1, PRE_TOPC, EUCLID, MCART_1, TOPREAL1, RCOMP_1,
      FINSEQ_1, RELAT_1, TOPS_2, FUNCT_1, TOPMETR, ARYTM_3, SUBSET_1, BOOLE,
      TREAL_1, SEQ_1, FUNCT_4, COMPTS_1, TARSKI, ORDINAL2, PCOMPS_1, METRIC_1,
      JORDAN3, RFINSEQ, FINSEQ_5, GROUP_2, SEQM_3, GOBOARD5, GOBOARD2, TREES_1,
      TOPREAL4, GOBOARD1, MATRIX_1, FINSEQ_4;
 notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, BINARITH, RCOMP_1, RELAT_1,
      FINSEQ_1, FUNCT_1, FUNCT_2, TOPMETR, FINSEQ_4, JORDAN3, STRUCT_0,
      TOPREAL1, RFINSEQ, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, EUCLID, TREAL_1,
      METRIC_1, GOBOARD1, GOBOARD2, MATRIX_1, TOPREAL4, GOBOARD5, FUNCT_4,
      FINSEQ_5, PCOMPS_1;
 constructors REAL_1, FUNCT_4, RFINSEQ, TOPREAL4, SEQM_3, TOPS_2, COMPTS_1,
      RCOMP_1, TREAL_1, FINSEQ_5, GOBOARD5, JORDAN3, GOBOARD2, BINARITH,
      FINSEQ_4, INT_1, SEQ_4;
 clusters BORSUK_1, EUCLID, FUNCT_1, PRE_TOPC, RELSET_1, GOBOARD5, GOBOARD2,
      STRUCT_0, TOPMETR, TOPREAL1, METRIC_1, INT_1, JORDAN3, XREAL_0, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

theorem :: JORDAN5B:1
 for i1 being Nat st 1 <= i1 holds i1-'1<i1;

theorem :: JORDAN5B:2
   for i, k being Nat holds i+1 <= k implies 1 <= k-'i;

theorem :: JORDAN5B:3
   for i, k being Nat holds 1 <= i & 1 <= k implies (k-'i)+1 <= k;

theorem :: JORDAN5B:4
    for r being Real st r in the carrier of I[01] holds
   1-r in the carrier of I[01];

theorem :: JORDAN5B:5
    for p, q, p1 being Point of TOP-REAL 2 st p`2 <> q`2 & p1 in LSeg (p, q)
   holds
    ( p1`2 = p`2 implies p1 = p );

theorem :: JORDAN5B:6
    for p, q, p1 being Point of TOP-REAL 2 st p`1 <> q`1 & p1 in LSeg (p, q)
   holds
    ( p1`1 = p`1 implies p1 = p );

theorem :: JORDAN5B:7
 for f being FinSequence of TOP-REAL 2,
     P being non empty Subset of TOP-REAL 2,
     F being map of I[01], (TOP-REAL 2) | P,
     i being Nat st 1 <= i & i+1 <= len f & f is_S-Seq & P = L~f &
       F is_homeomorphism & F.0 = f/.1 & F.1 = f/.len f
      ex p1, p2 being Real st p1 < p2 &
       0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 &
       LSeg (f, i) = F.:[.p1, p2.] & F.p1 = f/.i & F.p2 = f/.(i+1);

theorem :: JORDAN5B:8
   for f being FinSequence of TOP-REAL 2,
     Q, R being non empty Subset of TOP-REAL 2,
     F being map of I[01], (TOP-REAL 2)|Q,
     i being Nat,
     P being non empty Subset of I[01] st
     f is_S-Seq & F is_homeomorphism & F.0 = f/.1 & F.1 = f/.len f &
       1 <= i & i+1 <= len f & F.:P = LSeg (f,i) & Q = L~f & R = LSeg(f,i)
    ex G being map of I[01]|P, (TOP-REAL 2)|R st
           G = F|P & G is_homeomorphism;

begin :: Some properties of real intervals

theorem :: JORDAN5B:9
 for p1, p2, p being Point of TOP-REAL 2 st
  p1 <> p2 & p in LSeg(p1,p2) holds LE p,p,p1,p2;

theorem :: JORDAN5B:10
 for p, p1, p2 being Point of TOP-REAL 2 st p1 <> p2 &
  p in LSeg(p1,p2) holds LE p1,p,p1,p2;

theorem :: JORDAN5B:11
 for p, p1, p2 being Point of TOP-REAL 2 st p in LSeg(p1,p2) & p1 <> p2
 holds LE p,p2,p1,p2;

theorem :: JORDAN5B:12
   for p1, p2, q1, q2, q3 being Point of TOP-REAL 2 st p1 <> p2 &
   LE q1,q2,p1,p2 & LE q2,q3,p1,p2 holds LE q1,q3,p1,p2;

theorem :: JORDAN5B:13
   for p, q being Point of TOP-REAL 2 st p <> q holds
  LSeg (p, q) =
   { p1 where p1 is Point of TOP-REAL 2 : LE p, p1, p, q & LE p1, q, p, q };

theorem :: JORDAN5B:14
   for n being Nat,
     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_an_arc_of p2,p1;

theorem :: JORDAN5B:15
   for i being Nat,
     f being FinSequence of TOP-REAL 2,
     P being Subset of TOP-REAL 2 st
  f is_S-Seq & 1 <= i & i+1 <= len f & P = LSeg(f,i) holds
   P is_an_arc_of f/.i, f/.(i+1);

begin :: Cutting off sequences

theorem :: JORDAN5B:16
   for g1 being FinSequence of TOP-REAL 2, i being Nat st 1 <= i & i <= len g1
   & g1 is_S-Seq holds
  g1/.1 in L~mid(g1, i, len g1) implies i = 1;

theorem :: JORDAN5B:17
   for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st f is_S-Seq & p = f.len f holds
   L_Cut (f,p) = <*p*>;

canceled 3;

theorem :: JORDAN5B:21
   for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st
      p in L~f & p <> f.len f & f is_S-Seq holds
  Index (p, L_Cut(f,p)) = 1;

theorem :: JORDAN5B:22
 for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st
      p in L~f & f is_S-Seq & p <> f.len f holds
 p in L~L_Cut (f,p);

theorem :: JORDAN5B:23
   for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st
      p in L~f & f is_S-Seq & p <> f.1 holds
 p in L~R_Cut (f,p);

theorem :: JORDAN5B:24
 for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st p in L~f & f is_S-Seq
 holds B_Cut(f,p,p) = <*p*>;

theorem :: JORDAN5B:25
 for f being non empty FinSequence of TOP-REAL 2,
     p, q being Point of TOP-REAL 2 st
      p in L~f & q in L~f & q <> f.len f & p = f.len f & f is_S-Seq holds
    p in L~L_Cut(f,q);

theorem :: JORDAN5B:26
   for f being non empty FinSequence of TOP-REAL 2,
     p, q being Point of TOP-REAL 2 st
      (p <> f.len f or q <> f.len f) &
      p in L~f & q in L~f & f is_S-Seq holds
    p in L~L_Cut(f,q) or q in L~L_Cut(f,p);

theorem :: JORDAN5B:27
   for f being non empty FinSequence of TOP-REAL 2,
     p, q being Point of TOP-REAL 2 st p in L~f & q in L~f & f is_S-Seq
 holds L~B_Cut(f,p,q) c= L~f;

theorem :: JORDAN5B:28
   for f being non constant standard special_circular_sequence,
     i, j being Nat st 1 <= i & j <= len GoB f & i < j holds
   LSeg((GoB f)*(1,width GoB f), (GoB f)*(i,width GoB f)) /\
   LSeg((GoB f)*(j,width GoB f), (GoB f)*(len GoB f,width GoB f)) = {};

theorem :: JORDAN5B:29
   for f being non constant standard special_circular_sequence,
     i, j being Nat st 1 <= i & j <= width GoB f & i < j holds
   LSeg((GoB f)*(len GoB f,1), (GoB f)*(len GoB f,i)) /\
   LSeg((GoB f)*(len GoB f,j), (GoB f)*(len GoB f,width GoB f)) = {};

theorem :: JORDAN5B:30
 for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st f is_S-Seq holds
   L_Cut (f,f/.1) = f;

theorem :: JORDAN5B:31
   for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st f is_S-Seq holds
   R_Cut (f,f/.len f) = f;

theorem :: JORDAN5B:32
   for f being FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st p in L~f
     holds
   p in LSeg ( f/.Index(p,f), f/.(Index(p,f)+1) );

theorem :: JORDAN5B:33
     for f be FinSequence of TOP-REAL 2
   for p be Point of TOP-REAL 2
   for i be Nat st
   f is unfolded s.n.c. one-to-one & len f >= 2 & f/.1 in LSeg (f,i) holds
   i = 1;

theorem :: JORDAN5B:34
   for f be non constant standard special_circular_sequence,
     j be Nat,
     P be Subset of TOP-REAL 2 st
     1 <= j & j <= width GoB f &
     P = LSeg ((GoB f)*(1,j), (GoB f)*(len (GoB f),j)) holds
 P is_S-P_arc_joining (GoB f)*(1,j),
                      (GoB f)*(len (GoB f),j);

theorem :: JORDAN5B:35
   for f be non constant standard special_circular_sequence,
     j be Nat,
     P be Subset of TOP-REAL 2 st
     1 <= j & j <= len GoB f &
     P = LSeg ((GoB f)*(j,1), (GoB f)*(j,width GoB f)) holds
 P is_S-P_arc_joining (GoB f)*(j,1),
                      (GoB f)*(j,width GoB f);