equal
deleted
inserted
replaced
31 *} |
31 *} |
32 |
32 |
33 text {* Only used in HOL/Import/HOL4Compat.thy; delete? *} |
33 text {* Only used in HOL/Import/HOL4Compat.thy; delete? *} |
34 |
34 |
35 lemma posreal_complete: |
35 lemma posreal_complete: |
36 assumes positive_P: "\<forall>x \<in> P. (0::real) < x" |
36 fixes P :: "real set" |
37 and not_empty_P: "\<exists>x. x \<in> P" |
37 assumes not_empty_P: "\<exists>x. x \<in> P" |
38 and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y" |
38 and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y" |
39 shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" |
39 shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" |
40 proof - |
40 proof - |
41 from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z" |
41 from upper_bound_Ex have "\<exists>z. \<forall>x\<in>P. x \<le> z" |
42 by (auto intro: less_imp_le) |
42 by (auto intro: less_imp_le) |