Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

Some Properties of Restrictions of Finite Sequences

by
Czeslaw Bylinski

MML identifier: FINSEQ_5
[ Mizar article, MML identifier index ]

environ

vocabulary ARYTM_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_4, REALSET1, RFINSEQ,
BOOLE, RLSUB_2, FINSEQ_5;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, RELAT_1,
FUNCT_1, FINSEQ_1, FINSEQ_4, REALSET1, RFINSEQ, TOPREAL1;
constructors REAL_1, NAT_1, REALSET1, RFINSEQ, TOPREAL1, FINSEQ_4, INT_1,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, FINSEQ_1, RELSET_1, INT_1, TOPREAL1, NAT_1,
MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve i,j,k,m,n for Nat;

theorem :: FINSEQ_5:1
i <= n implies n - i + 1 is Nat;

theorem :: FINSEQ_5:2
i in Seg n implies n - i + 1 in Seg n;

theorem :: FINSEQ_5:3
for f being Function, x,y being set 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 set
st f is one-to-one & y1 in rng f & y2 in rng f & f"{y1} = f"{y2}
holds y1 = y2;

definition let x be set;
cluster <*x*> -> non empty;
end;

definition
cluster empty -> trivial set;
end;

definition let x be set;
cluster <*x*> -> trivial;

let y be set;
cluster <*x,y*> -> non trivial;
end;

definition
cluster one-to-one non empty 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 st i+1 = len f;

theorem :: FINSEQ_5:8
for x being set, f being FinSequence holds len(<*x*>^f) = 1 + len f;

scheme domSeqLambda{A()->Nat,F(set) -> set}:
ex p being FinSequence st len p = A() & for k st k in dom p holds p.k=F(k);

canceled;

theorem :: FINSEQ_5:10
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:11
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:12
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;

definition let D be non empty set;
cluster one-to-one non empty FinSequence of D;
end;

:: FINSEQ_1:17

theorem :: FINSEQ_5:13
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:14
len f = len g & (for k st 1 <= k & k <= len f holds f/.k = g/.k)
implies f = g;

theorem :: FINSEQ_5:15
len f = 1 implies f = <*f/.1*>;

theorem :: FINSEQ_5:16
for D being non empty set, p being Element of D,
f being FinSequence of D holds
(<*p*>^f)/.1 = p;

canceled;

theorem :: FINSEQ_5:18
for D being set, f being FinSequence of D holds
len(f|i) <= len f;

theorem :: FINSEQ_5:19
for D being set, f being FinSequence of D holds
len(f|i) <= i;

theorem :: FINSEQ_5:20
for D being set, f being FinSequence of D holds
dom(f|i) c= dom f;

theorem :: FINSEQ_5:21
rng(f|i) c= rng f;

canceled;

theorem :: FINSEQ_5:23
for D being set, f being FinSequence of D holds
f is non empty implies f|1 = <*f/.1*>;

theorem :: FINSEQ_5:24
i+1 = len f implies f = (f|i)^<*f/.len f*>;

definition let i,D; let f be one-to-one FinSequence of D;
cluster f|i -> one-to-one;
end;

theorem :: FINSEQ_5:25
for D being set, f, g being FinSequence of D holds
i <= len f implies (f^g)|i = f|i;

theorem :: FINSEQ_5:26
for D being set, f, g being FinSequence of D holds
(f^g)|(len f) = f;

theorem :: FINSEQ_5:27
for D being set, f being FinSequence of D holds
p in rng f implies (f-|p)^<*p*> = f|(p..f);

theorem :: FINSEQ_5:28
len(f/^i) <= len f;

theorem :: FINSEQ_5:29
i in dom(f/^n) implies n+i in dom f;

theorem :: FINSEQ_5:30
i in dom(f/^n) implies (f/^n)/.i = f/.(n+i);

theorem :: FINSEQ_5:31
f/^0 = f;

theorem :: FINSEQ_5:32
f is non empty implies f = <*f/.1*>^(f/^1);

theorem :: FINSEQ_5:33
i+1 = len f implies f/^i = <*f/.len f*>;

theorem :: FINSEQ_5:34
j+1 = i & i in dom f implies <*f/.i*>^(f/^i) = f/^j;

theorem :: FINSEQ_5:35
for D being set, f being FinSequence of D holds
len f <= i implies f/^i is empty;

theorem :: FINSEQ_5:36
rng(f/^n) c= rng f;

definition let i,D; let f be one-to-one FinSequence of D;
cluster f/^i -> one-to-one;
end;

theorem :: FINSEQ_5:37
f is one-to-one implies rng(f|n) misses rng(f/^n);

theorem :: FINSEQ_5:38
p in rng f implies f |-- p = f/^(p..f);

theorem :: FINSEQ_5:39
(f^g)/^(len f + i) = g/^i;

theorem :: FINSEQ_5:40
(f^g)/^(len f) = g;

