From b5f51e592232d16fb1286f059a597c8ab443b4c4 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 18 Dec 2012 13:41:34 +0000 Subject: [PATCH] addenda --- matita/matita/lib/arithmetics/sigma_pi.ma | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma index 32153b352..7e3fe19f0 100644 --- a/matita/matita/lib/arithmetics/sigma_pi.ma +++ b/matita/matita/lib/arithmetics/sigma_pi.ma @@ -178,3 +178,11 @@ theorem exp_pi: ∀n,m,p,f. |#m1 #Hind >times_pi >Hind % ] qed. + +theorem exp_sigma_l: ∀n,a,p,f. + ∏_{i < n | p i} (exp a (f i)) = exp a (∑_{i < n | p i}(f i)). +#n #a #p #f elim n // #i #Hind cases (true_or_false (p i)) #Hc + [>bigop_Strue [>bigop_Strue [>Hind >exp_plus_times // |//] |//] + |>bigop_Sfalse [>bigop_Sfalse [@Hind|//] | //] + ] +qed. -- 2.39.2