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

begin

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:102;

end;

definition

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

for f being FinSequence holds
( f is almost-one-to-one iff for i, j being Element of 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 :Def2: :: JORDAN23:def 2
for i being Element of NAT st 1 <= i & i < len f holds
f . i <> f . (i + 1);

end;

:: deftheorem Def2 defines weakly-one-to-one JORDAN23:def 2 :

for f being FinSequence holds
( f is weakly-one-to-one iff for i being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) ) )

proof end;

registration

cluster one-to-one -> almost-one-to-one set ;
coherence
for b₁ being FinSequence st b₁ is one-to-one holds
b₁ is almost-one-to-one

proof end;

end;

registration

cluster almost-one-to-one -> poorly-one-to-one set ;
coherence
for b₁ being FinSequence st b₁ is almost-one-to-one holds
b₁ 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 )

proof end;

registration

cluster empty -> weakly-one-to-one set ;
coherence
for b₁ being FinSequence st b₁ is empty holds
b₁ is weakly-one-to-one

proof end;

end;

registration

let x be set ;
cluster <*x*> -> weakly-one-to-one ;
coherence
<*x*> is weakly-one-to-one

proof end;

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 non empty weakly-one-to-one set ;
existence
ex b₁ being FinSequence st
( b₁ is weakly-one-to-one & not b₁ is empty )

proof end;

end;

registration

let D be non empty set ;
cluster non empty circular weakly-one-to-one FinSequence of D;
existence
ex b₁ being FinSequence of D st
( b₁ is weakly-one-to-one & b₁ is circular & not b₁ 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 one-to-one non empty set ;
existence
ex b₁ being FinSequence st
( b₁ is one-to-one & not b₁ 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 one-to-one non empty circular FinSequence of D;
existence
ex b₁ being FinSequence of D st
( b₁ is one-to-one & b₁ is circular & not b₁ 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 Element of 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 Element of 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 one-to-one -> weakly-one-to-one set ;
coherence
for b₁ being FinSequence st b₁ is one-to-one holds
b₁ 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 Element of 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 Element of 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 Element of 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 Element of 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 non constant standard special_circular_sequence st g = B1 ^' P ) ) )

proof end;