[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


"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)"
  "big \<approx>  Emedding(embed, small, big)" and
  "small \<subseteq> Emedding(embed, small, big)"



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