[isabelle] One more theorem missing in ZF



It seems that the following theorem is also forgotten in ZF:
 
lemma fun_range_subset: "f: A->B ==> range(f) <= B" sorry
 
What is the best way to prove it? (Ideally I would like to see both apply-style and ISAR proofs.)
 
I started to maintain the theory ZF_Addons, a theory where lemmas forgotten in ZF would be stored until they will be added to the ZF core in a next release of Isabelle. (I plan to submit this to IsarMathLib.)
 
--
Victor Porton - http://portonvictor.org


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