:: Special Polygons
:: by Czes\law Byli\'nski and Yatsuka Nakamura
::
:: Received January 30, 1995
:: Copyright (c) 1995-2017 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;