:: The Ordering of Points on a Curve, Part { I }
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997-2021 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, 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 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;
constructors 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;
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;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
theorem :: JORDAN5B:1
for i1 being Nat st 1 <= i1 holds i1-'1 q`2 & p1 in LSeg (p, q)
holds ( p1`2 = p`2 implies p1 = p );
theorem :: JORDAN5B:6
for p, q, p1 being Point of TOP-REAL 2 st p`1 <> q`1 & p1 in LSeg (p, q)
holds ( p1`1 = p`1 implies p1 = p );
theorem :: JORDAN5B:7
for f being FinSequence of TOP-REAL 2,
P being non empty Subset of TOP-REAL 2,
F being Function of I[01], (TOP-REAL 2) | P,
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
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);
theorem :: JORDAN5B:8
for f being FinSequence of TOP-REAL 2,
Q, R being non empty Subset of TOP-REAL 2,
F being Function of I[01], (TOP-REAL 2)|Q, i being Nat,
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)
ex G being Function of I[01]|P, (TOP-REAL 2)|R st
G = F|P & G is being_homeomorphism;
begin :: Some properties of real intervals
theorem :: 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;
theorem :: 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;
theorem :: 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;
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;
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 };
theorem :: JORDAN5B:14
for n being Nat, P being Subset of TOP-REAL n,
p1, p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 holds P is_an_arc_of p2,p1;
theorem :: JORDAN5B:15
for i being Nat, f being FinSequence of TOP-REAL 2,
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);
begin :: Cutting off sequences
theorem :: JORDAN5B:16
for g1 being FinSequence of TOP-REAL 2, i being Nat
st 1 <= i & i <= len g1 & g1 is being_S-Seq holds
g1/.1 in L~mid(g1, i, len g1) implies i = 1;
theorem :: JORDAN5B:17
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st f is being_S-Seq & p = f.len f holds
L_Cut (f,p) = <*p*>;
theorem :: JORDAN5B:18
for f being FinSequence of TOP-REAL 2, 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;
theorem :: JORDAN5B:19
for f being FinSequence of TOP-REAL 2, 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);
theorem :: JORDAN5B:20
for f being FinSequence of TOP-REAL 2, 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);
theorem :: JORDAN5B:21
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st p in L~f & f is one-to-one
holds B_Cut(f,p,p) = <*p*>;
theorem :: JORDAN5B:22
for f being FinSequence of TOP-REAL 2, 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);
theorem :: JORDAN5B:23
for f being FinSequence of TOP-REAL 2, 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 holds
p in L~L_Cut(f,q) or q in L~L_Cut(f,p);
theorem :: JORDAN5B:24
for f being FinSequence of TOP-REAL 2,
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;
theorem :: JORDAN5B:25
for f being non constant standard special_circular_sequence,
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)) = {};
theorem :: JORDAN5B:26
for f being non constant standard special_circular_sequence,
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)) = {};
theorem :: JORDAN5B:27
for f being FinSequence of TOP-REAL 2 st f is being_S-Seq
holds L_Cut (f,f/.1) = f;
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;
theorem :: JORDAN5B:29
for f being FinSequence of TOP-REAL 2,
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) );
theorem :: JORDAN5B:30
for f be FinSequence of TOP-REAL 2 for i be Nat st
f is unfolded s.n.c. one-to-one & len f >= 2 & f/.1 in LSeg (f,i) holds
i = 1;
theorem :: JORDAN5B:31
for f be non constant standard special_circular_sequence,
j be Nat, P be 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);
theorem :: JORDAN5B:32
for f be non constant standard special_circular_sequence,
j be Nat, P be 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);
theorem :: JORDAN5B:33
for f be FinSequence of TOP-REAL 2
for p,q be 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;