Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

The abstract of the Mizar article:

Upper and Lower Sequence on the Cage, Upper and Lower Arcs

by
Robert Milewski

Received April 5, 2002

MML identifier: JORDAN1J
[ Mizar article, MML identifier index ]


environ

 vocabulary JORDAN8, PSCOMP_1, BOOLE, JORDAN1A, JORDAN9, GOBOARD1, GOBOARD5,
      JORDAN6, SPRECT_2, JORDAN3, FINSEQ_5, JORDAN2C, SPPOL_2, GROUP_2,
      RFINSEQ, REALSET1, JORDAN1E, SQUARE_1, FINSEQ_4, TOPREAL2, CONNSP_1,
      COMPTS_1, TOPREAL1, SPPOL_1, FINSEQ_1, TREES_1, EUCLID, RELAT_1, MCART_1,
      MATRIX_1, GOBOARD9, PRE_TOPC, RELAT_2, SEQM_3, SUBSET_1, FUNCT_1,
      ARYTM_1, FINSEQ_6, CARD_1, GOBOARD2, GROUP_1, GRAPH_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, SQUARE_1,
      FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1,
      FINSEQ_6, REALSET1, GRAPH_2, STRUCT_0, PRE_TOPC, TOPREAL2, CARD_1,
      CARD_4, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2,
      GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1,
      SPPOL_2, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A,
      JORDAN1E;
 constructors JORDAN8, REALSET1, GOBOARD9, JORDAN6, REAL_1, CARD_4, PSCOMP_1,
      BINARITH, JORDAN2C, CONNSP_1, JORDAN9, JORDAN1A, SQUARE_1, FINSEQ_4,
      GOBRD13, JORDAN1, JORDAN3, RFINSEQ, MATRIX_2, TOPREAL2, JORDAN5C,
      PARTFUN1, GRAPH_2, SPRECT_1, GOBOARD2, INT_1, TOPS_1, FINSOP_1, JORDAN1E,
      MEMBERED;
 clusters SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, INT_1, RELSET_1, SUBSET_1,
      PRE_TOPC, SPRECT_3, GOBOARD2, FINSEQ_1, FINSEQ_5, SPPOL_2, JORDAN1A,
      JORDAN1B, JORDAN1E, JORDAN1G, GOBRD11, FUNCT_7, XBOOLE_0, XREAL_0,
      MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

  reserve n for Nat;

  theorem :: JORDAN1J:1
   for G be Go-board
   for i1,i2,j1,j2 be Nat st
    1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G &
    1 <= i1 & i1 < i2 & i2 <= len G holds
     G*(i1,j1)`1 < G*(i2,j2)`1;

  theorem :: JORDAN1J:2
   for G be Go-board
   for i1,i2,j1,j2 be Nat st
    1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G &
    1 <= j1 & j1 < j2 & j2 <= width G holds
     G*(i1,j1)`2 < G*(i2,j2)`2;

  definition
   let f be non empty FinSequence;
   let g be FinSequence;
   cluster f^'g -> non empty;
  end;

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

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

  theorem :: JORDAN1J:5
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    W-min L~Cage(C,n) in rng Upper_Seq(C,n) &
    W-min L~Cage(C,n) in L~Upper_Seq(C,n);

  theorem :: JORDAN1J:6
     for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2 holds
    W-max L~Cage(C,n) in rng Upper_Seq(C,n) &
    W-max L~Cage(C,n) in L~Upper_Seq(C,n);

  theorem :: JORDAN1J:7
   for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2 holds
    N-min L~Cage(C,n) in rng Upper_Seq(C,n) &
    N-min L~Cage(C,n) in L~Upper_Seq(C,n);

  theorem :: JORDAN1J:8
     for C be compact connected non vertical non horizontal
     Subset of TOP-REAL 2 holds
    N-max L~Cage(C,n) in rng Upper_Seq(C,n) &
    N-max L~Cage(C,n) in L~Upper_Seq(C,n);

  theorem :: JORDAN1J:9
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    E-max L~Cage(C,n) in rng Upper_Seq(C,n) &
    E-max L~Cage(C,n) in L~Upper_Seq(C,n);

  theorem :: JORDAN1J:10
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    E-max L~Cage(C,n) in rng Lower_Seq(C,n) &
    E-max L~Cage(C,n) in L~Lower_Seq(C,n);

  theorem :: JORDAN1J:11
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    E-min L~Cage(C,n) in rng Lower_Seq(C,n) &
    E-min L~Cage(C,n) in L~Lower_Seq(C,n);

  theorem :: JORDAN1J:12
   for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    S-max L~Cage(C,n) in rng Lower_Seq(C,n) &
    S-max L~Cage(C,n) in L~Lower_Seq(C,n);

  theorem :: JORDAN1J:13
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    S-min L~Cage(C,n) in rng Lower_Seq(C,n) &
    S-min L~Cage(C,n) in L~Lower_Seq(C,n);

  theorem :: JORDAN1J:14
     for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds
    W-min L~Cage(C,n) in rng Lower_Seq(C,n) &
    W-min L~Cage(C,n) in L~Lower_Seq(C,n);

  theorem :: JORDAN1J:15
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & N-min Y in X holds
     N-min X = N-min Y;

  theorem :: JORDAN1J:16
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & N-max Y in X holds
     N-max X = N-max Y;

  theorem :: JORDAN1J:17
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & E-min Y in X holds
     E-min X = E-min Y;

  theorem :: JORDAN1J:18
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & E-max Y in X holds
     E-max X = E-max Y;

  theorem :: JORDAN1J:19
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & S-min Y in X holds
     S-min X = S-min Y;

  theorem :: JORDAN1J:20
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & S-max Y in X holds
     S-max X = S-max Y;

  theorem :: JORDAN1J:21
   for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & W-min Y in X holds
     W-min X = W-min Y;

  theorem :: JORDAN1J:22
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    X c= Y & W-max Y in X holds
     W-max X = W-max Y;

  theorem :: JORDAN1J:23
   for X,Y be non empty compact Subset of TOP-REAL 2 st
    N-bound X < N-bound Y holds
     N-bound (X\/Y) = N-bound Y;

  theorem :: JORDAN1J:24
   for X,Y be non empty compact Subset of TOP-REAL 2 st
    E-bound X < E-bound Y holds
     E-bound (X\/Y) = E-bound Y;

  theorem :: JORDAN1J:25
   for X,Y be non empty compact Subset of TOP-REAL 2 st
    S-bound X < S-bound Y holds
     S-bound (X\/Y) = S-bound X;

  theorem :: JORDAN1J:26
   for X,Y be non empty compact Subset of TOP-REAL 2 st
    W-bound X < W-bound Y holds
     W-bound (X\/Y) = W-bound X;

  theorem :: JORDAN1J:27
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    N-bound X < N-bound Y holds
     N-min (X\/Y) = N-min Y;

  theorem :: JORDAN1J:28
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    N-bound X < N-bound Y holds
     N-max (X\/Y) = N-max Y;

  theorem :: JORDAN1J:29
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    E-bound X < E-bound Y holds
     E-min (X\/Y) = E-min Y;

  theorem :: JORDAN1J:30
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    E-bound X < E-bound Y holds
     E-max (X\/Y) = E-max Y;

  theorem :: JORDAN1J:31
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    S-bound X < S-bound Y holds
     S-min (X\/Y) = S-min X;

  theorem :: JORDAN1J:32
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    S-bound X < S-bound Y holds
     S-max (X\/Y) = S-max X;

  theorem :: JORDAN1J:33
   for X,Y be non empty compact Subset of TOP-REAL 2 st
    W-bound X < W-bound Y holds
     W-min (X\/Y) = W-min X;

  theorem :: JORDAN1J:34
     for X,Y be non empty compact Subset of TOP-REAL 2 st
    W-bound X < W-bound Y holds
     W-max (X\/Y) = W-max X;

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

  theorem :: JORDAN1J:36
   for f be non constant standard special_circular_sequence
   for p,q be Point of TOP-REAL 2
   for g be connected Subset of TOP-REAL 2 st
    p in RightComp f & q in LeftComp f & p in g & q in g holds
     g meets L~f;

  definition
   cluster non constant standard s.c.c.
    (being_S-Seq FinSequence of TOP-REAL 2);
  end;

  theorem :: JORDAN1J:37
   for f be S-Sequence_in_R2
   for p be Point of TOP-REAL 2 st p in rng f holds
    L_Cut(f,p) = mid(f,p..f,len f);

  theorem :: JORDAN1J:38
   for M be Go-board
   for f be S-Sequence_in_R2 st f is_sequence_on M
   for p be Point of TOP-REAL 2 st p in rng f holds
    R_Cut(f,p) is_sequence_on M;

  theorem :: JORDAN1J:39
   for M be Go-board
   for f be S-Sequence_in_R2 st f is_sequence_on M
   for p be Point of TOP-REAL 2 st p in rng f holds
    L_Cut(f,p) is_sequence_on M;

  theorem :: JORDAN1J:40
   for G be Go-board
   for f be FinSequence of TOP-REAL 2 st f is_sequence_on G
   for i,j be Nat st 1 <= i & i <= len G & 1 <= j & j <= width G holds
    G*(i,j) in L~f implies G*(i,j) in rng f;

  theorem :: JORDAN1J:41
     for f be S-Sequence_in_R2
   for g be FinSequence of TOP-REAL 2 holds
    g is unfolded s.n.c. one-to-one & L~f /\ L~g = {f/.1} & f/.1 = g/.len g &
    (for i be Nat st 1<=i & i+2 <= len f holds
     LSeg(f,i) /\ LSeg(f/.len f,g/.1) = {}) &
    (for i be Nat st 2<=i & i+1 <= len g holds
     LSeg(g,i) /\ LSeg(f/.len f,g/.1) = {}) implies f^g is s.c.c.;

  theorem :: JORDAN1J:42
     for C be compact non vertical non horizontal non empty Subset of TOP-REAL
