The Mizar abstract of SPPOL

Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users
The abstract of the Mizar article:: Extremal Properties of Vertices on Special Polygons, Part I
by
Yatsuka Nakamura, and
Czeslaw Bylinski
Received May 11, 1994
MML identifier: SPPOL_1
[ Mizar article, MML identifier index ]
environ

 vocabulary FINSET_1, REALSET1, CARD_1, ARYTM, ARYTM_1, FINSEQ_1, ARYTM_3,
      SQUARE_1, RELAT_1, COMPLEX1, PRE_TOPC, EUCLID, METRIC_1, FUNCT_1,
      TOPREAL1, SEQ_2, SEQ_4, BOOLE, SUBSET_1, PCOMPS_1, ABSVALUE, COMPTS_1,
      TEX_2, BORSUK_1, TOPS_2, ORDINAL2, MCART_1, FINSEQ_4, SETFAM_1, TARSKI,
      SPPOL_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, ABSVALUE, SQUARE_1, STRUCT_0, SEQ_4, FUNCT_1, PRE_TOPC,
      BORSUK_1, FINSET_1, CARD_1, FINSEQ_1, METRIC_1, PCOMPS_1, TOPS_2,
      REALSET1, COMPTS_1, FINSEQ_4, EUCLID, TEX_2, TOPREAL1;
 constructors NAT_1, REAL_1, INT_1, ABSVALUE, SQUARE_1, SEQ_4, TOPS_2,
      REALSET1, COMPTS_1, TOPMETR, TDLAT_3, TEX_2, TOPREAL1, FINSEQ_4,
      MEMBERED, ORDINAL2;
 clusters FINSET_1, PRE_TOPC, INT_1, TEX_2, RELSET_1, TREES_3, PRELAMB,
      STRUCT_0, EUCLID, TOPREAL1, XREAL_0, MEMBERED, ZFMISC_1, NUMBERS,
      ORDINAL2, FINSEQ_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaires

canceled;

theorem :: SPPOL_1:2
    for A being finite set holds A is trivial iff card A < 2;

theorem :: SPPOL_1:3
  for A being set holds A is non trivial iff
   ex a1,a2 being set st a1 in A & a2 in A & a1 <> a2;

theorem :: SPPOL_1:4
  for D being set, A being Subset of D
   holds A is non trivial iff
    ex d1,d2 being Element of D st d1 in A & d2 in A & d1 <> d2;

reserve n,i,j,k,m for Nat;
reserve r,r1,r2,s,s1,s2 for real number;

theorem :: SPPOL_1:5
  r<=s implies r-1<=s & r-1<s & r<=s+1 & r<s+1;

theorem :: SPPOL_1:6
    (n<k implies n<=k-1) &
  (r<s implies r-1<=s & r-1<s & r<=s+1 & r<s+1);

theorem :: SPPOL_1:7
    1<=k-m & k-m<=n implies k-m in Seg n & k-m is Nat;

theorem :: SPPOL_1:8
  r1>=0 & r2>=0 & r1+r2=0 implies r1=0 & r2=0;

theorem :: SPPOL_1:9
     r1<=0 & r2<=0 & r1+r2=0 implies r1=0 & r2=0;

theorem :: SPPOL_1:10
    0<=r1 & r1<=1 & 0<=r2 & r2<=1 & r1*r2=1 implies r1=1 & r2=1;

theorem :: SPPOL_1:11
   r1>=0 & r2>=0 & s1>=0 & s2>=0 & r1*s1+r2*s2=0
     implies (r1=0 or s1=0) & (r2=0 or s2=0);

theorem :: SPPOL_1:12
  0<=r & r<=1 & s1>=0 & s2>=0 & r*s1+(1-r)*s2=0
   implies r=0 & s2=0 or r=1 & s1=0 or s1=0 & s2=0;

theorem :: SPPOL_1:13
  r<r1 & r<r2 implies r<min(r1,r2);

theorem :: SPPOL_1:14
  r>r1 & r>r2 implies r>max(r1,r2);

scheme FinSeqFam{D()-> non empty set,f()->FinSequence of D(),
                 F(FinSequence of D(),Nat)->set,P[Nat]}:
  {F(f(),i): i in dom f() & P[i]} is finite;

scheme FinSeqFam'{D()-> non empty set,f()-> FinSequence of D(),
                 F(FinSequence of D(),Nat)->set,P[Nat]}:
  {F(f(),i): 1<=i & i<=len f() & P[i]} is finite;

theorem :: SPPOL_1:15
 for x1,x2,x3 being Element of REAL n
  holds |.x1 - x2.|- |.x2 - x3.| <= |.x1 - x3.|;

theorem :: SPPOL_1:16
   for x1,x2,x3 being Element of REAL n
  holds |.x2 - x1.|- |.x2 - x3.| <= |.x3 - x1.|;

theorem :: SPPOL_1:17
 for p being Point of TOP-REAL n
  holds p is Element of REAL n & p is Point of Euclid n;

