1304 then show ?thesis |
1308 then show ?thesis |
1305 using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto |
1309 using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto |
1306 qed |
1310 qed |
1307 |
1311 |
1308 lemma compact_translation: |
1312 lemma compact_translation: |
1309 fixes s :: "'a::real_normed_vector set" |
1313 "compact ((+) a ` s)" if "compact s" for s :: "'a::real_normed_vector set" |
1310 assumes "compact s" |
|
1311 shows "compact ((\<lambda>x. a + x) ` s)" |
|
1312 proof - |
1314 proof - |
1313 have "{x + y |x y. x \<in> s \<and> y \<in> {a}} = (\<lambda>x. a + x) ` s" |
1315 have "{x + y |x y. x \<in> s \<and> y \<in> {a}} = (\<lambda>x. a + x) ` s" |
1314 by auto |
1316 by auto |
1315 then show ?thesis |
1317 then show ?thesis |
1316 using compact_sums[OF assms compact_sing[of a]] by auto |
1318 using compact_sums [OF that compact_sing [of a]] by auto |
1317 qed |
1319 qed |
|
1320 |
|
1321 lemma compact_translation_subtract: |
|
1322 "compact ((\<lambda>x. x - a) ` s)" if "compact s" for s :: "'a::real_normed_vector set" |
|
1323 using that compact_translation [of s "- a"] by (simp cong: image_cong_simp) |
1318 |
1324 |
1319 lemma compact_affinity: |
1325 lemma compact_affinity: |
1320 fixes s :: "'a::real_normed_vector set" |
1326 fixes s :: "'a::real_normed_vector set" |
1321 assumes "compact s" |
1327 assumes "compact s" |
1322 shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
1328 shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)" |
1418 then show ?thesis |
1424 then show ?thesis |
1419 using closed_compact_sums[OF assms(1) compact_negations[OF assms(2)]] by simp |
1425 using closed_compact_sums[OF assms(1) compact_negations[OF assms(2)]] by simp |
1420 qed |
1426 qed |
1421 |
1427 |
1422 lemma closed_translation: |
1428 lemma closed_translation: |
1423 fixes a :: "'a::real_normed_vector" |
1429 "closed ((+) a ` S)" if "closed S" for a :: "'a::real_normed_vector" |
1424 assumes "closed S" |
|
1425 shows "closed ((\<lambda>x. a + x) ` S)" |
|
1426 proof - |
1430 proof - |
1427 have "(\<Union>x\<in> {a}. \<Union>y \<in> S. {x + y}) = ((+) a ` S)" by auto |
1431 have "(\<Union>x\<in> {a}. \<Union>y \<in> S. {x + y}) = ((+) a ` S)" by auto |
1428 then show ?thesis |
1432 then show ?thesis |
1429 using compact_closed_sums[OF compact_sing[of a] assms] by auto |
1433 using compact_closed_sums [OF compact_sing [of a] that] by auto |
1430 qed |
1434 qed |
|
1435 |
|
1436 lemma closed_translation_subtract: |
|
1437 "closed ((\<lambda>x. x - a) ` S)" if "closed S" for a :: "'a::real_normed_vector" |
|
1438 using that closed_translation [of S "- a"] by (simp cong: image_cong_simp) |
1431 |
1439 |
1432 lemma closure_translation: |
1440 lemma closure_translation: |
1433 fixes a :: "'a::real_normed_vector" |
1441 "closure ((+) a ` s) = (+) a ` closure s" for a :: "'a::real_normed_vector" |
1434 shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)" |
|
1435 proof - |
1442 proof - |
1436 have *: "(+) a ` (- s) = - (+) a ` s" |
1443 have *: "(+) a ` (- s) = - (+) a ` s" |
1437 by (auto intro!: image_eqI[where x="x - a" for x]) |
1444 by (auto intro!: image_eqI [where x = "x - a" for x]) |
1438 show ?thesis |
1445 show ?thesis |
1439 unfolding closure_interior translation_Compl |
1446 using interior_translation [of a "- s", symmetric] |
1440 using interior_translation[of a "- s"] |
1447 by (simp add: closure_interior translation_Compl *) |
1441 unfolding * |
1448 qed |
1442 by auto |
1449 |
1443 qed |
1450 lemma closure_translation_subtract: |
|
1451 "closure ((\<lambda>x. x - a) ` s) = (\<lambda>x. x - a) ` closure s" for a :: "'a::real_normed_vector" |
|
1452 using closure_translation [of "- a" s] by (simp cong: image_cong_simp) |
1444 |
1453 |
1445 lemma frontier_translation: |
1454 lemma frontier_translation: |
1446 fixes a :: "'a::real_normed_vector" |
1455 "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector" |
1447 shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)" |
1456 by (auto simp add: frontier_def translation_diff interior_translation closure_translation) |
1448 unfolding frontier_def translation_diff interior_translation closure_translation |
1457 |
1449 by auto |
1458 lemma frontier_translation_subtract: |
|
1459 "frontier ((+) a ` s) = (+) a ` frontier s" for a :: "'a::real_normed_vector" |
|
1460 by (auto simp add: frontier_def translation_diff interior_translation closure_translation) |
1450 |
1461 |
1451 lemma sphere_translation: |
1462 lemma sphere_translation: |
1452 fixes a :: "'n::real_normed_vector" |
1463 "sphere (a + c) r = (+) a ` sphere c r" for a :: "'n::real_normed_vector" |
1453 shows "sphere (a+c) r = (+) a ` sphere c r" |
1464 by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x]) |
1454 by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x]) |
1465 |
|
1466 lemma sphere_translation_subtract: |
|
1467 "sphere (c - a) r = (\<lambda>x. x - a) ` sphere c r" for a :: "'n::real_normed_vector" |
|
1468 using sphere_translation [of "- a" c] by (simp cong: image_cong_simp) |
1455 |
1469 |
1456 lemma cball_translation: |
1470 lemma cball_translation: |
1457 fixes a :: "'n::real_normed_vector" |
1471 "cball (a + c) r = (+) a ` cball c r" for a :: "'n::real_normed_vector" |
1458 shows "cball (a+c) r = (+) a ` cball c r" |
1472 by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x]) |
1459 by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x]) |
1473 |
|
1474 lemma cball_translation_subtract: |
|
1475 "cball (c - a) r = (\<lambda>x. x - a) ` cball c r" for a :: "'n::real_normed_vector" |
|
1476 using cball_translation [of "- a" c] by (simp cong: image_cong_simp) |
1460 |
1477 |
1461 lemma ball_translation: |
1478 lemma ball_translation: |
1462 fixes a :: "'n::real_normed_vector" |
1479 "ball (a + c) r = (+) a ` ball c r" for a :: "'n::real_normed_vector" |
1463 shows "ball (a+c) r = (+) a ` ball c r" |
1480 by (auto simp: dist_norm algebra_simps intro!: image_eqI [where x = "x - a" for x]) |
1464 by (auto simp: dist_norm algebra_simps intro!: image_eqI[where x="x - a" for x]) |
1481 |
|
1482 lemma ball_translation_subtract: |
|
1483 "ball (c - a) r = (\<lambda>x. x - a) ` ball c r" for a :: "'n::real_normed_vector" |
|
1484 using ball_translation [of "- a" c] by (simp cong: image_cong_simp) |
1465 |
1485 |
1466 |
1486 |
1467 subsection%unimportant\<open>Homeomorphisms\<close> |
1487 subsection%unimportant\<open>Homeomorphisms\<close> |
1468 |
1488 |
1469 lemma homeomorphic_scaling: |
1489 lemma homeomorphic_scaling: |