:: Subsequences of Almost, Weakly and Poorly One-to-one Finite Sequences
:: by Robert Milewski
::
:: Received February 1, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


theorem Th1: :: JORDAN23:1
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
len (L_Cut (f,p)) >= 1
proof end;

theorem :: JORDAN23:2
for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds len (R_Cut (f,p)) >= 1
proof end;

theorem Th3: :: JORDAN23:3
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) holds B_Cut (f,p,q) <> {}
proof end;

registration
let x be set ;
cluster <*x*> -> one-to-one ;
coherence
<*x*> is one-to-one by FINSEQ_3:93;
end;

definition
let f be FinSequence;
attr f is almost-one-to-one means :: JORDAN23:def 1
 for i, j being 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;

:: deftheorem defines almost-one-to-one JORDAN23:def 1 :
for f being FinSequence holds
( f is almost-one-to-one iff for i, j being 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 );

definition
let f be FinSequence;
attr f is weakly-one-to-one means :: JORDAN23:def 2
 for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1);
end;

:: deftheorem defines weakly-one-to-one JORDAN23:def 2 :
for f being FinSequence holds
( f is weakly-one-to-one iff for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1) );

definition
let f be FinSequence;
attr f is poorly-one-to-one means :Def3: :: JORDAN23:def 3
 for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1) if len f <> 2
otherwise verum;
consistency
verum ;
end;

:: deftheorem Def3 defines poorly-one-to-one JORDAN23:def 3 :
for f being FinSequence holds
( ( len f <> 2 implies ( f is poorly-one-to-one iff for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1) ) ) & ( not len f <> 2 implies ( f is poorly-one-to-one iff verum ) ) );

theorem :: JORDAN23:4
for D being set
for f being FinSequence of D holds
( f is almost-one-to-one iff for i, j being 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 )
proof end;

theorem Th5: :: JORDAN23:5
for D being set
for f being FinSequence of D holds
( f is weakly-one-to-one iff for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) )
proof end;

theorem :: JORDAN23:6
for D being set
for f being FinSequence of D holds
( f is poorly-one-to-one iff ( len f <> 2 implies for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) ) )
proof end;

registration
cluster V1() Function-like one-to-one FinSequence-like -> almost-one-to-one for set ;
coherence
for b1 being FinSequence st b1 is one-to-one holds
b1 is almost-one-to-one ;
end;

registration
cluster V1() Function-like FinSequence-like almost-one-to-one -> poorly-one-to-one for set ;
coherence
for b1 being FinSequence st b1 is almost-one-to-one holds
b1 is poorly-one-to-one
proof end;
end;

theorem Th7: :: JORDAN23:7
for f being FinSequence st len f <> 2 holds
( f is weakly-one-to-one iff f is poorly-one-to-one ) by Def3;

registration
cluster V1() empty Function-like FinSequence-like -> weakly-one-to-one for set ;
coherence
for b1 being FinSequence st b1 is empty holds
b1 is weakly-one-to-one ;
end;

registration
let x be set ;
cluster <*x*> -> weakly-one-to-one ;
coherence
<*x*> is weakly-one-to-one by FINSEQ_1:39;
end;

registration
let x, y be set ;
cluster <*x,y*> -> poorly-one-to-one ;
coherence
<*x,y*> is poorly-one-to-one
proof end;
end;

registration
cluster V1() V4( NAT ) non empty Function-like V28() FinSequence-like FinSubsequence-like weakly-one-to-one for set ;
existence
ex b1 being FinSequence st
( b1 is weakly-one-to-one & not b1 is empty )
proof end;
end;

registration
let D be non empty set ;
cluster V1() V4( NAT ) V5(D) non empty Function-like V28() FinSequence-like FinSubsequence-like circular weakly-one-to-one for FinSequence of D;
existence
ex b1 being FinSequence of D st
( b1 is weakly-one-to-one & b1 is circular & not b1 is empty )
proof end;
end;

