:: The Ordering of Points on a Curve, Part { I }
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, NAT_1, XXREAL_0, ARYTM_1, ARYTM_3, CARD_1, STRUCT_0, BORSUK_1, PRE_TOPC, EUCLID, MCART_1, RLTOPSP1, REAL_1, RELAT_1, SUPINF_2, XXREAL_1, FINSEQ_1, XBOOLE_0, SUBSET_1, FUNCT_1, TOPREAL1, TOPS_2, PARTFUN1, TOPMETR, TREAL_1, VALUED_1, FUNCT_4, RCOMP_1, TARSKI, ORDINAL2, PCOMPS_1, METRIC_1, JORDAN3, RFINSEQ, FINSEQ_5, GROUP_2, ORDINAL4, GOBOARD5, GOBOARD2, TREES_1, TOPREAL4, GOBOARD1, MATRIX_1, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, RCOMP_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4, TOPMETR, FINSEQ_6, SEQ_4, JORDAN3, STRUCT_0, TOPREAL1, RFINSEQ, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1, RLVECT_1, RLTOPSP1, EUCLID, TREAL_1, METRIC_1, GOBOARD1, GOBOARD2, MATRIX_0, TOPREAL4, GOBOARD5, FUNCT_4, FINSEQ_5, PCOMPS_1;
definitions TARSKI, JORDAN3, TOPREAL4, XBOOLE_0;
theorems BORSUK_1, COMPTS_1, EUCLID, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2, RELAT_1, JORDAN3, GOBOARD1, NAT_1, GOBOARD9, FUNCT_4, TOPMETR2, GOBOARD2, PRE_TOPC, RCOMP_1, HEINE, PCOMPS_1, SPPOL_2, TARSKI, TOPMETR, TOPREAL1, TOPREAL3, RFINSEQ, FINSEQ_5, GOBOARD5, GOBOARD7, FINSEQ_1, TOPS_2, TREAL_1, JORDAN5A, ZFMISC_1, JORDAN4, PARTFUN2, INT_1, RELSET_1, FINSEQ_6, XBOOLE_0, XBOOLE_1, XCMPLX_1, FINSEQ_2, XREAL_1, XXREAL_0, PARTFUN1, CARD_1, MATRIX_0, XXREAL_1, XXREAL_2, NAT_D, RLTOPSP1, SEQ_4, RLVECT_1;
schemes NAT_1;
registrations FUNCT_1, RELSET_1, FUNCT_2, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, GOBOARD2, GOBOARD5, VALUED_0, XXREAL_2, RLTOPSP1, SEQ_4, SPPOL_2, NAT_1, ORDINAL1;
constructors HIDDEN, FUNCT_4, REAL_1, SEQ_4, RCOMP_1, FINSEQ_4, RFINSEQ, NAT_D, FINSEQ_5, TOPS_2, COMPTS_1, TREAL_1, TOPREAL4, GOBOARD2, GOBOARD5, JORDAN3, GOBOARD1, CONVEX1, BINOP_2, PCOMPS_1, MONOID_0;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, STRUCT_0, RELAT_1, RLTOPSP1, RLVECT_1;
expansions TARSKI, JORDAN3, XBOOLE_0;


theorem Th1: :: JORDAN5B:1
for i1 being Nat st 1 <= i1 holds
i1 -' 1 < i1
proof end;

theorem :: JORDAN5B:2
for i, k being Nat st i + 1 <= k holds
1 <= k -' i
proof end;

theorem :: JORDAN5B:3
for i, k being Nat st 1 <= i & 1 <= k holds
(k -' i) + 1 <= k
proof end;

Lm1: for r being Real st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )
proof end;

theorem :: JORDAN5B:4
for r being Real st r in the carrier of I[01] holds
1 - r in the carrier of I[01]
proof end;

theorem :: JORDAN5B:5
for p, q, p1 being Point of (TOP-REAL 2) st p `2 <> q `2 & p1 in LSeg (p,q) & p1 `2 = p `2 holds
p1 = p
proof end;

theorem :: JORDAN5B:6
for p, q, p1 being Point of (TOP-REAL 2) st p `1 <> q `1 & p1 in LSeg (p,q) & p1 `1 = p `1 holds
p1 = p
proof end;

reconsider jj = 1 as Real ;

theorem Th7: :: JORDAN5B:7
for f being FinSequence of (TOP-REAL 2)
for P being non empty Subset of (TOP-REAL 2)
for F being Function of I[01],((TOP-REAL 2) | P)
for i being Nat st 1 <= i & i + 1 <= len f & f is being_S-Seq & P = L~ f & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,i) = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) )
proof end;

