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;

Back to top