equal
deleted
inserted
replaced
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) |