begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
begin
:: deftheorem JORDAN3:def 1 :
canceled;
:: deftheorem Def2 defines Index JORDAN3:def 2 :
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
:: deftheorem Def3 defines is_S-Seq_joining JORDAN3:def 3 :
theorem Th48:
theorem Th49:
theorem
theorem Th51:
theorem Th52:
begin
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:
<*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:
(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:
theorem Th54:
theorem
canceled;
theorem
canceled;
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem Th61:
:: 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
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:
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:
theorem Th65:
theorem Th66:
begin
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:
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:
theorem Th68:
theorem Th69:
theorem Th70:
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:
theorem
theorem Th73:
theorem Th74:
theorem
theorem Th76:
Lm2:
for i being Element of NAT
for D being non empty set holds (<*> D) | i = <*> D
Lm3:
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 )
Lm4:
for D being non empty set
for f1 being FinSequence of D holds mid f1,0 ,0 = f1 | 1
Lm5:
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
Lm6:
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)
Lm7:
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
Lm8:
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
Lm9:
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
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
(mid f,i,j) /. 1 = f /. i
theorem Th77:
theorem Th78:
theorem
theorem Th80:
theorem Th81:
theorem Th82:
theorem