[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.