equal
deleted
inserted
replaced
1103 lemma natLeq_on_injective_ordIso: |
1103 lemma natLeq_on_injective_ordIso: |
1104 "(natLeq_on m =o natLeq_on n) = (m = n)" |
1104 "(natLeq_on m =o natLeq_on n) = (m = n)" |
1105 proof(auto simp add: natLeq_on_Well_order ordIso_reflexive) |
1105 proof(auto simp add: natLeq_on_Well_order ordIso_reflexive) |
1106 assume "natLeq_on m =o natLeq_on n" |
1106 assume "natLeq_on m =o natLeq_on n" |
1107 then obtain f where "bij_betw f {x. x<m} {x. x<n}" |
1107 then obtain f where "bij_betw f {x. x<m} {x. x<n}" |
1108 using Field_natLeq_on assms unfolding ordIso_def iso_def[abs_def] by auto |
1108 using Field_natLeq_on unfolding ordIso_def iso_def[abs_def] by auto |
1109 thus "m = n" using atLeastLessThan_injective2[of f m n] |
1109 thus "m = n" using atLeastLessThan_injective2[of f m n] |
1110 unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast |
1110 unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast |
1111 qed |
1111 qed |
1112 |
1112 |
1113 |
1113 |