[isabelle] Cancellation lemmas for setprod and setsum



Hallo,

I recently needed something like a "cancellation lemma" for setprod but
was unable to find anyting like it in the libraries.

The lemma I needed and proved was the following:
lemma setprod_cancel: fixes A::"nat set" and B::"nat set"
assumes "B ⊆ A" and "finite A" and "0 ∉ B" shows "∏A / ∏B = ∏(A-B)"

Is there a lemma like this somewhere? If yes, what is it called? If not,
it might be a good idea to add this (or a generalised version of this)
and a version for setsum to the libraries, since it seems like something
one needs quite often when dealing with products and sums.

Cheers,
Manuel





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.