I developed the first version of my first real theory, ZF_Addons.thy, suggested additions to core of Isabelle/ZF
I suggest to add it to IsarMathLib but because it is my first work in this area I want first hear your replies. Is it done in a good way? What may be changed? What may be simplified? What else you may suggest?
Should I import Main_ZF here? If not what to import instead?
lemma inj_inj_range: "f: inj(A,B) ==> f : inj(A,range(f))"
apply (unfold inj_def)
apply (auto simp add: Pi_iff function_def)
lemma inj_bij_range: "f: inj(A,B) ==> f : bij(A,range(f))"
apply (auto simp add: bij_def inj_inj_range)
apply (blast intro: inj_is_fun fun_is_surj elim:)
lemma range_subset: "f: A->B ==> range(f) <= B"
assume "f: A->B"
hence "f: Pow(A*B)" by (simp add: Pi_def)
hence "f <= A*B" by auto
hence "range(A*B) <= B" by auto
ultimately show "range(f) <= B" by auto
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and