equal
deleted
inserted
replaced
1087 done |
1087 done |
1088 |
1088 |
1089 lemma finite_less_ub: |
1089 lemma finite_less_ub: |
1090 "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}" |
1090 "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}" |
1091 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) |
1091 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) |
|
1092 |
|
1093 lemma bounded_Max_nat: |
|
1094 fixes P :: "nat \<Rightarrow> bool" |
|
1095 assumes x: "P x" and M: "\<And>x. P x \<Longrightarrow> x \<le> M" |
|
1096 obtains m where "P m" "\<And>x. P x \<Longrightarrow> x \<le> m" |
|
1097 proof - |
|
1098 have "finite {x. P x}" |
|
1099 using M finite_nat_set_iff_bounded_le by auto |
|
1100 then have "Max {x. P x} \<in> {x. P x}" |
|
1101 using Max_in x by auto |
|
1102 then show ?thesis |
|
1103 by (simp add: \<open>finite {x. P x}\<close> that) |
|
1104 qed |
1092 |
1105 |
1093 |
1106 |
1094 text\<open>Any subset of an interval of natural numbers the size of the |
1107 text\<open>Any subset of an interval of natural numbers the size of the |
1095 subset is exactly that interval.\<close> |
1108 subset is exactly that interval.\<close> |
1096 |
1109 |