equal
deleted
inserted
replaced
1065 shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" |
1065 shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" |
1066 proof transfer |
1066 proof transfer |
1067 fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y" |
1067 fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y" |
1068 moreover |
1068 moreover |
1069 from ereal_dense3[OF \<open>x < y\<close>] |
1069 from ereal_dense3[OF \<open>x < y\<close>] |
1070 obtain r where "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y" |
1070 obtain r where r: "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y" |
1071 by auto |
1071 by auto |
1072 moreover then have "0 \<le> r" |
1072 then have "0 \<le> r" |
1073 using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto |
1073 using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto |
1074 ultimately show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y" |
1074 with r show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y" |
1075 by (intro exI[of _ r]) (auto simp: max_absorb2) |
1075 by (intro exI[of _ r]) (auto simp: max_absorb2) |
1076 qed |
1076 qed |
1077 |
1077 |
1078 lemma ennreal_Ex_less_of_nat: "(x::ennreal) < top \<Longrightarrow> \<exists>n. x < of_nat n" |
1078 lemma ennreal_Ex_less_of_nat: "(x::ennreal) < top \<Longrightarrow> \<exists>n. x < of_nat n" |
1079 by (cases x rule: ennreal_cases) |
1079 by (cases x rule: ennreal_cases) |
1170 have "\<exists>y\<in>X. r < ennreal_of_enat y" if r: "r < top" for r |
1170 have "\<exists>y\<in>X. r < ennreal_of_enat y" if r: "r < top" for r |
1171 proof - |
1171 proof - |
1172 from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this |
1172 from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this |
1173 have "\<not> (X \<subseteq> enat ` {.. n})" |
1173 have "\<not> (X \<subseteq> enat ` {.. n})" |
1174 using \<open>infinite X\<close> by (auto dest: finite_subset) |
1174 using \<open>infinite X\<close> by (auto dest: finite_subset) |
1175 then obtain x where "x \<in> X" "x \<notin> enat ` {..n}" |
1175 then obtain x where x: "x \<in> X" "x \<notin> enat ` {..n}" |
1176 by blast |
1176 by blast |
1177 moreover then have "of_nat n \<le> x" |
1177 then have "of_nat n \<le> x" |
1178 by (cases x) (auto simp: of_nat_eq_enat) |
1178 by (cases x) (auto simp: of_nat_eq_enat) |
1179 ultimately show ?thesis |
1179 with x show ?thesis |
1180 by (auto intro!: bexI[of _ x] less_le_trans[OF n]) |
1180 by (auto intro!: bexI[of _ x] less_le_trans[OF n]) |
1181 qed |
1181 qed |
1182 then have "(SUP x : X. ennreal_of_enat x) = top" |
1182 then have "(SUP x : X. ennreal_of_enat x) = top" |
1183 by simp |
1183 by simp |
1184 then show "top \<le> (SUP x : X. ennreal_of_enat x)" |
1184 then show "top \<le> (SUP x : X. ennreal_of_enat x)" |