:: Subsequences of Almost, Weakly and Poorly One-to-one Finite Sequences
:: by Robert Milewski
::
:: Received February 1, 2005
:: Copyright (c) 2005-2016 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, SUBSET_1, FINSEQ_1, EUCLID, PRE_TOPC, TOPREAL1, JORDAN3,
XXREAL_0, XBOOLE_0, CARD_1, ARYTM_3, GROUP_2, PARTFUN1, FINSEQ_5,
FUNCT_1, RELAT_1, FINSEQ_6, ARYTM_1, FINSEQ_4, RFINSEQ, ORDINAL4,
RCOMP_1, SPPOL_1, JORDAN9, RLTOPSP1, NAT_1, TARSKI, GRAPH_2, MCART_1,
REAL_1, SUPINF_2, JORDAN2C, SPPOL_2, JORDAN18, GOBOARD1, GOBOARD2,
GOBOARD5, MATRIX_1, JORDAN23;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5,
RFINSEQ, MATRIX_0, FINSEQ_6, GRAPH_2, STRUCT_0, PRE_TOPC, NAT_D,
COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, GOBOARD1, TOPREAL1, GOBOARD2,
GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN5C, JORDAN9, JORDAN2C,
JORDAN18;
constructors REAL_1, FINSEQ_4, REALSET1, RFINSEQ, NAT_D, FINSEQ_5, GOBOARD2,
GRAPH_2, JORDAN3, JORDAN5C, SPRECT_1, JORDAN2C, JORDAN9, JORDAN18,
GOBOARD1, RELSET_1;
registrations RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_6,
STRUCT_0, GOBOARD2, SPPOL_2, SPRECT_1, REVROT_1, TOPREAL6, JORDAN1J,
ORDINAL1, CARD_1, EUCLID, SPRECT_5, ZFMISC_1, SUBSET_1;
requirements ARITHM, NUMERALS, BOOLE, SUBSET, REAL;
begin
reserve n for Nat;
theorem :: JORDAN23:1
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f holds len L_Cut(f,p) >= 1;
theorem :: JORDAN23:2
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 holds len R_Cut(f,p) >= 1;
theorem :: JORDAN23:3
for f be FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL 2
holds B_Cut (f,p,q) <> {};
registration
let x be set;
cluster <*x*> -> one-to-one;
end;
definition
let f be FinSequence;
attr f is almost-one-to-one means
:: JORDAN23:def 1
for i,j be Nat st i in
dom f & j in dom f & (i <> 1 or j <> len f) & (i <> len f or j <> 1) & f.i = f.
j holds i = j;
end;
definition
let f be FinSequence;
attr f is weakly-one-to-one means
:: JORDAN23:def 2
for i be Nat st 1 <= i & i < len f holds f.i <> f.(i+1);
end;
definition
let f be FinSequence;
attr f is poorly-one-to-one means
:: JORDAN23:def 3
for i be Nat st 1 <= i &
i < len f holds f.i <> f.(i+1) if len f <> 2 otherwise not contradiction;
end;
theorem :: JORDAN23:4
for D be set for f be FinSequence of D holds f is almost-one-to-one
iff for i,j be Nat st i in dom f & j in dom f & (i <> 1 or j <> len
f) & (i <> len f or j <> 1) & f/.i = f/.j holds i = j;
theorem :: JORDAN23:5
for D be set for f be FinSequence of D holds f is
weakly-one-to-one iff for i be Nat st 1 <= i & i < len f holds f/.i
<> f/.(i+1);
theorem :: JORDAN23:6
for D be set for f be FinSequence of D holds f is poorly-one-to-one
iff (len f <> 2 implies for i be Nat st 1 <= i & i < len f holds f/.
i <> f/.(i+1));
registration
cluster one-to-one -> almost-one-to-one for FinSequence;
end;
registration
cluster almost-one-to-one -> poorly-one-to-one for FinSequence;
end;
theorem :: JORDAN23:7
for f be FinSequence st len f <> 2 holds f is weakly-one-to-one
iff f is poorly-one-to-one;
registration
cluster empty -> weakly-one-to-one for FinSequence;
end;
registration
let x be set;
cluster <*x*> -> weakly-one-to-one;
end;
registration
let x,y be set;
cluster <*x,y*> -> poorly-one-to-one;
end;
registration
cluster weakly-one-to-one non empty for FinSequence;
end;
registration
let D be non empty set;
cluster weakly-one-to-one circular non empty for FinSequence of D;
end;
theorem :: JORDAN23:8
for f be FinSequence st f is almost-one-to-one holds Rev f is
almost-one-to-one;
theorem :: JORDAN23:9
for f be FinSequence st f is weakly-one-to-one holds Rev f is
weakly-one-to-one;
theorem :: JORDAN23:10
for f be FinSequence st f is poorly-one-to-one holds Rev f is
poorly-one-to-one;
registration
cluster one-to-one non empty for FinSequence;
end;
registration
let f be almost-one-to-one FinSequence;
cluster Rev f -> almost-one-to-one;
end;
registration
let f be weakly-one-to-one FinSequence;
cluster Rev f -> weakly-one-to-one;
end;
registration
let f be poorly-one-to-one FinSequence;
cluster Rev f -> poorly-one-to-one;
end;
theorem :: JORDAN23:11
for D be non empty set for f be FinSequence of D st f is
almost-one-to-one for p be Element of D holds Rotate(f,p) is almost-one-to-one;
theorem :: JORDAN23:12
for D be non empty set for f be FinSequence of D st f is
weakly-one-to-one circular for p be Element of D holds Rotate(f,p) is
weakly-one-to-one;
theorem :: JORDAN23:13
for D be non empty set for f be FinSequence of D st f is
poorly-one-to-one circular for p be Element of D holds Rotate(f,p) is
poorly-one-to-one;
registration
let D be non empty set;
cluster one-to-one circular non empty for FinSequence of D;
end;
registration
let D be non empty set;
let f be almost-one-to-one FinSequence of D;
let p be Element of D;
cluster Rotate(f,p) -> almost-one-to-one;
end;
registration
let D be non empty set;
let f be circular weakly-one-to-one FinSequence of D;
let p be Element of D;
cluster Rotate(f,p) -> weakly-one-to-one;
end;
registration
let D be non empty set;
let f be circular poorly-one-to-one FinSequence of D;
let p be Element of D;
cluster Rotate(f,p) -> poorly-one-to-one;
end;
theorem :: JORDAN23:14
for D be non empty set for f be FinSequence of D holds f is
almost-one-to-one iff f/^1 is one-to-one & f|(len f-'1) is one-to-one;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Cage(C,n) -> almost-one-to-one;
end;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Cage(C,n) -> weakly-one-to-one;
end;
theorem :: JORDAN23:15 :: JORDAN5B:24
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f & f is weakly-one-to-one holds B_Cut(f,p,p) = <*p*>;
theorem :: JORDAN23:16
for f being FinSequence st f is one-to-one holds f is weakly-one-to-one;
registration
cluster one-to-one -> weakly-one-to-one for FinSequence;
end;
theorem :: JORDAN23:17
for f be FinSequence of TOP-REAL 2 st f is weakly-one-to-one for
p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q) = Rev
B_Cut(f,q,p);
theorem :: JORDAN23:18
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
for i1 be Nat st f is poorly-one-to-one unfolded s.n.c. & 1 {}
holds g is constant;
theorem :: JORDAN23:27
for f be special FinSequence of TOP-REAL 2 for i,j be Nat
holds mid(f,i,j) is special;
theorem :: JORDAN23:28
for f be unfolded FinSequence of TOP-REAL 2 for i,j be Nat
holds mid(f,i,j) is unfolded;
theorem :: JORDAN23:29
for f be FinSequence of TOP-REAL 2 st f is special for p be
Point of TOP-REAL 2 st p in L~f holds L_Cut(f,p) is special;
theorem :: JORDAN23:30
for f be FinSequence of TOP-REAL 2 st f is special for p be
Point of TOP-REAL 2 st p in L~f holds R_Cut(f,p) is special;
theorem :: JORDAN23:31
for f be FinSequence of TOP-REAL 2 st f is special weakly-one-to-one
for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q) is
special;
theorem :: JORDAN23:32
for f be FinSequence of TOP-REAL 2 st f is unfolded for p be
Point of TOP-REAL 2 st p in L~f holds L_Cut(f,p) is unfolded;
theorem :: JORDAN23:33
for f be FinSequence of TOP-REAL 2 st f is unfolded for p be
Point of TOP-REAL 2 st p in L~f holds R_Cut(f,p) is unfolded;
theorem :: JORDAN23:34
for f be FinSequence of TOP-REAL 2 st f is unfolded weakly-one-to-one
for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q) is
unfolded;
theorem :: JORDAN23:35
for f,g be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL
2 st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.1 & g=mid
(f,1,Index(p,f))^<*p*> holds g is_S-Seq_joining f/.1,p;
theorem :: JORDAN23:36
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st f is poorly-one-to-one unfolded s.n.c. & p in L~f & p = f.(Index(p,f)+1) & p
<> f.len f holds Index(p,Rev f) + Index(p,f) + 1 = len f;
theorem :: JORDAN23:37
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is weakly-one-to-one & len f >= 2 holds L_Cut (f,f/.1) = f;
theorem :: JORDAN23:38
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is poorly-one-to-one unfolded s.n.c. & p in L~f & p <> f.len f
holds L_Cut(Rev f,p) = Rev R_Cut(f,p);
theorem :: JORDAN23:39
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.1 holds
R_Cut(f,p) is_S-Seq_joining f/.1,p;
theorem :: JORDAN23:40
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.
len f & p <> f.1 holds L_Cut(f,p) is_S-Seq_joining p,f/.len f;
theorem :: JORDAN23:41
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f
is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.1 holds R_Cut(f,
p) is being_S-Seq;
theorem :: JORDAN23:42
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p <>
f.len f & p <> f.1 holds L_Cut(f,p) is being_S-Seq;
theorem :: JORDAN23:43
for f be non empty FinSequence of TOP-REAL 2 for p,q be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & len f <> 2 & p
in L~f & q in L~f & p<>q & p <> f.1 & q <> f.1 holds B_Cut(f,p,q)
is_S-Seq_joining p,q;
theorem :: JORDAN23:44
for f be non empty FinSequence of TOP-REAL 2 for p,q be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & len f <> 2 & p
in L~f & q in L~f & p<>q & p <> f.1 & q <> f.1 holds B_Cut(f,p,q) is
being_S-Seq;
theorem :: JORDAN23:45
for C be compact non vertical non horizontal Subset of TOP-REAL 2 for
p,q be Point of TOP-REAL 2 st p in BDD L~Cage(C,n) ex B be S-Sequence_in_R2 st
B = B_Cut(Rotate(Cage(C,n),Cage(C,n)/.Index(South-Bound(p,L~Cage(C,n)), Cage(C,
n)))|(len Rotate(Cage(C,n),Cage(C,n)/. Index(South-Bound(p,L~Cage(C,n)), Cage(C
,n)))-'1),South-Bound(p,L~Cage(C,n)),North-Bound(p,L~Cage(C,n))) & ex P be
S-Sequence_in_R2 st P is_sequence_on GoB(B^'<*North-Bound(p,L~Cage(C,n)),
South-Bound(p,L~Cage(C,n))*>) & L~<*North-Bound(p,L~Cage(C,n)),South-Bound(p,L~
Cage(C,n))*> = L~P & P/.1 = North-Bound(p,L~Cage(C,n)) & P/.len P = South-Bound
(p,L~Cage(C,n)) & len P >= 2 & ex B1 be S-Sequence_in_R2 st B1 is_sequence_on
GoB(B^'<*North-Bound(p,L~Cage(C,n)),South-Bound(p,L~Cage(C,n))*>) & L~B = L~B1
& B/.1 = B1/.1 & B/.len B = B1/.len B1 & len B <= len B1 & ex g be non constant
standard special_circular_sequence st g = B1^'P;