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

theorem Th1: :: SPRECT_4:1
for f being S-Sequence_in_R2
for Q being closed Subset of () 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 ()
for p being Point of () 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 ()
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 ()
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 () 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 V22() standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LeftComp f <> RightComp f

proof end;

Lm2: for f being V22() 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 V22() standard special_circular_sequence holds LeftComp f <> RightComp f
proof end;
{"ft_lang_label":"__label__en","ft_lang_prob":0.5737925,"math_prob":0.99923277,"size":1929,"snap":"2022-27-2022-33","text_gpt3_token_len":928,"char_repetition_ratio":0.16987012,"word_repetition_ratio":0.5612648,"special_character_ratio":0.45723173,"punctuation_ratio":0.21226415,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9995302,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-07-05T10:49:58Z\",\"WARC-Record-ID\":\"<urn:uuid:a9a2a3b7-7af1-480d-89ed-06b72327018e>\",\"Content-Length\":\"28232\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:799709c3-eec4-48b7-aff8-609148d29b01>\",\"WARC-Concurrent-To\":\"<urn:uuid:723ef340-d947-411f-a469-1e007cf745df>\",\"WARC-IP-Address\":\"212.33.73.131\",\"WARC-Target-URI\":\"https://mizar.uwb.edu.pl/version/current/html/sprect_4.html\",\"WARC-Payload-Digest\":\"sha1:L2W4ECPODS3LF3VR6L4KRVNDLFMBTGGR\",\"WARC-Block-Digest\":\"sha1:OJPFMBX6PAOSEBCD2YLBGDS2YIP3YDN4\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-27/CC-MAIN-2022-27_segments_1656104542759.82_warc_CC-MAIN-20220705083545-20220705113545-00010.warc.gz\"}"}