:: Some Properties of Restrictions of Finite Sequences
:: by Czes\law Byli\'nski
::
:: Received January 25, 1995
:: Copyright (c) 1995-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, XXREAL_0, ARYTM_1, ARYTM_3, SUBSET_1, FINSEQ_1,
CARD_1, FUNCT_1, RELAT_1, FINSEQ_4, ZFMISC_1, XBOOLE_0, ORDINAL4, TARSKI,
PARTFUN1, RFINSEQ, FINSEQ_3, FINSEQ_5;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, NAT_1,
RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_3, FINSEQ_4, ZFMISC_1,
RFINSEQ, NAT_D, XXREAL_0;
constructors XXREAL_0, NAT_1, INT_1, PARTFUN1, FINSEQ_4, ZFMISC_1, RFINSEQ,
NAT_D, REAL_1, RELSET_1, FINSEQ_3;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1,
INT_1, FINSEQ_1, CARD_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve i,j,k,n for Nat;
theorem :: FINSEQ_5:1
for i, n being Nat holds i <= n implies n - i + 1 is Element of NAT;
theorem :: FINSEQ_5:2
for i,n being Nat holds i in Seg n implies n - i + 1 in Seg n;
theorem :: FINSEQ_5:3
for f being Function, x,y being object st f"{y} = {x} holds x in dom
f & y in rng f & f.x = y;
theorem :: FINSEQ_5:4
for f being Function holds f is one-to-one iff for x being set st x in
dom f holds f"{f.x} = {x};
theorem :: FINSEQ_5:5
for f being Function, y1,y2 being object st f is one-to-one & y1 in rng f
& f"{y1} = f"{y2} holds y1 = y2;
registration
let x be object;
cluster <*x*> -> trivial;
let y be object;
cluster <*x,y*> -> non trivial;
end;
registration
cluster one-to-one non empty for FinSequence;
end;
theorem :: FINSEQ_5:6
for f being non empty FinSequence holds 1 in dom f & len f in dom f;
theorem :: FINSEQ_5:7
for f being non empty FinSequence ex i being Nat st i+1 = len f;
theorem :: FINSEQ_5:8
for x being object, f being FinSequence holds len(<*x*>^f) = 1 + len f;
theorem :: FINSEQ_5:9
for f being FinSequence, p,q being set st p in rng f & q in rng f &
p..f = q..f holds p = q;
theorem :: FINSEQ_5:10
for f,g being FinSequence st n+1 in dom f & g = f|Seg n holds f|
Seg(n+1) = g^<*f.(n+1)*>;
theorem :: FINSEQ_5:11
for f being one-to-one FinSequence st i in dom f holds (f.i)..f = i;
reserve D for non empty set,
p for Element of D,
f,g for FinSequence of D;
registration
let D be non empty set;
cluster one-to-one non empty for FinSequence of D;
end;
:: FINSEQ_1:17
theorem :: FINSEQ_5:12
dom f = dom g & (for i st i in dom f holds f/.i = g/.i) implies f = g;
:: FINSEQ_1:18
theorem :: FINSEQ_5:13
len f = len g & (for k st 1 <= k & k <= len f holds f/.k = g/.k)
implies f = g;
theorem :: FINSEQ_5:14
for f being FinSequence st
len f = 1 holds f = <*f.1*>;
theorem :: FINSEQ_5:15
for D being non empty set, p being Element of D, f being
FinSequence of D holds (<*p*>^f)/.1 = p;
theorem :: FINSEQ_5:16
for f being FinSequence, i being Nat holds len(f|i) <= len f;
theorem :: FINSEQ_5:17
for f being FinSequence, i being Nat holds len(f|i) <= i;
theorem :: FINSEQ_5:18
for f being FinSequence, i being Nat holds dom(f|i) c= dom f;
theorem :: FINSEQ_5:19
for f being FinSequence, i being Nat holds rng(f|i) c= rng f;
theorem :: FINSEQ_5:20
for f being FinSequence st f is non empty holds f|1 = <*f.1*>;
theorem :: FINSEQ_5:21
i+1 = len f implies f = (f|i)^<*f/.len f*>;
registration
let i,D;
let f be one-to-one FinSequence of D;
cluster f|i -> one-to-one;
end;
theorem :: FINSEQ_5:22
for f, g being FinSequence st i <= len f holds
(f^g)|i = f|i;
theorem :: FINSEQ_5:23
for f, g being FinSequence holds (f^g)|(len f) = f;
theorem :: FINSEQ_5:24
for f being FinSequence of D st p in rng f holds
(f-|p)^<*p*> = f|(p..f);
theorem :: FINSEQ_5:25
for f being FinSequence holds
len(f/^i) <= len f;
theorem :: FINSEQ_5:26
for f being FinSequence st
i in dom(f/^n) holds n+i in dom f;
theorem :: FINSEQ_5:27
(for f being FinSequence st i in dom(f/^n) holds (f/^n).i = f.(n+i)) &
(i in dom(f/^n) implies (f/^n)/.i = f/.(n+i));
theorem :: FINSEQ_5:28
for f being FinSequence holds f/^0 = f;
registration
let f be FinSequence;
reduce f /^ 0 to f;
end;
reserve D for non empty set,
p for Element of D,
f,g for FinSequence of D;
theorem :: FINSEQ_5:29
f is non empty implies f = <*f/.1*>^(f/^1);
theorem :: FINSEQ_5:30
for f being FinSequence st
i+1 = len f holds f/^i = <*f.len f*>;
theorem :: FINSEQ_5:31
j+1 = i & i in dom f implies <*f/.i*>^(f/^i) = f/^j;
theorem :: FINSEQ_5:32
for f being FinSequence st len f <= i holds f/^i is empty;
theorem :: FINSEQ_5:33
for f being FinSequence holds rng(f/^n) c= rng f;
registration
let i,D;
let f be one-to-one FinSequence of D;
cluster f/^i -> one-to-one;
end;
theorem :: FINSEQ_5:34
for f being FinSequence st
f is one-to-one holds rng(f|n) misses rng(f/^n);
theorem :: FINSEQ_5:35
p in rng f implies f |-- p = f/^(p..f);
theorem :: FINSEQ_5:36
for f, g being FinSequence holds
(f^g)/^(len f + i) = g/^i;
theorem :: FINSEQ_5:37
for f, g being FinSequence holds
(f^g)/^(len f) = g;
registration
let f,g be FinSequence;
reduce (f^g)/^(len f) to g;
end;
theorem :: FINSEQ_5:38
p in rng f implies f/.(p..f) = p;
theorem :: FINSEQ_5:39
i in dom f implies f/.i..f <= i;
theorem :: FINSEQ_5:40
p in rng(f|i) implies p..(f|i) = p..f;
theorem :: FINSEQ_5:41
i in dom f & f is one-to-one implies f/.i..f = i;
definition
let D, f;
let p be set;
func f-:p -> FinSequence of D equals
:: FINSEQ_5:def 1
f|(p..f);
end;
theorem :: FINSEQ_5:42
p in rng f implies len(f-:p) = p..f;
theorem :: FINSEQ_5:43
p in rng f & i in Seg(p..f) implies (f-:p)/.i = f/.i;
theorem :: FINSEQ_5:44
p in rng f implies (f-:p)/.1 = f/.1;
theorem :: FINSEQ_5:45
p in rng f implies (f-:p)/.(p..f) = p;
theorem :: FINSEQ_5:46
for x being set st x in rng f & p in rng f & x..f<=p..f holds x in rng(f-:p);
theorem :: FINSEQ_5:47
p in rng f implies f-:p is non empty;
theorem :: FINSEQ_5:48
rng(f-:p) c= rng f;
registration
let D,p;
let f be one-to-one FinSequence of D;
cluster f-:p -> one-to-one;
end;
definition
let D, f, p;
func f:-p -> FinSequence of D equals
:: FINSEQ_5:def 2
<*p*>^(f/^p..f);
end;
theorem :: FINSEQ_5:49
p in rng f implies ex i being Element of NAT st i+1 = p..f & f:- p = f/^i;
theorem :: FINSEQ_5:50
p in rng f implies len (f:-p) = len f - p..f + 1;
theorem :: FINSEQ_5:51
p in rng f & j+1 in dom(f:-p) implies j+p..f in dom f;
registration
let D,p,f;
cluster f:-p -> non empty;
end;
theorem :: FINSEQ_5:52
p in rng f & j+1 in dom(f:-p) implies (f:-p)/.(j+1) = f/.(j+p..f );
theorem :: FINSEQ_5:53
(f:-p)/.1 = p;
theorem :: FINSEQ_5:54
p in rng f implies (f:-p)/.(len(f:-p)) = f/.len f;
theorem :: FINSEQ_5:55
p in rng f implies rng(f:-p) c= rng f;
theorem :: FINSEQ_5:56
p in rng f & f is one-to-one implies f:-p is one-to-one;
reserve i for Nat;
definition
let f be FinSequence;
func Rev f -> FinSequence means
:: FINSEQ_5:def 3
len it = len f & for i st i in dom it holds it.i = f.(len f - i + 1);
involutiveness;
end;
theorem :: FINSEQ_5:57
for f being FinSequence holds dom f = dom Rev f & rng f = rng Rev f;
theorem :: FINSEQ_5:58
for f being FinSequence st i in dom f holds (Rev f).i = f.(len f - i + 1);
theorem :: FINSEQ_5:59
for f being FinSequence, i,j being Nat st
i in dom f & i+j = len f + 1 holds j in dom Rev f;
registration
let f be empty FinSequence;
cluster Rev f -> empty;
end;
theorem :: FINSEQ_5:60
for x being object holds Rev <*x*> = <*x*>;
theorem :: FINSEQ_5:61
for x1,x2 being object holds Rev <*x1,x2*> = <*x2,x1*>;
theorem :: FINSEQ_5:62
for f being FinSequence holds f.1 = (Rev f).(len f) & f.(len f) = (Rev f).1;
registration
let f be one-to-one FinSequence;
cluster Rev f -> one-to-one;
end;
theorem :: FINSEQ_5:63
for f being FinSequence, x being object holds Rev(f^<*x*>) = <*x*>^ (Rev f);
theorem :: FINSEQ_5:64
for f,g being FinSequence holds Rev(f^g) = (Rev g)^(Rev f);
definition
let D be set, f be FinSequence of D;
redefine func Rev f -> FinSequence of D;
end;
theorem :: FINSEQ_5:65
f is non empty implies f/.1 = (Rev f)/.len f & f/.len f = (Rev f)/.1;
theorem :: FINSEQ_5:66
i in dom f & i+j = len f + 1 implies f/.i = (Rev f)/.j;
definition
let D,f,p;
let n be Nat;
func Ins(f,n,p) -> FinSequence of D equals
:: FINSEQ_5:def 4
(f|n)^<*p*>^(f/^n);
end;
theorem :: FINSEQ_5:67
Ins(f,0,p) = <*p*>^f;
theorem :: FINSEQ_5:68
len f <= n implies Ins(f,n,p) = f^<*p*>;
theorem :: FINSEQ_5:69
len(Ins(f,n,p)) = len f + 1;
theorem :: FINSEQ_5:70
rng Ins(f,n,p) = {p} \/ rng f;
registration
let D,f,n,p;
cluster Ins(f,n,p) -> non empty;
end;
theorem :: FINSEQ_5:71
p in rng Ins(f,n,p);
theorem :: FINSEQ_5:72
i in dom(f|n) implies (Ins(f,n,p)).i = f.i;
theorem :: FINSEQ_5:73
n <= len f implies (Ins(f,n,p)).(n+1) = p;
theorem :: FINSEQ_5:74
n+1 <= i & i <= len f implies (Ins(f,n,p)).(i+1) = f.i;
theorem :: FINSEQ_5:75
1 <= n & f is non empty implies (Ins(f,n,p)).1 = f.1;
theorem :: FINSEQ_5:76
f is one-to-one & not p in rng f implies Ins(f,n,p) is one-to-one;
begin :: Addenda
:: from JORDAN4, 2005.11.16, A.T.
theorem :: FINSEQ_5:77
for i1,i2 be Nat st i1<=i2 holds (f|i1)|i2=f|i1 & (f|i2)|i1=f|i1;
theorem :: FINSEQ_5:78
for i be Nat holds (<*>D)|i=<*>D;
theorem :: FINSEQ_5:79
Rev <*>D = <*>D;
:: from AMISTD_1, 2006.03,15, A.T.
registration
cluster non trivial for FinSequence;
end;
:: from JORDAN3, 2007.03.09, A.T
theorem :: FINSEQ_5:80
for f being FinSequence of D,l1,l2 being Nat holds
(f/^l1)|(l2-'l1)=(f|l2)/^l1;
:: from JORDAN8, 2007.03.18, A.T.
reserve D for set,
f for FinSequence of D;
theorem :: FINSEQ_5:81
len f >= 2 implies f|2 = <*f/.1,f/.2*>;
theorem :: FINSEQ_5:82
k+1 <= len f implies f|(k+1) = f|k^<*f/.(k+1)*>;
:: from JORDAN3, 2007.03.18, A.T.
theorem :: FINSEQ_5:83
for D being set, p be FinSequence of D for i be Nat st i < len p
holds p|(i+1) = p|i ^ <*p.(i+1)*>;
:: from POLYNOM4, 2007.03.18, A.T.
theorem :: FINSEQ_5:84
for D be non empty set for p be FinSequence of D for n be Nat st 1 <=
n & n <= len p holds p = (p|(n-'1))^<*p.n*>^(p/^n);
:: from POLYALG1, 2016.10.19, A.K.
theorem :: FINSEQ_5:85
for D be non empty set for f being non empty FinSequence of D
holds f/^1 = Del(f,1);
theorem :: FINSEQ_5:86
for D be non empty set for f being non empty FinSequence of D
holds f = <*f.1*>^Del(f,1);