theorem Th8: :: JORDAN23:8
for f being FinSequence st f is almost-one-to-one holds
Rev f is almost-one-to-one
proof end;

theorem Th9: :: JORDAN23:9
for f being FinSequence st f is weakly-one-to-one holds
Rev f is weakly-one-to-one
proof end;

theorem Th10: :: JORDAN23:10
for f being FinSequence st f is poorly-one-to-one holds
Rev f is poorly-one-to-one
proof end;

registration
cluster V1() V4( NAT ) non empty Function-like one-to-one V28() FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st
( b1 is one-to-one & not b1 is empty )
proof end;
end;

registration
let f be almost-one-to-one FinSequence;
cluster Rev f -> almost-one-to-one ;
coherence
Rev f is almost-one-to-one by Th8;
end;

registration
let f be weakly-one-to-one FinSequence;
cluster Rev f -> weakly-one-to-one ;
coherence
Rev f is weakly-one-to-one by Th9;
end;

registration
let f be poorly-one-to-one FinSequence;
cluster Rev f -> poorly-one-to-one ;
coherence
Rev f is poorly-one-to-one by Th10;
end;

theorem Th11: :: JORDAN23:11
for D being non empty set
for f being FinSequence of D st f is almost-one-to-one holds
for p being Element of D holds Rotate (f,p) is almost-one-to-one
proof end;

theorem Th12: :: JORDAN23:12
for D being non empty set
for f being FinSequence of D st f is weakly-one-to-one & f is circular holds
for p being Element of D holds Rotate (f,p) is weakly-one-to-one
proof end;

theorem Th13: :: JORDAN23:13
for D being non empty set
for f being FinSequence of D st f is poorly-one-to-one & f is circular holds
for p being Element of D holds Rotate (f,p) is poorly-one-to-one
proof end;

registration
let D be non empty set ;
cluster V1() V4( NAT ) V5(D) non empty Function-like one-to-one V28() FinSequence-like FinSubsequence-like circular for FinSequence of D;
existence
ex b1 being FinSequence of D st
( b1 is one-to-one & b1 is circular & not b1 is empty )
proof end;
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 ;
coherence
Rotate (f,p) is almost-one-to-one by Th11;
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 ;
coherence
Rotate (f,p) is weakly-one-to-one by Th12;
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 ;
coherence
Rotate (f,p) is poorly-one-to-one by Th13;
end;

theorem Th14: :: JORDAN23:14
for D being non empty set
for f being 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 ) )
proof end;

registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Cage (C,n) -> almost-one-to-one ;
coherence
Cage (C,n) is almost-one-to-one
proof end;
end;

registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Cage (C,n) -> weakly-one-to-one ;
coherence
Cage (C,n) is weakly-one-to-one
proof end;
end;

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

theorem Th16: :: JORDAN23:16
for f being FinSequence st f is one-to-one holds
f is weakly-one-to-one
proof end;

registration
cluster V1() Function-like one-to-one FinSequence-like -> weakly-one-to-one for set ;
coherence
for b1 being FinSequence st b1 is one-to-one holds
b1 is weakly-one-to-one by Th16;
end;

theorem Th17: :: JORDAN23:17
for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds
for p, q being 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))
proof end;

theorem Th18: :: JORDAN23:18
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for i1 being Nat st f is poorly-one-to-one & f is unfolded & f is s.n.c. & 1 < i1 & i1 <= len f & p = f . i1 holds
(Index (p,f)) + 1 = i1
proof end;

theorem Th19: :: JORDAN23:19
for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
(B_Cut (f,p,q)) /. 1 = p
proof end;

theorem Th20: :: JORDAN23:20
for f being FinSequence of (TOP-REAL 2) st f is weakly-one-to-one holds
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
(B_Cut (f,p,q)) /. (len (B_Cut (f,p,q))) = q
proof end;

theorem :: JORDAN23:21
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
L~ (L_Cut (f,p)) c= L~ f
proof end;

