45 by (auto simp: support_on_def) |
45 by (auto simp: support_on_def) |
46 |
46 |
47 lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}" |
47 lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}" |
48 by (auto simp: support_on_def) |
48 by (auto simp: support_on_def) |
49 |
49 |
50 lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support_on s f)" |
50 lemma finite_support[intro]: "finite S \<Longrightarrow> finite (support_on S f)" |
51 unfolding support_on_def by auto |
51 unfolding support_on_def by auto |
52 |
52 |
53 (* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) |
53 (* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *) |
54 definition (in comm_monoid_add) supp_sum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a" |
54 definition (in comm_monoid_add) supp_sum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a" |
55 where "supp_sum f s = (\<Sum>x\<in>support_on s f. f x)" |
55 where "supp_sum f S = (\<Sum>x\<in>support_on S f. f x)" |
56 |
56 |
57 lemma supp_sum_empty[simp]: "supp_sum f {} = 0" |
57 lemma supp_sum_empty[simp]: "supp_sum f {} = 0" |
58 unfolding supp_sum_def by auto |
58 unfolding supp_sum_def by auto |
59 |
59 |
60 lemma supp_sum_insert[simp]: |
60 lemma supp_sum_insert[simp]: |
61 "finite (support_on s f) \<Longrightarrow> |
61 "finite (support_on S f) \<Longrightarrow> |
62 supp_sum f (insert x s) = (if x \<in> s then supp_sum f s else f x + supp_sum f s)" |
62 supp_sum f (insert x S) = (if x \<in> S then supp_sum f S else f x + supp_sum f S)" |
63 by (simp add: supp_sum_def in_support_on insert_absorb) |
63 by (simp add: supp_sum_def in_support_on insert_absorb) |
64 |
64 |
65 lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\<lambda>n. f n / r) A" |
65 lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\<lambda>n. f n / r) A" |
66 by (cases "r = 0") |
66 by (cases "r = 0") |
67 (auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong) |
67 (auto simp: supp_sum_def sum_divide_distrib intro!: sum.cong support_on_cong) |
68 |
68 |
69 (*END OF SUPPORT, ETC.*) |
69 (*END OF SUPPORT, ETC.*) |
70 |
70 |
71 lemma image_affinity_interval: |
71 lemma image_affinity_interval: |
72 fixes c :: "'a::ordered_real_vector" |
72 fixes c :: "'a::ordered_real_vector" |
73 shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {} |
73 shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = |
74 else if 0 <= m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} |
74 (if {a..b}={} then {} |
|
75 else if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} |
75 else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" |
76 else {m *\<^sub>R b + c .. m *\<^sub>R a + c})" |
76 apply (case_tac "m=0", force) |
77 (is "?lhs = ?rhs") |
77 apply (auto simp: scaleR_left_mono) |
78 proof (cases "m=0") |
78 apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg) |
79 case True |
79 apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive) |
80 then show ?thesis |
80 apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq) |
81 by force |
81 using le_diff_eq scaleR_le_cancel_left_neg |
82 next |
82 apply fastforce |
83 case False |
83 done |
84 show ?thesis |
|
85 proof |
|
86 show "?lhs \<subseteq> ?rhs" |
|
87 by (auto simp: scaleR_left_mono scaleR_left_mono_neg) |
|
88 show "?rhs \<subseteq> ?lhs" |
|
89 proof (clarsimp, intro conjI impI subsetI) |
|
90 show "\<lbrakk>0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}\<rbrakk> |
|
91 \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x |
|
92 apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) |
|
93 using False apply (auto simp: le_diff_eq pos_le_divideRI) |
|
94 using diff_le_eq pos_le_divideR_eq by force |
|
95 show "\<lbrakk>\<not> 0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk> |
|
96 \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x |
|
97 apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI) |
|
98 apply (auto simp: diff_le_eq neg_le_divideR_eq) |
|
99 using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce |
|
100 qed |
|
101 qed |
|
102 qed |
84 |
103 |
85 lemma countable_PiE: |
104 lemma countable_PiE: |
86 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)" |
105 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)" |
87 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
106 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
88 |
107 |
284 using countable_dense_exists by blast |
303 using countable_dense_exists by blast |
285 |
304 |
286 end |
305 end |
287 |
306 |
288 lemma (in first_countable_topology) first_countable_basisE: |
307 lemma (in first_countable_topology) first_countable_basisE: |
289 obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
308 fixes x :: 'a |
290 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" |
309 obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A" |
291 using first_countable_basis[of x] |
310 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)" |
292 apply atomize_elim |
311 proof - |
293 apply (elim exE) |
312 obtain \<A> where \<A>: "(\<forall>i::nat. x \<in> \<A> i \<and> open (\<A> i))" "(\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))" |
294 apply (rule_tac x="range A" in exI, auto) |
313 using first_countable_basis[of x] by metis |
295 done |
314 show thesis |
|
315 proof |
|
316 show "countable (range \<A>)" |
|
317 by simp |
|
318 qed (use \<A> in auto) |
|
319 qed |
296 |
320 |
297 lemma (in first_countable_topology) first_countable_basis_Int_stableE: |
321 lemma (in first_countable_topology) first_countable_basis_Int_stableE: |
298 obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
322 obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A" |
299 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)" |
323 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)" |
300 "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A" |
324 "\<And>A B. A \<in> \<A> \<Longrightarrow> B \<in> \<A> \<Longrightarrow> A \<inter> B \<in> \<A>" |
301 proof atomize_elim |
325 proof atomize_elim |
302 obtain A' where A': |
326 obtain \<B> where \<B>: |
303 "countable A'" |
327 "countable \<B>" |
304 "\<And>a. a \<in> A' \<Longrightarrow> x \<in> a" |
328 "\<And>B. B \<in> \<B> \<Longrightarrow> x \<in> B" |
305 "\<And>a. a \<in> A' \<Longrightarrow> open a" |
329 "\<And>B. B \<in> \<B> \<Longrightarrow> open B" |
306 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S" |
330 "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>B\<in>\<B>. B \<subseteq> S" |
307 by (rule first_countable_basisE) blast |
331 by (rule first_countable_basisE) blast |
308 define A where [abs_def]: |
332 define \<A> where [abs_def]: |
309 "A = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)" |
333 "\<A> = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into \<B> n) ` N)) ` (Collect finite::nat set set)" |
310 then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and> |
334 then show "\<exists>\<A>. countable \<A> \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> x \<in> A) \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> open A) \<and> |
311 (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" |
335 (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)) \<and> (\<forall>A B. A \<in> \<A> \<longrightarrow> B \<in> \<A> \<longrightarrow> A \<inter> B \<in> \<A>)" |
312 proof (safe intro!: exI[where x=A]) |
336 proof (safe intro!: exI[where x=\<A>]) |
313 show "countable A" |
337 show "countable \<A>" |
314 unfolding A_def by (intro countable_image countable_Collect_finite) |
338 unfolding \<A>_def by (intro countable_image countable_Collect_finite) |
315 fix a |
339 fix A |
316 assume "a \<in> A" |
340 assume "A \<in> \<A>" |
317 then show "x \<in> a" "open a" |
341 then show "x \<in> A" "open A" |
318 using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into) |
342 using \<B>(4)[OF open_UNIV] by (auto simp: \<A>_def intro: \<B> from_nat_into) |
319 next |
343 next |
320 let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)" |
344 let ?int = "\<lambda>N. \<Inter>(from_nat_into \<B> ` N)" |
321 fix a b |
345 fix A B |
322 assume "a \<in> A" "b \<in> A" |
346 assume "A \<in> \<A>" "B \<in> \<A>" |
323 then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" |
347 then obtain N M where "A = ?int N" "B = ?int M" "finite (N \<union> M)" |
324 by (auto simp: A_def) |
348 by (auto simp: \<A>_def) |
325 then show "a \<inter> b \<in> A" |
349 then show "A \<inter> B \<in> \<A>" |
326 by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"]) |
350 by (auto simp: \<A>_def intro!: image_eqI[where x="N \<union> M"]) |
327 next |
351 next |
328 fix S |
352 fix S |
329 assume "open S" "x \<in> S" |
353 assume "open S" "x \<in> S" |
330 then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast |
354 then obtain a where a: "a\<in>\<B>" "a \<subseteq> S" using \<B> by blast |
331 then show "\<exists>a\<in>A. a \<subseteq> S" using a A' |
355 then show "\<exists>a\<in>\<A>. a \<subseteq> S" using a \<B> |
332 by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"]) |
356 by (intro bexI[where x=a]) (auto simp: \<A>_def intro: image_eqI[where x="{to_nat_on \<B> a}"]) |
333 qed |
357 qed |
334 qed |
358 qed |
335 |
359 |
336 lemma (in topological_space) first_countableI: |
360 lemma (in topological_space) first_countableI: |
337 assumes "countable A" |
361 assumes "countable \<A>" |
338 and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a" |
362 and 1: "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A" |
339 and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" |
363 and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>A\<in>\<A>. A \<subseteq> S" |
340 shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
364 shows "\<exists>\<A>::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> \<A> i \<and> open (\<A> i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))" |
341 proof (safe intro!: exI[of _ "from_nat_into A"]) |
365 proof (safe intro!: exI[of _ "from_nat_into \<A>"]) |
342 fix i |
366 fix i |
343 have "A \<noteq> {}" using 2[of UNIV] by auto |
367 have "\<A> \<noteq> {}" using 2[of UNIV] by auto |
344 show "x \<in> from_nat_into A i" "open (from_nat_into A i)" |
368 show "x \<in> from_nat_into \<A> i" "open (from_nat_into \<A> i)" |
345 using range_from_nat_into_subset[OF \<open>A \<noteq> {}\<close>] 1 by auto |
369 using range_from_nat_into_subset[OF \<open>\<A> \<noteq> {}\<close>] 1 by auto |
346 next |
370 next |
347 fix S |
371 fix S |
348 assume "open S" "x\<in>S" from 2[OF this] |
372 assume "open S" "x\<in>S" from 2[OF this] |
349 show "\<exists>i. from_nat_into A i \<subseteq> S" |
373 show "\<exists>i. from_nat_into \<A> i \<subseteq> S" |
350 using subset_range_from_nat_into[OF \<open>countable A\<close>] by auto |
374 using subset_range_from_nat_into[OF \<open>countable \<A>\<close>] by auto |
351 qed |
375 qed |
352 |
376 |
353 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology |
377 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology |
354 proof |
378 proof |
355 fix x :: "'a \<times> 'b" |
379 fix x :: "'a \<times> 'b" |
356 obtain A where A: |
380 obtain \<A> where \<A>: |
357 "countable A" |
381 "countable \<A>" |
358 "\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a" |
382 "\<And>a. a \<in> \<A> \<Longrightarrow> fst x \<in> a" |
359 "\<And>a. a \<in> A \<Longrightarrow> open a" |
383 "\<And>a. a \<in> \<A> \<Longrightarrow> open a" |
360 "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S" |
384 "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>\<A>. a \<subseteq> S" |
361 by (rule first_countable_basisE[of "fst x"]) blast |
385 by (rule first_countable_basisE[of "fst x"]) blast |
362 obtain B where B: |
386 obtain B where B: |
363 "countable B" |
387 "countable B" |
364 "\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a" |
388 "\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a" |
365 "\<And>a. a \<in> B \<Longrightarrow> open a" |
389 "\<And>a. a \<in> B \<Longrightarrow> open a" |
366 "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S" |
390 "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S" |
367 by (rule first_countable_basisE[of "snd x"]) blast |
391 by (rule first_countable_basisE[of "snd x"]) blast |
368 show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. |
392 show "\<exists>\<A>::nat \<Rightarrow> ('a \<times> 'b) set. |
369 (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
393 (\<forall>i. x \<in> \<A> i \<and> open (\<A> i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))" |
370 proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe) |
394 proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B)"], safe) |
371 fix a b |
395 fix a b |
372 assume x: "a \<in> A" "b \<in> B" |
396 assume x: "a \<in> \<A>" "b \<in> B" |
373 with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)" |
397 show "x \<in> a \<times> b" |
374 unfolding mem_Times_iff |
398 by (simp add: \<A>(2) B(2) mem_Times_iff x) |
375 by (auto intro: open_Times) |
399 show "open (a \<times> b)" |
|
400 by (simp add: \<A>(3) B(3) open_Times x) |
376 next |
401 next |
377 fix S |
402 fix S |
378 assume "open S" "x \<in> S" |
403 assume "open S" "x \<in> S" |
379 then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S" |
404 then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S" |
380 by (rule open_prod_elim) |
405 by (rule open_prod_elim) |
381 moreover |
406 moreover |
382 from a'b' A(4)[of a'] B(4)[of b'] |
407 from a'b' \<A>(4)[of a'] B(4)[of b'] |
383 obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" |
408 obtain a b where "a \<in> \<A>" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" |
384 by auto |
409 by auto |
385 ultimately |
410 ultimately |
386 show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S" |
411 show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B). a \<subseteq> S" |
387 by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) |
412 by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b]) |
388 qed (simp add: A B) |
413 qed (simp add: \<A> B) |
389 qed |
414 qed |
390 |
415 |
391 class second_countable_topology = topological_space + |
416 class second_countable_topology = topological_space + |
392 assumes ex_countable_subbasis: |
417 assumes ex_countable_subbasis: |
393 "\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B" |
418 "\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B" |
960 from 1 2 show ?lhs |
985 from 1 2 show ?lhs |
961 unfolding openin_open open_dist by fast |
986 unfolding openin_open open_dist by fast |
962 qed |
987 qed |
963 |
988 |
964 lemma connected_openin: |
989 lemma connected_openin: |
965 "connected s \<longleftrightarrow> |
990 "connected S \<longleftrightarrow> |
966 ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and> |
991 ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and> |
967 openin (subtopology euclidean s) e2 \<and> |
992 openin (subtopology euclidean S) E2 \<and> |
968 s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})" |
993 S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})" |
969 apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe) |
994 apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe) |
970 apply (simp_all, blast+) (* SLOW *) |
995 apply (simp_all, blast+) (* SLOW *) |
971 done |
996 done |
972 |
997 |
973 lemma connected_openin_eq: |
998 lemma connected_openin_eq: |
974 "connected s \<longleftrightarrow> |
999 "connected S \<longleftrightarrow> |
975 ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and> |
1000 ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and> |
976 openin (subtopology euclidean s) e2 \<and> |
1001 openin (subtopology euclidean S) E2 \<and> |
977 e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and> |
1002 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and> |
978 e1 \<noteq> {} \<and> e2 \<noteq> {})" |
1003 E1 \<noteq> {} \<and> E2 \<noteq> {})" |
979 apply (simp add: connected_openin, safe, blast) |
1004 apply (simp add: connected_openin, safe, blast) |
980 by (metis Int_lower1 Un_subset_iff openin_open subset_antisym) |
1005 by (metis Int_lower1 Un_subset_iff openin_open subset_antisym) |
981 |
1006 |
982 lemma connected_closedin: |
1007 lemma connected_closedin: |
983 "connected s \<longleftrightarrow> |
1008 "connected S \<longleftrightarrow> |
984 ~(\<exists>e1 e2. |
1009 (\<nexists>E1 E2. |
985 closedin (subtopology euclidean s) e1 \<and> |
1010 closedin (subtopology euclidean S) E1 \<and> |
986 closedin (subtopology euclidean s) e2 \<and> |
1011 closedin (subtopology euclidean S) E2 \<and> |
987 s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> |
1012 S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})" |
988 e1 \<noteq> {} \<and> e2 \<noteq> {})" |
1013 (is "?lhs = ?rhs") |
989 proof - |
1014 proof |
990 { fix A B x x' |
1015 assume ?lhs |
991 assume s_sub: "s \<subseteq> A \<union> B" |
1016 then show ?rhs |
992 and disj: "A \<inter> B \<inter> s = {}" |
1017 by (auto simp add: connected_closed closedin_closed) |
993 and x: "x \<in> s" "x \<in> B" and x': "x' \<in> s" "x' \<in> A" |
1018 next |
994 and cl: "closed A" "closed B" |
1019 assume R: ?rhs |
995 assume "\<forall>e1. (\<forall>T. closed T \<longrightarrow> e1 \<noteq> s \<inter> T) \<or> (\<forall>e2. e1 \<inter> e2 = {} \<longrightarrow> s \<subseteq> e1 \<union> e2 \<longrightarrow> (\<forall>T. closed T \<longrightarrow> e2 \<noteq> s \<inter> T) \<or> e1 = {} \<or> e2 = {})" |
1020 then show ?lhs |
996 then have "\<And>C D. s \<inter> C = {} \<or> s \<inter> D = {} \<or> s \<inter> (C \<inter> (s \<inter> D)) \<noteq> {} \<or> \<not> s \<subseteq> s \<inter> (C \<union> D) \<or> \<not> closed C \<or> \<not> closed D" |
1021 proof (clarsimp simp add: connected_closed closedin_closed) |
997 by (metis (no_types) Int_Un_distrib Int_assoc) |
1022 fix A B |
998 moreover have "s \<inter> (A \<inter> B) = {}" "s \<inter> (A \<union> B) = s" "s \<inter> B \<noteq> {}" |
1023 assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}" |
999 using disj s_sub x by blast+ |
1024 and disj: "A \<inter> B \<inter> S = {}" |
1000 ultimately have "s \<inter> A = {}" |
1025 and cl: "closed A" "closed B" |
1001 using cl by (metis inf.left_commute inf_bot_right order_refl) |
1026 have "S \<inter> (A \<union> B) = S" |
1002 then have False |
1027 using s_sub(1) by auto |
1003 using x' by blast |
1028 have "S - A = B \<inter> S" |
1004 } note * = this |
1029 using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto |
1005 show ?thesis |
1030 then have "S \<inter> A = {}" |
1006 apply (simp add: connected_closed closedin_closed) |
1031 by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2)) |
1007 apply (safe; simp) |
1032 then show "A \<inter> S = {}" |
1008 apply blast |
1033 by blast |
1009 apply (blast intro: *) |
1034 qed |
1010 done |
|
1011 qed |
1035 qed |
1012 |
1036 |
1013 lemma connected_closedin_eq: |
1037 lemma connected_closedin_eq: |
1014 "connected s \<longleftrightarrow> |
1038 "connected S \<longleftrightarrow> |
1015 ~(\<exists>e1 e2. |
1039 ~(\<exists>E1 E2. |
1016 closedin (subtopology euclidean s) e1 \<and> |
1040 closedin (subtopology euclidean S) E1 \<and> |
1017 closedin (subtopology euclidean s) e2 \<and> |
1041 closedin (subtopology euclidean S) E2 \<and> |
1018 e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and> |
1042 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and> |
1019 e1 \<noteq> {} \<and> e2 \<noteq> {})" |
1043 E1 \<noteq> {} \<and> E2 \<noteq> {})" |
1020 apply (simp add: connected_closedin, safe, blast) |
1044 apply (simp add: connected_closedin, safe, blast) |
1021 by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym) |
1045 by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym) |
1022 |
1046 |
1023 text \<open>These "transitivity" results are handy too\<close> |
1047 text \<open>These "transitivity" results are handy too\<close> |
1024 |
1048 |
1660 shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1) |
1684 shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1) |
1661 and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2) |
1685 and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2) |
1662 and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3) |
1686 and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3) |
1663 and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4) |
1687 and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4) |
1664 proof - |
1688 proof - |
1665 show ?th1 |
1689 let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" |
1666 unfolding subset_eq and Ball_def and mem_box |
1690 let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
1667 by (auto intro: order_trans) |
1691 show ?th1 ?th2 |
1668 show ?th2 |
1692 by (fastforce simp: mem_box)+ |
1669 unfolding subset_eq and Ball_def and mem_box |
1693 have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
1670 by (auto intro: le_less_trans less_le_trans order_trans less_imp_le) |
1694 if i: "i \<in> Basis" and box: "box c d \<subseteq> cbox a b" and cd: "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i |
1671 { |
1695 proof - |
1672 assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" |
1696 have "box c d \<noteq> {}" |
1673 then have "box c d \<noteq> {}" |
1697 using that |
1674 unfolding box_eq_empty by auto |
1698 unfolding box_eq_empty by force |
1675 fix i :: 'a |
1699 { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
1676 assume i: "i \<in> Basis" |
1700 assume *: "a\<bullet>i > c\<bullet>i" |
1677 (** TODO combine the following two parts as done in the HOL_light version. **) |
1701 then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j |
1678 { |
1702 using cd that by (fastforce simp add: i *) |
1679 let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
1703 then have "?x \<in> box c d" |
1680 assume as2: "a\<bullet>i > c\<bullet>i" |
1704 unfolding mem_box by auto |
1681 { |
1705 moreover have "?x \<notin> cbox a b" |
1682 fix j :: 'a |
1706 using i cd * by (force simp: mem_box) |
1683 assume j: "j \<in> Basis" |
1707 ultimately have False using box by auto |
1684 then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" |
|
1685 apply (cases "j = i") |
|
1686 using as(2)[THEN bspec[where x=j]] i |
|
1687 apply (auto simp: as2) |
|
1688 done |
|
1689 } |
|
1690 then have "?x\<in>box c d" |
|
1691 using i unfolding mem_box by auto |
|
1692 moreover |
|
1693 have "?x \<notin> cbox a b" |
|
1694 unfolding mem_box |
|
1695 apply auto |
|
1696 apply (rule_tac x=i in bexI) |
|
1697 using as(2)[THEN bspec[where x=i]] and as2 i |
|
1698 apply auto |
|
1699 done |
|
1700 ultimately have False using as by auto |
|
1701 } |
1708 } |
1702 then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto |
1709 then have "a\<bullet>i \<le> c\<bullet>i" by force |
1703 moreover |
1710 moreover |
1704 { |
1711 { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
1705 let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
1712 assume *: "b\<bullet>i < d\<bullet>i" |
1706 assume as2: "b\<bullet>i < d\<bullet>i" |
1713 then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j |
1707 { |
1714 using cd that by (fastforce simp add: i *) |
1708 fix j :: 'a |
1715 then have "?x \<in> box c d" |
1709 assume "j\<in>Basis" |
|
1710 then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" |
|
1711 apply (cases "j = i") |
|
1712 using as(2)[THEN bspec[where x=j]] |
|
1713 apply (auto simp: as2) |
|
1714 done |
|
1715 } |
|
1716 then have "?x\<in>box c d" |
|
1717 unfolding mem_box by auto |
1716 unfolding mem_box by auto |
1718 moreover |
1717 moreover have "?x \<notin> cbox a b" |
1719 have "?x\<notin>cbox a b" |
1718 using i cd * by (force simp: mem_box) |
1720 unfolding mem_box |
1719 ultimately have False using box by auto |
1721 apply auto |
|
1722 apply (rule_tac x=i in bexI) |
|
1723 using as(2)[THEN bspec[where x=i]] and as2 using i |
|
1724 apply auto |
|
1725 done |
|
1726 ultimately have False using as by auto |
|
1727 } |
1720 } |
1728 then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto |
1721 then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto |
1729 ultimately |
1722 ultimately show ?thesis by auto |
1730 have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto |
1723 qed |
1731 } note part1 = this |
|
1732 show ?th3 |
1724 show ?th3 |
1733 unfolding subset_eq and Ball_def and mem_box |
1725 using acdb by (fastforce simp add: mem_box) |
1734 apply (rule, rule, rule, rule) |
1726 have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
1735 apply (rule part1) |
1727 if "i \<in> Basis" "box c d \<subseteq> box a b" "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i |
1736 unfolding subset_eq and Ball_def and mem_box |
1728 using box_subset_cbox[of a b] that acdb by auto |
1737 prefer 4 |
|
1738 apply auto |
|
1739 apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+ |
|
1740 done |
|
1741 { |
|
1742 assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" |
|
1743 fix i :: 'a |
|
1744 assume i:"i\<in>Basis" |
|
1745 from as(1) have "box c d \<subseteq> cbox a b" |
|
1746 using box_subset_cbox[of a b] by auto |
|
1747 then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
|
1748 using part1 and as(2) using i by auto |
|
1749 } note * = this |
|
1750 show ?th4 |
1729 show ?th4 |
1751 unfolding subset_eq and Ball_def and mem_box |
1730 using acdb' by (fastforce simp add: mem_box) |
1752 apply (rule, rule, rule, rule) |
|
1753 apply (rule *) |
|
1754 unfolding subset_eq and Ball_def and mem_box |
|
1755 prefer 4 |
|
1756 apply auto |
|
1757 apply (erule_tac x=xa in allE, simp)+ |
|
1758 done |
|
1759 qed |
1731 qed |
1760 |
1732 |
1761 lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d" |
1733 lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d" |
1762 (is "?lhs = ?rhs") |
1734 (is "?lhs = ?rhs") |
1763 proof |
1735 proof |
1773 qed |
1745 qed |
1774 |
1746 |
1775 lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}" |
1747 lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}" |
1776 (is "?lhs \<longleftrightarrow> ?rhs") |
1748 (is "?lhs \<longleftrightarrow> ?rhs") |
1777 proof |
1749 proof |
1778 assume ?lhs |
1750 assume L: ?lhs |
1779 then have "cbox a b \<subseteq> box c d" "box c d \<subseteq>cbox a b" |
1751 then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b" |
1780 by auto |
1752 by auto |
1781 then show ?rhs |
1753 then show ?rhs |
1782 apply (simp add: subset_box) |
1754 apply (simp add: subset_box) |
1783 using \<open>cbox a b = box c d\<close> box_ne_empty box_sing |
1755 using L box_ne_empty box_sing apply (fastforce simp add:) |
1784 apply (fastforce simp add:) |
|
1785 done |
1756 done |
1786 next |
1757 qed force |
1787 assume ?rhs |
|
1788 then show ?lhs |
|
1789 by force |
|
1790 qed |
|
1791 |
1758 |
1792 lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}" |
1759 lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}" |
1793 by (metis eq_cbox_box) |
1760 by (metis eq_cbox_box) |
1794 |
1761 |
1795 lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d" |
1762 lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d" |
1796 (is "?lhs \<longleftrightarrow> ?rhs") |
1763 (is "?lhs \<longleftrightarrow> ?rhs") |
1797 proof |
1764 proof |
1798 assume ?lhs |
1765 assume L: ?lhs |
1799 then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b" |
1766 then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b" |
1800 by auto |
1767 by auto |
1801 then show ?rhs |
1768 then show ?rhs |
1802 apply (simp add: subset_box) |
1769 apply (simp add: subset_box) |
1803 using box_ne_empty(2) \<open>box a b = box c d\<close> |
1770 using box_ne_empty(2) L |
1804 apply auto |
1771 apply auto |
1805 apply (meson euclidean_eqI less_eq_real_def not_less)+ |
1772 apply (meson euclidean_eqI less_eq_real_def not_less)+ |
1806 done |
1773 done |
1807 next |
1774 qed force |
1808 assume ?rhs |
|
1809 then show ?lhs |
|
1810 by force |
|
1811 qed |
|
1812 |
1775 |
1813 lemma subset_box_complex: |
1776 lemma subset_box_complex: |
1814 "cbox a b \<subseteq> cbox c d \<longleftrightarrow> |
1777 "cbox a b \<subseteq> cbox c d \<longleftrightarrow> |
1815 (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d" |
1778 (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d" |
1816 "cbox a b \<subseteq> box c d \<longleftrightarrow> |
1779 "cbox a b \<subseteq> box c d \<longleftrightarrow> |
5943 fix i :: 'a |
5892 fix i :: 'a |
5944 assume i: "i \<in> Basis" |
5893 assume i: "i \<in> Basis" |
5945 have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)" |
5894 have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)" |
5946 unfolding left_diff_distrib by simp |
5895 unfolding left_diff_distrib by simp |
5947 also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
5896 also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
5948 apply (rule add_less_le_mono) |
5897 proof (rule add_less_le_mono) |
5949 using e unfolding mult_less_cancel_left and mult_le_cancel_left |
5898 show "e * (a \<bullet> i) < e * (x \<bullet> i)" |
5950 apply simp_all |
5899 using \<open>0 < e\<close> i mem_box(1) x by auto |
5951 using x unfolding mem_box using i |
5900 show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)" |
5952 apply simp |
5901 by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y) |
5953 using y unfolding mem_box using i |
5902 qed |
5954 apply simp |
|
5955 done |
|
5956 finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i" |
5903 finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i" |
5957 unfolding inner_simps by auto |
5904 unfolding inner_simps by auto |
5958 moreover |
5905 moreover |
5959 { |
5906 { |
5960 have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)" |
5907 have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)" |
5961 unfolding left_diff_distrib by simp |
5908 unfolding left_diff_distrib by simp |
5962 also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
5909 also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
5963 proof (rule add_less_le_mono) |
5910 proof (rule add_less_le_mono) |
5964 show "e * (x \<bullet> i) < e * (b \<bullet> i)" |
5911 show "e * (x \<bullet> i) < e * (b \<bullet> i)" |
5965 using e(1) i mem_box(1) x by auto |
5912 using \<open>0 < e\<close> i mem_box(1) x by auto |
5966 show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)" |
5913 show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)" |
5967 by (meson diff_ge_0_iff_ge e(2) i mem_box(2) ordered_comm_semiring_class.comm_mult_left_mono y) |
5914 by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y) |
5968 qed |
5915 qed |
5969 finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
5916 finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
5970 unfolding inner_simps by auto |
5917 unfolding inner_simps by auto |
5971 } |
5918 } |
5972 ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
5919 ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
6029 using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
5971 using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
6030 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] |
5972 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] |
6031 by auto |
5973 by auto |
6032 } |
5974 } |
6033 ultimately have "x \<in> closure (box a b)" |
5975 ultimately have "x \<in> closure (box a b)" |
6034 using as and box_midpoint[OF assms] |
5976 using as box_midpoint[OF assms] |
6035 unfolding closure_def |
5977 unfolding closure_def islimpt_sequential |
6036 unfolding islimpt_sequential |
|
6037 by (cases "x=?c") (auto simp: in_box_eucl_less) |
5978 by (cases "x=?c") (auto simp: in_box_eucl_less) |
6038 } |
5979 } |
6039 then show ?thesis |
5980 then show ?thesis |
6040 using closure_minimal[OF box_subset_cbox, of a b] by blast |
5981 using closure_minimal[OF box_subset_cbox, of a b] by blast |
6041 qed |
5982 qed |
6042 |
5983 |
6043 lemma bounded_subset_box_symmetric: |
5984 lemma bounded_subset_box_symmetric: |
6044 fixes s::"('a::euclidean_space) set" |
5985 fixes S :: "('a::euclidean_space) set" |
6045 assumes "bounded s" |
5986 assumes "bounded S" |
6046 shows "\<exists>a. s \<subseteq> box (-a) a" |
5987 obtains a where "S \<subseteq> box (-a) a" |
6047 proof - |
5988 proof - |
6048 obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b" |
5989 obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b" |
6049 using assms[unfolded bounded_pos] by auto |
5990 using assms[unfolded bounded_pos] by auto |
6050 define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)" |
5991 define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)" |
6051 { |
5992 have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" if "x \<in> S" and i: "i \<in> Basis" for x i |
6052 fix x |
5993 using b Basis_le_norm[OF i, of x] that by (auto simp: a_def) |
6053 assume "x \<in> s" |
5994 then have "S \<subseteq> box (-a) a" |
6054 fix i :: 'a |
5995 by (auto simp: simp add: box_def) |
6055 assume i: "i \<in> Basis" |
5996 then show ?thesis .. |
6056 then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" |
5997 qed |
6057 using b[THEN bspec[where x=x], OF \<open>x\<in>s\<close>] |
|
6058 using Basis_le_norm[OF i, of x] |
|
6059 unfolding inner_simps and a_def |
|
6060 by auto |
|
6061 } |
|
6062 then show ?thesis |
|
6063 by (auto intro: exI[where x=a] simp add: box_def) |
|
6064 qed |
|
6065 |
|
6066 lemma bounded_subset_open_interval: |
|
6067 fixes s :: "('a::euclidean_space) set" |
|
6068 shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)" |
|
6069 by (auto dest!: bounded_subset_box_symmetric) |
|
6070 |
5998 |
6071 lemma bounded_subset_cbox_symmetric: |
5999 lemma bounded_subset_cbox_symmetric: |
6072 fixes s :: "('a::euclidean_space) set" |
6000 fixes S :: "('a::euclidean_space) set" |
6073 assumes "bounded s" |
6001 assumes "bounded S" |
6074 shows "\<exists>a. s \<subseteq> cbox (-a) a" |
6002 obtains a where "S \<subseteq> cbox (-a) a" |
6075 proof - |
6003 proof - |
6076 obtain a where "s \<subseteq> box (-a) a" |
6004 obtain a where "S \<subseteq> box (-a) a" |
6077 using bounded_subset_box_symmetric[OF assms] by auto |
6005 using bounded_subset_box_symmetric[OF assms] by auto |
6078 then show ?thesis |
6006 then show ?thesis |
6079 using box_subset_cbox[of "-a" a] by auto |
6007 by (meson box_subset_cbox dual_order.trans that) |
6080 qed |
6008 qed |
6081 |
|
6082 lemma bounded_subset_cbox: |
|
6083 fixes s :: "('a::euclidean_space) set" |
|
6084 shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a b" |
|
6085 using bounded_subset_cbox_symmetric[of s] by auto |
|
6086 |
6009 |
6087 lemma frontier_cbox: |
6010 lemma frontier_cbox: |
6088 fixes a b :: "'a::euclidean_space" |
6011 fixes a b :: "'a::euclidean_space" |
6089 shows "frontier (cbox a b) = cbox a b - box a b" |
6012 shows "frontier (cbox a b) = cbox a b - box a b" |
6090 unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] .. |
6013 unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] .. |