theorem :: SPPOL_1:18
   for up being Point of Euclid n
  holds up is Element of REAL n & up is Point of TOP-REAL n;

theorem :: SPPOL_1:19
    for x being Element of REAL n
   holds x is Point of Euclid n & x is Point of TOP-REAL n;

begin
:: Extremal properties of endpoints of line segments in n-dimensional
:: Euclidean space

reserve r,r1,r2,s,s1,s2 for Real;
reserve p,p1,p2,q1,q2 for Point of TOP-REAL n;

theorem :: SPPOL_1:20
  for u1,u2 being Point of Euclid n, v1,v2 being Element of REAL n
    st v1=u1 & v2=u2 holds dist(u1,u2) = |.v1-v2.|;

theorem :: SPPOL_1:21
 for p,p1,p2 st p in LSeg(p1,p2) ex r st 0<=r & r<=1 & p = (1-r)*p1+r*p2;

theorem :: SPPOL_1:22
   for p1,p2,r st 0<=r & r<=1 holds (1-r)*p1+r*p2 in LSeg(p1,p2);

theorem :: SPPOL_1:23
   for P being non empty Subset of TOP-REAL n
  st P is closed & P c= LSeg(p1,p2)
 ex s st (1-s)*p1+s*p2 in P &
 for r st 0<=r & r<=1 & (1-r)*p1+r*p2 in P holds s<=r;

theorem :: SPPOL_1:24
 for p1,p2,q1,q2 st LSeg(q1,q2) c= LSeg(p1,p2) & p1 in LSeg(q1,q2)
   holds p1=q1 or p1=q2;

theorem :: SPPOL_1:25
     for p1,p2,q1,q2 st LSeg(p1,p2) = LSeg(q1,q2)
     holds p1=q1 & p2=q2 or p1=q2 & p2=q1;

theorem :: SPPOL_1:26
  TOP-REAL n is_T2;

theorem :: SPPOL_1:27
    {p} is closed;

theorem :: SPPOL_1:28
  LSeg(p1,p2) is compact;

theorem :: SPPOL_1:29
  LSeg(p1,p2) is closed;

definition let n,p; let P be Subset of TOP-REAL n;
 pred p is_extremal_in P means
:: SPPOL_1:def 1
 p in P &
  for p1,p2 st p in LSeg(p1,p2) & LSeg(p1,p2) c= P holds p=p1 or p=p2;
end;

theorem :: SPPOL_1:30
    for P,Q being Subset of TOP-REAL n
   st p is_extremal_in P & Q c= P & p in Q holds p is_extremal_in Q;

theorem :: SPPOL_1:31
     p is_extremal_in {p};

theorem :: SPPOL_1:32
  p1 is_extremal_in LSeg(p1,p2);

theorem :: SPPOL_1:33
   p2 is_extremal_in LSeg(p1,p2);

theorem :: SPPOL_1:34
    p is_extremal_in LSeg(p1,p2) implies p = p1 or p = p2;


begin
:: Extremal properties of vertices of special polygons

reserve P,Q for Subset of TOP-REAL 2,
   f,f1,f2 for FinSequence of the carrier of TOP-REAL 2,
   p,p1,p2,p3,q,q3 for Point of TOP-REAL 2;

theorem :: SPPOL_1:35
 for p1,p2 st p1`1<>p2`1 & p1`2<>p2`2
  ex p st p in LSeg(p1,p2) & p`1<>p1`1 & p`1<>p2`1 & p`2<>p1`2 & p`2<>p2`2;

definition let P;
 attr P is horizontal means
:: SPPOL_1:def 2
  for p,q st p in P & q in P holds p`2=q`2;
 attr P is vertical means
:: SPPOL_1:def 3
  for p,q st p in P & q in P holds p`1=q`1;
end;

definition
 cluster non trivial horizontal -> non vertical Subset of TOP-REAL 2;
 cluster non trivial vertical -> non horizontal Subset of TOP-REAL 2;
end;

theorem :: SPPOL_1:36
  p`2=q`2 iff LSeg(p,q) is horizontal;

theorem :: SPPOL_1:37
  p`1=q`1 iff LSeg(p,q) is vertical;

theorem :: SPPOL_1:38
    p1 in LSeg(p,q) & p2 in LSeg(p,q) & p1`1<>p2`1 & p1`2=p2`2
   implies LSeg(p,q) is horizontal;

theorem :: SPPOL_1:39
    p1 in LSeg(p,q) & p2 in LSeg(p,q) & p1`2<>p2`2 & p1`1=p2`1
   implies LSeg(p,q) is vertical;

theorem :: SPPOL_1:40
  LSeg(f,i) is closed;

theorem :: SPPOL_1:41
  f is special implies LSeg(f,i) is vertical or LSeg(f,i) is horizontal;

theorem :: SPPOL_1:42
  f is one-to-one & 1 <= i & i+1 <= len f implies LSeg(f,i) is non trivial;

theorem :: SPPOL_1:43
    f is one-to-one & 1 <= i & i+1 <= len f & LSeg(f,i) is vertical
    implies LSeg(f,i) is non horizontal;

