The abstract of the Mizar article:

Upper and Lower Sequence on the Cage. Part II

by

Robert Milewski

Received September 28, 2001

MML identifier: JORDAN1G

[ Mizar article, MML identifier index ]

environ

 vocabulary REALSET1, FINSEQ_1, BOOLE, RELAT_1, FINSEQ_5, MATRIX_1, GOBOARD1,
      FINSEQ_4, RFINSEQ, COMPTS_1, RELAT_2, SPPOL_1, EUCLID, JORDAN1E, JORDAN8,
      JORDAN9, FINSEQ_6, PSCOMP_1, TOPREAL1, GOBOARD5, MCART_1, TREES_1,
      FUNCT_1, ARYTM_1, CARD_1, PRE_TOPC, ARYTM_3, GROUP_1, JORDAN1A, SPPOL_2,
      JORDAN3, SPRECT_2, GROUP_2, JORDAN5C, JORDAN6;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XREAL_0, REAL_1, NAT_1,
      FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1,
      REALSET1, FINSEQ_6, STRUCT_0, PRE_TOPC, CARD_1, CARD_4, BINARITH,
      CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1,
      GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN5C, JORDAN6, JORDAN9,
      JORDAN1A, JORDAN1E;
 constructors JORDAN8, REALSET1, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH,
      CONNSP_1, JORDAN9, JORDAN1A, WSIERP_1, FINSEQ_4, GOBRD13, JORDAN3,
      RFINSEQ, TOPS_2, TOPMETR, TOPREAL2, JORDAN5C, SPRECT_1, FINSEQ_5,
      ENUMSET1, FINSOP_1, JORDAN1E, INT_1;
 clusters XREAL_0, SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, RELSET_1, ARYTM_3,
      SUBSET_1, FINSEQ_6, SPRECT_3, AMISTD_1, GOBOARD1, FINSEQ_1, FINSEQ_5,
      SPPOL_2, JORDAN1A, GOBOARD4, JORDAN1E, BINARITH, REALSET1, MEMBERED,
      ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

  reserve n for Nat;

  definition
   cluster trivial FinSequence;
  end;

  theorem :: JORDAN1G:1
   for f be trivial FinSequence holds
    f is empty or ex x be set st f = <*x*>;

  definition
   let p be non trivial FinSequence;
   cluster Rev p -> non trivial;
  end;

  theorem :: JORDAN1G:2
   for D be non empty set
   for f be FinSequence of D
   for G be Matrix of D
   for p be set holds
    f is_sequence_on G implies f-:p is_sequence_on G;

  theorem :: JORDAN1G:3
   for D be non empty set
   for f be FinSequence of D
   for G be Matrix of D
   for p be Element of D st p in rng f holds
    f is_sequence_on G implies f:-p is_sequence_on G;

  theorem :: JORDAN1G:4
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     Upper_Seq(C,n) is_sequence_on Gauge(C,n);

  theorem :: JORDAN1G:5
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     Lower_Seq(C,n) is_sequence_on Gauge(C,n);

  definition
   let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
   let n be Nat;
   cluster Upper_Seq(C,n) -> standard;
   cluster Lower_Seq(C,n) -> standard;
  end;

  theorem :: JORDAN1G:6
   for G be Y_equal-in-column Y_increasing-in-line Matrix of TOP-REAL 2
   for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds
    G*(i1,j1)`2 = G*(i2,j2)`2 implies j1 = j2;

  theorem :: JORDAN1G:7
   for G be X_equal-in-line X_increasing-in-column Matrix of TOP-REAL 2
   for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds
    G*(i1,j1)`1 = G*(i2,j2)`1 implies i1 = i2;

