Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Finite Sequences and Tuples of Elements of a Non-empty Sets

**by****Czeslaw Bylinski**- Received March 1, 1990
- MML identifier: FINSEQ_2

- [ Mizar article, MML identifier index ]

environ vocabulary ORDINAL2, ARYTM, FINSEQ_1, SQUARE_1, BOOLE, ARYTM_1, FUNCT_1, RELAT_1, FUNCT_2, FUNCOP_1, PARTFUN1, TARSKI, FINSEQ_2; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, NUMBERS, XCMPLX_0, XREAL_0, DOMAIN_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, FINSEQ_1, BINOP_1, FUNCOP_1; constructors DOMAIN_1, NAT_1, SQUARE_1, FUNCT_3, FINSEQ_1, BINOP_1, FUNCOP_1, PARTFUN1, MEMBERED, RELAT_2, XBOOLE_0; clusters SUBSET_1, FUNCT_1, FINSEQ_1, RELSET_1, XREAL_0, FUNCOP_1, FUNCT_2, NAT_1, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve i,j,l for Nat; reserve k for natural number; reserve A,a,b,x,x1,x2,x3 for set; reserve D,D',E for non empty set; reserve d,d1,d2,d3 for Element of D; reserve d',d1',d2',d3' for Element of D'; reserve p,q,r for FinSequence; :: Auxiliary theorems theorem :: FINSEQ_2:1 min(i,j) is Nat & max(i,j) is Nat; theorem :: FINSEQ_2:2 l = min(i,j) implies Seg i /\ Seg j = Seg l; theorem :: FINSEQ_2:3 i <= j implies max(0,i-j) = 0; theorem :: FINSEQ_2:4 j <= i implies max(0,i-j) = i-j; theorem :: FINSEQ_2:5 max(0,i-j) is Nat; theorem :: FINSEQ_2:6 min(0,i) = 0 & min(i,0) = 0 & max(0,i) = i & max(i,0) = i; :: Non-empty Segments of Natural Numbers canceled; theorem :: FINSEQ_2:8 i in Seg (l+1) implies i in Seg l or i = l+1; theorem :: FINSEQ_2:9 i in Seg l implies i in Seg(l+j); :: Additional propositions related to Finite Sequences theorem :: FINSEQ_2:10 len p = i & len q = i & (for j st j in Seg i holds p.j = q.j) implies p = q; theorem :: FINSEQ_2:11 b in rng p implies ex i st i in dom p & p.i = b; canceled; theorem :: FINSEQ_2:13 for D being set for p being FinSequence of D st i in dom p holds p.i in D; theorem :: FINSEQ_2:14 for D being set holds (for i st i in dom p holds p.i in D) implies p is FinSequence of D; theorem :: FINSEQ_2:15 <*d1,d2*> is FinSequence of D; theorem :: FINSEQ_2:16 <*d1,d2,d3*> is FinSequence of D; canceled; theorem :: FINSEQ_2:18 i in dom p implies i in dom(p^q); theorem :: FINSEQ_2:19 len(p^<*a*>) = len p + 1; theorem :: FINSEQ_2:20 p^<*a*> = q^<*b*> implies p = q & a = b; theorem :: FINSEQ_2:21 len p = i + 1 implies ex q,a st p = q^<*a*>; theorem :: FINSEQ_2:22 for p being FinSequence of D st len p <> 0 ex q being (FinSequence of D),d st p = q^<*d*>; theorem :: FINSEQ_2:23 q = p|(Seg i) & len p <= i implies p = q; theorem :: FINSEQ_2:24 q = p|(Seg i) implies len q = min(i,len p); theorem :: FINSEQ_2:25 len r = i+j implies ex p,q st len p = i & len q = j & r = p^q; theorem :: FINSEQ_2:26 for r being FinSequence of D st len r = i+j ex p,q being FinSequence of D st len p = i & len q = j & r = p^q; scheme SeqLambdaD{i()->Nat,D()->non empty set,F(set)->Element of D()}: ex z being FinSequence of D() st len z = i() & for j st j in Seg i() holds z.j = F(j); scheme IndSeqD{D()->non empty set, P[set]}: for p being FinSequence of D() holds P[p] provided P[<*> D()] and for p being FinSequence of D() for x being Element of D() st P[p] holds P[p^<*x*>]; theorem :: FINSEQ_2:27 for D' being non empty Subset of D for p being FinSequence of D' holds p is FinSequence of D; theorem :: FINSEQ_2:28 for f being Function of Seg i, D holds f is FinSequence of D; canceled; theorem :: FINSEQ_2:30 for p being FinSequence of D holds p is Function of dom p, D; theorem :: FINSEQ_2:31 for f being Function of NAT,D holds f|(Seg i) is FinSequence of D; theorem :: FINSEQ_2:32 for f being Function of NAT,D st q = f|(Seg i) holds len q = i; theorem :: FINSEQ_2:33 for f being Function st rng p c= dom f & q = f*p holds len q = len p; theorem :: FINSEQ_2:34 D = Seg i implies for p being FinSequence for q being FinSequence of D st i <= len p holds p*q is FinSequence; theorem :: FINSEQ_2:35 D = Seg i implies for p being FinSequence of D' for q being FinSequence of D st i <= len p holds p*q is FinSequence of D'; theorem :: FINSEQ_2:36 for A,D being set for p being FinSequence of A for f being Function of A,D holds f*p is FinSequence of D; theorem :: FINSEQ_2:37 for p being FinSequence of A for f being Function of A,D' st q = f*p holds len q = len p; theorem :: FINSEQ_2:38 for f being Function of A,D' holds f*(<*>A) = <*>D'; theorem :: FINSEQ_2:39 for p being FinSequence of D for f being Function of D,D' st p = <*x1*> holds f*p = <*f.x1*>; theorem :: FINSEQ_2:40 for p being FinSequence of D for f being Function of D,D' st p = <*x1,x2*> holds f*p = <*f.x1,f.x2*>; theorem :: FINSEQ_2:41 for p being FinSequence of D for f being Function of D,D' st p = <*x1,x2,x3*> holds f*p = <*f.x1,f.x2,f.x3*>; theorem :: FINSEQ_2:42 for f being Function of Seg i,Seg j st (j = 0 implies i = 0) & j <= len p holds p*f is FinSequence; theorem :: FINSEQ_2:43 for f being Function of Seg i,Seg i st i <= len p holds p*f is FinSequence; theorem :: FINSEQ_2:44 for f being Function of dom p,dom p holds p*f is FinSequence; theorem :: FINSEQ_2:45 for f being Function of Seg i,Seg i st rng f = Seg i & i <= len p & q = p*f holds len q = i; theorem :: FINSEQ_2:46 for f being Function of dom p,dom p st rng f = dom p & q = p*f holds len q = len p; theorem :: FINSEQ_2:47 for f being Permutation of Seg i st i <= len p & q = p*f holds len q = i; theorem :: FINSEQ_2:48 for f being Permutation of dom p st q = p*f holds len q = len p; theorem :: FINSEQ_2:49 for p being FinSequence of D for f being Function of Seg i,Seg j st (j = 0 implies i = 0) & j <= len p holds p*f is FinSequence of D; theorem :: FINSEQ_2:50 for p being FinSequence of D for f being Function of Seg i,Seg i st i <= len p holds p*f is FinSequence of D; theorem :: FINSEQ_2:51 for p being FinSequence of D for f being Function of dom p,dom p holds p*f is FinSequence of D; theorem :: FINSEQ_2:52 id Seg k is FinSequence of NAT; definition let i be natural number; func idseq i -> FinSequence equals :: FINSEQ_2:def 1 id Seg i; end; canceled; theorem :: FINSEQ_2:54 dom idseq k = Seg k; theorem :: FINSEQ_2:55 len idseq k = k; theorem :: FINSEQ_2:56 j in Seg i implies (idseq i).j = j; theorem :: FINSEQ_2:57 i<>0 implies for k being Element of Seg i holds (idseq i).k = k; theorem :: FINSEQ_2:58 idseq 0 = {}; theorem :: FINSEQ_2:59 idseq 1 = <*1*>; theorem :: FINSEQ_2:60 idseq (i+1) = (idseq i) ^ <*i+1*>; theorem :: FINSEQ_2:61 idseq 2 = <*1,2*>; theorem :: FINSEQ_2:62 idseq 3 = <*1,2,3*>; theorem :: FINSEQ_2:63 p*(idseq k) = p|(Seg k); theorem :: FINSEQ_2:64 len p <= k implies p*(idseq k) = p; theorem :: FINSEQ_2:65 idseq k is Permutation of Seg k; theorem :: FINSEQ_2:66 (Seg k) --> a is FinSequence; definition let i be natural number, a be set; func i |-> a -> FinSequence equals :: FINSEQ_2:def 2 Seg i --> a; end; canceled; theorem :: FINSEQ_2:68 dom(k |-> a) = Seg k; theorem :: FINSEQ_2:69 len(k |-> a) = k; theorem :: FINSEQ_2:70 b in Seg k implies (k |-> a).b = a; theorem :: FINSEQ_2:71 k<>0 implies for w being Element of Seg k holds (k |-> d).w = d; theorem :: FINSEQ_2:72 0 |-> a = {}; theorem :: FINSEQ_2:73 1 |-> a = <*a*>; theorem :: FINSEQ_2:74 (i+1) |-> a = (i |-> a) ^ <*a*>; theorem :: FINSEQ_2:75 2 |-> a = <*a,a*>; theorem :: FINSEQ_2:76 3 |-> a = <*a,a,a*>; theorem :: FINSEQ_2:77 k |-> d is FinSequence of D; theorem :: FINSEQ_2:78 for F being Function st [:rng p,rng q:] c= dom F holds F.:(p,q) is FinSequence; theorem :: FINSEQ_2:79 for F being Function st [:rng p,rng q:] c= dom F & r = F.:(p,q) holds len r = min(len p,len q); theorem :: FINSEQ_2:80 for F being Function st [:{a},rng p:] c= dom F holds F[;](a,p) is FinSequence; theorem :: FINSEQ_2:81 for F being Function st [:{a},rng p:] c= dom F & r = F[;](a,p) holds len r = len p; theorem :: FINSEQ_2:82 for F being Function st [:rng p,{a}:] c= dom F holds F[:](p,a) is FinSequence; theorem :: FINSEQ_2:83 for F being Function st [:rng p,{a}:] c= dom F & r = F[:](p,a) holds len r = len p; theorem :: FINSEQ_2:84 for F being Function of [:D,D':],E for p being FinSequence of D for q being FinSequence of D' holds F.:(p,q) is FinSequence of E; theorem :: FINSEQ_2:85 for F being Function of [:D,D':],E for p being FinSequence of D for q being FinSequence of D' st r = F.:(p,q) holds len r = min(len p,len q); theorem :: FINSEQ_2:86 for F being Function of [:D,D':],E for p being FinSequence of D for q being FinSequence of D' st len p = len q & r = F.:(p,q) holds len r = len p & len r = len q; theorem :: FINSEQ_2:87 for F being Function of [:D,D':],E for p being FinSequence of D for p' being FinSequence of D' holds F.:(<*>D,p') = <*>E & F.:(p,<*>D') = <*>E; theorem :: FINSEQ_2:88 for F being Function of [:D,D':],E for p being FinSequence of D for q being FinSequence of D' st p = <*d1*> & q = <*d1'*> holds F.:(p,q) = <*F.(d1,d1')*>; theorem :: FINSEQ_2:89 for F being Function of [:D,D':],E for p being FinSequence of D for q being FinSequence of D' st p = <*d1,d2*> & q = <*d1',d2'*> holds F.:(p,q) = <*F.(d1,d1'),F.(d2,d2')*>; theorem :: FINSEQ_2:90 for F being Function of [:D,D':],E for p being FinSequence of D for q being FinSequence of D' st p = <*d1,d2,d3*> & q = <*d1',d2',d3'*> holds F.:(p,q) = <*F.(d1,d1'),F.(d2,d2'),F.(d3,d3')*>; theorem :: FINSEQ_2:91 for F being Function of [:D,D':],E for p being FinSequence of D' holds F[;](d,p) is FinSequence of E; theorem :: FINSEQ_2:92 for F being Function of [:D,D':],E for p being FinSequence of D' st r = F[;](d,p) holds len r = len p; theorem :: FINSEQ_2:93 for F being Function of [:D,D':],E holds F[;](d,<*>D') = <*>E; theorem :: FINSEQ_2:94 for F being Function of [:D,D':],E for p being FinSequence of D' st p = <*d1'*> holds F[;](d,p) = <*F.(d,d1')*>; theorem :: FINSEQ_2:95 for F being Function of [:D,D':],E for p being FinSequence of D' st p = <*d1',d2'*> holds F[;](d,p) = <*F.(d,d1'),F.(d,d2')*>; theorem :: FINSEQ_2:96 for F being Function of [:D,D':],E for p being FinSequence of D' st p = <*d1',d2',d3'*> holds F[;](d,p) = <*F.(d,d1'),F.(d,d2'),F.(d,d3')*>; theorem :: FINSEQ_2:97 for F being Function of [:D,D':],E for p being FinSequence of D holds F[:](p,d') is FinSequence of E; theorem :: FINSEQ_2:98 for F being Function of [:D,D':],E for p being FinSequence of D st r = F[:](p,d') holds len r = len p; theorem :: FINSEQ_2:99 for F being Function of [:D,D':],E holds F[:](<*>D,d') = <*>E; theorem :: FINSEQ_2:100 for F being Function of [:D,D':],E for p being FinSequence of D st p = <*d1*> holds F[:](p,d') = <*F.(d1,d')*>; theorem :: FINSEQ_2:101 for F being Function of [:D,D':],E for p being FinSequence of D st p = <*d1,d2*> holds F[:](p,d') = <*F.(d1,d'),F.(d2,d')*>; theorem :: FINSEQ_2:102 for F being Function of [:D,D':],E for p being FinSequence of D st p = <*d1,d2,d3*> holds F[:](p,d') = <*F.(d1,d'),F.(d2,d'),F.(d3,d')*>; :: T u p l e s definition let D be set; mode FinSequenceSet of D -> set means :: FINSEQ_2:def 3 a in it implies a is FinSequence of D; end; definition let D be set; cluster non empty FinSequenceSet of D; end; definition let D be set; mode FinSequence-DOMAIN of D is non empty FinSequenceSet of D; end; canceled; theorem :: FINSEQ_2:104 for D being set holds D* is FinSequence-DOMAIN of D; definition let D be set; redefine func D* -> FinSequence-DOMAIN of D; end; theorem :: FINSEQ_2:105 for D being set, D' being FinSequence-DOMAIN of D holds D' c= D*; definition let D be set, S be FinSequence-DOMAIN of D; redefine mode Element of S -> FinSequence of D; end; canceled; theorem :: FINSEQ_2:107 for D' being non empty Subset of D, S being FinSequence-DOMAIN of D' holds S is FinSequence-DOMAIN of D; reserve s for Element of D*; definition let i be natural number; let D be set; func i-tuples_on D -> FinSequenceSet of D equals :: FINSEQ_2:def 4 { s where s is Element of D*: len s = i }; end; definition let i be natural number, D; cluster i-tuples_on D -> non empty; end; canceled; theorem :: FINSEQ_2:109 for z being Element of i-tuples_on D holds len z = i; theorem :: FINSEQ_2:110 for D be set, z being FinSequence of D holds z is Element of (len z)-tuples_on D; theorem :: FINSEQ_2:111 i-tuples_on D = Funcs(Seg i,D); theorem :: FINSEQ_2:112 for D being set holds 0-tuples_on D = { <*>D }; theorem :: FINSEQ_2:113 for D be set, z being Element of 0-tuples_on D holds z = <*>D; theorem :: FINSEQ_2:114 for D be set holds <*>D is Element of 0-tuples_on D; theorem :: FINSEQ_2:115 for z being Element of 0-tuples_on D for t being Element of i-tuples_on D holds z^t = t & t^z = t; theorem :: FINSEQ_2:116 1-tuples_on D = { <*d*>: not contradiction }; theorem :: FINSEQ_2:117 for z being Element of 1-tuples_on D ex d st z = <*d*>; theorem :: FINSEQ_2:118 <*d*> is Element of 1-tuples_on D; theorem :: FINSEQ_2:119 2-tuples_on D = { <*d1,d2*>: not contradiction }; theorem :: FINSEQ_2:120 for z being Element of 2-tuples_on D ex d1,d2 st z = <*d1,d2*>; theorem :: FINSEQ_2:121 <*d1,d2*> is Element of 2-tuples_on D; theorem :: FINSEQ_2:122 3-tuples_on D = { <*d1,d2,d3*>: not contradiction }; theorem :: FINSEQ_2:123 for z being Element of 3-tuples_on D ex d1,d2,d3 st z = <*d1,d2,d3*>; theorem :: FINSEQ_2:124 <*d1,d2,d3*> is Element of 3-tuples_on D; theorem :: FINSEQ_2:125 (i+j)-tuples_on D = {z^t where z is (Element of i-tuples_on D), t is Element of j-tuples_on D: not contradiction}; theorem :: FINSEQ_2:126 for s being Element of (i+j)-tuples_on D ex z being (Element of i-tuples_on D), t being Element of j-tuples_on D st s = z^t; theorem :: FINSEQ_2:127 for z being Element of i-tuples_on D for t being Element of j-tuples_on D holds z^t is Element of (i+j)-tuples_on D; theorem :: FINSEQ_2:128 D* = union {i-tuples_on D: not contradiction}; theorem :: FINSEQ_2:129 for D' being non empty Subset of D for z being Element of i-tuples_on D' holds z is Element of i-tuples_on D; theorem :: FINSEQ_2:130 i-tuples_on D = j-tuples_on D implies i = j; theorem :: FINSEQ_2:131 idseq i is Element of i-tuples_on NAT; theorem :: FINSEQ_2:132 i |-> d is Element of i-tuples_on D; theorem :: FINSEQ_2:133 for z being Element of i-tuples_on D for f being Function of D,D' holds f*z is Element of i-tuples_on D'; theorem :: FINSEQ_2:134 for z being Element of i-tuples_on D for f being Function of Seg i,Seg i st rng f = Seg i holds z*f is Element of i-tuples_on D; theorem :: FINSEQ_2:135 for z being Element of i-tuples_on D for f being Permutation of Seg i holds z*f is Element of i-tuples_on D; theorem :: FINSEQ_2:136 for z being Element of i-tuples_on D for d holds (z^<*d*>).(i+1) = d; theorem :: FINSEQ_2:137 for z being Element of (i+1)-tuples_on D ex t being (Element of i-tuples_on D), d st z = t^<*d*>; theorem :: FINSEQ_2:138 for z being Element of i-tuples_on D holds z*(idseq i) = z; theorem :: FINSEQ_2:139 for z1,z2 being Element of i-tuples_on D st for j st j in Seg i holds z1.j = z2.j holds z1 = z2; theorem :: FINSEQ_2:140 for F being Function of [:D,D':],E for z1 being Element of i-tuples_on D for z2 being Element of i-tuples_on D' holds F.:(z1,z2) is Element of i-tuples_on E; theorem :: FINSEQ_2:141 for F being Function of [:D,D':],E for z being Element of i-tuples_on D' holds F[;](d,z) is Element of i-tuples_on E; theorem :: FINSEQ_2:142 for F being Function of [:D,D':],E for z being Element of i-tuples_on D holds F[:](z,d') is Element of i-tuples_on E; theorem :: FINSEQ_2:143 (i+j)|->x = (i|->x)^(j|->x); :: Addendum, 2002.07.08 theorem :: FINSEQ_2:144 for i, D for x being Element of i-tuples_on D holds dom x = Seg i; theorem :: FINSEQ_2:145 for f being Function, x, y being set st x in dom f & y in dom f holds f*<*x,y*> = <*f.x,f.y*>; theorem :: FINSEQ_2:146 for f being Function, x, y, z being set st x in dom f & y in dom f & z in dom f holds f*<*x,y,z*> = <*f.x,f.y,f.z*>; theorem :: FINSEQ_2:147 rng <*x1,x2*> = {x1,x2}; theorem :: FINSEQ_2:148 rng <*x1,x2,x3*> = {x1,x2,x3};

Back to top