:: On the components of the complement of a special polygonal curve
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received January 21, 1999
:: Copyright (c) 1999-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, SPPOL_2, RCOMP_1, EUCLID, TOPREAL1, XBOOLE_0, PARTFUN1, JORDAN3, JORDAN5C, FINSEQ_1, XXREAL_0, ARYTM_3, GROUP_2, RELAT_1, TARSKI, PRE_TOPC, FUNCT_1, ARYTM_1, RLTOPSP1, ORDINAL4, SPRECT_2, GOBOARD5, PSCOMP_1, GOBOARD9, SPRECT_1, GOBOARD2, TREES_1, MATRIX_1, TOPS_1, MCART_1, TOPREAL4, SPPOL_1, FINSEQ_5, FINSEQ_4, FINSEQ_6, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, MATRIX_0, STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL4, FINSEQ_5, FINSEQ_6, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9, JORDAN3, PSCOMP_1, JORDAN5C, SPRECT_1, SPRECT_2, XXREAL_0;
definitions ;
theorems TOPREAL1, JORDAN5C, JORDAN3, FINSEQ_3, SPPOL_2, TOPS_1, SPPOL_1, TOPREAL3, FINSEQ_5, NAT_1, SPRECT_1, JORDAN5B, SPRECT_2, GOBOARD5, FINSEQ_4, GOBOARD7, GOBOARD6, GOBOARD9, ZFMISC_1, TOPREAL4, PSCOMP_1, JORDAN4, FINSEQ_6, FINSEQ_1, TARSKI, EUCLID, SUBSET_1, JORDAN5D, SPRECT_3, REVROT_1, PARTFUN2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, CARD_1, NAT_D, RLTOPSP1, MATRIX_0, RLVECT_1;
schemes ;
registrations XBOOLE_0, RELSET_1, MEMBERED, FINSEQ_6, STRUCT_0, COMPTS_1, TOPREAL1, GOBOARD2, SPPOL_2, GOBOARD9, SPRECT_1, SPRECT_3, REVROT_1, FUNCT_1, EUCLID, ZFMISC_1, XREAL_0, NAT_1;
constructors HIDDEN, REAL_1, FINSEQ_4, TOPS_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL4, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN3, JORDAN5C, SPRECT_1, SPRECT_2, GOBOARD1, NAT_D, MATRIX_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities PSCOMP_1, RLTOPSP1;
expansions ;


theorem Th1: :: SPRECT_4:1
for f being S-Sequence_in_R2
for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. 1 in Q holds
(L~ (R_Cut (f,(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
proof end;

theorem :: SPRECT_4:2
for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is being_S-Seq & p = f /. (len f) holds
L~ (L_Cut (f,p)) = {}
proof end;

theorem Th3: :: SPRECT_4:3
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2)
for j being Nat st 1 <= j & j < len f & p in L~ (mid (f,j,(len f))) holds
LE f /. j,p, L~ f,f /. 1,f /. (len f)
proof end;

theorem Th4: :: SPRECT_4:4
for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2)
for j being Nat st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) holds
LE p,q, L~ f,f /. 1,f /. (len f)
proof end;

theorem Th5: :: SPRECT_4:5
for f being S-Sequence_in_R2
for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. (len f) in Q holds
(L~ (L_Cut (f,(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))))) /\ Q = {(Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
proof end;

Lm1: for f being non constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f
proof end;

Lm2: for f being non constant standard special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f
proof end;

theorem :: SPRECT_4:6
for f being non constant standard special_circular_sequence holds LeftComp f <> RightComp f
proof end;