equal
deleted
inserted
replaced
1293 |
1293 |
1294 lemma rel_frontier_translation: |
1294 lemma rel_frontier_translation: |
1295 fixes a :: "'a::euclidean_space" |
1295 fixes a :: "'a::euclidean_space" |
1296 shows "rel_frontier((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (rel_frontier S)" |
1296 shows "rel_frontier((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (rel_frontier S)" |
1297 by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation) |
1297 by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation) |
1298 |
|
1299 lemma closed_affine_hull [iff]: |
|
1300 fixes S :: "'n::euclidean_space set" |
|
1301 shows "closed (affine hull S)" |
|
1302 by (metis affine_affine_hull affine_closed) |
|
1303 |
1298 |
1304 lemma rel_frontier_nonempty_interior: |
1299 lemma rel_frontier_nonempty_interior: |
1305 fixes S :: "'n::euclidean_space set" |
1300 fixes S :: "'n::euclidean_space set" |
1306 shows "interior S \<noteq> {} \<Longrightarrow> rel_frontier S = frontier S" |
1301 shows "interior S \<noteq> {} \<Longrightarrow> rel_frontier S = frontier S" |
1307 by (metis frontier_def interior_rel_interior_gen rel_frontier_def) |
1302 by (metis frontier_def interior_rel_interior_gen rel_frontier_def) |