src/HOL/Cardinals/Wellorder_Embedding_Base.thy
changeset 49753 a344f1a21211
parent 49310 6e30078de4f0
child 49922 b76937179ff5
equal deleted inserted replaced
49752:2bbb0013ff82 49753:a344f1a21211
   271   by (auto simp add: total_on_def)
   271   by (auto simp add: total_on_def)
   272 qed
   272 qed
   273 
   273 
   274 
   274 
   275 lemma embed_underS:
   275 lemma embed_underS:
   276 assumes WELL: "Well_order r" and WELL: "Well_order r'" and
   276 assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   277         EMB: "embed r r' f" and IN: "a \<in> Field r"
   277         EMB: "embed r r' f" and IN: "a \<in> Field r"
   278 shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
   278 shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
   279 proof-
   279 proof-
   280   have "bij_betw f (rel.under r a) (rel.under r' (f a))"
   280   have "bij_betw f (rel.under r a) (rel.under r' (f a))"
   281   using assms by (auto simp add: embed_def)
   281   using assms by (auto simp add: embed_def)