theorem :: SPPOL_1:44
   for f holds {LSeg(f,i): 1<=i & i<=len f} is finite;

theorem :: SPPOL_1:45
  for f holds {LSeg(f,i): 1<=i & i+1<=len f} is finite;

theorem :: SPPOL_1:46
    for f holds {LSeg(f,i): 1<=i & i<=len f} is Subset-Family of TOP-REAL 2;

theorem :: SPPOL_1:47
  for f holds {LSeg(f,i): 1<=i & i+1<=len f} is Subset-Family of TOP-REAL 2;

theorem :: SPPOL_1:48
 for f st Q = union{LSeg(f,i): 1<=i & i+1<=len f} holds Q is closed;

theorem :: SPPOL_1:49
     L~f is closed;

definition let IT be FinSequence of TOP-REAL 2;
  attr IT is alternating means
:: SPPOL_1:def 4

 for i st 1 <= i & i+2 <= len IT holds
  (IT/.i)`1 <> (IT/.(i+2))`1 & (IT/.i)`2 <> (IT/.(i+2))`2;
end;

theorem :: SPPOL_1:50
 f is special alternating & 1 <= i & i+2 <= len f & (f/.i)`1 = (f/.(i+1))`1
  implies (f/.(i+1))`2 = (f/.(i+2))`2;

theorem :: SPPOL_1:51
 f is special alternating & 1 <= i & i+2 <= len f & (f/.i)`2 = (f/.(i+1))`2
  implies (f/.(i+1))`1 = (f/.(i+2))`1;

theorem :: SPPOL_1:52
 f is special alternating & 1 <= i & i+2 <= len f &
   p1 = f/.i & p2 = f/.(i+1) & p3 = f/.(i+2)
 implies (p1`1 = p2`1 & p3`1 <> p2`1) or (p1`2 = p2`2 & p3`2 <> p2`2);

theorem :: SPPOL_1:53
   f is special alternating & 1 <= i & i+2 <= len f &
   p1 = f/.i & p2 = f/.(i+1) & p3 = f/.(i+2)
 implies (p2`1 = p3`1 & p1`1 <> p2`1) or (p2`2 = p3`2 & p1`2 <> p2`2);

theorem :: SPPOL_1:54
    f is special alternating & 1<=i & i+2<=len f implies
   not LSeg(f/.i,f/.(i+2)) c= LSeg(f,i) \/ LSeg(f,i+1);

theorem :: SPPOL_1:55
  f is special alternating & 1<=i & i+2<=len f & LSeg(f,i) is vertical
   implies LSeg(f,i+1) is horizontal;

theorem :: SPPOL_1:56
  f is special alternating & 1<=i & i+2<=len f & LSeg(f,i) is horizontal
   implies LSeg(f,i+1) is vertical;

theorem :: SPPOL_1:57
   f is special alternating & 1<=i & i+2<=len f
  implies LSeg(f,i) is vertical & LSeg(f,i+1) is horizontal
    or LSeg(f,i) is horizontal & LSeg(f,i+1) is vertical;

theorem :: SPPOL_1:58
  f is special alternating & 1<=i & i+2<=len f &
    f/.(i+1) in LSeg(p,q) & LSeg(p,q) c= LSeg(f,i) \/ LSeg(f,i+1)
   implies f/.(i+1)=p or f/.(i+1)=q;

theorem :: SPPOL_1:59
  f is special alternating & 1<=i & i+2<=len f
   implies f/.(i+1) is_extremal_in LSeg(f,i) \/ LSeg(f,i+1);

theorem :: SPPOL_1:60
 for u being Point of Euclid 2
  st f is special alternating
   & 1<=i & i+2<=len f & u = f/.(i+1) & f/.(i+1) in LSeg(p,q) & f/.(i+1)<>q
   & not p in LSeg(f,i) \/ LSeg(f,i+1)
  holds for s st s>0
   ex p3 st not p3 in LSeg(f,i) \/ LSeg(f,i+1) &
   p3 in LSeg(p,q) & p3 in Ball(u,s);

definition let f1,f2,P;
 pred f1,f2 are_generators_of P means
:: SPPOL_1:def 5
  f1 is alternating being_S-Seq &
        f2 is alternating being_S-Seq &
   f1/.1 = f2/.1 & f1/.len f1 = f2/.len f2 &
   <*f1/.2,f1/.1,f2/.2*> is alternating &
   <*f1/.(len f1 - 1),f1/.len f1,f2/.(len f2 - 1)*> is alternating &
   f1/.1 <> f1/.len f1 & L~f1 /\ L~f2 = {f1/.1,f1/.len f1} &
   P = L~f1 \/ L~f2;
end;

theorem :: SPPOL_1:61
    f1,f2 are_generators_of P & 1<i & i<len f1
   implies f1/.i is_extremal_in P;
The abstract of the Mizar article:

Extremal Properties of Vertices on Special Polygons, Part I
