|
%------------------------------------------------------------------------------
% Re-ordering of sums
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
sigma_bijection[T: TYPE FROM int]: THEORY
BEGIN
ASSUMING
connected_domain: ASSUMPTION (FORALL (x, y: T), (z: integer):
x <= z AND z <= y IMPLIES T_pred(z))
ENDASSUMING
IMPORTING reals@sigma
low,high,
l,h,n,m,i : VAR T
rng, nn : VAR nat
pn : VAR posnat
z : VAR int
a,x,B : VAR real
F : VAR [T->real]
subrange_T(n,m): TYPE = {k:T | n <= k AND k <= m}
% The following theorem shows that we can re-order the summation of
% any finite sum.
sigma_bijection: LEMMA
low <= high IMPLIES
FORALL (phi:(bijective?[subrange_T(low,high),subrange_T(low,high)])):
sigma[subrange_T(low,high)](low,high,F)
= sigma[subrange_T(low,high)](low,high,F o phi)
END sigma_bijection
[ zur Elbe Produktseite wechseln0.18Quellennavigators
Analyse erneut starten
]
|
