:: Special Polygons :: by Czes\law Byli\'nski and Yatsuka Nakamura :: :: Received January 30, 1995 :: Copyright (c) 1995-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, EUCLID, FINSEQ_1, PRE_TOPC, NAT_1, ARYTM_3, RLTOPSP1, FINSEQ_5, XXREAL_0, RELAT_1, PARTFUN1, CARD_1, XBOOLE_0, RFINSEQ, ARYTM_1, ORDINAL4, FINSEQ_4, TOPREAL1, STRUCT_0, TARSKI, MCART_1, FUNCT_1, ZFMISC_1, TOPREAL4, XXREAL_1, RCOMP_1, BORSUK_1, TOPS_2, ORDINAL2, SPPOL_2, REAL_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, ZFMISC_1, FINSEQ_4, RFINSEQ, STRUCT_0, PRE_TOPC, COMPTS_1, TOPS_2, RLTOPSP1, EUCLID, BORSUK_1, TOPREAL1, TOPREAL4, FINSEQ_5; constructors XXREAL_0, NAT_1, FINSEQ_4, ZFMISC_1, RFINSEQ, BINARITH, FINSEQ_5, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, TOPREAL4, REAL_1, CONVEX1; registrations XBOOLE_0, RELAT_1, ORDINAL1, XREAL_0, FINSEQ_1, FINSEQ_5, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, NAT_1, INT_1, CARD_1, RLTOPSP1, SPPOL_1; 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,r19,r29 for Real, i,j,k,n for Nat; theorem :: SPPOL_2:1 |[ r1,r2 ]| = |[ r19,r29 ]| implies r1 = r19 & r2 = r29; theorem :: SPPOL_2:2 for i, j being Nat holds i+j = len f implies LSeg(f,i) = LSeg(Rev f,j); theorem :: SPPOL_2:3 for i, n being Nat holds i+1 <= len(f|n) implies LSeg(f|n,i) = LSeg(f,i); theorem :: SPPOL_2:4 for i, n being Nat holds n <= len f & 1 <= i implies LSeg(f/^n,i) = LSeg(f,n+i); theorem :: SPPOL_2:5 for i, n being Nat holds 1 <= i & i+1 <= len f - n implies LSeg(f /^n,i) = LSeg(f,n+i); theorem :: SPPOL_2:6 for i being Nat holds i+1 <= len f implies LSeg(f^g,i) = LSeg(f,i ); theorem :: SPPOL_2:7 for i being Nat holds 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 for i being Nat holds i+1 <= len(f-:p) implies LSeg(f-:p,i) = LSeg(f,i); theorem :: SPPOL_2:10 for i being Nat holds 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; theorem :: SPPOL_2:24 q in rng f implies L~f = L~(f-:q) \/ L~(f:-q); theorem :: SPPOL_2:25 p in LSeg(f,n) implies L~f = L~Ins(f,n,p); begin registration cluster being_S-Seq for FinSequence of TOP-REAL 2; cluster being_S-Seq -> one-to-one unfolded s.n.c. special non trivial for FinSequence of TOP-REAL 2; cluster one-to-one unfolded s.n.c. special non trivial -> being_S-Seq for FinSequence of TOP-REAL 2; cluster being_S-Seq -> non empty for FinSequence of TOP-REAL 2; end; registration cluster one-to-one unfolded s.n.c. special non trivial for FinSequence of TOP-REAL 2; end; theorem :: SPPOL_2:26 len f <= 2 implies f is unfolded; registration let f be unfolded FinSequence of TOP-REAL 2, n; cluster f|n -> unfolded for FinSequence of TOP-REAL 2; cluster f/^n -> unfolded for FinSequence of TOP-REAL 2; end; theorem :: SPPOL_2:27 p in rng f & f is unfolded implies f:-p is unfolded; registration let f be unfolded FinSequence of TOP-REAL 2, p; cluster f-:p -> unfolded; end; theorem :: SPPOL_2:28 f is unfolded implies Rev f is unfolded; theorem :: SPPOL_2:29 g is unfolded & LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1} implies <*p*> ^g is unfolded; theorem :: SPPOL_2:30 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:31 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:32 f is unfolded & p in LSeg(f,n) implies Ins(f,n,p) is unfolded; theorem :: SPPOL_2:33 len f <= 2 implies f is s.n.c.; registration let f be s.n.c. FinSequence of TOP-REAL 2, n; cluster f|n -> s.n.c. for FinSequence of TOP-REAL 2; cluster f/^n -> s.n.c. for FinSequence of TOP-REAL 2; end; registration let f be s.n.c. FinSequence of TOP-REAL 2, p; cluster f-:p -> s.n.c.; end; theorem :: SPPOL_2:34 p in rng f & f is s.n.c. implies f:-p is s.n.c.; theorem :: SPPOL_2:35 f is s.n.c. implies Rev f is s.n.c.; theorem :: SPPOL_2:36 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:37 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.; registration cluster <*>(the carrier of TOP-REAL 2) -> special; end; registration let p; cluster <*p*> -> special for FinSequence of TOP-REAL 2; end; theorem :: SPPOL_2:38 p`1 = q`1 or p`2 = q`2 implies <*p,q*> is special; registration let f be special FinSequence of TOP-REAL 2, n; cluster f|n -> special for FinSequence of TOP-REAL 2; cluster f/^n -> special for FinSequence of TOP-REAL 2; end; theorem :: SPPOL_2:39 p in rng f & f is special implies f:-p is special; registration let f be special FinSequence of TOP-REAL 2, p; cluster f-:p -> special; end; theorem :: SPPOL_2:40 f is special implies Rev f is special; theorem :: SPPOL_2:41 f is special & p in LSeg(f,n) implies Ins(f,n,p) is special; theorem :: SPPOL_2:42 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:43 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; registration let f be S-Sequence_in_R2; cluster Rev f -> being_S-Seq for FinSequence of TOP-REAL 2; end; theorem :: SPPOL_2:44 for f being S-Sequence_in_R2 st i in dom f holds f/.i in L~f; theorem :: SPPOL_2:45 p <> q & (p`1 = q`1 or p`2 = q`2) implies LSeg(p,q) is being_S-P_arc; theorem :: SPPOL_2:46 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:47 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:48 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 registration cluster being_S-P_arc for Subset of TOP-REAL 2; end; theorem :: SPPOL_2:49 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:50 p1,p2 split P implies p2,p1 split P; theorem :: SPPOL_2:51 p1,p2 split P & q in P & q <> p1 implies p1,q split P; theorem :: SPPOL_2:52 p1,p2 split P & q in P & q <> p2 implies q,p2 split P; theorem :: SPPOL_2:53 p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P; notation let P be Subset of TOP-REAL 2; synonym P is special_polygonal for P is being_special_polygon; end; definition let P be Subset of TOP-REAL 2; redefine attr P is special_polygonal means :: SPPOL_2:def 2 ex p1,p2 st p1,p2 split P; end; definition let r1,r2,r19,r29 be Real; func [.r1,r2,r19,r29.] -> Subset of TOP-REAL 2 equals :: SPPOL_2:def 3 ( LSeg(|[r1,r19]|,|[r1 ,r29]|) \/ LSeg(|[r1,r29]|,|[r2,r29]|) ) \/ ( LSeg(|[r2,r29]|,|[r2,r19]|) \/ LSeg(|[r2,r19]|,|[r1,r19]|) ); end; registration let n be Element of NAT; let p1, p2 be Point of TOP-REAL n; cluster LSeg(p1,p2) -> compact; end; registration let r1,r2,r19,r29; cluster [.r1,r2,r19,r29.] -> non empty compact; end; theorem :: SPPOL_2:54 r1<=r2 & r19<=r29 implies [.r1,r2,r19,r29.] = { p: p`1 = r1 & p`2 <= r29 & p`2 >= r19 or p`1 <= r2 & p`1 >= r1 & p`2 = r29 or p`1 <= r2 & p`1 >= r1 & p`2 = r19 or p`1 = r2 & p`2 <= r29 & p`2 >= r19}; theorem :: SPPOL_2:55 r1<>r2 & r19<>r29 implies [.r1,r2,r19,r29.] is special_polygonal; theorem :: SPPOL_2:56 R^2-unit_square = [.0,1,0,1.]; registration cluster special_polygonal for Subset of TOP-REAL 2; end; registration cluster R^2-unit_square -> special_polygonal; end; registration cluster special_polygonal for Subset of TOP-REAL 2; cluster special_polygonal -> non empty for Subset of TOP-REAL 2; cluster special_polygonal -> non trivial for Subset of TOP-REAL 2; end; definition mode Special_polygon_in_R2 is special_polygonal Subset of TOP-REAL 2; end; theorem :: SPPOL_2:57 P is being_S-P_arc implies P is compact; registration cluster -> compact for Special_polygon_in_R2; end; theorem :: SPPOL_2:58 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:59 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;