theorem :: JORDAN5B:8
for f being FinSequence of (TOP-REAL 2)
for Q, R being non empty Subset of (TOP-REAL 2)
for F being Function of I[01],((TOP-REAL 2) | Q)
for i being Nat
for P being non empty Subset of I[01] st f is being_S-Seq & F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg (f,i) & Q = L~ f & R = LSeg (f,i) holds
ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st
( G = F | P & G is being_homeomorphism )
proof end;

theorem Th9: :: JORDAN5B:9
for p1, p2, p being Point of (TOP-REAL 2) st p1 <> p2 & p in LSeg (p1,p2) holds
LE p,p,p1,p2 by JORDAN5A:2;

theorem Th10: :: JORDAN5B:10
for p, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p in LSeg (p1,p2) holds
LE p1,p,p1,p2
proof end;

theorem Th11: :: JORDAN5B:11
for p, p1, p2 being Point of (TOP-REAL 2) st p in LSeg (p1,p2) & p1 <> p2 holds
LE p,p2,p1,p2
proof end;

theorem :: JORDAN5B:12
for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2,p1,p2 & LE q2,q3,p1,p2 holds
LE q1,q3,p1,p2
proof end;

theorem :: JORDAN5B:13
for p, q being Point of (TOP-REAL 2) st p <> q holds
LSeg (p,q) = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }
proof end;

theorem :: JORDAN5B:14
for n being Nat
for P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P is_an_arc_of p2,p1
proof end;

theorem :: JORDAN5B:15
for i being Nat
for f being FinSequence of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg (f,i) holds
P is_an_arc_of f /. i,f /. (i + 1)
proof end;

theorem :: JORDAN5B:16
for g1 being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) holds
i = 1
proof end;

theorem :: JORDAN5B:17
for f being 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_Cut (f,p) = <*p*>
proof end;

theorem :: JORDAN5B:18
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & p <> f . (len f) & f is being_S-Seq holds
Index (p,(L_Cut (f,p))) = 1
proof end;

theorem Th19: :: JORDAN5B:19
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . (len f) holds
p in L~ (L_Cut (f,p))
proof end;

theorem :: JORDAN5B:20
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . 1 holds
p in L~ (R_Cut (f,p))
proof end;

theorem Th21: :: JORDAN5B:21
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & f is one-to-one holds
B_Cut (f,p,p) = <*p*>
proof end;

Lm2: for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds
q in L~ (L_Cut (f,p))
proof end;

theorem Th22: :: JORDAN5B:22
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is being_S-Seq holds
p in L~ (L_Cut (f,q))
proof end;

theorem :: JORDAN5B:23
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p <> f . (len f) & p in L~ f & q in L~ f & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds
q in L~ (L_Cut (f,p))
proof end;

Lm3: for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q holds
L~ (B_Cut (f,p,q)) c= L~ f
proof end;

theorem :: JORDAN5B:24
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is being_S-Seq holds
L~ (B_Cut (f,p,q)) c= L~ f
proof end;

theorem :: JORDAN5B:25
for f being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & j <= len (GoB f) & i < j holds
(LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}
proof end;

theorem :: JORDAN5B:26
for f being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & j <= width (GoB f) & i < j holds
(LSeg (((GoB f) * ((len (GoB f)),1)),((GoB f) * ((len (GoB f)),i)))) /\ (LSeg (((GoB f) * ((len (GoB f)),j)),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}
proof end;

theorem Th27: :: JORDAN5B:27
for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds
L_Cut (f,(f /. 1)) = f
proof end;

theorem :: JORDAN5B:28
for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds
R_Cut (f,(f /. (len f))) = f
proof end;

theorem :: JORDAN5B:29
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))
proof end;

theorem :: JORDAN5B:30
for f being FinSequence of (TOP-REAL 2)
for i being Nat st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) holds
i = 1
proof end;

theorem :: JORDAN5B:31
for f being non constant standard special_circular_sequence
for j being Nat
for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg (((GoB f) * (1,j)),((GoB f) * ((len (GoB f)),j))) holds
P is_S-P_arc_joining (GoB f) * (1,j),(GoB f) * ((len (GoB f)),j)
proof end;

theorem :: JORDAN5B:32
for f being non constant standard special_circular_sequence
for j being Nat
for P being Subset of (TOP-REAL 2) st 1 <= j & j <= len (GoB f) & P = LSeg (((GoB f) * (j,1)),((GoB f) * (j,(width (GoB f))))) holds
P is_S-P_arc_joining (GoB f) * (j,1),(GoB f) * (j,(width (GoB f)))
proof end;

theorem :: JORDAN5B:33
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index (p,f) < Index (q,f) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) ) & p <> q holds
L~ (B_Cut (f,p,q)) c= L~ f by Lm3;