begin
begin
begin
definition
let f be
FinSequence of
(TOP-REAL 2);
let p be
Point of
(TOP-REAL 2);
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;
;
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 Def3 defines
L_Cut JORDAN3:def 3 :
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)) ) );
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 Th28:
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 ) )
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 :
Def7:
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 Def7 defines
B_Cut JORDAN3:def 7 :
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)) ) );
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
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
:: A Concept of Index for Finite Sequences in TOP-REAL 2 :
::---------------------------------------------------------: