Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] One more theorem missing in ZF

view this post on Zulip Email Gateway (Aug 18 2022 at 16:43):

From: Victor Porton <porton@narod.ru>
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

Last updated: May 07 2024 at 01:07 UTC