The abstract of the Mizar article:

Upper and Lower Sequence of a Cage

by

Robert Milewski

Received August 8, 2001

MML identifier: JORDAN1E

[ Mizar article, MML identifier index ]

environ

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


begin  :: Preliminaries

  reserve n for Nat;

  theorem :: JORDAN1E:1
     for X be non empty Subset of TOP-REAL 2
   for Y be compact Subset of TOP-REAL 2 st X c= Y holds
    N-bound X <= N-bound Y;

  theorem :: JORDAN1E:2
     for X be non empty Subset of TOP-REAL 2
   for Y be compact Subset of TOP-REAL 2 st X c= Y holds
    E-bound X <= E-bound Y;

  theorem :: JORDAN1E:3
     for X be non empty Subset of TOP-REAL 2
   for Y be compact Subset of TOP-REAL 2 st X c= Y holds
    S-bound X >= S-bound Y;

  theorem :: JORDAN1E:4
     for X be non empty Subset of TOP-REAL 2
   for Y be compact Subset of TOP-REAL 2 st X c= Y holds
    W-bound X >= W-bound Y;

  theorem :: JORDAN1E:5
   for f,g be FinSequence of TOP-REAL 2 st f is_in_the_area_of g
   for p be Element of TOP-REAL 2 st p in rng f holds
    f-:p is_in_the_area_of g;

  theorem :: JORDAN1E:6
   for f,g be FinSequence of TOP-REAL 2 st f is_in_the_area_of g
   for p be Element of TOP-REAL 2 st p in rng f holds
    f:-p is_in_the_area_of g;

  theorem :: JORDAN1E:7
     for f be non empty FinSequence of TOP-REAL 2
   for p be Point of TOP-REAL 2 st p in L~f holds
    L_Cut (f,p) <> {};

  theorem :: JORDAN1E:8
     for f be non empty FinSequence of TOP-REAL 2
   for p be Point of TOP-REAL 2 st p in L~f & len R_Cut(f,p) >= 2 holds
    f.1 in L~R_Cut(f,p);

  theorem :: JORDAN1E:9
   for f be non empty FinSequence of TOP-REAL 2 st f is_S-Seq
   for p be Point of TOP-REAL 2
    st p in L~f holds not f.1 in L~mid(f,Index(p,f)+1,len f);

  theorem :: JORDAN1E:10
   for i,j,m,n be Nat holds
    i+j = m+n & i <= m & j <= n implies i = m;

  theorem :: JORDAN1E:11
     for f be non empty FinSequence of TOP-REAL 2 st f is_S-Seq
   for p be Point of TOP-REAL 2 st p in L~f & f.1 in L~L_Cut(f,p) holds
    f.1 = p;

begin  :: About Upper and Lower Sequence of a Cage

  definition
   let C be compact non vertical non horizontal Subset of TOP-REAL 2;
   let n be Nat;
   func Upper_Seq(C,n) -> FinSequence of TOP-REAL 2 equals
:: JORDAN1E:def 1
    Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n);
  end;

  theorem :: JORDAN1E:12
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds len Upper_Seq(C,n) =
    (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n));

  definition
   let C be compact non vertical non horizontal Subset of TOP-REAL 2;
   let n be Nat;
   func Lower_Seq(C,n) -> FinSequence of TOP-REAL 2 equals
:: JORDAN1E:def 2
    Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n);
  end;

  theorem :: JORDAN1E:13
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds len Lower_Seq(C,n) =
    len Rotate(Cage(C,n),W-min L~Cage(C,n))-
    (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+1;

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

  definition
   let C be compact non vertical non horizontal Subset of TOP-REAL 2;
   let n be Nat;
   cluster Upper_Seq(C,n) -> one-to-one special unfolded s.n.c.;
   cluster Lower_Seq(C,n) -> one-to-one special unfolded s.n.c.;
  end;

  theorem :: JORDAN1E:14
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds
    len Upper_Seq(C,n) + len Lower_Seq(C,n) = len Cage(C,n)+1;

  theorem :: JORDAN1E:15
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds
    Rotate(Cage(C,n),W-min L~Cage(C,n)) = Upper_Seq(C,n) ^' Lower_Seq(C,n);

  theorem :: JORDAN1E:16
     for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds
    L~Cage(C,n) = L~(Upper_Seq(C,n) ^' Lower_Seq(C,n));

  theorem :: JORDAN1E:17
     for C be compact non vertical non horizontal non empty Subset of TOP-REAL
2
   for n be Nat holds
    L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~Lower_Seq(C,n);

  theorem :: JORDAN1E:18
   for P be Simple_closed_curve holds W-min(P) <> E-min(P);

  theorem :: JORDAN1E:19
   for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds
    len Upper_Seq(C,n) >= 3 & len Lower_Seq(C,n) >= 3;

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

  theorem :: JORDAN1E:20
     for C be compact non vertical non horizontal Subset of TOP-REAL 2
   for n be Nat holds
    L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) =
     {W-min L~Cage(C,n),E-max L~Cage(C,n)};

  theorem :: JORDAN1E:21
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    Upper_Seq(C,n) is_in_the_area_of Cage(C,n);

  theorem :: JORDAN1E:22
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    Lower_Seq(C,n) is_in_the_area_of Cage(C,n);

  theorem :: JORDAN1E:23
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
     holds (Cage(C,n)/.2)`2 = N-bound L~Cage(C,n);

  theorem :: JORDAN1E:24
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for k be Nat st 1 <= k & k+1 <= len Cage(C,n) &
    Cage(C,n)/.k = E-max L~Cage(C,n) holds
     (Cage(C,n)/.(k+1))`1 = E-bound L~Cage(C,n);

  theorem :: JORDAN1E:25
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for k be Nat st 1 <= k & k+1 <= len Cage(C,n) &
    Cage(C,n)/.k = S-max L~Cage(C,n) holds
     (Cage(C,n)/.(k+1))`2 = S-bound L~Cage(C,n);

  theorem :: JORDAN1E:26
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for k be Nat st 1 <= k & k+1 <= len Cage(C,n) &
    Cage(C,n)/.k = W-min L~Cage(C,n) holds
     (Cage(C,n)/.(k+1))`1 = W-bound L~Cage(C,n);