Email Gateway (Aug 18 2022 at 16:43): Email Gateway (Aug 18 2022 at 16:43):From: Victor Porton <porton@narod.ru>
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)"
proof -
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
moreover
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
qed
(I put it into my file ZF_Addons.thy.)
I'd like to hear a critique.
\--
Victor Porton - http://portonvictor.org
Last updated: Apr 25 2024 at 04:18 UTC