61 lemma closed_contains_Sup_cl: |
61 lemma closed_contains_Sup_cl: |
62 fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set" |
62 fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set" |
63 assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S" |
63 assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S" |
64 proof - |
64 proof - |
65 from compact_eq_closed[of S] compact_attains_sup[of S] assms |
65 from compact_eq_closed[of S] compact_attains_sup[of S] assms |
66 obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto |
66 obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto |
67 moreover then have "Sup S = s" |
67 then have "Sup S = s" |
68 by (auto intro!: Sup_eqI) |
68 by (auto intro!: Sup_eqI) |
69 ultimately show ?thesis |
69 with S show ?thesis |
70 by simp |
70 by simp |
71 qed |
71 qed |
72 |
72 |
73 lemma closed_contains_Inf_cl: |
73 lemma closed_contains_Inf_cl: |
74 fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set" |
74 fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set" |
75 assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S" |
75 assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S" |
76 proof - |
76 proof - |
77 from compact_eq_closed[of S] compact_attains_inf[of S] assms |
77 from compact_eq_closed[of S] compact_attains_inf[of S] assms |
78 obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto |
78 obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto |
79 moreover then have "Inf S = s" |
79 then have "Inf S = s" |
80 by (auto intro!: Inf_eqI) |
80 by (auto intro!: Inf_eqI) |
81 ultimately show ?thesis |
81 with S show ?thesis |
82 by simp |
82 by simp |
83 qed |
83 qed |
84 |
84 |
85 lemma ereal_dense3: |
85 lemma ereal_dense3: |
86 fixes x y :: ereal shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" |
86 fixes x y :: ereal shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y" |