The Mizar abstract of SPPOL

Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users
The abstract of the Mizar article:: Special Polygons
by
Czeslaw Bylinski, and
Yatsuka Nakamura
Received January 30, 1995
MML identifier: SPPOL_2
[ Mizar article, MML identifier index ]
environ

 vocabulary EUCLID, FINSEQ_1, PRE_TOPC, ARYTM, MCART_1, TOPREAL1, FINSEQ_5,
      RELAT_1, FINSEQ_4, BOOLE, RFINSEQ, ARYTM_1, TARSKI, FUNCT_1, REALSET1,
      TOPREAL4, RCOMP_1, COMPTS_1, BORSUK_1, TOPS_2, ORDINAL2, SUBSET_1,
      SPPOL_2;
 notation TARSKI, XBOOLE_0, ORDINAL1, XREAL_0, STRUCT_0, REAL_1, NAT_1,
      FUNCT_1, FINSEQ_1, REALSET1, FINSEQ_4, RFINSEQ, PRE_TOPC, COMPTS_1,
      TOPS_2, EUCLID, BORSUK_1, TOPREAL1, TOPREAL4, FINSEQ_5;
 constructors TOPMETR, REAL_1, NAT_1, REALSET1, RFINSEQ, COMPTS_1, TOPS_2,
      TOPREAL1, TOPREAL4, FINSEQ_4, FINSEQ_5, INT_1, MEMBERED, XBOOLE_0;
 clusters PRE_TOPC, FINSEQ_5, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1,
      INT_1, TOPREAL1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Segments in TOP-REAL 2

reserve P for Subset of TOP-REAL 2,
        f,f1,f2,g for FinSequence of TOP-REAL 2,
        p,p1,p2,q,q1,q2 for Point of TOP-REAL 2,
        r1,r2,r1',r2' for Real,
        i,j,k,n for Nat;

theorem :: SPPOL_2:1
  for r1, r2, r1', r2' being real number st
   |[ r1,r2 ]| = |[ r1',r2' ]| holds r1 = r1' & r2 = r2';

theorem :: SPPOL_2:2
   i+j = len f implies LSeg(f,i) = LSeg(Rev f,j);

theorem :: SPPOL_2:3
   i+1 <= len(f|n) implies LSeg(f|n,i) = LSeg(f,i);

theorem :: SPPOL_2:4
   n <= len f & 1 <= i implies LSeg(f/^n,i) = LSeg(f,n+i);

theorem :: SPPOL_2:5
   1 <= i & i+1 <= len f - n implies LSeg(f/^n,i) = LSeg(f,n+i);

theorem :: SPPOL_2:6
   i+1 <= len f implies LSeg(f^g,i) = LSeg(f,i);

theorem :: SPPOL_2:7
   1 <= i implies LSeg(f^g,len f + i) = LSeg(g,i);

theorem :: SPPOL_2:8
  f is non empty & g is non empty
   implies LSeg(f^g,len f) = LSeg(f/.len f,g/.1);

theorem :: SPPOL_2:9
   i+1 <= len(f-:p) implies LSeg(f-:p,i) = LSeg(f,i);

theorem :: SPPOL_2:10
   p in rng f implies LSeg(f:-p,i+1) = LSeg(f,i+p..f);

theorem :: SPPOL_2:11
   L~<*>(the carrier of TOP-REAL 2) = {};

theorem :: SPPOL_2:12
   L~<*p*> = {};

theorem :: SPPOL_2:13
   p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f,i);

theorem :: SPPOL_2:14
   p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1));

theorem :: SPPOL_2:15
   1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1)) implies p in L~f;

theorem :: SPPOL_2:16
     1 <= i & i+1 <= len f implies LSeg(f/.i,f/.(i+1)) c= L~f;

theorem :: SPPOL_2:17
     p in LSeg(f,i) implies p in L~f;

theorem :: SPPOL_2:18
   len f >= 2 implies rng f c= L~f;

theorem :: SPPOL_2:19
   f is non empty implies L~(f^<*p*>) = L~f \/ LSeg(f/.len f,p);

theorem :: SPPOL_2:20
   f is non empty implies L~(<*p*>^f) = LSeg(p,f/.1) \/ L~f;

theorem :: SPPOL_2:21
   L~<*p,q*> = LSeg(p,q);

theorem :: SPPOL_2:22
   L~f = L~(Rev f);

