以下等式在伊莎贝尔中是否成立：
setprod f (UNIV :: 'n∷finite set) = setprod (λx. x) (f ` (UNIV :: 'n∷finite set))
如果是，我该如何证明？
(* tested with Isabelle2013-2 *)
theory Notepad
imports
Main
"~~/src/HOL/Library/Polynomial"
begin
notepad
begin{
fix f :: "'n∷finite ⇒ ('a::comm_ring_1 poly)"
have "finite (UNIV :: 'n∷finite set)" by simp
from this have "setprod f (UNIV :: 'n∷finite set) = setprod (λx. x) (f ` (UNIV :: 'n∷finite set))"
sorry (* can this be proven ? *)
仅当您添加假设时，引理才成立inj f说明f是单射的。然后引理来自库引理setprod_reindex_id，可以使用命令找到find_theorems setprod image.
setprod_reindex_id [unfolded id_def]为您提供您所要求的引理的通用版本。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
