:: Some properties of special polygonal curves
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 22, 1998
:: Copyright (c) 1998-2019 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, NAT_1, XBOOLE_0, FINSEQ_1, ORDINAL4, PARTFUN1, XXREAL_0,
ARYTM_3, MATRIX_1, ZFMISC_1, SUBSET_1, PRE_TOPC, EUCLID, REAL_1, CARD_1,
ARYTM_1, RELAT_1, SUPINF_2, RLTOPSP1, METRIC_1, RELAT_2, CONVEX1,
RCOMP_1, CONNSP_1, TARSKI, PCOMPS_1, SPPOL_1, MCART_1, GOBOARD1, TREES_1,
PSCOMP_1, TOPREAL1, SPRECT_1, SPPOL_2, JORDAN3, FUNCT_1, RFINSEQ,
GROUP_2, GOBOARD5, GOBOARD9, TOPREAL4, JORDAN5D, GOBOARD2, SPRECT_2,
COMPLEX1, ORDINAL2, TOPS_1, JORDAN5C, FINSEQ_5;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, NAT_D, CARD_1, RFINSEQ,
FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_0, MATRIX_1,
SEQM_3, SEQ_4, FINSEQ_6, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1,
CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL4,
PSCOMP_1, GOBOARD1, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9,
JORDAN3, JORDAN5C, JORDAN5D, SPRECT_1, SPRECT_2, XXREAL_0;
constructors REAL_1, FINSEQ_4, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, TOPS_2,
COMPTS_1, MATRIX_1, TOPMETR, TOPREAL2, TOPREAL4, GOBOARD2, SPPOL_1,
PSCOMP_1, GOBOARD9, JORDAN3, JORDAN5C, SPRECT_1, SPRECT_2, JORDAN5D,
GOBOARD1, PCOMPS_1, BINARITH, FUNCSDOM, CONVEX1, SEQ_4, RVSUM_1,
VALUED_0;
registrations RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2,
SPPOL_2, SPRECT_1, SPRECT_2, VALUED_0, CARD_1, FUNCT_1, SEQ_4, SPPOL_1,
TOPS_1, JORDAN1, RVSUM_1, NAT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
theorem :: SPRECT_3:1
for D being non empty set for f being non empty FinSequence of D, g
being FinSequence of D holds (g^f)/.len(g^f) = f/.len f;
theorem :: SPRECT_3:2
for a,b,c,d being set holds Indices (a,b)][(c,d) = {[1,1],[1,2], [2,1],[2,2]}
;
begin :: Euclidean Space
reserve i,j,k,n,m for Nat;
theorem :: SPRECT_3:3
for p,q being Point of TOP-REAL n, r being Real st 0 < r & p = (
1-r)*p+r*q holds p = q;
theorem :: SPRECT_3:4
for p,q being Point of TOP-REAL n, r being Real st r < 1 & p = (
1-r)*q+r*p holds p = q;
theorem :: SPRECT_3:5
for p,q being Point of TOP-REAL n st p = 1/2*(p+q) holds p = q;
theorem :: SPRECT_3:6
for p,q,r being Point of TOP-REAL n st q in LSeg(p,r) & r in
LSeg(p,q) holds q = r;
begin :: Euclidean Plane
theorem :: SPRECT_3:7
for A being non empty Subset of TOP-REAL 2, p being Element of
Euclid 2, r being Real st A = Ball(p,r) holds A is connected;
theorem :: SPRECT_3:8
for A, B being Subset of TOP-REAL 2 st A is open & B
is_a_component_of A holds B is open;
theorem :: SPRECT_3:9
for p,q,r,s being Point of TOP-REAL 2 st LSeg(p,q) is horizontal &
LSeg(r,s) is horizontal & LSeg(p,q) meets LSeg(r,s) holds p`2= r`2;
theorem :: SPRECT_3:10
for p,q,r being Point of TOP-REAL 2 st LSeg(p,q) is vertical & LSeg(q,
r) is horizontal holds LSeg(p,q) /\ LSeg(q,r) = {q};
theorem :: SPRECT_3:11
for p,q,r,s being Point of TOP-REAL 2 st LSeg(p,q) is horizontal &
LSeg(s,r) is vertical & r in LSeg(p,q) holds LSeg(p,q) /\ LSeg(s,r) = {r};
begin :: Main
reserve p,q for Point of TOP-REAL 2;
reserve G for Go-board;
theorem :: SPRECT_3:12
1 <= j & j <= k & k <= width G & 1 <= i & i <= len G implies G*(i,j)`2
<= G*(i,k)`2;
theorem :: SPRECT_3:13
1 <= j & j <= width G & 1 <= i & i <= k & k <= len G implies G*(i,j)`1
<= G*(k,j)`1;
reserve C for Subset of TOP-REAL 2;
theorem :: SPRECT_3:14
LSeg(NW-corner C,NE-corner C) c= L~SpStSeq C;
theorem :: SPRECT_3:15
for C being non empty compact Subset of TOP-REAL 2 holds N-min C
in LSeg(NW-corner C,NE-corner C);
registration
let C;
cluster LSeg(NW-corner C,NE-corner C) -> horizontal;
end;
theorem :: SPRECT_3:16
for g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st
g/.1 <> p & ((g/.1)`1 = p`1 or (g/.1)`2 = p`2) & g is being_S-Seq & LSeg(p,g/.1
) /\ L~g={ g/.1 } holds <*p*>^g is being_S-Seq;
theorem :: SPRECT_3:17
for f being S-Sequence_in_R2, p being Point of TOP-REAL 2 st 1 non vertical non horizontal;
cluster LeftComp f -> being_Region;
cluster RightComp f -> being_Region;
end;
theorem :: SPRECT_3:25
for f being non constant standard special_circular_sequence
holds RightComp f misses L~f;
theorem :: SPRECT_3:26
for f being non constant standard special_circular_sequence
holds LeftComp f misses L~f;
theorem :: SPRECT_3:27
for f being non constant standard special_circular_sequence
holds i_w_n f < i_e_n f;
theorem :: SPRECT_3:28
for f being non constant standard special_circular_sequence ex i
st 1 <= i & i < len GoB f & N-min L~f = (GoB f)*(i,width GoB f);
theorem :: SPRECT_3:29
for f being clockwise_oriented non constant standard
special_circular_sequence st i in dom GoB f & f/.1 = (GoB f)*(i,width GoB f) &
f/.1 = N-min L~f holds f/.2 = (GoB f)*(i+1,width GoB f) & f/.(len f -' 1) = (
GoB f)*(i,width GoB f -' 1);
theorem :: SPRECT_3:30
for f being non constant standard special_circular_sequence st 1 <= i
& i < j & j <= len f & f/.1 in L~mid(f,i,j) holds i = 1 or j = len f;
theorem :: SPRECT_3:31
for f being clockwise_oriented non constant standard
special_circular_sequence st f/.1 = N-min L~f holds LSeg(f/.1,f/.2) c= L~
SpStSeq L~f;
begin :: Rectangular
theorem :: SPRECT_3:32
for f being rectangular FinSequence of TOP-REAL 2, p being Point
of TOP-REAL 2 st p in L~f holds p`1 = W-bound L~f or p`1 = E-bound L~f or p`2 =
S-bound L~f or p`2 = N-bound L~f;
registration
cluster rectangular for special_circular_sequence;
end;
theorem :: SPRECT_3:33
for f being rectangular special_circular_sequence, g being
S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds L~f
meets L~g;
theorem :: SPRECT_3:34
for f being rectangular special_circular_sequence holds SpStSeq L~f = f;
theorem :: SPRECT_3:35
for f being rectangular special_circular_sequence holds L~f = {
p where p is Point of TOP-REAL 2: p`1 = W-bound L~f & p`2 <= N-bound L~f & p`2
>= S-bound L~f or p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = N-bound L~f
or p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = S-bound L~f or p`1 = E-bound
L~f & p`2 <= N-bound L~f & p`2 >= S-bound L~f};
theorem :: SPRECT_3:36
for f being rectangular special_circular_sequence holds GoB f =
(f/.4,f/.1)][(f/.3,f/.2);
theorem :: SPRECT_3:37
for f being rectangular special_circular_sequence holds LeftComp
f = {p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f & S-bound L~f <= p`2 & p`2
<= N-bound L~f)} & RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f &
S-bound L~f < q`2 & q`2 < N-bound L~f};
registration
cluster clockwise_oriented for rectangular special_circular_sequence;
end;
registration
cluster -> clockwise_oriented for rectangular special_circular_sequence;
end;
theorem :: SPRECT_3:38
for f being rectangular special_circular_sequence, g being
S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds
Last_Point(L~g,g/.1,g/.len g,L~f) <> NW-corner L~f;
theorem :: SPRECT_3:39
for f being rectangular special_circular_sequence, g being
S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds
Last_Point(L~g,g/.1,g/.len g,L~f) <> SE-corner L~f;
theorem :: SPRECT_3:40
for f being rectangular special_circular_sequence, p being Point
of TOP-REAL 2 st W-bound L~f > p`1 or p`1 > E-bound L~f or S-bound L~f > p`2 or
p`2 > N-bound L~f holds p in LeftComp f;
theorem :: SPRECT_3:41
for f being clockwise_oriented non constant standard
special_circular_sequence st f/.1 = N-min L~f holds LeftComp SpStSeq L~f c=
LeftComp f;
begin :: In the area
theorem :: SPRECT_3:42
for f being FinSequence of TOP-REAL 2, p,q being Point of
TOP-REAL 2 holds <*p,q*> is_in_the_area_of f iff <*p*> is_in_the_area_of f & <*
q*> is_in_the_area_of f;
theorem :: SPRECT_3:43
for f being rectangular FinSequence of TOP-REAL 2, p being Point
of TOP-REAL 2 st <*p*> is_in_the_area_of f & (p`1 = W-bound L~f or p`1 =
E-bound L~f or p`2 = S-bound L~f or p`2 = N-bound L~f) holds p in L~f;
theorem :: SPRECT_3:44
for f being FinSequence of TOP-REAL 2, p,q being Point of
TOP-REAL 2, r being Real
st 0<=r & r <= 1 & <*p,q*> is_in_the_area_of f holds
<*(1-r)*p+r*q*> is_in_the_area_of f;
theorem :: SPRECT_3:45
for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of
f & i in dom g holds <*g/.i*> is_in_the_area_of f;
theorem :: SPRECT_3:46
for f, g being FinSequence of TOP-REAL 2, p being Point of
TOP-REAL 2 st g is_in_the_area_of f & p in L~g holds <*p*> is_in_the_area_of f;
theorem :: SPRECT_3:47
for f being rectangular FinSequence of TOP-REAL 2, p,q being
Point of TOP-REAL 2 st not q in L~f & <*p,q*> is_in_the_area_of f holds LSeg(p,
q) /\ L~f c= {p};
theorem :: SPRECT_3:48
for f being rectangular FinSequence of TOP-REAL 2, p,q being Point of
TOP-REAL 2 st p in L~f & not q in L~f & <*q*> is_in_the_area_of f holds LSeg(p,
q) /\ L~f = {p};
theorem :: SPRECT_3:49
for f being non constant standard special_circular_sequence st 1
<= i & i <= len GoB f & 1 <= j & j <= width GoB f holds <*(GoB f)*(i,j)*>
is_in_the_area_of f;
theorem :: SPRECT_3:50
for g being FinSequence of TOP-REAL 2, p,q being Point of TOP-REAL 2
st <*p,q*> is_in_the_area_of g holds <*1/2*(p+q)*> is_in_the_area_of g;
theorem :: SPRECT_3:51
for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of f
holds Rev g is_in_the_area_of f;
theorem :: SPRECT_3:52
for f, g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in
L~g holds R_Cut(g,p) is_in_the_area_of f;
theorem :: SPRECT_3:53
for f being non constant standard special_circular_sequence, g being
FinSequence of TOP-REAL2 holds g is_in_the_area_of f iff g is_in_the_area_of
SpStSeq L~f;
theorem :: SPRECT_3:54
for f being rectangular special_circular_sequence, g being
S-Sequence_in_R2 st g/.1 in LeftComp f & g/.len g in RightComp f holds L_Cut(g,
Last_Point(L~g,g/.1,g/.len g,L~f)) is_in_the_area_of f;
theorem :: SPRECT_3:55
for f being non constant standard special_circular_sequence st 1 <= i
& i < len GoB f & 1 <= j & j < width GoB f holds Int cell(GoB f,i,j) misses L~
SpStSeq L~f;
theorem :: SPRECT_3:56
for f, g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2
st g is_in_the_area_of f & <*p*> is_in_the_area_of f & g is being_S-Seq & p in
L~g holds L_Cut(g,p) is_in_the_area_of f;