theorem :: SPPOL_2:23
   f1 is non empty & f2 is non empty implies
    L~(f1^f2) = L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2;

canceled;

theorem :: SPPOL_2:25
   q in rng f implies L~f = L~(f-:q) \/ L~(f:-q);

theorem :: SPPOL_2:26
   p in LSeg(f,n) implies L~f = L~Ins(f,n,p);

begin

definition
 cluster being_S-Seq FinSequence of TOP-REAL 2;
 cluster being_S-Seq ->
     one-to-one unfolded s.n.c. special non trivial FinSequence of TOP-REAL 2;
 cluster one-to-one unfolded s.n.c. special non trivial ->
     being_S-Seq FinSequence of TOP-REAL 2;
 cluster being_S-Seq -> non empty FinSequence of TOP-REAL 2;
end;

definition
 cluster
  one-to-one unfolded s.n.c. special non trivial FinSequence of TOP-REAL 2;
end;

theorem :: SPPOL_2:27
   len f <= 2 implies f is unfolded;

definition let f be unfolded FinSequence of TOP-REAL 2, n;
 cluster f|n -> unfolded;
 cluster f/^n -> unfolded;
end;

theorem :: SPPOL_2:28
   p in rng f & f is unfolded implies f:-p is unfolded;

definition let f be unfolded FinSequence of TOP-REAL 2, p;
 cluster f-:p -> unfolded;
end;

theorem :: SPPOL_2:29
   f is unfolded implies Rev f is unfolded;

theorem :: SPPOL_2:30
  g is unfolded & LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1}
   implies <*p*>^g is unfolded;

theorem :: SPPOL_2:31
  f is unfolded & k+1 = len f & LSeg(f,k) /\
 LSeg(f/.len f,p) = {f/.len f}
   implies f^<*p*> is unfolded;

theorem :: SPPOL_2:32
  f is unfolded & g is unfolded &
    k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,g/.1) = {f/.len f} &
    LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1}
   implies f^g is unfolded;

theorem :: SPPOL_2:33
   f is unfolded & p in LSeg(f,n) implies Ins(f,n,p) is unfolded;

theorem :: SPPOL_2:34
   len f <= 2 implies f is s.n.c.;

definition let f be s.n.c. FinSequence of TOP-REAL 2, n;
  cluster f|n -> s.n.c.;
  cluster f/^n -> s.n.c.;
end;

definition let f be s.n.c. FinSequence of TOP-REAL 2, p;
  cluster f-:p -> s.n.c.;
end;

theorem :: SPPOL_2:35
  p in rng f & f is s.n.c. implies f:-p is s.n.c.;

theorem :: SPPOL_2:36
   f is s.n.c. implies Rev f is s.n.c.;

theorem :: SPPOL_2:37
  f is s.n.c. & g is s.n.c. & L~f misses L~g &
 (for i st 1<=i & i+2 <= len f holds LSeg(f,i) misses LSeg(f/.len f,g/.1)) &
 (for i st 2<=i & i+1 <= len g holds LSeg(g,i) misses LSeg(f/.len f,g/.1))
   implies f^g is s.n.c.;

theorem :: SPPOL_2:38
   f is unfolded s.n.c. & p in LSeg(f,n) & not p in rng f
    implies Ins(f,n,p) is s.n.c.;

definition
 cluster <*>(the carrier of TOP-REAL 2) -> special;
end;

theorem :: SPPOL_2:39
   <*p*> is special;

theorem :: SPPOL_2:40
   p`1 = q`1 or p`2 = q`2 implies <*p,q*> is special;

definition let f be special FinSequence of TOP-REAL 2, n;
 cluster f|n -> special;
 cluster f/^n -> special;
end;

theorem :: SPPOL_2:41
   p in rng f & f is special implies f:-p is special;

definition let f be special FinSequence of TOP-REAL 2, p;
 cluster f-:p -> special;
end;

theorem :: SPPOL_2:42
   f is special implies Rev f is special;

canceled;

theorem :: SPPOL_2:44
   f is special & p in LSeg(f,n) implies Ins(f,n,p) is special;

theorem :: SPPOL_2:45
   q in rng f & 1<>q..f & q..f<>len f & f is unfolded s.n.c.
    implies L~(f-:q) /\ L~(f:-q) = {q};

theorem :: SPPOL_2:46
   p <> q & (p`1 = q`1 or p`2 = q`2) implies <*p,q*> is being_S-Seq;

