이자벨 : 이자벨에서 다음 평등 보류 setprod

Question

와 문제를합니까 : 어떻게 그것을 예라면

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 ? *) 

Answer 1

보조 정리는 가정 inj f는 f가 단사했다는 설명이 추가 경우에만 보유하고 있습니다. 보조 정리는 도서관 보조 정리 setprod_reindex_id에서 따릅니다.이 보조 표는 find_theorems setprod image 명령을 사용하여 찾을 수 있습니다.

setprod_reindex_id [unfolded id_def]은 요청한 보조 정리의 일반화 된 버전을 제공합니다.