# [isabelle] Fw: How to apply a theorem?

> Suppose (in ZF) we have two sets
> 'small' and 'big' (not necessarily disjoint)
> and an injection 'embed' from small to big. I want
> to replace 'big' with 'newbig' so that
> 'newbig' would bijectively correspond to
> 'big' but 'small' would become a subset of
> 'newbig'.
Technically, you can do it by removing the image of small from big and putting small in place of it. Something like this
theory test2 imports Cardinal
begin
definition
"Emedding(embed, small, big) \<equiv> small \<union> (big - embed``(small))"
text{*Embedding is bijective with big and small is contained in it.*}
lemma emmbed_prop: assumes "embed \<in> inj(small, big)"
shows
"big \<approx> Emedding(embed, small, big)" and
"small \<subseteq> Emedding(embed, small, big)"
sorry
Slawekk

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