|
sigma_lemmas: THEORY
% Linear Algebra library
% Heber Herencia-Zapana NIA
% Gilberto Pérez University of Coruña Spain
% Pablo Ascariz University of Coruña Spain
% Felicidad Aguado University of Coruña Spain
% Date: December, 2013
BEGIN
IMPORTING vectors@vectors
%------------------------------------------------------------
% Lemmas about sums
%------------------------------------------------------------
% These lemmas go from more specific to more general
% There are three kinds of lemmas:
% 1. Restricting the domain of the function
% 2. Shifting the domain of the function
% 3. Changing the notation of the domain of the function (although it remains the same)
sigma_restrict_dom: LEMMA FORALL (j: posnat, m: posnat, F: [below[m] -> real],G: [below[m+1] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j <= m IMPLIES sigma[below[m]](0,j - 1,F) = sigma[below[m+1]](0,j-1,G))
sigma_restrict_dom2: LEMMA FORALL (j: posnat, m: posnat, F: [below[m] -> real],G: [below[m+1] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j < m IMPLIES sigma[below[m]](1,j,F) = sigma[below[m+1]](1,j,G))
sigma_below_shift: LEMMA FORALL (m: posnat, F:[below[m + 1] -> real]): sigma(1, m, LAMBDA (i: below[1 + m]): F(i)) = sigma(0, m - 1, LAMBDA (i: below[m]): F(i + 1))
sigma_eq_index: LEMMA FORALL (m,n: posnat, F: [below[m] -> real],G: [below[n] -> real]): (m = n AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,m - 1,LAMBDA(i: Index[m]): F(i)) = sigma(0,n - 1,LAMBDA(i: Index[n]): G(i))
aux_sigma: LEMMA FORALL (m: posnat,n: nat, F: [below[m] -> real],G: [below[m + n] -> real]): (n = 0 AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,m - 1,LAMBDA(i: below[m]): F(i)) = sigma(0,m + n - 1,LAMBDA(i: below[m + n]): G(i))
aux_sigma2: LEMMA FORALL (m,j: posnat,n: nat, F: [below[m] -> real],G: [below[m + n] -> real]): (n = 0 AND j <= m AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,j - 1,LAMBDA(i: below[m]): F(i)) = sigma(0,j + n - 1,LAMBDA(i: below[m + n]): G(i))
sigma_restrict_gen: LEMMA FORALL (j: posnat, m,n: posnat, F: [below[m] -> real],G: [below[m + n] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j <= m IMPLIES sigma[below[m]](0,j - 1,F) = sigma[below[m + n]](0,j-1,G))
sigma_eq_index2: LEMMA FORALL (m,n,j: posnat, F: [below[m] -> real],G: [below[n] -> real]): (m = n AND j <= m AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(0,j - 1,LAMBDA(i: Index[m]): F(i)) = sigma(0,j - 1,LAMBDA(i: Index[n]): G(i))
sigma_restrict_gen2: LEMMA FORALL (j: posnat,k: nat,m,n: posnat, F: [below[m] -> real],G: [below[m + n] -> real]): (FORALL (i: below[m]): F(i) = G(i)) IMPLIES (j <= m AND k < j IMPLIES sigma[below[m]](k,j - 1,F) = sigma[below[m + n]](k,j-1,G))
sigma_eq_index3: LEMMA FORALL (m,n,j,k: posnat, F: [below[m] -> real],G: [below[n] -> real]): (m = n AND j <= m AND k < j AND FORALL (i: below[m]): F(i) = G(i)) IMPLIES sigma(k,j - 1,LAMBDA(i: Index[m]): F(i)) = sigma(k,j - 1,LAMBDA(i: Index[n]): G(i))
sigma_shift_gen: LEMMA FORALL (j: posnat, m,n: posnat,F: [below[m + n] -> real]): (j <= m IMPLIES sigma[below[m]](0,j - 1,LAMBDA (i: below[m]): F(i + n)) = sigma[below[m + n]](n,j - 1 + n, LAMBDA (i: below[m + n]): F(i)))
END sigma_lemmas
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
