equal
deleted
inserted
replaced
859 qed |
859 qed |
860 |
860 |
861 |
861 |
862 lemma finite_ordLess_infinite: |
862 lemma finite_ordLess_infinite: |
863 assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
863 assumes WELL: "Well_order r" and WELL': "Well_order r'" and |
864 FIN: "finite(Field r)" and INF: "infinite(Field r')" |
864 FIN: "finite(Field r)" and INF: "\<not>finite(Field r')" |
865 shows "r <o r'" |
865 shows "r <o r'" |
866 proof- |
866 proof- |
867 {assume "r' \<le>o r" |
867 {assume "r' \<le>o r" |
868 then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r" |
868 then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r" |
869 unfolding ordLeq_def using assms embed_inj_on embed_Field by blast |
869 unfolding ordLeq_def using assms embed_inj_on embed_Field by blast |