Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Yatsuka Nakamura,
- Roman Matuszewski,
and
- Adam Grabowski
- Received May 12, 1997
- MML identifier: JORDAN4
- [
Mizar article,
MML identifier index
]
environ
vocabulary ARYTM_1, NAT_1, RELAT_1, ARYTM_3, FINSEQ_1, FINSEQ_6, FUNCT_1,
FINSEQ_5, RFINSEQ, EUCLID, TOPREAL1, JORDAN3, SEQM_3, GOBOARD5, TARSKI,
BOOLE, PRE_TOPC, TOPREAL4, TOPREAL2, MCART_1, JORDAN4, FINSEQ_4;
notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, BINARITH, RELAT_1,
FINSEQ_1, FUNCT_1, FINSEQ_4, FINSEQ_5, STRUCT_0, TOPREAL1, TOPREAL2,
TOPREAL4, GOBOARD1, GOBOARD5, PRE_TOPC, EUCLID, FINSEQ_6, RFINSEQ,
JORDAN3;
constructors GOBOARD9, BINARITH, TOPREAL4, TOPREAL2, REAL_1, RFINSEQ, JORDAN3,
FINSEQ_4, MEMBERED;
clusters STRUCT_0, GOBOARD5, RELSET_1, EUCLID, SPPOL_2, XREAL_0, ARYTM_3,
MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve i, i1, i2, i3, j, k, n for Nat,
r, r1, r2, s, s1 for Real;
theorem :: JORDAN4:1
n-'i=0 implies n<=i;
theorem :: JORDAN4:2
i<=j implies j+k-'i=j+k-i;
theorem :: JORDAN4:3
i<=j implies j+k-'i=j-'i+k;
theorem :: JORDAN4:4
i1<>0 & i2=i3*i1 implies i3<=i2;
theorem :: JORDAN4:5
i1<i2 implies i1 div i2=0;
theorem :: JORDAN4:6
0<j & j<i & i<j+j implies i mod j<>0;
theorem :: JORDAN4:7
0<j & j<=i & i<j+j implies i mod j=i-j & i mod j=i-'j;
theorem :: JORDAN4:8
(j+j)mod j=0;
theorem :: JORDAN4:9
0<k & k<=j & k mod j=0 implies k=j;
begin :: Some facts about cutting of finite sequences
reserve D for non empty set,
f1 for FinSequence of D;
canceled 4;
theorem :: JORDAN4:14
for f1 st f1 is circular & 1<=len f1 holds f1.1=f1.len f1;
theorem :: JORDAN4:15
for f1,i1,i2 st i1<=i2 holds
(f1|i1)|i2=f1|i1 & (f1|i2)|i1=f1|i1;
theorem :: JORDAN4:16
(<*>D)|i=<*>D;
theorem :: JORDAN4:17
Rev (<*>D)=<*>D;
theorem :: JORDAN4:18
for f1,k st k<len f1 holds
(f1/^k).len (f1/^k)=f1.len f1 & (f1/^k)/.len (f1/^k)=f1/.len f1;
theorem :: JORDAN4:19
for g being FinSequence of TOP-REAL 2,i
st g is_S-Seq & i+1<len g holds g/^i is_S-Seq;
theorem :: JORDAN4:20
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1
holds len mid(f1,i2,i1)=i1-'i2+1;
theorem :: JORDAN4:21
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1
holds len mid(f1,i1,i2)=i1-'i2+1;
theorem :: JORDAN4:22
for f1,i1,i2,j st 1<=i1 & i1<=i2 & i2<=len f1
holds mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2;
theorem :: JORDAN4:23
for f1,i1,i2,j st 1<=i1 & i1<=len f1 & 1<=i2 & i2<=len f1
holds mid(f1,i1,i2).(len mid(f1,i1,i2))=f1.i2;
theorem :: JORDAN4:24
for f1,i1,i2,j st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j
& j<=i1-'i2+1 holds mid(f1,i1,i2).j=f1.(i1-'j+1);
theorem :: JORDAN4:25
for f1,i1,i2 st 1<=i2 & i2<=i1 & i1<=len f1 & 1<=j & j<=i1-'i2+1
holds mid(f1,i1,i2).j=mid(f1,i2,i1).(i1-i2+1-j+1)
& i1-i2+1-j+1=i1-'i2+1-'j+1;
theorem :: JORDAN4:26
for f1,i1,i2 st 1<=i1 & i1<=i2 & i2<=len f1 & 1<=j & j<=i2-'i1+1
holds mid(f1,i1,i2).j=mid(f1,i2,i1).(i2-i1+1-j+1)
& i2-i1+1-j+1=i2-'i1+1-'j+1;
theorem :: JORDAN4:27
for f1,k st 1<=k & k<=len f1
holds mid(f1,k,k)=<*f1/.k*> & len mid(f1,k,k)=1;
theorem :: JORDAN4:28
mid(f1,0,0)=f1|1;
theorem :: JORDAN4:29
for f1,k st len f1<k
holds mid(f1,k,k)=<*>D;
theorem :: JORDAN4:30
for f1,i1,i2 holds mid(f1,i1,i2)=Rev mid(f1,i2,i1);
theorem :: JORDAN4:31
for f being FinSequence of TOP-REAL 2,i1,i2,i
st 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1
holds LSeg(mid(f,i1,i2),i)=LSeg(f,i+i1-'1);
theorem :: JORDAN4:32
for f being FinSequence of TOP-REAL 2,i1,i2,i
st 1<=i1 & i1<i2 & i2<=len f & 1<=i & i<i2-'i1+1
holds LSeg(mid(f,i2,i1),i)=LSeg(f,i2-'i);
begin :: Dividing of special circular sequences into parts
definition let n be Nat, f be FinSequence;
func S_Drop(n,f) -> Nat equals
:: JORDAN4:def 1
(n mod (len f -'1)) if n mod (len f -'1)<>0
otherwise len f -'1;
end;
theorem :: JORDAN4:33
for f being FinSequence holds S_Drop(len f-'1,f)=len f-'1;
theorem :: JORDAN4:34
for n being Nat, f being FinSequence
st 1<=n & n<=len f-'1 holds S_Drop(n,f)=n;
theorem :: JORDAN4:35
for n being Nat,f being FinSequence holds
S_Drop(n,f)=S_Drop(n+(len f-'1),f) &
S_Drop(n,f)=S_Drop(len f-'1+n,f);
definition let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part>_of f,i1,i2 means
:: JORDAN4:def 2
1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f));
end;
definition let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part<_of f,i1,i2 means
:: JORDAN4:def 3
1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f));
end;
definition let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL 2,i1,i2 be Nat;
pred g is_a_part_of f,i1,i2 means
:: JORDAN4:def 4
g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2;
end;
theorem :: JORDAN4:36
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part_of f,i1,i2 holds
1<=i1 & i1+1<=len f &
1<=i2 & i2+1<=len f & g.len g=f.i2 & 1<=len g & len g<len f &
((for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop((i1+i)-'1,f))or
(for i being Nat st 1<=i & i<=len g holds g.i=f.S_Drop(len f +i1-'i,f)));
theorem :: JORDAN4:37
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1<=i2 holds len g=i2-'i1+1 & g=mid(f,i1,i2);
theorem :: JORDAN4:38
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1>i2 holds len g=len f+i2-'i1
& g=mid(f,i1,len f-'1)^(f|i2)
& g=mid(f,i1,len f-'1)^mid(f,1,i2);
theorem :: JORDAN4:39
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1>=i2 holds len g=i1-'i2+1 & g=mid(f,i1,i2);
theorem :: JORDAN4:40
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1<i2 holds len g=len f+i1-'i2
& g=mid(f,i1,1)^mid(f,len f-'1,i2);
theorem :: JORDAN4:41
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 holds Rev g is_a_part<_of f,i2,i1;
theorem :: JORDAN4:42
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 holds Rev g is_a_part>_of f,i2,i1;
theorem :: JORDAN4:43
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<=i2 & i2<len f
holds mid(f,i1,i2) is_a_part>_of f,i1,i2;
theorem :: JORDAN4:44
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<=i2 & i2<len f
holds mid(f,i2,i1) is_a_part<_of f,i2,i1;
theorem :: JORDAN4:45
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i2 & i1>i2 & i1<len f
holds mid(f,i1,len f-'1)^mid(f,1,i2) is_a_part>_of f,i1,i2;
theorem :: JORDAN4:46
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st 1<=i1 & i1<i2 & i2<len f
holds mid(f,i1,1)^mid(f,len f-'1,i2) is_a_part<_of f,i1,i2;
theorem :: JORDAN4:47
for h being FinSequence of TOP-REAL 2,i1,i2 st
1<=i1 & i1<=len h & 1<=i2 & i2<=len h holds L~mid(h,i1,i2) c= L~h;
theorem :: JORDAN4:48
for g being FinSequence of D holds
g is one-to-one iff for i1,i2 st 1<=i1 & i1<=len g & 1<=i2 & i2<=len g &
(g.i1=g.i2 or g/.i1=g/.i2) holds i1=i2;
theorem :: JORDAN4:49
for f being non constant standard special_circular_sequence,
i2 st 1<i2 & i2+1<=len f holds f|i2 is_S-Seq;
theorem :: JORDAN4:50
for f being non constant standard special_circular_sequence,
i2 st 1<=i2 & i2+1<len f holds f/^i2 is_S-Seq;
theorem :: JORDAN4:51
for f being non constant standard special_circular_sequence,
i1,i2 st 1<=i1 & i1<i2 & i2+1<=len f holds mid(f,i1,i2) is_S-Seq;
theorem :: JORDAN4:52
for f being non constant standard special_circular_sequence,
i1,i2 st 1<i1 & i1<i2 & i2<=len f holds mid(f,i1,i2) is_S-Seq;
theorem :: JORDAN4:53
for p0,p,q1,q2 being Point of TOP-REAL 2 st
p0 in LSeg(p,q1) & p0 in LSeg(p,q2) & p<>p0 holds
q1 in LSeg(p,q2) or q2 in LSeg(p,q1);
theorem :: JORDAN4:54
for f being non constant standard special_circular_sequence
holds LSeg(f,1)/\ LSeg(f,len f-'1)={f.1};
theorem :: JORDAN4:55
for f being non constant standard special_circular_sequence,
i1,i2 being Nat,g1,g2 being FinSequence of TOP-REAL 2
st 1<=i1 & i1<i2 & i2<len f & g1=mid(f,i1,i2)
& g2=mid(f,i1,1)^mid(f,len f-'1,i2)
holds (L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f;
theorem :: JORDAN4:56
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1<i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2;
theorem :: JORDAN4:57
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1>i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2;
theorem :: JORDAN4:58
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part>_of f,i1,i2 & i1<>i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2;
theorem :: JORDAN4:59
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat st
g is_a_part<_of f,i1,i2 & i1<>i2 holds
L~g is_S-P_arc_joining f/.i1,f/.i2;
theorem :: JORDAN4:60
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat
st g is_a_part_of f,i1,i2 & i1<>i2
holds L~g is_S-P_arc_joining f/.i1,f/.i2;
theorem :: JORDAN4:61
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL 2,i1,i2 being Nat
st g is_a_part_of f,i1,i2 & g.1<>g.len g
holds L~g is_S-P_arc_joining f/.i1,f/.i2;
theorem :: JORDAN4:62
for f being non constant standard special_circular_sequence,
i1,i2 being Nat st
1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & i1<>i2 holds
ex g1,g2 being FinSequence of TOP-REAL 2 st
g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2
& (L~g1)/\(L~g2)={f.i1,f.i2} & (L~g1) \/ (L~g2)=L~f &
L~g1 is_S-P_arc_joining f/.i1,f/.i2 &
L~g2 is_S-P_arc_joining f/.i1,f/.i2 &
for g being FinSequence of TOP-REAL 2 st g is_a_part_of f,i1,i2 holds
g=g1 or g=g2;
reserve g, g1, g2 for FinSequence of TOP-REAL 2;
theorem :: JORDAN4:63
for f being non constant standard special_circular_sequence,
P being non empty Subset of TOP-REAL 2 st P = L~f
holds P is_simple_closed_curve;
theorem :: JORDAN4:64
for f being non constant standard special_circular_sequence,
g1,g2 st g1 is_a_part>_of f,i1,i2 & g2 is_a_part>_of f,i1,i2
holds g1=g2;
theorem :: JORDAN4:65
for f being non constant standard special_circular_sequence,
g1,g2 st g1 is_a_part<_of f,i1,i2 & g2 is_a_part<_of f,i1,i2
holds g1=g2;
theorem :: JORDAN4:66
for f being non constant standard special_circular_sequence,
g1,g2 st i1<>i2 & g1 is_a_part>_of f,i1,i2 & g2 is_a_part<_of f,i1,i2
holds g1.2<>g2.2;
theorem :: JORDAN4:67
for f being non constant standard special_circular_sequence,
g1,g2 st i1<>i2 & g1 is_a_part_of f,i1,i2 & g2 is_a_part_of f,i1,i2
& g1.2=g2.2 holds g1=g2;
definition let f be non constant standard special_circular_sequence,
i1,i2 be Nat;
assume 1<=i1 & i1+1<=len f & 1<=i2 & i2+1<=len f & i1<>i2;
func Lower (f,i1,i2) -> FinSequence of TOP-REAL 2 means
:: JORDAN4:def 5
it is_a_part_of f,i1,i2 &
((f/.(i1+1))`1<(f/.i1)`1 or (f/.(i1+1))`2<(f/.i1)`2 implies it.2=f.(i1+1))&
((f/.(i1+1))`1>=(f/.i1)`1 & (f/.(i1+1))`2>=(f/.i1)`2
implies it.2=f.S_Drop(i1-'1,f));
func Upper (f,i1,i2) -> FinSequence of TOP-REAL 2 means
:: JORDAN4:def 6
it is_a_part_of f,i1,i2 &
((f/.(i1+1))`1>(f/.i1)`1 or (f/.(i1+1))`2>(f/.i1)`2 implies it.2=f.(i1+1))&
((f/.(i1+1))`1<=(f/.i1)`1 & (f/.(i1+1))`2<=(f/.i1)`2
implies it.2=f.S_Drop(i1-'1,f));
end;
Back to top