theorem :: JORDAN23: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 & f is weakly-one-to-one holds
L~ (B_Cut (f,p,q)) c= L~ f
proof end;

theorem Th23: :: JORDAN23:23
for f, g being FinSequence holds dom f c= dom (f ^' g)
proof end;

theorem :: JORDAN23:24
for f being non empty FinSequence
for g being FinSequence holds dom g c= dom (f ^' g)
proof end;

theorem Th25: :: JORDAN23:25
for f, g being FinSequence st f ^' g is constant holds
f is constant
proof end;

theorem :: JORDAN23:26
for f, g being FinSequence st f ^' g is constant & f . (len f) = g . 1 & f <> {} holds
g is constant
proof end;

theorem Th27: :: JORDAN23:27
for f being special FinSequence of (TOP-REAL 2)
for i, j being Nat holds mid (f,i,j) is special
proof end;

theorem Th28: :: JORDAN23:28
for f being unfolded FinSequence of (TOP-REAL 2)
for i, j being Nat holds mid (f,i,j) is unfolded
proof end;

theorem Th29: :: JORDAN23:29
for f being FinSequence of (TOP-REAL 2) st f is special holds
for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) is special
proof end;

theorem Th30: :: JORDAN23:30
for f being FinSequence of (TOP-REAL 2) st f is special holds
for p being Point of (TOP-REAL 2) st p in L~ f holds
R_Cut (f,p) is special
proof end;

theorem :: JORDAN23:31
for f being FinSequence of (TOP-REAL 2) st f is special & f is weakly-one-to-one holds
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
B_Cut (f,p,q) is special
proof end;

theorem Th32: :: JORDAN23:32
for f being FinSequence of (TOP-REAL 2) st f is unfolded holds
for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) is unfolded
proof end;

theorem Th33: :: JORDAN23:33
for f being FinSequence of (TOP-REAL 2) st f is unfolded holds
for p being Point of (TOP-REAL 2) st p in L~ f holds
R_Cut (f,p) is unfolded
proof end;

theorem :: JORDAN23:34
for f being FinSequence of (TOP-REAL 2) st f is unfolded & f is weakly-one-to-one holds
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f holds
B_Cut (f,p,q) is unfolded
proof end;

theorem Th35: :: JORDAN23:35
for f, g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is 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
proof end;

theorem Th36: :: JORDAN23:36
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is 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
proof end;

theorem :: JORDAN23:37
for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is weakly-one-to-one & len f >= 2 holds
L_Cut (f,(f /. 1)) = f
proof end;

theorem Th38: :: JORDAN23:38
for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is poorly-one-to-one & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) holds
L_Cut ((Rev f),p) = Rev (R_Cut (f,p))
proof end;

theorem Th39: :: JORDAN23:39
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds
R_Cut (f,p) is_S-Seq_joining f /. 1,p
proof end;

theorem Th40: :: JORDAN23:40
for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is 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)
proof end;

theorem :: JORDAN23:41
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . 1 holds
R_Cut (f,p) is being_S-Seq
proof end;

theorem Th42: :: JORDAN23:42
for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & p <> f . (len f) & p <> f . 1 holds
L_Cut (f,p) is being_S-Seq
proof end;

Lm1: for f being non empty FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is s.n.c. & p in L~ f & q in L~ f & p <> q & p <> f . 1 & ( 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) ) ) holds
B_Cut (f,p,q) is_S-Seq_joining p,q
proof end;

theorem Th43: :: JORDAN23:43
for f being non empty FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is 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
proof end;

theorem :: JORDAN23:44
for f being non empty FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is almost-one-to-one & f is special & f is unfolded & f is 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
proof end;

theorem :: JORDAN23:45
for n being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in BDD (L~ (Cage (C,n))) holds
ex B being 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 being 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 being 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 being V22() standard special_circular_sequence st g = B1 ^' P ) ) )
proof end;