Re: [isabelle] Cancellation lemmas for setprod and setsum
On 12.08.2012 23:59, Manuel Eberl wrote:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and