:: 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
theorem Th1: :: JORDAN23:1
theorem :: JORDAN23:2
theorem Th3: :: JORDAN23:3
:: deftheorem Def1 defines almost-one-to-one JORDAN23:def 1 :
:: deftheorem Def2 defines weakly-one-to-one JORDAN23:def 2 :
:: deftheorem Def3 defines poorly-one-to-one JORDAN23:def 3 :
theorem :: JORDAN23:4
theorem Th5: :: JORDAN23:5
theorem :: JORDAN23:6
theorem Th7: :: JORDAN23:7
theorem Th8: :: JORDAN23:8
theorem Th9: :: JORDAN23:9
theorem Th10: :: JORDAN23:10
theorem Th11: :: JORDAN23:11
theorem Th12: :: JORDAN23:12
theorem Th13: :: JORDAN23:13
theorem Th14: :: JORDAN23:14
theorem Th15: :: JORDAN23:15
theorem Th16: :: JORDAN23:16
theorem Th17: :: JORDAN23:17
theorem Th18: :: JORDAN23:18
theorem Th19: :: JORDAN23:19
theorem Th20: :: JORDAN23:20
theorem :: JORDAN23:21
theorem :: JORDAN23:22
theorem Th23: :: JORDAN23:23
theorem :: JORDAN23:24
theorem Th25: :: JORDAN23:25
theorem :: JORDAN23:26
theorem Th27: :: JORDAN23:27
theorem Th28: :: JORDAN23:28
theorem Th29: :: JORDAN23:29
theorem Th30: :: JORDAN23:30
theorem :: JORDAN23:31
theorem Th32: :: JORDAN23:32
theorem Th33: :: JORDAN23:33
theorem :: JORDAN23:34
theorem Th35: :: JORDAN23:35
theorem Th36: :: JORDAN23:36
theorem :: JORDAN23:37
theorem Th38: :: JORDAN23:38
theorem Th39: :: JORDAN23:39
theorem Th40: :: JORDAN23:40
theorem :: JORDAN23:41
theorem Th42: :: JORDAN23:42
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
theorem Th43: :: JORDAN23:43
theorem :: JORDAN23:44
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 ) ) )