canceled 8;

  theorem :: JORDAN1G:16
   for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or
       (f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds
     (N-min L~f)`1 < (N-max L~f)`1;

  theorem :: JORDAN1G:17
     for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or
       (f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds
     N-min L~f <> N-max L~f;

  theorem :: JORDAN1G:18
   for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or
       (f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds
     (S-min L~f)`1 < (S-max L~f)`1;

  theorem :: JORDAN1G:19
     for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or
       (f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds
     S-min L~f <> S-max L~f;

  theorem :: JORDAN1G:20
   for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or
       (f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds
     (W-min L~f)`2 < (W-max L~f)`2;

  theorem :: JORDAN1G:21
     for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or
       (f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds
     W-min L~f <> W-max L~f;

  theorem :: JORDAN1G:22
   for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or
       (f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds
     (E-min L~f)`2 < (E-max L~f)`2;

  theorem :: JORDAN1G:23
     for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2)
    st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or
       (f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds
     E-min L~f <> E-max L~f;

  theorem :: JORDAN1G:24
   for D be non empty set
   for f be FinSequence of D
   for p,q be Element of D st p in rng f & q in rng f & q..f <= p..f holds
    (f-:p):-q = (f:-q)-:p;

  theorem :: JORDAN1G:25
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds
    L~(Cage(C,n)-:W-min L~Cage(C,n)) /\ L~(Cage(C,n):-W-min L~Cage(C,n)) =
     {N-min L~Cage(C,n),W-min L~Cage(C,n)};

  theorem :: JORDAN1G:26
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:W-min L~Cage(C,n);

  theorem :: JORDAN1G:27
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    (W-min L~Cage(C,n))..Upper_Seq(C,n) = 1;

  theorem :: JORDAN1G:28
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    (W-min L~Cage(C,n))..Upper_Seq(C,n) < (W-max L~Cage(C,n))..Upper_Seq(C,n);

  theorem :: JORDAN1G:29
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    (W-max L~Cage(C,n))..Upper_Seq(C,n) <= (N-min L~Cage(C,n))..Upper_Seq(C,n);

  theorem :: JORDAN1G:30
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    (N-min L~Cage(C,n))..Upper_Seq(C,n) < (N-max L~Cage(C,n))..Upper_Seq(C,n);

  theorem :: JORDAN1G:31
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    (N-max L~Cage(C,n))..Upper_Seq(C,n) <= (E-max L~Cage(C,n))..Upper_Seq(C,n);

  theorem :: JORDAN1G:32
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    (E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n);

  theorem :: JORDAN1G:33
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    (E-max L~Cage(C,n))..Lower_Seq(C,n) = 1;

  theorem :: JORDAN1G:34
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     (E-max L~Cage(C,n))..Lower_Seq(C,n) < (E-min L~Cage(C,n))..Lower_Seq(C,n);

  theorem :: JORDAN1G:35
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
    (E-min L~Cage(C,n))..Lower_Seq(C,n) <= (S-max L~Cage(C,n))..Lower_Seq(C,n);

  theorem :: JORDAN1G:36
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     (S-max L~Cage(C,n))..Lower_Seq(C,n) < (S-min L~Cage(C,n))..Lower_Seq(C,n);

  theorem :: JORDAN1G:37
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
    (S-min L~Cage(C,n))..Lower_Seq(C,n) <= (W-min L~Cage(C,n))..Lower_Seq(C,n);

  theorem :: JORDAN1G:38
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     (W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n);

  theorem :: JORDAN1G:39
   for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     (Upper_Seq(C,n)/.2)`1 = W-bound L~Cage(C,n);

  theorem :: JORDAN1G:40
     for C be compact connected non vertical non horizontal
    Subset of TOP-REAL 2 holds
     (Lower_Seq(C,n)/.2)`1 = E-bound L~Cage(C,n);

  theorem :: JORDAN1G:41
   for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2 holds
    W-bound L~Cage(C,n) + E-bound L~Cage(C,n) = W-bound C + E-bound C;

  theorem :: JORDAN1G:42
     for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2 holds
    S-bound L~Cage(C,n) + N-bound L~Cage(C,n) = S-bound C + N-bound C;

  theorem :: JORDAN1G:43
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for n,i be Nat st 1 <= i & i <= width Gauge(C,n) & n > 0 holds
    Gauge(C,n)*(Center Gauge(C,n),i)`1 = (W-bound C + E-bound C) / 2;

  theorem :: JORDAN1G:44
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for n,i be Nat st 1 <= i & i <= len Gauge(C,n) & n > 0 holds
    Gauge(C,n)*(i,Center Gauge(C,n))`2 = (S-bound C + N-bound C) / 2;

  theorem :: JORDAN1G:45
   for f be S-Sequence_in_R2
   for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f &
    f/.1 in L~mid(f,k1,k2) holds k1 = 1 or k2 = 1;

  theorem :: JORDAN1G:46
   for f be S-Sequence_in_R2
   for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f &
    f/.(len f) in L~mid(f,k1,k2) holds k1 = len f or k2 = len f;

  theorem :: JORDAN1G:47
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds
    rng Upper_Seq(C,n) c= rng Cage(C,n) &
    rng Lower_Seq(C,n) c= rng Cage(C,n);

  theorem :: JORDAN1G:48
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    Upper_Seq(C,n) is_a_h.c._for Cage(C,n);

  theorem :: JORDAN1G:49
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n);

  theorem :: JORDAN1G:50
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for i be Nat st 1 < i & i <= len Gauge(C,n) holds
    not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n);

  theorem :: JORDAN1G:51
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for i be Nat st 1 <= i & i < len Gauge(C,n) holds
    not Gauge(C,n)*(i,width Gauge(C,n)) in rng Lower_Seq(C,n);

  theorem :: JORDAN1G:52
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for i be Nat st 1 < i & i <= len Gauge(C,n) holds
    not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n);

  theorem :: JORDAN1G:53
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for i be Nat st 1 <= i & i < len Gauge(C,n) holds
    not Gauge(C,n)*(i,width Gauge(C,n)) in L~Lower_Seq(C,n);

  theorem :: JORDAN1G:54
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for i,j be Nat st 1 <= i & i <= len Gauge(C,n) &
    1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds
     LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets L~Lower_Seq(C,n);

  theorem :: JORDAN1G:55
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat st n > 0 holds
    First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),
     Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))
      in rng Upper_Seq(C,n);

  theorem :: JORDAN1G:56
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat st n > 0 holds
    Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n),
     Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))
      in rng Lower_Seq(C,n);

  theorem :: JORDAN1G:57
   for f be S-Sequence_in_R2
   for p be Point of TOP-REAL 2 st p in rng f holds
    R_Cut(f,p) = mid(f,1,p..f);

  theorem :: JORDAN1G:58
   for f be S-Sequence_in_R2
   for Q be closed Subset of TOP-REAL 2 st L~f meets Q & not f/.1 in Q &
    First_Point(L~f,f/.1,f/.len f,Q) in rng f holds
     L~mid(f,1,First_Point(L~f,f/.1,f/.len f,Q)..f) /\ Q =
      {First_Point(L~f,f/.1,f/.len f,Q)};

  theorem :: JORDAN1G:59
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat st n > 0
   for k be Nat st
    1 <= k &
    k < First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),
     Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))..
      Upper_Seq(C,n) holds
     (Upper_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;

  theorem :: JORDAN1G:60
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat st n > 0
   for k be Nat st
    1 <= k &
    k < First_Point(L~Rev Lower_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),
     Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))..
      Rev Lower_Seq(C,n) holds
     (Rev Lower_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;

  theorem :: JORDAN1G:61
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat st n > 0
   for q be Point of TOP-REAL 2 holds
    q in rng mid(Upper_Seq(C,n),2,First_Point(L~Upper_Seq(C,n),
     W-min L~Cage(C,n),E-max L~Cage(C,n),Vertical_Line
      ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))..Upper_Seq(C,n)) implies
     q`1 <= (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2;

  theorem :: JORDAN1G:62
   for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2
   for n be Nat st n > 0 holds
    First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n),
     Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 >
    Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n),
     Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2;

  theorem :: JORDAN1G:63
   for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2
   for n be Nat st n > 0 holds
    L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n);

  theorem :: JORDAN1G:64
   for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2
   for n be Nat st n > 0 holds
    L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n);

  theorem :: JORDAN1G:65
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for n be Nat st n > 0
   for i,j be Nat st 1 <= i & i <= len Gauge(C,n) &
    1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds
     LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets Lower_Arc L~Cage(C,n);