:: by Robert Milewski

::

:: Received February 1, 2005

:: Copyright (c) 2005-2016 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

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

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) <> {}

for p, q being Point of (TOP-REAL 2) holds B_Cut (f,p,q) <> {}

proof end;

registration
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 );

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 );

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

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;

verum ;

end;
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 for i being Nat st 1 <= i & i < len f holds

f . i <> f . (i + 1) if len f <> 2

otherwise verum;

verum ;

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

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 )

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) )

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) ) )

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
end;

registration

coherence

for b_{1} being FinSequence st b_{1} is almost-one-to-one holds

b_{1} is poorly-one-to-one

end;
for b

b

proof 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;

( f is weakly-one-to-one iff f is poorly-one-to-one ) by Def3;

registration
end;

registration

ex b_{1} being FinSequence st

( b_{1} is weakly-one-to-one & not b_{1} is empty )
end;

cluster V1() V4( NAT ) non empty Function-like V28() FinSequence-like FinSubsequence-like weakly-one-to-one for set ;

existence ex b

( b

proof end;

registration

let D be non empty set ;

ex b_{1} being FinSequence of D st

( b_{1} is weakly-one-to-one & b_{1} is circular & not b_{1} is empty )

end;
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

( b

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is one-to-one & not b_{1} is empty )
end;

cluster V1() V4( NAT ) non empty Function-like one-to-one V28() FinSequence-like FinSubsequence-like for set ;

existence ex b

( b

proof end;

registration
end;

registration
end;

registration
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

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

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

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 ;

ex b_{1} being FinSequence of D st

( b_{1} is one-to-one & b_{1} is circular & not b_{1} is empty )

end;
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

( b

proof end;

registration

let D be non empty set ;

let f be almost-one-to-one FinSequence of D;

let p be Element of D;

coherence

Rotate (f,p) is almost-one-to-one by Th11;

end;
let f be almost-one-to-one FinSequence of D;

let p be Element of D;

coherence

Rotate (f,p) is almost-one-to-one by Th11;

registration

let D be non empty set ;

let f be circular weakly-one-to-one FinSequence of D;

let p be Element of D;

coherence

Rotate (f,p) is weakly-one-to-one by Th12;

end;
let f be circular weakly-one-to-one FinSequence of D;

let p be Element of D;

coherence

Rotate (f,p) is weakly-one-to-one by Th12;

registration

let D be non empty set ;

let f be circular poorly-one-to-one FinSequence of D;

let p be Element of D;

coherence

Rotate (f,p) is poorly-one-to-one by Th13;

end;
let f be circular poorly-one-to-one FinSequence of D;

let p be Element of D;

coherence

Rotate (f,p) is poorly-one-to-one by Th13;

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 ) )

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;

coherence

Cage (C,n) is almost-one-to-one

end;
let n be Nat;

coherence

Cage (C,n) is almost-one-to-one

proof end;

registration

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);

let n be Nat;

coherence

Cage (C,n) is weakly-one-to-one

end;
let n be Nat;

coherence

Cage (C,n) is weakly-one-to-one

proof 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*>

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;

registration

coherence

for b_{1} being FinSequence st b_{1} is one-to-one holds

b_{1} is weakly-one-to-one
by Th16;

end;
for b

b

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))

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

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

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

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

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

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 :: JORDAN23:26

for f, g being FinSequence st f ^' g is constant & f . (len f) = g . 1 & f <> {} holds

g is constant

g is constant

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

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

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

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

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

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

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

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

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

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))

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

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)

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

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

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

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

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 non constant standard special_circular_sequence st g = B1 ^' P ) ) )

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;