[isabelle] domain of function


Let A be a naive set, then is it true that
arbitrary \<in> A ?

The question arose when I tryed to prove the following:

domain_test::"['a set, nat, nat => 'a] => bool"
"domain_test A n f == f \<in> extensional {j. j \<le> n} \<and>
(\<forall>j \<le> n. f j \<in> A)"

lemma test:"[| domain_test A n f; domain_test A m f |] ==> n = m"

Is this lemma true? If this is true, is there any proof?

Hidetsune Kobayashi

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