definition
 mode S-Sequence_in_R2 is being_S-Seq FinSequence of TOP-REAL 2;
end;

theorem :: SPPOL_2:47
   for f being S-Sequence_in_R2 holds Rev f is being_S-Seq;

theorem :: SPPOL_2:48
     for f being S-Sequence_in_R2 st i in dom f holds f/.i in L~f;

theorem :: SPPOL_2:49
     p <> q & (p`1 = q`1 or p`2 = q`2) implies LSeg(p,q) is being_S-P_arc;

theorem :: SPPOL_2:50
   for f being S-Sequence_in_R2 st p in rng f & p..f <> 1
    holds f-:p is being_S-Seq;

theorem :: SPPOL_2:51
     for f being S-Sequence_in_R2 st p in rng f & p..f <> len f
    holds f:-p is being_S-Seq;

theorem :: SPPOL_2:52
   for f being S-Sequence_in_R2 st p in LSeg(f,i) & not p in rng f
    holds Ins(f,i,p) is being_S-Seq;

begin :: Special Polygons in TOP-REAL 2

definition
 cluster being_S-P_arc Subset of TOP-REAL 2;
end;

theorem :: SPPOL_2:53
     P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1;

definition let p1,p2; let P be Subset of TOP-REAL 2;
 pred p1,p2 split P means
:: SPPOL_2:def 1
 p1 <> p2 &
  ex f1,f2 being S-Sequence_in_R2 st
   p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 &
   L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2;
end;

theorem :: SPPOL_2:54
   p1,p2 split P implies p2,p1 split P;

theorem :: SPPOL_2:55
   p1,p2 split P & q in P & q <> p1 implies p1,q split P;

theorem :: SPPOL_2:56
   p1,p2 split P & q in P & q <> p2 implies q,p2 split P;

theorem :: SPPOL_2:57
   p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P;

definition let P be Subset of TOP-REAL 2;
 redefine attr P is being_special_polygon means
:: SPPOL_2:def 2
 ex p1,p2 st p1,p2 split P;
  synonym P is special_polygonal;
end;

definition let r1,r2,r1',r2';
 func [.r1,r2,r1',r2'.] -> Subset of TOP-REAL 2 equals
:: SPPOL_2:def 3

    { p: p`1 = r1 & p`2 <= r2' & p`2 >= r1' or
             p`1 <= r2 & p`1 >= r1 & p`2 = r2' or
             p`1 <= r2 & p`1 >= r1 & p`2 = r1' or
             p`1 = r2 & p`2 <= r2' & p`2 >= r1'};
end;

theorem :: SPPOL_2:58
   r1<r2 & r1'<r2' implies
     [.r1,r2,r1',r2'.] =
       ( LSeg(|[r1,r1']|,|[r1,r2']|) \/ LSeg(|[r1,r2']|,|[r2,r2']|) ) \/
       ( LSeg(|[r2,r2']|,|[r2,r1']|) \/ LSeg(|[r2,r1']|,|[r1,r1']|) );

theorem :: SPPOL_2:59
   r1<r2 & r1'<r2' implies [.r1,r2,r1',r2'.] is special_polygonal;

theorem :: SPPOL_2:60
   R^2-unit_square = [.0,1,0,1.];

definition
 cluster special_polygonal Subset of TOP-REAL 2;
end;

theorem :: SPPOL_2:61
  R^2-unit_square is special_polygonal;

definition
 cluster special_polygonal Subset of TOP-REAL 2;
 cluster special_polygonal -> non empty Subset of TOP-REAL 2;
 cluster special_polygonal ->
    non trivial Subset of TOP-REAL 2;
end;

definition
 mode Special_polygon_in_R2 is special_polygonal Subset of TOP-REAL 2;
end;

theorem :: SPPOL_2:62
   P is being_S-P_arc implies P is compact;

theorem :: SPPOL_2:63
     for G being Special_polygon_in_R2 holds G is compact;

theorem :: SPPOL_2:64
  P is special_polygonal implies
   for p1,p2 st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P;

theorem :: SPPOL_2:65
    P is special_polygonal implies
   for p1,p2 st p1 <> p2 & p1 in P & p2 in P
    ex P1,P2 being Subset of TOP-REAL 2
     st P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 &
     P1 /\ P2 = {p1,p2} & P = P1 \/ P2;
The abstract of the Mizar article:

Special Polygons