theorem :: FINSEQ_5:41
p in rng f implies f/.(p..f) = p;

theorem :: FINSEQ_5:42
i in dom f implies f/.i..f <= i;

theorem :: FINSEQ_5:43
p in rng(f|i) implies p..(f|i) = p..f;

theorem :: FINSEQ_5:44
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:45
p in rng f implies len(f-:p) = p..f;

theorem :: FINSEQ_5:46
p in rng f & i in Seg(p..f) implies (f-:p)/.i = f/.i;

theorem :: FINSEQ_5:47
p in rng f implies (f-:p)/.1 = f/.1;

theorem :: FINSEQ_5:48
p in rng f implies (f-:p)/.(p..f) = p;

theorem :: FINSEQ_5:49
for x being set holds
x in rng f & p in rng f & x..f<=p..f implies x in rng(f-:p);

theorem :: FINSEQ_5:50
p in rng f implies f-:p is non empty;

theorem :: FINSEQ_5:51
rng(f-:p) c= rng f;

definition 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:52
p in rng f implies ex i st i+1 = p..f & f:-p = f/^i;

theorem :: FINSEQ_5:53
p in rng f implies len (f:-p) = len f - p..f + 1;

theorem :: FINSEQ_5:54
p in rng f & j+1 in dom(f:-p) implies j+p..f in dom f;

definition let D,p,f;
cluster f:-p -> non empty;
end;

theorem :: FINSEQ_5:55
p in rng f & j+1 in dom(f:-p) implies (f:-p)/.(j+1) = f/.(j+p..f);

theorem :: FINSEQ_5:56
(f:-p)/.1 = p;

theorem :: FINSEQ_5:57
p in rng f implies (f:-p)/.(len(f:-p)) = f/.len f;

theorem :: FINSEQ_5:58
p in rng f implies rng(f:-p) c= rng f;

theorem :: FINSEQ_5:59
p in rng f & f is one-to-one implies f:-p is one-to-one;

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);
end;

theorem :: FINSEQ_5:60
for f being FinSequence holds dom f = dom Rev f & rng f = rng Rev f;

theorem :: FINSEQ_5:61
for f being FinSequence st i in dom f holds (Rev f).i = f.(len f - i + 1);

theorem :: FINSEQ_5:62
for f being FinSequence, i,j being Nat
st i in dom f & i+j = len f + 1
holds j in dom Rev f;

definition let f be empty FinSequence;
cluster Rev f -> empty;
end;

theorem :: FINSEQ_5:63
for x being set holds Rev <*x*> = <*x*>;

theorem :: FINSEQ_5:64
for x1,x2 being set holds Rev <*x1,x2*> = <*x2,x1*>;

theorem :: FINSEQ_5:65
for f being FinSequence
holds f.1 = (Rev f).(len f) & f.(len f) = (Rev f).1;

definition let f be one-to-one FinSequence;
cluster Rev f -> one-to-one;
end;

theorem :: FINSEQ_5:66
for f being FinSequence, x being set holds Rev(f^<*x*>) = <*x*>^(Rev f);

theorem :: FINSEQ_5:67
for f,g being FinSequence holds Rev(f^g) = (Rev g)^(Rev f);

definition let D,f;
redefine func Rev f -> FinSequence of D;
end;

theorem :: FINSEQ_5:68
f is non empty implies f/.1 = (Rev f)/.len f & f/.len f = (Rev f)/.1;

theorem :: FINSEQ_5:69
i in dom f & i+j = len f + 1 implies f/.i = (Rev f)/.j;

definition let D,f,p,n;
func Ins(f,n,p) -> FinSequence of D equals
:: FINSEQ_5:def 4
(f|n)^<*p*>^(f/^n);
end;

theorem :: FINSEQ_5:70
Ins(f,0,p) = <*p*>^f;

theorem :: FINSEQ_5:71
len f <= n implies Ins(f,n,p) = f^<*p*>;

theorem :: FINSEQ_5:72
len(Ins(f,n,p)) = len f + 1;

theorem :: FINSEQ_5:73
rng Ins(f,n,p) = {p} \/ rng f;

definition let D,f,n,p;
cluster Ins(f,n,p) -> non empty;
end;

theorem :: FINSEQ_5:74
p in rng Ins(f,n,p);

theorem :: FINSEQ_5:75
i in dom(f|n) implies (Ins(f,n,p))/.i = f/.i;

theorem :: FINSEQ_5:76
n <= len f implies (Ins(f,n,p))/.(n+1) = p;

theorem :: FINSEQ_5:77
n+1 <= i & i <= len f implies (Ins(f,n,p))/.(i+1) = f/.i;

theorem :: FINSEQ_5:78
1 <= n & f is non empty implies (Ins(f,n,p))/.1 = f/.1;

theorem :: FINSEQ_5:79
f is one-to-one & not p in rng f implies Ins(f,n,p) is one-to-one;