Re: [isabelle] Cancellation lemmas for setprod and setsum



On 12.08.2012 23:59, Manuel Eberl wrote:
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)"

Did you mean "div" instead of "/" or do you an implicit conversion to real in there?

> 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.

For sums, there is setsum_diff. For products, there is the question what the type class of the base type of A,B should be -- probably would need to be a field, to be useful (which then excludes the naturals).

Maybe one could generically prove "∏A = ∏(A-B) * ∏B" and derive your variant from there for specific types.

  -- Lars





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