9 |
9 |
10 theory Extended_Real_Limits |
10 theory Extended_Real_Limits |
11 imports |
11 imports |
12 Topology_Euclidean_Space |
12 Topology_Euclidean_Space |
13 "~~/src/HOL/Library/Extended_Real" |
13 "~~/src/HOL/Library/Extended_Real" |
|
14 "~~/src/HOL/Library/Extended_Nonnegative_Real" |
14 "~~/src/HOL/Library/Indicator_Function" |
15 "~~/src/HOL/Library/Indicator_Function" |
15 begin |
16 begin |
16 |
17 |
17 lemma compact_UNIV: |
18 lemma compact_UNIV: |
18 "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" |
19 "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)" |
83 then show "open S" |
84 then show "open S" |
84 by induct auto |
85 by induct auto |
85 qed |
86 qed |
86 qed |
87 qed |
87 |
88 |
|
89 text \<open>This is a copy from \<open>ereal :: second_countable_topology\<close>. Maybe find a common super class of |
|
90 topological spaces where the rational numbers are densely embedded ?\<close> |
|
91 instance ennreal :: second_countable_topology |
|
92 proof (standard, intro exI conjI) |
|
93 let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ennreal set set)" |
|
94 show "countable ?B" |
|
95 by (auto intro: countable_rat) |
|
96 show "open = generate_topology ?B" |
|
97 proof (intro ext iffI) |
|
98 fix S :: "ennreal set" |
|
99 assume "open S" |
|
100 then show "generate_topology ?B S" |
|
101 unfolding open_generated_order |
|
102 proof induct |
|
103 case (Basis b) |
|
104 then obtain e where "b = {..<e} \<or> b = {e<..}" |
|
105 by auto |
|
106 moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}" |
|
107 by (auto dest: ennreal_rat_dense |
|
108 simp del: ex_simps |
|
109 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff) |
|
110 ultimately show ?case |
|
111 by (auto intro: generate_topology.intros) |
|
112 qed (auto intro: generate_topology.intros) |
|
113 next |
|
114 fix S |
|
115 assume "generate_topology ?B S" |
|
116 then show "open S" |
|
117 by induct auto |
|
118 qed |
|
119 qed |
|
120 |
88 lemma ereal_open_closed_aux: |
121 lemma ereal_open_closed_aux: |
89 fixes S :: "ereal set" |
122 fixes S :: "ereal set" |
90 assumes "open S" |
123 assumes "open S" |
91 and "closed S" |
124 and "closed S" |
92 and S: "(-\<infinity>) \<notin> S" |
125 and S: "(-\<infinity>) \<notin> S" |
93 shows "S = {}" |
126 shows "S = {}" |
94 proof (rule ccontr) |
127 proof (rule ccontr) |
95 assume "\<not> ?thesis" |
128 assume "\<not> ?thesis" |
96 then have *: "Inf S \<in> S" |
129 then have *: "Inf S \<in> S" |
97 |
130 |
98 by (metis assms(2) closed_contains_Inf_cl) |
131 by (metis assms(2) closed_contains_Inf_cl) |
99 { |
132 { |
100 assume "Inf S = -\<infinity>" |
133 assume "Inf S = -\<infinity>" |
101 then have False |
134 then have False |
102 using * assms(3) by auto |
135 using * assms(3) by auto |