:: 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 b₁ being FinSequence st b₁ is one-to-one holds
b₁ 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 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 ) by Def3;

registration

cluster V1() empty Function-like FinSequence-like -> weakly-one-to-one for set ;

coherence
for b₁ being FinSequence st b₁ is empty holds
b₁ 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 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 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 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 V1() V4( NAT ) non empty Function-like one-to-one V28() FinSequence-like FinSubsequence-like for 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 V1() V4( NAT ) V5(D) non empty Function-like one-to-one V28() FinSequence-like FinSubsequence-like circular for 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 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 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 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;