2
   ex i be Nat st 1 <= i & i+1 <= len Gauge(C,n) &
    W-min C in cell(Gauge(C,n),1,i) & W-min C <> Gauge(C,n)*(2,i);

  theorem :: JORDAN1J:43
   for f be S-Sequence_in_R2
   for p be Point of TOP-REAL 2 st p in L~f & f.len f in L~R_Cut(f,p) holds
    f.len f = p;

  theorem :: JORDAN1J:44
   for f be non empty FinSequence of TOP-REAL 2
   for p be Point of TOP-REAL 2 holds
    R_Cut (f,p) <> {};

  theorem :: JORDAN1J:45
   for f be S-Sequence_in_R2
   for p be Point of TOP-REAL 2 st p in L~f holds
    R_Cut(f,p)/.(len R_Cut(f,p)) = p;

  theorem :: JORDAN1J:46
   for C be compact connected non vertical non horizontal Subset of TOP-REAL 2
   for p be Point of TOP-REAL 2 holds
    p in L~Upper_Seq(C,n) & p`1 = E-bound L~Cage(C,n) implies
     p = E-max L~Cage(C,n);

  theorem :: JORDAN1J:47
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for p be Point of TOP-REAL 2 holds
    p in L~Lower_Seq(C,n) & p`1 = W-bound L~Cage(C,n) implies
     p = W-min L~Cage(C,n);

  theorem :: JORDAN1J:48
     for G be Go-board
   for f,g be FinSequence of TOP-REAL 2
   for k be Nat holds
    1 <= k & k < len f & f^g is_sequence_on G implies
     left_cell(f^g,k,G) = left_cell(f,k,G) &
     right_cell(f^g,k,G) = right_cell(f,k,G);

  theorem :: JORDAN1J:49
   for D be set
   for f,g be FinSequence of D
   for i be Nat st i <= len f holds
    (f^'g)|i = f|i;

  theorem :: JORDAN1J:50
   for D be set
   for f,g be FinSequence of D holds
    (f^'g)|(len f) = f;

  theorem :: JORDAN1J:51
   for G be Go-board
   for f,g be FinSequence of TOP-REAL 2
   for k be Nat holds
    1 <= k & k < len f & f^'g is_sequence_on G implies
     left_cell(f^'g,k,G) = left_cell(f,k,G) &
     right_cell(f^'g,k,G) = right_cell(f,k,G);

  theorem :: JORDAN1J:52
   for G be Go-board
   for f be S-Sequence_in_R2
   for p be Point of TOP-REAL 2
   for k be Nat st 1 <= k & k < p..f & f is_sequence_on G & p in rng f holds
    left_cell(R_Cut(f,p),k,G) = left_cell(f,k,G) &
    right_cell(R_Cut(f,p),k,G) = right_cell(f,k,G);

  theorem :: JORDAN1J:53
   for G be Go-board
   for f be FinSequence of TOP-REAL 2
   for p be Point of TOP-REAL 2
   for k be Nat st 1 <= k & k < p..f & f is_sequence_on G holds
    left_cell(f-:p,k,G) = left_cell(f,k,G) &
    right_cell(f-:p,k,G) = right_cell(f,k,G);

  theorem :: JORDAN1J:54
   for f,g be FinSequence of TOP-REAL 2 st
    f is unfolded s.n.c. one-to-one & g is unfolded s.n.c. one-to-one &
     f/.len f = g/.1 & L~f /\ L~g = {g/.1} holds
      f^'g is s.n.c.;

  theorem :: JORDAN1J:55
   for f,g be FinSequence of TOP-REAL 2 st
    f is one-to-one & g is one-to-one & rng f /\ rng g c= {g/.1} holds
     f^'g is one-to-one;

  theorem :: JORDAN1J:56
   for f be FinSequence of TOP-REAL 2
   for p be Point of TOP-REAL 2 st f is_S-Seq & p in rng f & p <> f.1 holds
    Index(p,f)+1 = p..f;

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

  theorem :: JORDAN1J:58
   for C be Simple_closed_curve
   for i,j,k be Nat st
    1 < i & i < len Gauge(C,n) &
    1 <= j & j <= k & k <= width Gauge(C,n) &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) =
     {Gauge(C,n)*(i,k)} &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) =
     {Gauge(C,n)*(i,j)} holds
      LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;

  theorem :: JORDAN1J:59
   for C be Simple_closed_curve
   for i,j,k be Nat st
    1 < i & i < len Gauge(C,n) &
    1 <= j & j <= k & k <= width Gauge(C,n) &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Upper_Seq(C,n) =
     {Gauge(C,n)*(i,k)} &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ L~Lower_Seq(C,n) =
     {Gauge(C,n)*(i,j)} holds
      LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;

  theorem :: JORDAN1J:60
   for C be Simple_closed_curve
   for i,j,k be Nat st
    1 < i & i < len Gauge(C,n) &
    1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
     {Gauge(C,n)*(i,k)} &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
     {Gauge(C,n)*(i,j)} holds
     LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C;

  theorem :: JORDAN1J:61
   for C be Simple_closed_curve
   for i,j,k be Nat st
    1 < i & i < len Gauge(C,n) &
    1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Upper_Arc L~Cage(C,n) =
     {Gauge(C,n)*(i,k)} &
    LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) /\ Lower_Arc L~Cage(C,n) =
     {Gauge(C,n)*(i,j)} holds
      LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C;

  theorem :: JORDAN1J:62
     for C be compact connected non vertical non horizontal Subset of TOP-REAL
2
   for j be Nat holds
    Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Upper_Arc L~Cage(C,n+1) &
    1 <= j & j <= width Gauge(C,n+1) implies
    LSeg(Gauge(C,1)*(Center Gauge(C,1),1),Gauge(C,n+1)*(Center Gauge(C,n+1),j))
     meets Lower_Arc L~Cage(C,n+1);

  theorem :: JORDAN1J:63
     for C be Simple_closed_curve
   for j,k be Nat holds
    1 <= j & j <= k & k <= width Gauge(C,n+1) &
    LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
         Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) =
     {Gauge(C,n+1)*(Center Gauge(C,n+1),k)} &
    LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
         Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) =
     {Gauge(C,n+1)*(Center Gauge(C,n+1),j)} implies
     LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
          Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Lower_Arc C;

  theorem :: JORDAN1J:64
     for C be Simple_closed_curve
   for j,k be Nat holds
    1 <= j & j <= k & k <= width Gauge(C,n+1) &
    LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
         Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Upper_Arc L~Cage(C,n+1) =
     {Gauge(C,n+1)*(Center Gauge(C,n+1),k)} &
    LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
         Gauge(C,n+1)*(Center Gauge(C,n+1),k)) /\ Lower_Arc L~Cage(C,n+1) =
     {Gauge(C,n+1)*(Center Gauge(C,n+1),j)} implies
     LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j),
          Gauge(C,n+1)*(Center Gauge(C,n+1),k)) meets Upper_Arc C;


Back to top