:: Reconstructions of Special Sequences
:: by Yatsuka Nakamura and Roman Matuszewski
::
:: Received December 10, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: JORDAN3:1
canceled;
theorem :: JORDAN3:2
canceled;
theorem :: JORDAN3:3
canceled;
theorem :: JORDAN3:4
canceled;
theorem :: JORDAN3:5
canceled;
theorem :: JORDAN3:6
canceled;
theorem :: JORDAN3:7
canceled;
theorem :: JORDAN3:8
canceled;
theorem :: JORDAN3:9
canceled;
theorem :: JORDAN3:10
canceled;
theorem :: JORDAN3:11
canceled;
theorem :: JORDAN3:12
canceled;
theorem :: JORDAN3:13
canceled;
theorem :: JORDAN3:14
canceled;
theorem Th15: :: JORDAN3:15
theorem :: JORDAN3:16
canceled;
theorem Th17: :: JORDAN3:17
theorem Th18: :: JORDAN3:18
theorem :: JORDAN3:19
theorem :: JORDAN3:20
canceled;
theorem :: JORDAN3:21
:: deftheorem Def1 defines mid JORDAN3:def 1 :
theorem Th22: :: JORDAN3:22
theorem Th23: :: JORDAN3:23
theorem Th24: :: JORDAN3:24
theorem :: JORDAN3:25
theorem Th26: :: JORDAN3:26
theorem Th27: :: JORDAN3:27
for
D being non
empty set for
f being
FinSequence of
D for
k1,
k2 being
Element of
NAT st 1
<= k1 &
k1 <= len f & 1
<= k2 &
k2 <= len f holds
(
(mid f,k1,k2) . 1
= f . k1 & (
k1 <= k2 implies (
len (mid f,k1,k2) = (k2 -' k1) + 1 & ( for
i being
Element of
NAT st 1
<= i &
i <= len (mid f,k1,k2) holds
(mid f,k1,k2) . i = f . ((i + k1) -' 1) ) ) ) & (
k1 > k2 implies (
len (mid f,k1,k2) = (k1 -' k2) + 1 & ( for
i being
Element of
NAT st 1
<= i &
i <= len (mid f,k1,k2) holds
(mid f,k1,k2) . i = f . ((k1 -' i) + 1) ) ) ) )
theorem Th28: :: JORDAN3:28
theorem :: JORDAN3:29
theorem :: JORDAN3:30
theorem Th31: :: JORDAN3:31
for
D being non
empty set for
f being
FinSequence of
D for
k1,
k2,
i being
Element of
NAT st 1
<= k1 &
k1 <= k2 &
k2 <= len f & 1
<= i & (
i <= (k2 -' k1) + 1 or
i <= (k2 - k1) + 1 or
i <= (k2 + 1) - k1 ) holds
(
(mid f,k1,k2) . i = f . ((i + k1) -' 1) &
(mid f,k1,k2) . i = f . ((i -' 1) + k1) &
(mid f,k1,k2) . i = f . ((i + k1) - 1) &
(mid f,k1,k2) . i = f . ((i - 1) + k1) )
theorem Th32: :: JORDAN3:32
theorem :: JORDAN3:33
theorem :: JORDAN3:34
theorem Th35: :: JORDAN3:35
theorem Th36: :: JORDAN3:36
theorem Th37: :: JORDAN3:37
theorem Th38: :: JORDAN3:38
theorem :: JORDAN3:39
:: deftheorem Def2 defines Index JORDAN3:def 2 :
theorem Th40: :: JORDAN3:40
theorem Th41: :: JORDAN3:41
theorem Th42: :: JORDAN3:42
theorem Th43: :: JORDAN3:43
theorem Th44: :: JORDAN3:44
theorem Th45: :: JORDAN3:45
theorem Th46: :: JORDAN3:46
theorem Th47: :: JORDAN3:47
:: deftheorem Def3 defines is_S-Seq_joining JORDAN3:def 3 :
theorem Th48: :: JORDAN3:48
theorem Th49: :: JORDAN3:49
theorem :: JORDAN3:50
theorem Th51: :: JORDAN3:51
theorem Th52: :: JORDAN3:52
definition
let f be
FinSequence of
(TOP-REAL 2);
let p be
Point of
(TOP-REAL 2);
func L_Cut f,
p -> FinSequence of
(TOP-REAL 2) equals :
Def4:
:: JORDAN3:def 4
<*p*> ^ (mid f,((Index p,f) + 1),(len f)) if p <> f . ((Index p,f) + 1) otherwise mid f,
((Index p,f) + 1),
(len f);
correctness
coherence
( ( p <> f . ((Index p,f) + 1) implies <*p*> ^ (mid f,((Index p,f) + 1),(len f)) is FinSequence of (TOP-REAL 2) ) & ( not p <> f . ((Index p,f) + 1) implies mid f,((Index p,f) + 1),(len f) is FinSequence of (TOP-REAL 2) ) );
consistency
for b1 being FinSequence of (TOP-REAL 2) holds verum;
;
func R_Cut f,
p -> FinSequence of
(TOP-REAL 2) equals :
Def5:
:: JORDAN3:def 5
(mid f,1,(Index p,f)) ^ <*p*> if p <> f . 1
otherwise <*p*>;
correctness
coherence
( ( p <> f . 1 implies (mid f,1,(Index p,f)) ^ <*p*> is FinSequence of (TOP-REAL 2) ) & ( not p <> f . 1 implies <*p*> is FinSequence of (TOP-REAL 2) ) );
consistency
for b1 being FinSequence of (TOP-REAL 2) holds verum;
;
end;
:: deftheorem Def4 defines L_Cut JORDAN3:def 4 :
for
f being
FinSequence of
(TOP-REAL 2) for
p being
Point of
(TOP-REAL 2) holds
( (
p <> f . ((Index p,f) + 1) implies
L_Cut f,
p = <*p*> ^ (mid f,((Index p,f) + 1),(len f)) ) & ( not
p <> f . ((Index p,f) + 1) implies
L_Cut f,
p = mid f,
((Index p,f) + 1),
(len f) ) );
:: deftheorem Def5 defines R_Cut JORDAN3:def 5 :
theorem Th53: :: JORDAN3:53
theorem Th54: :: JORDAN3:54
theorem Th55: :: JORDAN3:55
theorem Th56: :: JORDAN3:56
theorem Th57: :: JORDAN3:57
theorem Th58: :: JORDAN3:58
theorem Th59: :: JORDAN3:59
theorem :: JORDAN3:60
theorem Th61: :: JORDAN3:61
:: deftheorem Def6 defines LE JORDAN3:def 6 :
for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) holds
(
LE q1,
q2,
p1,
p2 iff (
q1 in LSeg p1,
p2 &
q2 in LSeg p1,
p2 & ( for
r1,
r2 being
Real st
0 <= r1 &
r1 <= 1 &
q1 = ((1 - r1) * p1) + (r1 * p2) &
0 <= r2 &
r2 <= 1 &
q2 = ((1 - r2) * p1) + (r2 * p2) holds
r1 <= r2 ) ) );
:: deftheorem Def7 defines LT JORDAN3:def 7 :
for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) holds
(
LT q1,
q2,
p1,
p2 iff (
LE q1,
q2,
p1,
p2 &
q1 <> q2 ) );
theorem :: JORDAN3:62
for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
LE q1,
q2,
p1,
p2 &
LE q2,
q1,
p1,
p2 holds
q1 = q2
theorem Th63: :: JORDAN3:63
for
p1,
p2,
q1,
q2 being
Point of
(TOP-REAL 2) st
q1 in LSeg p1,
p2 &
q2 in LSeg p1,
p2 &
p1 <> p2 holds
( (
LE q1,
q2,
p1,
p2 or
LT q2,
q1,
p1,
p2 ) & ( not
LE q1,
q2,
p1,
p2 or not
LT q2,
q1,
p1,
p2 ) )
theorem Th64: :: JORDAN3:64
theorem Th65: :: JORDAN3:65
theorem Th66: :: JORDAN3:66
definition
let f be
FinSequence of
(TOP-REAL 2);
let p,
q be
Point of
(TOP-REAL 2);
func B_Cut f,
p,
q -> FinSequence of
(TOP-REAL 2) equals :
Def8:
:: JORDAN3:def 8
R_Cut (L_Cut f,p),
q if ( (
p in L~ f &
q in L~ f &
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) ) )
otherwise Rev (R_Cut (L_Cut f,q),p);
correctness
coherence
( ( ( ( p in L~ f & q in L~ f & 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) ) ) implies R_Cut (L_Cut f,p),q is FinSequence of (TOP-REAL 2) ) & ( ( p in L~ f & q in L~ f & 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) ) or Rev (R_Cut (L_Cut f,q),p) is FinSequence of (TOP-REAL 2) ) );
consistency
for b1 being FinSequence of (TOP-REAL 2) holds verum;
;
end;
:: deftheorem Def8 defines B_Cut JORDAN3:def 8 :
for
f being
FinSequence of
(TOP-REAL 2) for
p,
q being
Point of
(TOP-REAL 2) holds
( ( ( (
p in L~ f &
q in L~ f &
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) ) ) implies
B_Cut f,
p,
q = R_Cut (L_Cut f,p),
q ) & ( (
p in L~ f &
q in L~ f &
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) ) or
B_Cut f,
p,
q = Rev (R_Cut (L_Cut f,q),p) ) );
theorem Th67: :: JORDAN3:67
theorem Th68: :: JORDAN3:68
theorem Th69: :: JORDAN3:69
theorem Th70: :: JORDAN3:70
Lm1:
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & p <> q & ( 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 Th71: :: JORDAN3:71
theorem :: JORDAN3:72
theorem Th73: :: JORDAN3:73
theorem Th74: :: JORDAN3:74
theorem :: JORDAN3:75
theorem Th76: :: JORDAN3:76
Lm2:
for k being Nat
for i, j being Element of NAT st i <= j holds
(j + k) -' i = (j + k) - i
by NAT_1:12, XREAL_1:235;
Lm3:
for i being Element of NAT
for D being non empty set holds (<*> D) | i = <*> D
Lm5:
for D being non empty set
for f1 being FinSequence of D
for k being Element of NAT st 1 <= k & k <= len f1 holds
( mid f1,k,k = <*(f1 /. k)*> & len (mid f1,k,k) = 1 )
Lm6:
for D being non empty set
for f1 being FinSequence of D holds mid f1,0 ,0 = f1 | 1
Lm7:
for D being non empty set
for f1 being FinSequence of D
for k being Element of NAT st len f1 < k holds
mid f1,k,k = <*> D
Lm8:
for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Element of NAT holds mid f1,i1,i2 = Rev (mid f1,i2,i1)
Lm9:
for h being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st 1 <= i1 & i1 <= len h & 1 <= i2 & i2 <= len h holds
L~ (mid h,i1,i2) c= L~ h
Lm10:
for i, j being Element of NAT
for D being non empty set
for f being FinSequence of D st i in dom f & j in dom f holds
len (mid f,i,j) >= 1
Lm11:
for i, j being Element of NAT
for D being non empty set
for f being FinSequence of D st i in dom f & j in dom f holds
not mid f,i,j is empty
Lm12:
for i, j being Element of NAT
for D being non empty set
for f being FinSequence of D st i in dom f & j in dom f holds
(mid f,i,j) /. 1 = f /. i
theorem Th77: :: JORDAN3:77
theorem Th78: :: JORDAN3:78
theorem :: JORDAN3:79
theorem Th80: :: JORDAN3:80
theorem Th81: :: JORDAN3:81
theorem Th82: :: JORDAN3:82
theorem :: JORDAN3:83