[isabelle] A new theorem about lambda
The following theorem is also missing in Isabelle/ZF core and should be added there:
lemma lam_is_fun: "f = (lam x:d. b(x)) ==> f: d->range(f)"
assume eq: "f = (lam x:d. b(x))"
have dom: "domain(f) = d" using domain_lam by (auto simp add: eq)
with eq have "function(f)" using function_lam by auto
with eq have "relation(f)" using relation_lam by auto
ultimately have "f: domain(f)->range(f)" by (rule function_imp_Pi)
with dom show ?thesis by auto
(I put it into my file ZF_Addons.thy.)
I'd like to hear a critique.
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and